Michael Soegtrop (Nov 15 2021 at 10:15): Michael Soegtrop (Nov 15 2021 at 10:15):I did a status round for 2021.11 over the weekend. It looks fairly good, only two packages don't compile as yet:
If someone has contact to @Pierre Courtieu can (s)he please point him to (https://github.com/Matafou/LibHyps/issues/6)?
For some of the mathcomp extensions I am lacking feedback from the authors if the latest version is what they want to use, but this is not critical, if they don't answer I will use the latest version (which works). This affects bigenough, finmap and real-closed. @Enrico Tassi : can you please ping the authors? The issue links are all in (https://github.com/coq/platform/issues/139). But as I said, this is just a formality and done to avoid that people publish some great new features 2 days after a Coq Platform release.
For VST the pick confirmation is also missing as yet, but I don't think it will change. For everything else the package picks are formally confirmed.
On my todo list is to add another prover for coq-hammer (a special Z3 variant) via opam - I already added eprover a while back - so that we can add coq-hammer (assuming it works at al for 8.14). Also I wanted to write an opam package for the proof generator tool for coqprime (it currently doesn't have a portable configure mechanism and requires some non standard libraries).
Théo Zimmermann (Nov 15 2021 at 11:31):I have pinged @Pierre Courtieu on the GitHub issue: sometimes it helps people notice their GitHub notifications. If it doesn't work, I can send him an email.
Michael Soegtrop (Nov 15 2021 at 12:16):Thanks!
Pierre Courtieu (Nov 15 2021 at 15:19):Seen thanks I will try to fix this quickly.
P
Le lun. 15 nov. 2021 à 12:33, Zulip notifications <noreply@zulip.com> a
écrit :
Pierre Courtieu (Nov 15 2021 at 18:35):I managed to make things compile but sadly something seems to have changed in my ltac code semantics. I need to investigate further. I will try tomorrow but I don't have much time.
Pierre Courtieu (Nov 15 2021 at 18:36):Was there some non compatible changes in Ltac between 8.13.2 and 8.14?
Théo Zimmermann (Nov 15 2021 at 20:58):@Pierre Courtieu This is not an Ltac change but it could have an impact on how tactics behave: https://coq.inria.fr/refman/changes.html#caserepresentation. Other than this, all the documented changes in tactic language are related to Ltac2, not to Ltac1.
Pierre Courtieu (Nov 16 2021 at 19:06):Théo Zimmermann said:
Pierre Courtieu This is not an Ltac change but it could have an impact on how tactics behave: https://coq.inria.fr/refman/changes.html#caserepresentation. Other than this, all the documented changes in tactic language are related to Ltac2, not to Ltac1.
@Théo Zimmermann Nope it was not that. It is the following small incompatibility between 8.13.2 and 8.14:
Lemma foo: forall x y:nat, False.
Proof.
intros.
move x before x. ==> Error: No such hypothesis: x <== v8.13.2
v.8.14 (x and y swaped):
y, x : nat
============================
False
One function in LibHyps was relying on this.
@Karl Palmskog May I submit a new version tomorrow?
Karl Palmskog (Nov 16 2021 at 19:08):@Pierre Courtieu if you mean submit to Coq opam archive, you can submit any time, and you can ping Michael to let him know this is the version to use for the platform (or I can do it). We try to have turnaround time of a day or less to merge+deploy to the archive, but we can do faster (hours) if this is needed.
Karl Palmskog (Nov 16 2021 at 19:09):you could even replace an existing package, but generally I'd encourage just making a new one with version increment
Pierre Courtieu (Nov 16 2021 at 20:07):Actually it is a real bug of move after I will fill a bug report.
Théo Zimmermann (Nov 20 2021 at 22:19):@Michael Soegtrop I think that you should be aware that the V8.14.1 tag has been set (even if it hasn't yet been announced anywhere yet and no one seems to have prepared an opam package). I guess 2021.11 should include it.
Michael Soegtrop (Nov 23 2021 at 09:11):@Théo Zimmermann : thanks - indeed I would have skipped that!
Michael Soegtrop (Nov 30 2021 at 13:12):Just a short status update (since it is Nov 30): there are a few minor changes (Coq 8.14.1, ...) still open and one bigger package, which is coq-hammer. I have this working with eprover and z3 except on Windows (to which the tactic itself is entirely incompatible due to heavy use of fork), but there are discussions ongoing on changing the opam Z3 package which hold me up.
Also there are a few package requests, which I think to include. So I guess it will be one or 2 weeks until the release.
Karl Palmskog (Nov 30 2021 at 16:06):I think it would be huge to get CoqHammer + some provers working out of the box, even on just Linux and macOS. Getting all that stuff set up manually is a big blocker to using automation for regular users I believe.
Michael Soegtrop (Nov 30 2021 at 16:13):Yes, I guess so. Both the eprover and the z3 opam package are "compile from sources", so they should be quite robust.
Michael Soegtrop (Nov 30 2021 at 16:14):And I think it is OK to not have it for Windows for the time being, since one should anyway replace the hammer calls with the tactic it spits out.
Michael Soegtrop (Nov 30 2021 at 16:14):Btw.: How about your open requests, e.g. Ott?
Karl Palmskog (Nov 30 2021 at 16:16):I've been stuck with papers and proposals, but I hope I can do the Ott release tomorrow or Thursday
Michael Soegtrop (Nov 30 2021 at 16:18):That would still make it then. As I said it will likely be a week or so cause of coq-hammer and Z3. The discussion on the Z3 opam package seems to converge.
Paolo Giarrusso (Nov 30 2021 at 16:19):while at it, are there plans to include https://github.com/coin-or/Csdp for the psatz tactic that comes with Coq?
Karl Palmskog (Nov 30 2021 at 16:19):https://github.com/coq/platform/issues/39
Paolo Giarrusso (Nov 30 2021 at 16:20):thanks and apologies for the lazy question
Karl Palmskog (Nov 30 2021 at 16:20):well, it's a relevant question because the last issue message was on whether it would be included in 2021.11 or not
Paolo Giarrusso (Nov 30 2021 at 16:20):as penitence, I see https://github.com/coq/platform/releases/tag/2021.09.0 and I just got an M1 Max
Michael Soegtrop (Nov 30 2021 at 20:03):@Paolo Giarrusso : I don't plan for CSDP currently - it will be tricky to provide platform independent packages.
Michael Soegtrop (Dec 19 2021 at 09:35):I just wanted to note that I was super busy the last 3 weeks and didn't have time to work on the 2021.11 release, but will pick this up now.
Théo Zimmermann (Dec 19 2021 at 13:43):Since 8.15+rc1 has been released for quite some time now (even if it hasn't been announced to platform package maintainers), it might make sense to include it as a beta with whatever is compatible with it now.
Théo Zimmermann (Dec 19 2021 at 13:43):(but only if it does not cause delays with the 2021.11 release)
Théo Zimmermann (Dec 19 2021 at 13:44):BTW, since AFAIK the Snap track for 2021.11 has not been asked for yet, it is still time to rename this release into 2021.12.
Enrico Tassi (Dec 19 2021 at 15:14):Indeed, the last request is: https://forum.snapcraft.io/t/2021-09-track-creation-for-coq-prover/26451/3
@Michael Soegtrop you have write access to the snap store (as all core devs) so you can definitely ask for the track yourself by posting a message like mine
Enrico Tassi (Dec 19 2021 at 15:15):And I'm very sorry I can't really help, I'll be mostly unavailable until mid January :-/
Last updated: Oct 13 2024 at 01:02 UTC