Skip to content

Give Stdlib its own directory#19530

Merged
coqbot-app[bot] merged 98 commits intorocq-prover:masterfrom
proux01:stdlib_repo
Dec 6, 2024
Merged

Give Stdlib its own directory#19530
coqbot-app[bot] merged 98 commits intorocq-prover:masterfrom
proux01:stdlib_repo

Conversation

@proux01
Copy link
Copy Markdown
Contributor

@proux01 proux01 commented Sep 11, 2024 •
edited
Loading

This is a first step to implements part of CEP#83 that reached a common agreement during the dedicated Coq call discussions (tl;dr: give stdlib its own repository, clarify its internal dependencies and ensure they are kept with a CI check, "coq" metapackage keeps depending on "coq-stdlib" and no distribution of packages for induvidual subcomponents) The other parts are PR_to_open and rocq-prover/stdlib#2

  • split code in theories/ between Coq repo (here) and stdlib directory, almost everything (185 kloc) in stdlib but (16 kloc)

    • prelude (6 kloc): everything in Prelude.v, in practice Init/*

    • Setoid and Program and dependencies (4 kloc)

    • BinNums (1 kloc), List (145 loc), needed for primitive types

    • primitive types and their axioms (1262 loc) since they specify things in the kernel:
      Floats (726 loc), Int63 (357 loc), Strings (112 loc) and Array (67 loc)

    • ssreflect (4 kloc)

    • (after last rebase, just before merging) check again that all .v files from theories/ ends up in exactly one of the two directories

  • split test-suite (90% of tests are kept in Coq repo)
    • (after last rebase, just before merging) check again that all .v files from test-suite/ ends up in exactly one of the two directories
  • split the doc (refman in doc/sphinx and stdlib doc in doc/stdlib)
  • adapt README.md / INSTALL.md / CONTRIBUTING.md
  • retrieve a few README and tools from Coq repo
    • write some dev/ci/README.md
    • retrieve lint CI job
    • retrieve .github/PR_TEMPLATE and the like from Coq repo
    • retrieve doc/README.md from Coq repo
    • retrieve a few scripts from dev/tools from Coq repo
  • rename remaining coq-stdlib OPAM package in Coq repo (with now only prelude) to rocq-init, coq-stdlib being now the Stdlib
  • Added changelog (here)
  • fix CI (here), should be easy: just add a stdlib job and dependencies in Makefile.ci / .gitlab.yml
  • Opened overlay pull requests.
  • adapt deployment jobs for stdlib refman and doc
  • merge Adapt to coq/coq#19530. bot#330.
  • (when merging) update opam packages in core-dev [core-dev] Adapt to https://github.com/coq/coq/pull/19530 opam#3240

Overlays (to be merged before the current PR)

Overlays (to be merged in sync with the current PR)

Free overlays (can be merged or not before or after merging the current PR)

@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 11, 2024
@proux01 proux01 mentioned this pull request Sep 11, 2024
Closed
@proux01 proux01 added kind: infrastructure CI, build tools, development tools. zARCHIVED: standard library Previously standard library (do not use anymore, now its own repo). request: full CI Use this label when you want your next push to trigger a full CI. labels Sep 12, 2024
@coqbot-app coqbot-app Bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Sep 12, 2024
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 12, 2024
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 12, 2024
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 12, 2024
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 12, 2024
proux01 added a commit to proux01/Coqtail that referenced this pull request Sep 13, 2024
@proux01
Adapt to rocq-prover/rocq#19530
f9e1fd7
proux01 added a commit to proux01/coq-tools that referenced this pull request Sep 13, 2024
@proux01
Adapt to rocq-prover/rocq#19530
3b4afa1 
example_055 may reveal an actual issue though
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 13, 2024
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 13, 2024
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 13, 2024
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 13, 2024
proux01 added a commit to proux01/fiat that referenced this pull request Sep 14, 2024
@proux01
Adapt to rocq-prover/rocq#19530
f786853
proux01 added a commit to proux01/coq-tools that referenced this pull request Sep 14, 2024
@proux01
Adapt to rocq-prover/rocq#19530
81e2451 
example_055 may reveal an actual issue though
proux01 added a commit to proux01/coq-lsp that referenced this pull request Sep 14, 2024
@proux01
Failing to adapt to rocq-prover/rocq#19530
b7e9c12
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 14, 2024
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 14, 2024
proux01 added a commit to proux01/coq-lsp that referenced this pull request Sep 14, 2024
@proux01
Adapt to rocq-prover/rocq#19530
8c53986
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 14, 2024
proux01 added 10 commits December 5, 2024 22:55
@proux01
[refman] Compile the refman mostly without stdlib
f0c5229 
Using the previously introduced extra option
@proux01
Compile prelude doc without stdlib
36c9950
@proux01
Update CONTRIBUTING.md
1932eaf
@proux01
Rename OPAM package coq-stdlib -> rocq-core
5c34b6c 
This is only the coq-stdlib package in current dir that now only
contains the prelude and a few other things.
The actual coq-stdlib package in stdlib dir remains untouched.
@proux01
Use Corelib instead of Stdlib as namespace for rocq-core
4fa4864 
And add a compat layer in Stdlib.
@proux01
Rename target stdlib-html -> corelib-html
a58bbea
@proux01
[CI] Add stdlib
9519a60
@proux01
[CI] Add refman with all extras
c3dda1f
@proux01
Add changelog
fff68a5
@proux01
Add overlays
2dcc49d
@Zimmi48
Copy link
Copy Markdown
Member

Zimmi48 commented Dec 6, 2024

Windows CI is no longer failing on master. The error for this PR looks real and relevant:

 #=== ERROR while compiling coq-stdlib.dev =====================================#
# context              2.0.10 | win32/x86_64 | ocaml-variants.4.14.2+flambda+mingw64c | https://coq.inria.fr/opam/core-dev#2024-12-05 18:34
# path                 C:/ci/cygwin64/opam/CP.2024.10.1~ci/.opam-switch/build/coq-stdlib.dev
# command              C:\ci\cygwin64\opam\CP.2024.10.1~ci\bin\dune.exe build -p coq-stdlib -j 2 --promote-install-files=false @install
# exit-code            1
# env-file             C:/ci/cygwin64/opam/log/coq-stdlib-1760-837036.env
# output-file          C:/ci/cygwin64/opam/log/coq-stdlib-1760-837036.out
### output ###
# [...]
# Error: Cannot find a physical path bound to logical path
# Prelude with prefix Corelib.
# 
# File "theories/dune", line 1615, characters 1-350:
# 1615 |  (rule
# 1616 |   (targets CarryType.timing CarryType.glob CarryType.vos CarryType.vo)
# 1617 |   (deps ..\..\..\..\theories\Init/Prelude.vo)
# 1618 |   (action (chdir ..\..\..\..\. (run coqc -boot -R theories Stdlib -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories\Numbers\Cyclic\Abstract\CarryType.timing %{dep:CarryType.v}))))
# (cd _build/default && C:\ci\cygwin64\opam\CP.2024.10.1~ci\bin\coqc.exe -boot -R theories Stdlib -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories\Numbers\Cyclic\Abstract\CarryType.timing theories/Numbers/Cyclic/Abstract/CarryType.v)
# Error: Cannot find a physical path bound to logical path
# Prelude with prefix Corelib.

@proux01
Copy link
Copy Markdown
Contributor Author

proux01 commented Dec 6, 2024

Yes, that's expected, the windows CI being based on the core-dev opam repo, it will require an update of the coq.opam package there when merging, hence the checkbox in the top message.

@Zimmi48
Copy link
Copy Markdown
Member

Zimmi48 commented Dec 6, 2024

OK, then I can proceed with merging?
Will you merge the opam PR and ping the maintainers to merge the overlays?

@Zimmi48
Copy link
Copy Markdown
Member

Zimmi48 commented Dec 6, 2024

@coqbot merge now

@coqbot-app
Copy link
Copy Markdown
Contributor

coqbot-app Bot commented Dec 6, 2024

@Zimmi48: Please take care of the following overlays:

  • 19530-proux01-stdlib-repo.sh

@SkySkimmer
Copy link
Copy Markdown
Contributor

SkySkimmer commented Dec 6, 2024

Yes, that's expected, the windows CI being based on the core-dev opam repo, it will require an update of the coq.opam package there when merging, hence the checkbox in the top message.

Are you sure? In the rocq cli prototype windows is passing even though I added rocq-runtime

@proux01
Copy link
Copy Markdown
Contributor Author

proux01 commented Dec 6, 2024 •
edited
Loading

The difference is that the coq-stdlib package is no longer in the root directory I think, so the one in core-dev must be right.

@JasonGross
Copy link
Copy Markdown
Member

JasonGross commented Dec 6, 2024

I believe this PR has been merged too eagerly. The coq-tools overlay PR was only created within the past 24 hours and is not in a mergable state, despite apparently supposed to be merged in sync with this PR. The overlay breaks the ability of the bug minimizer to minimize across different versions of Coq. I do not understand the difference between Corelib and Stdlib well enough to fix it (and am currently too busy to figure this out). @proux01 @Zimmi48 could one of you fix the coq-tools overlay ASAP or else revert this PR?

@ejgallego ejgallego mentioned this pull request Dec 6, 2024
Merged
@ejgallego
Copy link
Copy Markdown
Contributor

ejgallego commented Dec 6, 2024

@JasonGross , you can regard Corelib as "internal". In principle Stdlib replaces Coq, and should be almost drop-in.

This PR indeed did a large amount of loosely changes at the same time, so apart from the renaming of Coq -> Stdlib, you need also to account for the fact that Stdlib now lives in user-contrib, and requires From Stdlib to work.

@Zimmi48
Copy link
Copy Markdown
Member

Zimmi48 commented Dec 6, 2024

Sorry @JasonGross, I was not aware that the coq-tools overlay was new from Corelib and had not been reviewed yet.

@erikmd
Copy link
Copy Markdown
Contributor

erikmd commented Dec 6, 2024 •
edited
Loading

FYI @proux01 the merge of this PR broke the coqorg/coq:dev and rocq/rocq-prover:dev builds.
Because of the coq-stdlib.opam → rocq-core.opam renaming, which should be applied in the Dockerfiles as well.

Maybe you could have opened an overlay for Docker-Coq and Docker-Rocq (albeit this situation is very rare),
or just pingged me that an *.opam file was renamed.

For the time being, I'll try to fix the build and let you know in this thread.

@erikmd
Copy link
Copy Markdown
Contributor

erikmd commented Dec 6, 2024 •
edited
Loading

FYI the build failed anew because it still tries to install coq-stdlib to no avail:

#6 100.4 === install 8 packages
#6 100.4   - install conf-linux-libc-dev 0            [required by coq-core]
#6 100.4   - install coq                 dev (pinned)
#6 100.4   - install coq-bignums         dev
#6 100.4   - install coq-core            dev (pinned)
#6 100.4   - install coq-native          1
#6 100.4   - install coq-stdlib          dev          [required by coq]
#6 100.4   - install coqide-server       dev (pinned)
#6 100.4   - install rocq-core           dev (pinned)

.
.
.

#6 233.4 #=== ERROR while compiling coq-stdlib.dev =====================================#
#6 233.4 "cd": command not found.

should this line be removed or changed?

https://github.com/coq/coq/blob/476460fb01e3f40edf2f4a63470d0cbbd1d89f7a/coq.opam#L28

Cc @proux01 @Zimmi48

@proux01 proux01 mentioned this pull request Dec 7, 2024
Merged
@proux01
Copy link
Copy Markdown
Contributor Author

proux01 commented Dec 7, 2024

@erikmd indeed the core-dev opam packages were broken, should be fixed now: rocq-prover/opam#3244

@erikmd
Copy link
Copy Markdown
Contributor

erikmd commented Dec 7, 2024

OK ! Did you check that the package is fixed also in core-dev / extra-dev ?

Cannot check right now as I'm away from keyboard right now - texting from my cell phone

@JasonGross JasonGross mentioned this pull request Dec 10, 2024
Merged
@Zimmi48 Zimmi48 mentioned this pull request Dec 11, 2024
Merged
@proux01 proux01 mentioned this pull request Dec 25, 2024
Merged
10 tasks
@ejgallego ejgallego mentioned this pull request Jan 17, 2025
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@JasonGross JasonGross JasonGross left review comments

@andres-erbsen andres-erbsen andres-erbsen left review comments

@Zimmi48 Zimmi48 Zimmi48 approved these changes

@jfehrle jfehrle jfehrle left review comments

@silene silene silene left review comments

@SkySkimmer SkySkimmer SkySkimmer left review comments

+1 more reviewer

@ejgallego ejgallego ejgallego left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@Zimmi48 Zimmi48

Labels

kind: infrastructure CI, build tools, development tools. zARCHIVED: standard library Previously standard library (do not use anymore, now its own repo).

Projects

None yet

Milestone

9.0+rc1

Development

Successfully merging this pull request may close these issues.