Since it does compile with the 8.16 branch, is there an easy way to see which Coq commit in master broke compilation?
There's no mystery and it's not that VST is not compatible with master. Our CI still builds flocq3 because VST required it. So we now have to remove the flocq3 job and plug VST on the flocq4 job (or even on the compcert job as this should work for a while and save some runner time).
It's just too bad that we don't get a heads up from VST developers when there are such changes.
I made a patch switching VST to flocq4 https://github.com/coq/coq/pull/16305
can I get an assignee?
when was the last vst success? Do we know why it keeps failing?
It looks definitely related to the new runners. AFAICT, I have not seen VST failing on the docker-coq-machine (except from runner failures that made every job fail).
VST takes a long time to build (I think #2 after Unimath in Coq Platform). Maybe it timeouts? I can't find logs which are not yet deleted ...
It is an out of memory: (https://gitlab.com/coq/coq/-/jobs/3204948296#L4101)
let's see if https://github.com/PrincetonUniversity/VST/pull/629 helps
@Pierre-Marie Pédrot : A side note: I expect that I could dramatically cut the memory consumption and run time of VST if there would be proper methods to handle symbol list for cbv as we discussed during the working group meeting in June. At least in all cases where it exceeds the RAM of my machines for my projects, this is the issue.
@Enrico Tassi helped to make progress here with Elpi and for me this is a good opportunity to learn Elpi,. but I am not sure which tactic language would be better for VST - it might also be a mix of both.
With Ltac2 and computing the required symbol lists with coqtop and text processing (the lists are static but depend on VST/CompCert version) I get frequent
simpl operations in VST from minutes to milliseconds and from many GB to not exceeding the usual memory consumption.
I've the impression that Elpi, as a language, gives you little advantage for this specific task. As an extension framework it does give you more APIs (and internally it is easy for me to add more, it is a bias I invested on a lot of engineering time on).
Imo you should mix and match all you got in the ecosystem to experiment, but finally, for this specific need, I think both languages/frameworks are not giving you much, so your solution could/should be coded in OCaml, maybe by a third-party familar with the nasty Coq APIs. After all this way of of using Elpi was expected since the very beginning: prototyping. I'm very happy the language turned out to be viable also for final implementation, but it may be too much of a dependency for this little task.
@Enrico Tassi : I am more thinking about rewriting larger parts of the VST proof automation in either Ltac2 or Elpi. I think the main advantage for sticking to one or another is the reduced learning curve for contributors. If I use both, there really must be a substantial advantage in both languages justifying this. At the time being I know Ltac2 muc better than Elpi and can't really tell which one will be more suitable for the overall task.
I don't think it will be of much use to go to OCaml - the time will likely go into executing computations and unifications and not so much in putting the commands together, so I don't think OCaml will speed up things noticeably.
Rigth, speed is not a concern. At the same time the feature you are working on has nothing VST specific to me, so having it "promoted" into coq vanilla could make sense
This of corse once it is finished, in terms of design.
FWIW VST is still randomly failing, but now it does one file later it seems?
@Pierre-Marie Pédrot : this run (latest commit) still fails cause of an out of memory (Linux error 137). I don't think the VST team can do anything about this in the short run - this is not a test or example file but a file with important lemmas.
Are you running with
-j 1 or
It would be a lot of work but it is imaginable to single out especially memory hungry files and make sure they run one by one.
The VST ci script doesn't pass an explicit -j option AFAICT.
Indeed, I double checked. Also as far as I can see the VST Makefile doesn't have a default here, so it should be -j=1. I would say we are out of options then besides increasing the runner memory size.
I am astonished that UniMath works then - or is https://github.com/coq/coq/blob/master/dev/ci/ci-unimath.sh excluded from CI?
Maybe it's native compilation dying, though. I think we deactivate native on unimath.
CI runs with -j2 usually
also unimath disables native and a bunch of the bigger files
(cf the script you linked)
should we deactivate native on VST?
I don't think so -
veric/binop_lemmas4.vo should be plain lemmas and when I looked last there was not much automation in the provided proofs - VST concentrates on automation for users.
the PR I wrote was precisely trying to fix a humongous proof relying on brute force search
it has not solved the problem so it must lie elsewhere
But I don't see any native compute stuff in (https://github.com/PrincetonUniversity/VST/blob/master/veric/binop_lemmas4.v) so how could it help?
native compilation affects everybody writing definitions, not only devs using native_compute
that said it's true that this file doesn't seem to define anything, even implicitly with Schemes
I was about to post the same conclusion ...
how much memory do we have on the runners exactly?
MemTotal: 4025640 kB MemFree: 1566020 kB MemAvailable: 3569548 kB
@Gaëtan Gilbert wrote above that Ci defaults to -j 2 (I guess via environment variables), so it might be an option to try -j 1. It might not be that much slower, because VST anyway has longer sequential dependency paths.
Gut feeling I would guess 1.5.
I just want to remind everyone that when the docker-coq-machine was not paused because of issues reported in #Coq devs & plugin devs > Runner failures on docker-machine runner, VST and fiat-crypto were working perfectly fine on these runners. It is only on the new runners that we are seeing OOM issues (cf. #Coq devs & plugin devs > Runner failures on ci-coq-02-runner-*). So it seemed that the new runners are somewhat less powerful?
Last updated: Nov 29 2023 at 21:01 UTC