Shape and checksum should use the same task information
Hello,
I think that shapes and checksums of task should use the exact same information. Currently, I think that checksums ignore attributes [EDIT: attributes or expl (EDIT2:which can be an attribute) ?] whereas shapes use attributes. Also, there should be a warning when shapes are out of date.
[Context]
Recently, I changed a bunch of transformations so that attributes are added to the head of the goal (for information's displaying). This affected all the shapes for goals under these transformations but I did not see it in nightly-build because the checksums were still ok: the merging/pairing used checksum and did not look at shapes.
In an unrelated commit, I made a change that affects checksums but not shapes (adding a meta in the task). This break the pairing for a lot of proofs.
[Test]
To test this, you can regenerate the shapes for isqrt_von_neumann
(on master).
mv examples/isqrt_von_neumann/why3shapes.gz saved_shapes
rm examples/isqrt_von_neumann/why3shapes.gz.bak
bin/why3ide examples/isqrt_von_neumann
[launch a prover on a goal]
[exit and save]
diff examples/isqrt_von_neumann/why3shapes.gz saved_shapes