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).
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.
Seen thanks I will try to fix this quickly.
Le lun. 15 nov. 2021 à 12:33, Zulip notifications <firstname.lastname@example.org> a
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.
Was there some non compatible changes in Ltac between 8.13.2 and 8.14?
@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 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?
@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.
you could even replace an existing package, but generally I'd encourage just making a new one with version increment
Actually it is a real bug of
move after I will fill a bug report.
@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.
@Théo Zimmermann : thanks - indeed I would have skipped that!
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.
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.
Yes, I guess so. Both the eprover and the z3 opam package are "compile from sources", so they should be quite robust.
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.
Btw.: How about your open requests, e.g. Ott?
I've been stuck with papers and proposals, but I hope I can do the Ott release tomorrow or Thursday
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.
while at it, are there plans to include https://github.com/coin-or/Csdp for the
psatz tactic that comes with Coq?
thanks and apologies for the lazy question
well, it's a relevant question because the last issue message was on whether it would be included in 2021.11 or not
as penitence, I see https://github.com/coq/platform/releases/tag/2021.09.0 and I just got an M1 Max
@Paolo Giarrusso : I don't plan for CSDP currently - it will be tricky to provide platform independent packages.
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.
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.
(but only if it does not cause delays with the 2021.11 release)
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.
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
And I'm very sorry I can't really help, I'll be mostly unavailable until mid January :-/
Last updated: Jan 30 2023 at 10:03 UTC