Shape and checksum should use the same task information
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.
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.
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