It seems that the CI for build:base+async has recently started to regularly time out. See e.g. https://gitlab.com/coq/coq/-/jobs/2498911484. Anybody knows what could have caused that?
Judging from the place where it dies (at the end of Reals) it's probably short of a few minutes, if not seconds.
Should we just bump the time limit?
I saw inconclusive measurements as well, like "time run: 1h" but still timeout.
We can just remove the async stuff IMO
soon, but not yet
If we are planning to remove it I'm not sure why we can just cleanup now
What is the utility, is much slower than regular compilation
why would be the use case?
moreover the job is not reliable
so we are just producing CO2 I think
didn't it catch some issues? in some close_proof refactoring IIRC
@Gaëtan Gilbert likely it did, it's been a while. But IIRC the issues were just problems in the Stm layer. So still not sure the right fix is just not to remove all that code.
We are supporting vio to vo for example, not sure why it makes sense to support a format that is O(n²) SPACE
on the document
I don't get why, after years me explaining it, you still think this job is there to test thr speed. It is there to test that coqide's jump to end does not exploses all the times.
I don't think this job is there to test speed
I do think what is testing is not very useful
and moreover taking a huge amount of time
We could surely test that coqide behavior a bit differently?
Then there is the issue that often, coqide "jump to end" is slower than a sequential compilation, so why we need that?
@Emilio Jesús Gallego Arias latency and throughput aren’t proportional. “Jump to the end” and “jump to point” are both lower-latency ways to (a) get to a given point (b) get a first-stage checking (like vos).
I don’t use coqide but benefit from this test via async proofs in vscoq
@Paolo Giarrusso we could maybe just then test your use case, which should be much faster?
I mean, don't get me wrong, but the async tests are taking huge CI time, so that testing methodology seems fishy to me, when async-based jobs are like 20% of the CI testing?
Really? Can you show us your calculation?
Core CI: build + test suite + validate:
Total CI time without the heavy ones: 665
Total CI time with (unimath, vst, and fiat-crypto): 1155
Things have gone really bad with unimath btw, that seems like a waste and we should optimize that too. The numbers don't include worker setup which is significant so I guess the first number is more like 600. Anyways would be cool to have better tools to understand that.
That total number is missing doc and 32bit build
@Emilio Jesús Gallego Arias would testing “jump to end and wait for all proofs” be faster? learning at some point that the proofs failed at some point is still useful. Otherwise I'd just use proof general's option to throw away proofs.
Mostl am just voting against throwing away the code until there is a better replacement. How to test that code I don’t know, but I imagine it’s not enough to test it on few files unless they are designed to maximize test coverage?
IIRC I have seen plugin-specific issues with async builds in past releases, and
Next Obligation. seems to have special treatment (or rather, to disable async)
@Paolo Giarrusso indeed the problem with the code we have today is that it is making the development of the replacement very difficult.
Supporting the current code takes a huge amount of available cycles, and moreover, blocks some important refactoring, API redesigns and the old code can't just work with a more dynamic model (which is IMHO what you want)
I think you should stop pushing it. It won't go away before we have a replacement.
I can see why you think that way, but as far as I can tell what we decide to do is not only your call
I don't see why having such discussion is a problem
whatever we decide
I have pretty strong technical and maintainership arguments in favor of the removal; so it is not like I'm coming to this point arbitrarily.
Moreover, such kind of process are common, for example, Isabelle did something similar and turned out pretty well for them
An indisputible fact is that Coq UI is in the same state than 10 year ago
and considerable resources have been spent without a result
I think we can agree on that (modulo jsCoq and unusable experiments such as coq-lsp)
Moreover, the current code seems like not maintained, and creates often problem for people working on other areas (which leads to strongly-worded complains every often in a while)
Anyways, when we discuss this I will present my arguments, then we can see.
that suggests that a separate branch for removing this code and developing the replacement is an option, even tho that has other downsides
but if the branch is master and the replacement is not ready in 6 months, some nontrivial annoyance will result.
I made that code optional, you can link a coq toplevel without the STM. This is whtat we are doing in the vscoqtop wip.
Here we are talking about removing the tests for the STM, which we should keep until some alternative is ready.
People are using CoqIDE and VSCoq, they use that code and we should keep testing it, even if it sucks.
Last updated: Dec 07 2023 at 06:38 UTC