Jason Gross (Apr 19 2021 at 22:12): Jason Gross (Apr 19 2021 at 22:12):Is there any hope of geting https://github.com/coq/coq/issues/8236 fixed? The issue is a regression of Coq 8.5 and later over Coq 8.4, was reported 2.5 years ago, and has had no comments from any of the devs.
Emilio Jesús Gallego Arias (Apr 19 2021 at 22:13):Isn't there a duplicate bug elsewhere?
Emilio Jesús Gallego Arias (Apr 19 2021 at 22:13):If the bug is due to the STM I'd say little hope to fix it;
Emilio Jesús Gallego Arias (Apr 19 2021 at 22:14):Flèche does indeed try to have excellent debug and performance monitoring built-in from the start.
Jason Gross (Apr 19 2021 at 22:40):Not sure if there's a duplicate elsewhere? And what's Flèche? And can you explain what the setup of the STM would be such that there'd be little hope of fixing it?
Emilio Jesús Gallego Arias (Apr 20 2021 at 10:59):And can you explain what the setup of the STM would be such that there'd be little hope of fixing it?
The Qed path is a bit convoluted, I tried to do some progress to time sentences in https://github.com/coq/coq/pull/12730 , however I didn't succeed, and it seems to me that dev time to fix this is pretty limited as both Enrico and I are working on different stuff, but if someone finds a solution why not?
And what's Flèche?
That's a new document manager that I've been working on for the last couple of years that I hope to release really soon.
Jason Gross (Apr 20 2021 at 11:48):Thanks for the explanation. Do you mind if I quote this on the GH issue so that if I come looking again in a couple years I find this?
Enrico Tassi (Apr 20 2021 at 12:31):My "grand plan" is to move the STM to CoqIDE, have coqc be a "simple compiler" (with par: be implemented via SEL as in vscoqtop). Unfortunately the third confinement did slow this path down.
When this plan is over, Time Qed will work fine in coqc. Said that -time already works fine withcoqceven today.
Andrej Dudenhefner (Apr 20 2021 at 12:46):with
par:be implemented via SEL as in vscoqtop
Is it possible to address ad-hoc-asynchronicity via SEL in a clean manner?
(it is somewhat frustrating having many CPU cores, but only a few threads while building some Coq projects)
Enrico Tassi (Apr 20 2021 at 13:26):I would say that it is orthogonal. You can implement async on the STM's asynctaskQueue as well for terminal goals. It is not that different than par, the main difference is that the "join" is not at the next . but at Qed., if I understand it right.
Enrico Tassi (Apr 20 2021 at 13:27):It seems indeed a good project for a week sprint
Andrej Dudenhefner (Apr 20 2021 at 13:32):@Enrico Tassi you mentioned in #9550 that the current implementation of par: is not a good one. So I figured adding more of the same is not the right way to go.
Enrico Tassi (Apr 20 2021 at 13:33):To clarify: STM = DAG + asyncTaskQueue[threads + fork], DM = documentManager + executionManager + delegationManager[SEL + fork]. The DAG was split into two components, actual delegation of tasks is based on fork, non-blocking communication moved from threads to SEL.
Enrico Tassi (Apr 20 2021 at 13:33):Part of spaghetti I talk about there is gone, it is still based on the STM but not that entangled.
Enrico Tassi (Apr 20 2021 at 13:35):But the scope of the "jobs queue" you want is more global than a single tactic invocation. So it has to be held at the lever of the proof I guess. par: allocates a pool of workers for the single tactic.
Andrej Dudenhefner (Apr 20 2021 at 13:36):And yes, "join" is not at the next . but at Qed. is the desired semantics. Also the workers have to come from a global pool.
Andrej Dudenhefner (Apr 20 2021 at 13:38):Alternatively, it could be already enough to have async collect the jobst until Qed. and then fire like par: at the end. This would not require global worker handling and could be possibly built directly on top of par.
Enrico Tassi (Apr 20 2021 at 13:38):One thing to notice is that "spawning" is expensive. in vscoqtop, on linux, I managed to use fork, which is fast. But the STM (or on windows) if you have ZArith around spawning can take 1/3 of a second.
Enrico Tassi (Apr 20 2021 at 13:39):It is only worth for long running tactics.
Enrico Tassi (Apr 20 2021 at 13:40):I've to work on something else now, but this looks like a nice project for the next CUDW to me
Enrico Tassi (Apr 20 2021 at 13:42):(IMO it make more sense to write async in front of { to delegate an entire, lengthy, proof branch)
Andrej Dudenhefner (Apr 20 2021 at 13:45):(IMO it make more sense to write async in front of { to delegate an entire, lengthy, proof branch)
There definitely is some design room of asynchronicity. Or maybe having parallel bullet points. (once again no evars allowed)
Paolo Giarrusso (Apr 20 2021 at 21:36):Enrico Tassi said:
One thing to notice is that "spawning" is expensive. in vscoqtop, on linux, I managed to use fork, which is fast. But the STM (or on windows) if you have ZArith around spawning can take 1/3 of a second.
The delay feels indeed visible on Mac
Paolo Giarrusso (Apr 20 2021 at 21:41):That is, given a short theorem with Proof. ltac-script. Qed., jumping to the end of ltac-script. seems synchronous and fast, while when jumping to the end of Qed. there’s always a visible delay even for quick scripts.
Last updated: Jun 08 2023 at 04:01 UTC