Skip to content

Give Stdlib its own directory #19530

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 98 commits into from
Dec 6, 2024
Merged

Give Stdlib its own directory #19530

merged 98 commits into from
Dec 6, 2024

Conversation

proux01
Copy link
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
@erikmd
Copy link
Member

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 added a commit to rocq-community/docker-coq that referenced this pull request Dec 6, 2024
@erikmd
hotfix: s/coq-stdlib/rocq-core/
cc9f12a 
docker-keeper: rebuild-keyword: dev

See-also: rocq-prover/rocq#19530 (comment)
erikmd added a commit to rocq-community/docker-rocq that referenced this pull request Dec 6, 2024
@erikmd
hotfix(docker-rocq): s/coq-stdlib/rocq-core/
b5fe3a7 
docker-keeper: rebuild-keyword: dev

See-also: rocq-prover/rocq#19530 (comment)
@erikmd
Copy link
Member

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

ppedrot added a commit to MetaRocq/metarocq that referenced this pull request Dec 7, 2024
@ppedrot
Merge pull request #1102 from proux01/stdlib_repo
a1b0749 
Adapt to rocq-prover/rocq#19530
samuelgruetter added a commit to mit-plv/coqutil that referenced this pull request Dec 7, 2024
@samuelgruetter
Merge pull request #121 from proux01/stdlib_repo
a2bbdb2 
Adapt to rocq-prover/rocq#19530
gares added a commit to LPCIC/coq-elpi that referenced this pull request Dec 7, 2024
@gares
Merge pull request #688 from proux01/stdlib_repo
c082aee 
Adapt to rocq-prover/rocq#19530
proux01 added a commit to proux01/rocq that referenced this pull request Dec 7, 2024
@proux01
Fix opam --with-test
d8ab559 
That I accidentally broke in rocq-prover#19530

See rocq-prover/opam#3240
@proux01 proux01 mentioned this pull request Dec 7, 2024
Merged
proux01 added a commit to proux01/rocq that referenced this pull request Dec 7, 2024
@proux01
Fix opam --with-test
bade053 
That I accidentally broke in rocq-prover#19530

See rocq-prover/opam#3240
@proux01
Copy link
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
Member

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

proux01 added a commit to proux01/coq-tools that referenced this pull request Dec 7, 2024
@proux01
Adapt to rocq-prover/rocq#19530
27538d0
JasonGross pushed a commit to proux01/coq-tools that referenced this pull request Dec 8, 2024
@proux01 @JasonGross
Adapt to rocq-prover/rocq#19530
7c72412
proux01 added a commit to proux01/QuickChick that referenced this pull request Dec 9, 2024
@proux01
Adapt to rocq-prover/rocq#19530
5fd22a0
JasonGross added a commit to JasonGross/coq-tools that referenced this pull request Dec 9, 2024
@proux01 @JasonGross
Adapt to rocq-prover/rocq#19530 (#240)
f513668 
* Adapt to rocq-prover/rocq#19530

* Apply suggestions from code review

---------

Co-authored-by: Jason Gross <jasongross9@gmail.com>
Lysxia pushed a commit to QuickChick/QuickChick that referenced this pull request Dec 9, 2024
@proux01 @Lysxia
Adapt to rocq-prover/rocq#19530
7b33d19
@JasonGross JasonGross mentioned this pull request Dec 10, 2024
Merged
@Zimmi48 Zimmi48 mentioned this pull request Dec 11, 2024
Merged
thery pushed a commit to thery/opam-coq-archive that referenced this pull request Dec 19, 2024
@proux01 @thery
Adapt to rocq-prover/rocq#19530
03da02a
proux01 added a commit to proux01/coq-tools that referenced this pull request Dec 23, 2024
@proux01
Adapt to rocq-prover/rocq#19530
d42b2a3
@proux01 proux01 mentioned this pull request Dec 25, 2024
Merged
10 tasks
proux01 added a commit to proux01/flocq that referenced this pull request Jan 6, 2025
@proux01 @silene
Adapt to rocq-prover/rocq#19530
d8a6fca
proux01 pushed a commit to proux01/flocq that referenced this pull request Jan 6, 2025
@silene
Merge branch 'stdlib_repo' into 'master'
d782e8d 
Adapt to rocq-prover/rocq#19530

See merge request flocq/flocq!24
proux01 added a commit to proux01/flocq that referenced this pull request Jan 6, 2025
@proux01
Partially revert "Adapt to rocq-prover/rocq#19530"
0a685a5 
This partially reverts commit d8a6fca.
andrew-appel pushed a commit to PrincetonUniversity/VST that referenced this pull request Jan 9, 2025
@andres-erbsen
Revert "Adapt to rocq-prover/rocq#19530 (#794)" (#799)
b19278e 
This reverts commit 8688af9.
@ejgallego ejgallego mentioned this pull request Jan 17, 2025
Open
palmskog pushed a commit to rocq-community/aac-tactics that referenced this pull request Feb 19, 2025
@proux01 @palmskog
Adapt to rocq-prover/rocq#19530
3b1eb3a
palmskog added a commit to rocq-community/aac-tactics that referenced this pull request Feb 19, 2025
@palmskog
Merge pull request #149 from coq-community/stdlib_repo
1dde529 
Adapt to rocq-prover/rocq#19530
andres-erbsen added a commit to mit-plv/rupicola that referenced this pull request Jun 17, 2025
@proux01 @andres-erbsen
Adapt to rocq-prover/rocq#19530 (#130)
2607e99 
Co-authored-by: Andres Erbsen <andres-github@andres.systems>
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

@ejgallego ejgallego ejgallego left review comments

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.