Adapt to https://github.com/coq/coq/pull/19530

[proux01]

To be merged in sync with the upstream PR

[ejgallego]

A way should be found for test that depend on Stdlib to work.

[ejgallego]

Note that to really test this in this CI you want to bump the vendor/coq submodule to the commit ID of your PR.

Note the development build setup we use here (and in jsCoq and some other projects) relies heavily on dune caching, in particular it has the following features:

• git bisects are cached and sound
• CI is fully cached
• local dev setup is fully cached

This saves literally hundreths of stdlib recompilation per month, and sometimes per week.

[proux01]

I let you do that as I tend to wreak havoc as soon as I touch a git submodule.

[proux01]

Anyway, this means this PR should now be backward compatible and should be merged before the upstream PR.

That being said, I thing that pulling a whole stdlib dependency just for a few tests is probably not worth the effort but well, your piece of software, your decision.

[ejgallego]

I let you do that as I tend to wreak havoc as soon as I touch a git submodule.

Ok, I've bumped to submodule to latest upstream.

Anyway, this means this PR should now be backward compatible and should be merged before the upstream PR.

I am not sure I understand the patch, but indeed it seems strange for the current main branch even?

Does the patch mean that after coq/coq#19530 coqc -config doesn't return a correct COQLIB value?

Because that is what fcc uses.

That being said, I thing that pulling a whole stdlib dependency just for a few tests is probably not worth the effort but well, your piece of software, your decision.

Well, we need to test all Coq plugins, and moreover, we need to do tests on complex files, for example Pfff.v is an essential use case, as well as Rtrigo.v. Redoing all these tests would actually be a huge amount of work, and moreover they would become more fragile as we would depend on plugin internals and thus we would have sync each time Coq / stdlib changes.

Indeed, I don't see how easily replace these tests and don't stop testing important stuff. (Happy to hear about that, for example, solving the bug about registration of generic args would allow us to remove most of serlib).

In fact, the testing we do with the current CI is way minimal compared to they way we are testing flèche in real world.

To give an example, we recently had an agent running for a week doing thousands and thousands of edits (RL application). Another important test is to load all of HoTT, math-comp, and Compcert, and interrupt, etc...

Anyways, the current coq-lsp developer setup does not depend on stdlib being in the Coq repos, it does depend essentially in the stdlib being dune-friendly tho, because of CI and dev caching. So if we lose that, it is a big regression.

[ejgallego]

Pushed a few commits fixing the build setup, but indeed all tests fails as Coq cannot find the stdlib anymore.

The new repository for the stdlib doesn't have build caching support, so that's an important regression; other than that, when this problem is fixed, there is no other blockage on view.

[ejgallego]

Adapted to roqc-init.

[proux01]

The new repository for the stdlib doesn't have build caching support, so that's an important regression; other than that, when this problem is fixed, there is no other blockage on view.

PR welcome on https://github.com/coq-community/stdlib-test/ if you want to add that but I won't do it myself, not skilled enough in dune.

[ejgallego]

PR welcome on https://github.com/coq-community/stdlib-test/ if you want to add that but I won't do it myself, not skilled enough in dune.

I can take care of that, however I failed to understand the new setup sorry. Questions:

• where does roqc-stdlib install now?
• how is the loadpath supossed to look? I see -Q is used now for dev, but likely not on install?

[proux01]

See the CoqProject / coq_makefile input https://github.com/coq-community/stdlib-test/blob/master/theories/Make.all for details

[ejgallego]

See the CoqProject / coq_makefile input https://github.com/coq-community/stdlib-test/blob/master/theories/Make.all for details

Sorry @proux01 , I cannot dechiper what it means, in particular I cannot see where the install location is specified.

Does it mean that the Makefile installs the .vo files in $coqlib/user-contrib/Stdlib ?

[proux01]

Sure, where else?

[ejgallego]

Changes look good, but pending on recovering caching on https://github.com/coq-community/stdlib-test

[ejgallego]

Sure, where else?

Oh, if that's the case Dune support should be trivial.

So once the split happens, people cannot do Require Import Lists. for example?

