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.
Isn't there a duplicate bug elsewhere?
If the bug is due to the STM I'd say little hope to fix it;
Flèche does indeed try to have excellent debug and performance monitoring built-in from the start.
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?
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.
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?
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 withcoqc
even today.
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)
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.
It seems indeed a good project for a week sprint
@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.
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.
Part of spaghetti I talk about there is gone, it is still based on the STM but not that entangled.
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.
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.
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
.
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.
It is only worth for long running tactics.
I've to work on something else now, but this looks like a nice project for the next CUDW to me
(IMO it make more sense to write async in front of { to delegate an entire, lengthy, proof branch)
(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)
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
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