Refactoring Framework Release History

Version 0.0.8

28th May 2010

A release of renaming/refactory (v0.0.8) compatible with Rodin v1.3.x is available in the main Rodin update site. A bug related to assignment using the "become such that" operator was fixed. Also, when renaming proofs, this is done by running a job which can run in background.

• Bug Fix
  • Bug 3005170: If a variable is renamed, which is used in a "becomes such that", the assignment does not type check any longer after the renaming operation, because the variable has disappeared.
  • Bug 3005202: When a renaming operation is performed, the provers are launched. The waiting time may be quite long and it is impossible to do anything else.

It is always necessary to run the provers? If it is indeed mandatory, the provers should be temporarily disconnected until the renaming has been performed, and run when this operation has completed.

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.