[ejgallego]

Just for info, another thing that is hard to test without loading lots of libs is printing.

[proux01]

So once the split happens, people cannot do Require Import Lists. for example?

Ultimately indeed, but as a temporary backward compatibility measure, any failing attempt at Require M would first trigger a From Stdlib Require M before failing. And in case of succes, the user will get a warning suggesting to add the From Stdlib: coq/coq@c8c6e49. We'll keep the warning for a few versions (likely a pair of years or so) before cleaning up the compatibility code.

[ejgallego]

Ultimately indeed, but as a temporary backward compatibility measure, any failing attempt at Require M would first trigger a From Stdlib Require M before failing. And in case of success, the user will get a warning suggesting to add the From Stdlib: coq/coq@c8c6e49. We'll keep the warning for a few versions (likely a pair of years or so) before cleaning up the compatibility code.

I see thanks; I went and checked the code myself.

The way is implemented seems problematic tho: it seems to me that coq-stdlib should be the one deciding this, and not coq-core, but I will think more about it. For now I've put a request for changes to remember to check that this doesn't introduce any problems, for now, coqdep is broken.

[proux01]

The way is implemented seems problematic tho: it seems to me that coq-stdlib should be the one deciding this, and not coq-core,

Well, I certainly wouldn't consider that acceptable as a definitive solution but it seems to work well enough as a temporary solution. The very fact that we were able to load that code without From was already quite debatable anyway, so if we have to keep that awkward thing a bit more in order to fix it, it may be acceptable in the end.

coqdep is broken.

I'll have a look

[ejgallego]

Well, I certainly wouldn't consider that acceptable as a definitive solution but it seems to work well enough as a temporary solution. The very fact that we were able to load that code without From was already quite debatable anyway, so if we have to keep that awkward thing a bit more in order to fix it, it may be acceptable in the end.

I need to think more about this, I was afraid that the "substitution" property would break, but maybe it can work like this.

Will take care of it and report back on the main PR.

