Release of the new system
Things to do before releasing master
:
-
Enumerate the changes -
Document the changes of syntax -
Remove the obsolete parts of documentation -
Update the Coq realizations (especially seq.Seq
)➡ seq.Seq
is no longer realized -
Update the Isabelle 2017 realizations -
Update the Isabelle 2016-1 realizations, or drop them -
Kill the Coq tactic (still used by about 20 proofs from the gallery) -
Port the 'prover' example (blocked by issue #87 (closed)) -
Stabilize Etry
-
Solve issue #9 (closed) -
Solve issue #6 (closed) -
Solve issue #63 (closed) (issue not fully solved but should not be a blocker anymore for the release) -
Not a regression, but I think it would be preferable to find a solution to the various problems related to the why3.conf
file (see issues #55 and #69 (closed) and !7 (merged)) -
Solve issue #118 (closed) -
Solve issue #128 (closed) -
Solve issue #131 (closed) -
Solve issue #125 (closed) -
Fix the gallery, possibly adopting issue #132 (closed) -
Solve issue #136 (closed)