Give Stdlib its own repository

.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:

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
 

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
 ########################################################################

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"
 )

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
 )

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
 )

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).

dune

@@ -96,5 +96,3 @@
   (source_tree plugins)))
 
 ; (dirs (:standard _build_ci))
-
-(dirs :standard \ stdlib)