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.Seqis 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.conffile (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)
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information