The current backtracking behavior on some instructions (load/store in particular) leads to confusing error messages in case of failure. (if the tactic tries rule1 || rule2, and we wanted to apply rule1 but it fails, it will try rule2, fail as well, and print a useless error message related to rule2.)
A related problem is with the jmp instruction; currently the proofmode decides on the rule depending on whether the content of the condition register is syntactically zero, which can be confusing (e.g. if it contains (z-z), one needs to take care of rewriting that to zero before applying the tactic)
One idea would be to regroup rules in different classes / lemma bases, where each lemma base should contain lemmas that can apply non-ambiguously wrt other lemmas in the base. Then, have a syntax for specifying a (set of) lemma base(s) in iInstr/iGo.
Also: it would be useful to be able to directly specify a lemma name...
The current backtracking behavior on some instructions (load/store in particular) leads to confusing error messages in case of failure. (if the tactic tries rule1 || rule2, and we wanted to apply rule1 but it fails, it will try rule2, fail as well, and print a useless error message related to rule2.)
A related problem is with the jmp instruction; currently the proofmode decides on the rule depending on whether the content of the condition register is syntactically zero, which can be confusing (e.g. if it contains
(z-z), one needs to take care of rewriting that to zero before applying the tactic)One idea would be to regroup rules in different classes / lemma bases, where each lemma base should contain lemmas that can apply non-ambiguously wrt other lemmas in the base. Then, have a syntax for specifying a (set of) lemma base(s) in iInstr/iGo.
Also: it would be useful to be able to directly specify a lemma name...