Refactoring Framework Release History

Version 0.0.4 [for Rodin 1.1.0]

Before starting the renaming, it is recommended to clean and build the project in order to have the indexer tables updated (IMPORTANT).

• Features
  • Renaming of machines and contexts is possible using the indexers. After the renaming of a machine/context, the change is propagated over the related files
  • Renaming of proofs: after the renaming, the proof obligations are also updated to reflect the renaming. It might be necessary to manually refresh the status of some proof obligations (although the proof is already discharged). This renaming is not fully-functional at the moment and some discharged proof obligations may have to be discharged again. We intend to fix this problem in the future.

• Bug fix
  • Renaming of proofs would not save the proof files after renaming
  • Renaming of labelled elements would not update the proofs.

• Possible Problem
  • If you try to rename and the operation runs successfully without any errors but does not have any effect, you should:
    • First, try to fix the renaming manually on the respective file (or using the renaming framework, revert to the original name)
    • Try to make a CLEAN and BUILD to ensure that the Rodin indexer is updated before the renaming.
    • Run the renaming again and should be working fine.