Michael Soegtrop (May 12 2022 at 08:42): Michael Soegtrop (May 12 2022 at 08:42):I have the feeling that -async-proofs-j is broken in 8.15.1. It does create the requested number of workers, but they don't do anything although there is plenty of parallel proof opportunity. The accumulated process time of all proof workers stays at 0.3s forever.
@Enrico Tassi : are you aware of any recent changes here? It did work for me (on the same file) not that far in the past.
Ali Caglayan (May 12 2022 at 08:44):I also noticed something like this, but I am unsure if I set up everything correctly. I also noticed in CoqIDE that more than the given number of workers can get created, though I am not sure if this is because the older ones got destroyed.
Michael Soegtrop (May 12 2022 at 08:45):OK, I will try some old switches later today (oh I love opam).
Ali Caglayan (May 12 2022 at 08:46):Jim also reported some similar behavior: https://github.com/coq/coq/issues/15998. Have a look if it is the same.
Enrico Tassi (May 12 2022 at 08:50):I'm not aware of anything like this.
Michael Soegtrop (May 12 2022 at 08:52):I will post test results around 5PM German time.
Ali Caglayan (May 12 2022 at 09:02):I did a demo. I have 16 cores on my machines, so I passed -async-proofs-j 14 to CoqIDE. Many jobs get done in parallel but there are quite a lot of idle workers especially towards the end. The test file is Pff.v:
async_idle_workers.gif
Ali Caglayan (May 12 2022 at 09:03):This is 8.15.1 FTR.
Ali Caglayan (May 12 2022 at 09:04):I do wonder what the workers are actually waiting for when they say they are idle however.
Enrico Tassi (May 12 2022 at 09:04):That seems pretty normal. the point is that master is still working to reach the end of the file, and fairness is not there (thanks ocaml), so the the threads managing the workers don't get a chance to start them.
Enrico Tassi (May 12 2022 at 09:05):Write a file with 15 slow proofs (test-suite/interactive/PralaITP.v as an example) and jump to the end. IMO you will see all workers doing work
Michael Soegtrop (May 12 2022 at 09:06):Well in my application it reaches the end very quickly (VsCoq) and then it does everything sequentially althoug I have 6 workers. I don't have sections.
Enrico Tassi (May 12 2022 at 09:06):That is odd...
Ali Caglayan (May 12 2022 at 09:06):@Michael Soegtrop Can you share your file?
Michael Soegtrop (May 12 2022 at 09:06):I would need a few 100 files to compile ...
Michael Soegtrop (May 12 2022 at 09:07):But I guess I can find something.
Ali Caglayan (May 12 2022 at 09:07):The bug minimizer tool can inline imports
Michael Soegtrop (May 12 2022 at 09:07):Let me try Pff - it should reach the end much quicker in VsCoq than in CoqIDE.
Ali Caglayan (May 12 2022 at 09:07):Michael Soegtrop said:
Let me try Pff - it should reach the end much quicker in VsCoq than in CoqIDE.
Why do you think that? Are they not using the same backend?
Enrico Tassi (May 12 2022 at 09:08):Yes, maybe it is just a feeling given by the colors
Michael Soegtrop (May 12 2022 at 09:08):Some slowness in parsing on CoqIDE is due to the Ltac debugger - which is not there in VsCoq. It has been improved quite a bit, but there is still a difference.
Michael Soegtrop (May 12 2022 at 09:09):There was some quadratic slow down in 8.15.0.
Ali Caglayan (May 12 2022 at 09:10):The behavior I observed is the same in 8.14 so perhaps there is nothing wrong with my test.
Michael Soegtrop (May 12 2022 at 09:13):The downside in VSCoq is that the syntax coloring or whatever takes a very long time before it even starts coqidetop. I am a bit busy right now - as I said I will do some analysis around 5 PM.
Last updated: Apr 20 2024 at 02:40 UTC