Merge PR coq#19975: Give Stdlib its own repository

Reviewed-by: ppedrot Co-authored-by: ppedrot <[email protected]>
SkySkimmer · Jan 13, 2025 · c4ea8b1 · c4ea8b1
2 parents b7dbba4 + 31aea72
commit c4ea8b1
Show file tree

Hide file tree

Showing 1,007 changed files with 20 additions and 230,448 deletions.
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -243,13 +243,11 @@ before_script:
     - if [ "$ROCQ_CI_NATIVE" = true ]; then opam install -y rocq-native; fi
     - opam pin add --kind=path rocq-runtime.dev .
     - opam pin add --kind=path rocq-core.dev .
-    - opam pin add --kind=path rocq-stdlib.dev stdlib/
     - if [ "$ROCQ_CI_NATIVE" = true ]; then echo "Definition f x := x + x." > test_native.v; fi
     - if [ "$ROCQ_CI_NATIVE" = true ]; then rocq c test_native.v; fi
     - if [ "$ROCQ_CI_NATIVE" = true ]; then test -f .coq-native/Ntest_native.cmxs; fi
     - if command -v coqc; then exit 1; fi # coq-core didn't get autoinstalled
     - opam pin add --kind=path coq-core.dev .
-    - opam pin add --kind=path coq-stdlib.dev stdlib/
     - opam pin add --kind=path coqide-server.dev .
     - opam pin add --kind=path coqide.dev .
   after_script:

