Stream: Coq users

Topic: Is `-async-proofs-j` broken in 8.15.1?


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (May 12 2022 at 08:45):

OK, I will try some old switches later today (oh I love opam).

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (May 12 2022 at 08:50):

I'm not aware of anything like this.

view this post on Zulip Michael Soegtrop (May 12 2022 at 08:52):

I will post test results around 5PM German time.

view this post on Zulip 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

view this post on Zulip Ali Caglayan (May 12 2022 at 09:03):

This is 8.15.1 FTR.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (May 12 2022 at 09:06):

That is odd...

view this post on Zulip Ali Caglayan (May 12 2022 at 09:06):

@Michael Soegtrop Can you share your file?

view this post on Zulip Michael Soegtrop (May 12 2022 at 09:06):

I would need a few 100 files to compile ...

view this post on Zulip Michael Soegtrop (May 12 2022 at 09:07):

But I guess I can find something.

view this post on Zulip Ali Caglayan (May 12 2022 at 09:07):

The bug minimizer tool can inline imports

view this post on Zulip Michael Soegtrop (May 12 2022 at 09:07):

Let me try Pff - it should reach the end much quicker in VsCoq than in CoqIDE.

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (May 12 2022 at 09:08):

Yes, maybe it is just a feeling given by the colors

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (May 12 2022 at 09:09):

There was some quadratic slow down in 8.15.0.

view this post on Zulip 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.

view this post on Zulip 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: Feb 09 2023 at 00:03 UTC