Gaëtan Gilbert (Jul 09 2022 at 19:19): Gaëtan Gilbert (Jul 09 2022 at 19:19):https://gitlab.com/coq/coq/-/jobs/2699877705#L856
probably https://github.com/PrincetonUniversity/VST/pull/578
Andrej Dudenhefner (Jul 10 2022 at 07:34):Since it does compile with the 8.16 branch, is there an easy way to see which Coq commit in master broke compilation?
Théo Zimmermann (Jul 10 2022 at 08:29):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).
Théo Zimmermann (Jul 10 2022 at 08:29):It's just too bad that we don't get a heads up from VST developers when there are such changes.
Ali Caglayan (Jul 10 2022 at 14:08):I made a patch switching VST to flocq4 https://github.com/coq/coq/pull/16305
Ali Caglayan (Jul 11 2022 at 15:05):can I get an assignee?
Gaëtan Gilbert (Oct 20 2022 at 20:31):when was the last vst success? Do we know why it keeps failing?
Théo Zimmermann (Oct 21 2022 at 06:59):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).
Michael Soegtrop (Oct 21 2022 at 10:27):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 ...
Gaëtan Gilbert (Oct 21 2022 at 10:36):https://gitlab.com/coq/coq/-/jobs/3204948296
Michael Soegtrop (Oct 21 2022 at 12:31):It is an out of memory: (https://gitlab.com/coq/coq/-/jobs/3204948296#L4101)
Michael Soegtrop (Oct 21 2022 at 12:32):(Error 137)
Pierre-Marie Pédrot (Oct 22 2022 at 11:50):let's see if https://github.com/PrincetonUniversity/VST/pull/629 helps
Michael Soegtrop (Oct 23 2022 at 08:56):@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.
Enrico Tassi (Oct 23 2022 at 12:16):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.
Michael Soegtrop (Oct 23 2022 at 13:08):@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.
Enrico Tassi (Oct 23 2022 at 13:21):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
Enrico Tassi (Oct 23 2022 at 13:30):This of corse once it is finished, in terms of design.
Pierre-Marie Pédrot (Oct 24 2022 at 11:50):FWIW VST is still randomly failing, but now it does one file later it seems?
Michael Soegtrop (Oct 24 2022 at 12:15):@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 -j 2?
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.
Pierre-Marie Pédrot (Oct 24 2022 at 12:18):The VST ci script doesn't pass an explicit -j option AFAICT.
Michael Soegtrop (Oct 24 2022 at 12:27):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?
Pierre-Marie Pédrot (Oct 24 2022 at 12:28):Maybe it's native compilation dying, though. I think we deactivate native on unimath.
Gaëtan Gilbert (Oct 24 2022 at 12:30):CI runs with -j2 usually
also unimath disables native and a bunch of the bigger files
Gaëtan Gilbert (Oct 24 2022 at 12:30):(cf the script you linked)
Pierre-Marie Pédrot (Oct 24 2022 at 12:30):should we deactivate native on VST?
Michael Soegtrop (Oct 24 2022 at 12:31):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.
Pierre-Marie Pédrot (Oct 24 2022 at 12:31):the PR I wrote was precisely trying to fix a humongous proof relying on brute force search
Pierre-Marie Pédrot (Oct 24 2022 at 12:32):it has not solved the problem so it must lie elsewhere
Michael Soegtrop (Oct 24 2022 at 12:33):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?
Pierre-Marie Pédrot (Oct 24 2022 at 12:34):native compilation affects everybody writing definitions, not only devs using native_compute
Pierre-Marie Pédrot (Oct 24 2022 at 12:34):that said it's true that this file doesn't seem to define anything, even implicitly with Schemes
Michael Soegtrop (Oct 24 2022 at 12:35):I was about to post the same conclusion ...
Pierre-Marie Pédrot (Oct 24 2022 at 12:35):how much memory do we have on the runners exactly?
Gaëtan Gilbert (Oct 24 2022 at 12:37):log says
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.
Michael Soegtrop (Oct 24 2022 at 12:38):Gut feeling I would guess 1.5.
Théo Zimmermann (Oct 24 2022 at 15:01):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