Give Stdlib its own repository

[proux01]

Reopening of #19686 to clearup github push history.

Follow up of #19530 (the new Stdlib repo for testing is at https://github.com/coq/stdlib-test (final URL should be https://github.com/coq/stdlib))

• Adapt changelog infrastructure
• add CI to stdlib with everything in Coq CI that depends from stdlib
  • everything works (c.f. CI status on https://github.com/coq/stdlib-test )
  • job stdlib-test for test-suite (the 10% of Coq test-suite that ends up in stdlib)
  • job stdlib-refman-html for refman
  • job stdlib-html for doc
• (when merging) rename coq/stdlib-test to coq/stdlib
• (when merging) update opam packages in core-dev (merge Adapt to https://github.com/coq/coq/pull/19975 (Give Stdlib its own repository) opam#3285 in sync with current PR)
• (when merging) create a dedicated zulip stream and mention it in CONTRIBUTING.md
• (after merge) move all issues / PR related to stdlib from Coq repo to Stdlib repo

[ppedrot]

Is this supposed to be part of 9.0?

[proux01]

Well, it would be better if it could be. That would avoid having a branch/release in the current intermediate state with stdlib only in a directory. That being said, it shouldn't delay the branching/release.

[proux01]

Thank you for the hint to use another repo (I followed this discussion). This is how far I get now in the stdlib repo:

/tmp/stdlib/dev/ci/ci-common.sh: line 13: syntax error near unexpected token `$which'

Don't know how I made that stupid typo, it's obviously $( and not ($

In the Coq repo, I can build ci-stdlib, but I haven't figured out yet how to edit a file in partially-built stdlib. In particular, if I do

vim stdlib/./theories/ZArith/Znumtheory.v # add a build error such as `Goal.`
make world
make -j ci-stdlib_test
dune exec -- vim stdlib/./theories/ZArith/Znumtheory.v

then I get "Cannot find a physical path bound to logical path ZArith_base". The same if I run dune exec from the stdlib directory. If all of stdlib does build, editing seems to work.

No idea what dune exec is doing. That being said, putting the local copy of the stdlib git repo inside the coq one doesn't sound like a very good idea.

[Zimmi48]

That being said, putting the local copy of the stdlib git repo inside the coq one doesn't sound like a very good idea.

Why? This is precisely what people who want so-called "composed builds" usually do: they clone one repo in a sub-folder on another (one way or the other).

[proux01]

Sounds like the best way for me to get confused about which git repo we are in.

[proux01]

In any case, in terms of directory structure, this should get you in the exact same situation as the current Coq master, so it's completely orthogonal to the current PR.

[ppedrot]

As the plenipotentiary RM.

[ppedrot]

@coqbot merge now

[Zimmi48]

In any case, in terms of directory structure, this should get you in the exact same situation as the current Coq master, so it's completely orthogonal to the current PR.

Yes, that's what I would expect. And it has been tested to work successfully with compositional Dune builds (after a few adjustments to the Dune files IIRC).

[proux01]

FTR about the said adjustments: https://coq.zulipchat.com/#narrow/channel/237656-Coq-devs-.26-plugin-devs/topic/stdlib.20composed.20build/near/486512903

[andres-erbsen]

@proux01 could you please fix this? I agree it's a regression from the directory-splitting PR, not the repository-splitting one, but it is still a regression. Breaking interactive editing with non-installed coq as well as composed builds significantly affects my workflow (and probably others', as @ Zimmi48 suggests above). Maybe the workaround you link to works well, but I am an unsophisticated dune user, and don't understand it, so wouldn't be able to troubleshoot if it ever goes wrong or stops working.

[proux01]

I unfortunately have no idea how to fix this dune thing. Have you tried the composed build setting discussed above? it might be linked. My understanding is that composed build is only used by a couple of users which doesn't help considering dune for Coq remains a pretty brittle thing already (particularly inside Coq itself with this dunestrap thing still lying around and apparently preventing proper composed builds).

[Zimmi48]

Of the two steps reported to make composed builds work:

• removed (dirs :standard \ stdlib) in the top-level dune file
• renamed dune.disabled into dune in both theories and user-contrib/Ltac2

the first has actually already been fixed in the PR that removed the stdlib sub-directory.

The second one means that having composed builds work require running "normal" Dune Coq support rather than the one that ships with the make dunestrap target here. I don't know if there is a way yet to get rid of make dunestrap in the Coq/Rocq repo.

[proux01]

Apparently we currently cannot: https://coq.zulipchat.com/#narrow/channel/237656-Coq-devs-.26-plugin-devs/topic/stdlib.20composed.20build/near/486516060

[ejgallego]

Apparently we currently cannot: https://coq.zulipchat.com/#narrow/channel/237656-Coq-devs-.26-plugin-devs/topic/stdlib.20composed.20build/near/486516060

The async and vok builds were actually relevant for the stdlib, now that the stdlib is not in the Coq repos anymore these builds do almost nothing tho.

[proux01]

Are you saying that we could actually get rid of dunestrap (or at least make dune.disabled the default) ?

[ejgallego]

Are you saying that we could actually get rid of dunestrap (or at least make dune.disabled the default) ?

I am saying that the async and vos builds that dunestrap support seem not to be relevant anymore. I guess they should be removed from CI too?

As to whether we could build Corelib with the built-in rules, I think it is hard to answer, IIRC there was quite a lot of discussion back in the day about it when we decided to introduce dunestrap. Each approach has a different set of pros and cons, it depends on the technical roadmap we'd like to follow. Briefly:

• dunestrap gives total control over the build rules, but it is less powerful, as it uses the dune language
• dune builtin Coq rules gives Coq way less control, on the other hand they can access the full Dune API which is way more powerful that what you can do from dune files

Note that we proposed to vendor dune back in the day, however that rejected, IMHO for the wrong reasons (c.f. #8615)

[proux01]

Ok, but concretely, what are the benefits of keeping dunestrap? the only one I can get out of you above message is

• dunestrap gives total control over the build rules

But what do we concretely get today out of this? that is important enough to justify disabling composed build for instance?

Sure, having full control over the build system like we still do with rocq_makefile would be good, but considering we don't get that anyway, I still fail to get the benefit of this kind of intermediate solution (but again, I'm no expert here).

[ejgallego]

Benefit @proux01 is that if you want to modify the rules you don't need to patch dune and wait for a new dune release.

This used to be relevant when we were building the stdlib. With the current status quo of just a few .v files in the coq source tree, indeed this doesn't seem very important.

On the other hand, it is well-known in the build system communities that use cases are very hard to anticipate, so I would personally think about the future roadmap in terms of build tooling for Coq before going and removing the custom rule generator as to be sure we are not missing anything.

[proux01]

Benefit @proux01 is that if you want to modify the rules you don't need to patch dune and wait for a new dune release.

I understand but my current feeling is that this is not very effective in practice (only my small experience on the recent renamings)

What about the following course of action:

• switch dune.disabled to be the default
• keep testing dunestrap in the CI (as we currently do for dune.disabled), at least for a while

That should enable to evaluate the situation for some time without loosing the possibility to come back to dunestrap, WDYT?
(actually, let's discuss that in call https://github.com/coq/coq/wiki/Coq-Call-2025-01-14 that discussion is verring a bit off-topic here )

[SkySkimmer]

Using builtin rules means we depend on coqc

[andres-erbsen]

Thank you all for looking into this. Fwiw, my concern above was primarily driven by interactive editing of stdlib when iterating on a WIP coq change that breaks it, not composed builds in the full sense (which I think are also great, but not that specifically important between stdlib and coq alone).