Open WolframPfeifer opened 2 weeks ago
Does this break/concern the taclet definitions used in KeY or is perhaps the printing to taclets.new.txt etc. broken?
Does this break/concern the taclet definitions used in KeY or is perhaps the printing to taclets.new.txt etc. broken?
The printing is broken. However, at the moment I do not know how to fix this. It seems that everything inside the by choice/taclet option switch is ignored by the toString() method of Taclet (and its subclasses).
I think there is another potential problem with the test case: Changes in the types of schema variables are not detected (their declarations are not included in the textual representation).
The printing is broken. However, at the moment I do not know how to fix this. It seems that everything inside the by choice/taclet option switch is ignored by the toString() method of Taclet (and its subclasses).
I think the printing would need to use the corresponding TacletBuilder class. The Taclet instance itself contains only the activated goals.
Description
While working on #3353, I noticed that changes inside of semantic switches in taclets are ignored.
For example, consider the following taclet:
Compare the corresponding entry in the taclets.old.txt:
Note that the part with the semantics switch
does not occur at all. Thus, changes here are not correctly detected.
Reproducible
always
Steps to reproduce
TestTacletEquality::createNewOracle
and rename it to taclets.old.txt.The file is identical to the old version, instead of correctly reflecting the changed taclet.