Stream: Coq devs & plugin devs

Topic: CI for base+async timing out


view this post on Zulip Pierre-Marie Pédrot (May 24 2022 at 14:21):

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?

view this post on Zulip Pierre-Marie Pédrot (May 24 2022 at 14:22):

Judging from the place where it dies (at the end of Reals) it's probably short of a few minutes, if not seconds.

view this post on Zulip Pierre-Marie Pédrot (May 24 2022 at 14:23):

Should we just bump the time limit?

view this post on Zulip Enrico Tassi (May 24 2022 at 14:53):

I saw inconclusive measurements as well, like "time run: 1h" but still timeout.

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 16:03):

We can just remove the async stuff IMO

view this post on Zulip Enrico Tassi (May 24 2022 at 19:52):

soon, but not yet

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 19:54):

If we are planning to remove it I'm not sure why we can just cleanup now

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 19:54):

What is the utility, is much slower than regular compilation

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 19:54):

?

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 19:54):

why would be the use case?

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 19:54):

moreover the job is not reliable

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 19:54):

so we are just producing CO2 I think

view this post on Zulip Gaëtan Gilbert (May 24 2022 at 19:56):

didn't it catch some issues? in some close_proof refactoring IIRC

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 19:57):

@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.

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 19:58):

We are supporting vio to vo for example, not sure why it makes sense to support a format that is O(n²) SPACE

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 19:58):

on the document

view this post on Zulip Enrico Tassi (May 24 2022 at 19:58):

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.

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 19:58):

I don't think this job is there to test speed

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 19:59):

I do think what is testing is not very useful

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 19:59):

and moreover taking a huge amount of time

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 19:59):

We could surely test that coqide behavior a bit differently?

view this post on Zulip Enrico Tassi (May 24 2022 at 19:59):

Good night

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 20:00):

Then there is the issue that often, coqide "jump to end" is slower than a sequential compilation, so why we need that?

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 20:00):

Good night

view this post on Zulip Paolo Giarrusso (May 24 2022 at 21:44):

@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).

view this post on Zulip Paolo Giarrusso (May 24 2022 at 21:45):

I don’t use coqide but benefit from this test via async proofs in vscoq

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 09:12):

@Paolo Giarrusso we could maybe just then test your use case, which should be much faster?

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 09:13):

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?

view this post on Zulip Enrico Tassi (May 25 2022 at 09:23):

Really? Can you show us your calculation?

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 09:38):

Core CI: build + test suite + validate:

Total CI time without the heavy ones: 665
Total CI time with (unimath, vst, and fiat-crypto): 1155

So 15%

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.

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 09:39):

That total number is missing doc and 32bit build

view this post on Zulip Paolo Giarrusso (May 25 2022 at 09:40):

@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?

view this post on Zulip Paolo Giarrusso (May 25 2022 at 09:41):

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)

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 09:43):

@Paolo Giarrusso indeed the problem with the code we have today is that it is making the development of the replacement very difficult.

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 09:44):

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)

view this post on Zulip Enrico Tassi (May 25 2022 at 09:46):

I think you should stop pushing it. It won't go away before we have a replacement.

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 09:49):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 09:49):

I don't see why having such discussion is a problem

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 09:49):

whatever we decide

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 09:50):

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.

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 09:51):

Moreover, such kind of process are common, for example, Isabelle did something similar and turned out pretty well for them

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 09:51):

An indisputible fact is that Coq UI is in the same state than 10 year ago

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 09:51):

and considerable resources have been spent without a result

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 09:52):

I think we can agree on that (modulo jsCoq and unusable experiments such as coq-lsp)

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 09:53):

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.

view this post on Zulip Paolo Giarrusso (May 25 2022 at 09:56):

that suggests that a separate branch for removing this code and developing the replacement is an option, even tho that has other downsides

view this post on Zulip Paolo Giarrusso (May 25 2022 at 09:58):

but if the branch is master and the replacement is not ready in 6 months, some nontrivial annoyance will result.

view this post on Zulip Enrico Tassi (May 25 2022 at 09:59):

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.

view this post on Zulip Gaëtan Gilbert (May 25 2022 at 19:17):

I have invented perhaps my greatest hack yet "ultradebug" https://github.com/coq/coq/commit/9f452746efc6698cde6d5ae4580e8dd3aa53b782
it dumps vernacstate + the current command to a file when a command fails
ran it over 70 times until I got a reproduction https://gitlab.com/SkySkimmer/coq/-/jobs/2506693702 (error in https://github.com/coq/coq/blob/f2031737b6ffed2a687f2bb8b27a12924f96619e/theories/Numbers/DecimalNat.v#L86 while checking the type) (50 times in this pipeline but there were a couple before it)
the first attempt to use it locally failed and I almost gave up, but I found that Future.chain forces and raises on NotHere
commenting out that force worked and I could reproduce in the debugger
as we might expect it fails in Reduction.check_leq on Set and Coq.Init.Logic.9 (also known as eq.u0)
the universe graph looks normal

(ocd) p univs
univs: UGraph.t =
  Set < Coq.setoid_ring.BinList.1
      < Coq.Numbers.BinNums.1
      < Coq.Init.Datatypes.1
...
      < Coq.Init.Logic.9
...

finally we reach https://github.com/coq/coq/blob/f2031737b6ffed2a687f2bb8b27a12924f96619e/lib/acyclicGraph.ml#L650
and repr_node u (where u is Set) produces....

view this post on Zulip Gaëtan Gilbert (May 25 2022 at 19:17):

  {canon = <abstr>; ltle = <abstr>; gtge = <abstr>;
   rank = 1000000; klvl = 0; ilvl = -2568; status = Visited}

VISITED?!

view this post on Zulip Maxime Dénès (May 25 2022 at 19:54):

Ah ah, nice methodology


Last updated: Feb 02 2023 at 15:04 UTC