For coqdep, unfortunately you need to patch coqdep's own copy of loadpath, also for coqcheck. I've been trying to remove this duplicity for years but without success :(

[proux01]

Coqdep fixed coq/coq@9cd7532 (still have to look at coqchk). Thanks for pointing the issue, I guess I didn't noticed it because I didn't really used it with -boot.

[ejgallego]

Yeah, the coqdep stuff is actually quite problematic because the warnings are a real problem, but they are ignored.

The, due to the way things work, if we hadn't noticed about coqdep, we would have merged, but then, a race condition is in the code, and users would have gotten build failures when using more processors than our CI.

I think the root of the issue here is that our CI doesn't require silent builds. This is a key practice used in industry, but unfortunately I didn't get very far moving the Coq setup towards it.

[proux01]

Yeah, the coqdep stuff is actually quite problematic because the warnings are a real problem, but they are ignored.

Yes, I'm also a bit surprised that this is only a warning.

I think the root of the issue here is that our CI doesn't require silent builds. This is a key practice used in industry, but unfortunately I didn't get very far moving the Coq setup towards it.

I hope that coq/coq#19562 will help moving in that direction: if we can expect from CI project maintainers to quickly adapt to new warnings (even by just selectively silencing them as a short term solution) it will be easier to request silent builds. UNfortunately, this kind of changes takes time, for instance we only added such a check very recently in mathcomp's CI: math-comp/math-comp#1254

[ejgallego]

Yes, I'm also a bit surprised that this is only a warning.

Indeed, see the corresponding Coq issue about it, but this is something we inherit from OCaml decades ago. The discussion on the OCaml issue is interesting.

IMHO it is time we fix this in Coq and make coqdep failing to find a dependency and error.

I hope that coq/coq#19562 will help moving in that direction: if we can expect from CI project maintainers to quickly adapt to new warnings (even by just selectively silencing them as a short term solution) it will be easier to request silent builds.

I hope it helps, however past experience with projects maintainers doesn't give me a lot of hope.

In general, people hate having to do stuff by hand. So either it happens because you have very advanced tooling, or the incentives need to be there.

Note that moreover coq_makefile , and even coqc don't really support silent builds yet, some relevant Coq issues are coq/coq#10910 coq/coq#12923 coq/coq#14114 coq/coq#15722

[proux01]

I hope it helps, however past experience with projects maintainers doesn't give me a lot of hope.
[...] the incentives need to be there.

That's what coq/coq#19562 is all about. We have been historically way to kind with CI project maintainers. Having clearer rules can only help.

[SkySkimmer]

Note that moreover coq_makefile , and even coqc don't really support silent builds yet, some relevant Coq issues are coq/coq#10910 coq/coq#12923 coq/coq#14114 coq/coq#15722

All those are about coqc, should we open an issue to have a coq_makefile silent mode (ie not printing COQC INSTALL etc)?

Although note that in CI we also print per-file timing info, so having silent build in CI would mean losing the timing info, not sure if that's a good tradeoff.

[ejgallego]

That's what coq/coq#19562 is all about. We have been historically way too kind with CI project maintainers. Having clearer rules can only help.

That's an interesting point of view, I guess in this case we have different versions of "historically".

IMHO it is more accurate to say that historically Coq didn't care too much about compatibility, with quite epic breakages happening in Coq history that brought large levels of pain to users.

CI is a very recent thing Pierre-Yves Strub started and me, then Gaëtan, developed to its current state (of course a lot more people did work in CI, but current design choices were mainly this way IIRC)

My view is that it is a really good thing that we have been kind to Coq users, and overall, I think our current approach has prevented a lot of pain, porting time, and frustration that grew common in Coq users before the current CI setup.

[ejgallego]

Hi @ejgallego
The stdlib-test repository is now built with dune https://github.com/coq-community/stdlib-test/blob/master/theories/dune could you please try to update the CI config here to test that?

Cool! Sure, I'll take care. When do you need it? I'm super busy this start of week.

[proux01]

Coq call on the subject is planned on October 8th so no need for it before that.

[proux01]

Thanks, according to the CI of coq/coq#19530 this works https://gitlab.inria.fr/coq/coq/-/jobs/4840390

[ejgallego]

Thanks @proux01 , indeed, as things stand upstream, there is no overlay needed for coq-lsp and you folks managed to make the case where Coq is installed fully backwards compatible.

However, our setup for development still breaks as we cannot vendor coq-stdlib anymore due to the (name Stdlib) conflict.

This would make development here pretty hard, and also for jsCoq, a typical example of our development workflow for example for the patch at coq/coq#19177 involves patching Coq and being able to build some file in CompCert pretty quick for testing; dune composed build provides large speedups here.

I agree this is a specific problem we folks that often patch Coq (like coq-lsp / jsCoq and bedrock) have.

[proux01]

I'm not sure I understand why we don't need an overlay here while coq-elpi needs one but well.

[ejgallego]

@proux01 no idea, can I help with coq-elpi overlay? Happy to look at the CI failure (maybe ping me on Zulip)

[ejgallego]

@proux01 I was trying to push to this branch but turns out that it was deleted, somehow magit didn't properly return an error message.

Do you want to restore the branch so I push the updated overlay?

Problem solved

[proux01]

I updated the upstream branch but I don't know how to update the submodule here, so I guess that explain all the red in the CI.

[ejgallego]

I updated the upstream branch but I don't know how to update the submodule here, so I guess that explain all the red in the CI.

@proux01 , the submodule can be updated in the usual way, just point the vendor/coq repos to whatever commit it should be at.

Usually it is not a big deal to have overlays without updating the submodule here, as Coq's CI doesn't use the submodule, but Coq master.

Submodule is here mainly to ensure git bisect works.

The idea is to have a mechanism in CI so overlays can tell downstream CI's what Coq commit to use, but I didn't have time to implement it yet.

[ejgallego]

I did update the ref, but it seems you reverted the change? (edit: I mean you reverted the change in 19530)

[proux01]

I don't know, I usually tend to wreck havoc with git submodules, so quite possible.

[ejgallego]

I mean the current version of 19530 doesn't seem to match the changes you pushed here?