diff --git a/dev/bench/bench.sh b/dev/bench/bench.sh
@@ -49,7 +49,7 @@ check_variable () {
 : "${old_coq_version:=dev}"
 : "${num_of_iterations:=1}"
 : "${timeout:=3h}"
-: "${coq_opam_packages:=coq-bignums coq-hott coq-performance-tests-lite coq-engine-bench-lite coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-mathcomp-analysis coq-math-classes coq-corn coq-compcert coq-equations coq-metacoq-utils coq-metacoq-common coq-metacoq-template coq-metacoq-pcuic coq-metacoq-safechecker coq-metacoq-erasure coq-metacoq-translations coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto-with-bedrock coq-unimath coq-coquelicot coq-iris-examples coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast coq-vst coq-category-theory coq-neural-net-interp-computed-lite}"
+: "${coq_opam_packages:=rocq-stdlib coq-bignums coq-hott coq-performance-tests-lite coq-engine-bench-lite coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-mathcomp-analysis coq-math-classes coq-corn coq-compcert coq-equations coq-metacoq-utils coq-metacoq-common coq-metacoq-template coq-metacoq-pcuic coq-metacoq-safechecker coq-metacoq-erasure coq-metacoq-translations coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto-with-bedrock coq-unimath coq-coquelicot coq-iris-examples coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast coq-vst coq-category-theory coq-neural-net-interp-computed-lite}"
 : "${coq_native:=}"
 
 # example: coq-hott.dev git+https://github.com/some-user/coq-hott#some-branch
@@ -389,6 +389,7 @@ create_opam() {
     opam var --global jobs=$number_of_processors >/dev/null
     if [ ! -z "$BENCH_DEBUG" ]; then opam config list; fi
 
+    opam repo add -q --this-switch coq-core-dev "$OPAM_COQ_DIR/core-dev"  # For rocq-stdlib
     opam repo add -q --this-switch coq-extra-dev "$OPAM_COQ_DIR/extra-dev"
     opam repo add -q --this-switch coq-released "$OPAM_COQ_DIR/released"
 
@@ -462,7 +463,7 @@ export PROFILING=1
 export COQ_PROFILE_COMPONENTS=command,parse_command,partac.perform
 
 # packages tied to the coq commit need to be pinned accordingly
-core_packages='rocq-runtime coq-core rocq-core coq-stdlib coqide-server coq'
+core_packages='rocq-runtime coq-core rocq-core coqide-server'
 
 for coq_opam_package in $core_packages $coq_opam_packages; do
 

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
@@ -416,6 +416,13 @@ project verdi "https://github.com/uwplse/verdi" "master"
 project verdi_raft "https://github.com/uwplse/verdi-raft" "master"
 # Contact @palmskog on github
 
+########################################################################
+# Stdlib
+########################################################################
+project stdlib "https://github.com/coq/stdlib-test" "master"
+# TODO replace temporary test repo by actual one
+# Contact TODO on github
+
 ########################################################################
 # argosy
 ########################################################################

diff --git a/dev/ci/ci-stdlib.sh b/dev/ci/ci-stdlib.sh
@@ -5,9 +5,11 @@ set -e
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
+git_download stdlib
+
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
-( cd "stdlib"
+( cd "${CI_BUILD_DIR}/stdlib"
   dev/with-rocq-wrap.sh dune build --root . --only-packages=rocq-stdlib @install
   dev/with-rocq-wrap.sh dune install --root . rocq-stdlib --prefix="$CI_INSTALL_DIR"
 )
diff --git a/dev/ci/ci-stdlib_doc.sh b/dev/ci/ci-stdlib_doc.sh
@@ -7,7 +7,7 @@ ci_dir="$(dirname "$0")"
 
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
-( cd "stdlib"
+( cd "${CI_BUILD_DIR}/stdlib"
   make refman-html
   make stdlib-html
 )
diff --git a/dev/ci/ci-stdlib_test.sh b/dev/ci/ci-stdlib_test.sh
@@ -7,6 +7,6 @@ ci_dir="$(dirname "$0")"
 
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
-( cd "stdlib/test-suite"
+( cd "${CI_BUILD_DIR}/stdlib/test-suite"
   make
 )
diff --git a/doc/changelog/11-standard-library/17560-nat_mul_reg.rst b/doc/changelog/11-standard-library/17560-nat_mul_reg.rst
diff --git a/doc/changelog/11-standard-library/18183-lt_list.rst b/doc/changelog/11-standard-library/18183-lt_list.rst
diff --git a/doc/changelog/11-standard-library/19269-adding_vectors_Forall2_lemma.rst b/doc/changelog/11-standard-library/19269-adding_vectors_Forall2_lemma.rst
diff --git a/doc/changelog/11-standard-library/19310-stdlib-logical-name.rst b/doc/changelog/11-standard-library/19310-stdlib-logical-name.rst
diff --git a/doc/changelog/11-standard-library/19479-master+misc-addition-lists.rst b/doc/changelog/11-standard-library/19479-master+misc-addition-lists.rst
diff --git a/doc/changelog/11-standard-library/19483-UIP-None-nil.rst b/doc/changelog/11-standard-library/19483-UIP-None-nil.rst
diff --git a/doc/changelog/11-standard-library/19515-Proper_map.rst b/doc/changelog/11-standard-library/19515-Proper_map.rst
diff --git a/doc/changelog/11-standard-library/19655-fin_L_R.rst b/doc/changelog/11-standard-library/19655-fin_L_R.rst
diff --git a/doc/changelog/11-standard-library/19748-list-for-Zmod.rst b/doc/changelog/11-standard-library/19748-list-for-Zmod.rst
diff --git a/doc/changelog/11-standard-library/19749-pos-iter-op-correct.rst b/doc/changelog/11-standard-library/19749-pos-iter-op-correct.rst
diff --git a/doc/changelog/11-standard-library/19750-n2z-bitwise.rst b/doc/changelog/11-standard-library/19750-n2z-bitwise.rst
diff --git a/doc/changelog/11-standard-library/19752-zdiv-facts.rst b/doc/changelog/11-standard-library/19752-zdiv-facts.rst
diff --git a/doc/changelog/11-standard-library/19801-less-ZArith_base.rst b/doc/changelog/11-standard-library/19801-less-ZArith_base.rst
diff --git a/doc/changelog/11-standard-library/19914-stdlib-all.rst b/doc/changelog/11-standard-library/19914-stdlib-all.rst
diff --git a/doc/changelog/11-standard-library/19949-option-eqdec.rst b/doc/changelog/11-standard-library/19949-option-eqdec.rst
diff --git a/doc/changelog/11-standard-library/19975-stdlib_repo.rst b/doc/changelog/11-standard-library/19975-stdlib_repo.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  Stdlib moved to its own repository, look for Stdlib own changelog
+  for other changes there
+  (`#19975 <https://github.com/coq/coq/pull/19686>`_,
+  by Pierre Roux).
diff --git a/dune b/dune
@@ -96,5 +96,3 @@
   (source_tree plugins)))
 
 ; (dirs (:standard _build_ci))
-
-(dirs :standard \ stdlib)
diff --git a/stdlib/.gitignore b/stdlib/.gitignore
diff --git a/stdlib/INSTALL.md b/stdlib/INSTALL.md
Original file line number	Diff line number	Diff line change
Expand Up		@@ -96,5 +96,3 @@
		(source_tree plugins)))

		; (dirs (:standard _build_ci))

		(dirs :standard \ stdlib)