Merge PR #9784: Add test-suite to Paramcoq CI

Reviewed-by: ejgallego

2 files changed, 70 insertions, 76 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 708ddced15..309044a1e9 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -55,7 +55,7 @@ after_script:
 ######################################################
 
 # TODO figure out how to build doc for installed Coq
-.build-template: &build-template
+.build-template:
   stage: build
   artifacts:
     name: "$CI_JOB_NAME"
@@ -91,7 +91,7 @@ after_script:
     - set +e
 
 # Template for building Coq + stdlib, typical use: overload the switch
-.dune-template: &dune-template
+.dune-template:
   stage: build
   dependencies: []
   script:
@@ -107,7 +107,7 @@ after_script:
       - _build/
     expire_in: 1 week
 
-.dune-ci-template: &dune-ci-template
+.dune-ci-template:
   stage: test
   dependencies:
     - build:edge+flambda:dune:dev
@@ -117,10 +117,10 @@ after_script:
     - make -f Makefile.dune "$DUNE_TARGET"
     - echo 'end:coq.test'
     - set +e
-  variables: &dune-ci-template-vars
+  variables:
     OPAM_SWITCH: edge
     OPAM_VARIANT: "+flambda"
-  artifacts: &dune-ci-template-artifacts
+  artifacts:
     name: "$CI_JOB_NAME"
     expire_in: 1 month
 
@@ -129,7 +129,7 @@ after_script:
 # purpose, we add a spurious dependency `not-a-real-job` that must be
 # overridden otherwise the CI will fail.
 
-.doc-template: &doc-template
+.doc-template:
   stage: test
   dependencies:
     - not-a-real-job
@@ -143,7 +143,7 @@ after_script:
       - _install_ci/share/doc/coq/
 
 # set dependencies when using
-.test-suite-template: &test-suite-template
+.test-suite-template:
   stage: test
   dependencies:
     - not-a-real-job
@@ -162,7 +162,7 @@ after_script:
       - test-suite/logs
 
 # set dependencies when using
-.validate-template: &validate-template
+.validate-template:
   stage: test
   dependencies:
     - not-a-real-job
@@ -172,7 +172,7 @@ after_script:
     - for regexp in 's/.vo//' 's:lib/coq/plugins:Coq:' 's:lib/coq/theories:Coq:' 's:/:.:g'; do sed -z -i "$regexp" vofiles; done
     - xargs -0 --arg-file=vofiles bin/coqchk -silent -o -m -coqlib lib/coq/
 
-.ci-template: &ci-template
+.ci-template:
   stage: test
   script:
     - set -e
@@ -183,15 +183,15 @@ after_script:
   dependencies:
     - build:base
 
-.ci-template-flambda: &ci-template-flambda
-  <<: *ci-template
+.ci-template-flambda:
+  extends: .ci-template
   dependencies:
     - build:edge+flambda
   variables:
     OPAM_SWITCH: "edge"
     OPAM_VARIANT: "+flambda"
 
-.windows-template: &windows-template
+.windows-template:
   stage: test
   artifacts:
     name: "%CI_JOB_NAME%"
@@ -209,7 +209,7 @@ after_script:
     variables:
       - $WINDOWS =~ /enabled/
 
-.deploy-template: &deploy-template
+.deploy-template:
   stage: deploy
   before_script:
     - which ssh-agent || ( apt-get update -y && apt-get install openssh-client -y )
@@ -221,7 +221,7 @@ after_script:
     - git config --global user.email "coqbot@users.noreply.github.com"
 
 build:base:
-  <<: *build-template
+  extends: .build-template
   variables:
     COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
     # coqdoc for stdlib, until we know how to build it from installed Coq
@@ -230,13 +230,13 @@ build:base:
 
 # no coqide for 32bit: libgtk installation problems
 build:base+32bit:
-  <<: *build-template
+  extends: .build-template
   variables:
     OPAM_VARIANT: "+32bit"
     COQ_EXTRA_CONF: "-native-compiler yes"
 
 build:edge+flambda:
-  <<: *build-template
+  extends: .build-template
   variables:
     OPAM_SWITCH: edge
     OPAM_VARIANT: "+flambda"
@@ -244,10 +244,10 @@ build:edge+flambda:
     COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures"
 
 build:edge+flambda:dune:dev:
-  <<: *dune-template
+  extends: .dune-template
 
 build:base+async:
-  <<: *build-template
+  extends: .build-template
   stage: test
   variables:
     COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
@@ -255,19 +255,19 @@ build:base+async:
   allow_failure: true # See https://github.com/coq/coq/issues/9658
 
 build:quick:
-  <<: *build-template
+  extends: .build-template
   variables:
     COQ_EXTRA_CONF: "-native-compiler no"
     QUICK: "1"
   allow_failure: true # See https://github.com/coq/coq/issues/9637
 
 windows64:
-  <<: *windows-template
+  extends: .windows-template
   variables:
     ARCH: "64"
 
 windows32:
-  <<: *windows-template
+  extends: .windows-template
   variables:
     ARCH: "32"
   except:
@@ -300,7 +300,7 @@ pkg:opam:
     OPAM_SWITCH: "edge"
     OPAM_VARIANT: "+flambda"
 
-.nix-template: &nix-template
+.nix-template:
   image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git
   stage: test
   variables:
@@ -327,7 +327,7 @@ pkg:opam:
       - nix-build-coq.drv-0/*/test-suite/logs
 
 pkg:nix:deploy:
-  <<: *nix-template
+  extends: .nix-template
   environment:
     name: cachix
     url: https://coq.cachix.org
@@ -339,7 +339,7 @@ pkg:nix:deploy:
     - /^v.*\..*$/
 
 pkg:nix:deploy:channel:
-  <<: *deploy-template
+  extends: .deploy-template
   environment:
     name: cachix
     url: https://coq.cachix.org
@@ -354,38 +354,34 @@ pkg:nix:deploy:channel:
     - git push git@github.com:coq/coq-on-cachix "${CI_COMMIT_REF_NAME}"
 
 pkg:nix:
-  <<: *nix-template
+  extends: .nix-template
   except:
     - master
     - /^v.*\..*$/
 
 doc:refman:
-  <<: *doc-template
+  extends: .doc-template
   dependencies:
     - build:base
 
 doc:refman:dune:
-  <<: *dune-ci-template
+  extends: .dune-ci-template
   variables:
-    <<: *dune-ci-template-vars
     DUNE_TARGET: refman-html
   artifacts:
-    <<: *dune-ci-template-artifacts
     paths:
       - _build/default/doc/sphinx_build/html
 
 doc:stdlib:dune:
-  <<: *dune-ci-template
+  extends: .dune-ci-template
   variables:
-    <<: *dune-ci-template-vars
     DUNE_TARGET: stdlib-html
   artifacts:
-    <<: *dune-ci-template-artifacts
     paths:
       - _build/default/doc/stdlib/html
 
 doc:refman:deploy:
-  <<: *deploy-template
+  extends: .deploy-template
   environment:
     name: deployment
     url: https://coq.github.io/
@@ -412,29 +408,27 @@ doc:refman:deploy:
     - git push # TODO: rebase and retry on failure
 
 doc:ml-api:odoc:
-  <<: *dune-ci-template
+  extends: .dune-ci-template
   variables:
-    <<: *dune-ci-template-vars
     DUNE_TARGET: apidoc
   artifacts:
-    <<: *dune-ci-template-artifacts
     paths:
       - _build/default/_doc/
 
 test-suite:base:
-  <<: *test-suite-template
+  extends: .test-suite-template
   dependencies:
     - build:base
 
 test-suite:base+32bit:
-  <<: *test-suite-template
+  extends: .test-suite-template
   dependencies:
     - build:base+32bit
   variables:
     OPAM_VARIANT: "+32bit"
 
 test-suite:edge+flambda:
-  <<: *test-suite-template
+  extends: .test-suite-template
   dependencies:
     - build:edge+flambda
   variables:
@@ -507,26 +501,26 @@ test-suite:edge+trunk+dune:
   allow_failure: true
 
 test-suite:base+async:
-  <<: *test-suite-template
+  extends: .test-suite-template
   dependencies:
     - build:base
   variables:
     COQFLAGS: "-async-proofs on"
 
 validate:base:
-  <<: *validate-template
+  extends: .validate-template
   dependencies:
     - build:base
 
 validate:base+32bit:
-  <<: *validate-template
+  extends: .validate-template
   dependencies:
     - build:base+32bit
   variables:
     OPAM_VARIANT: "+32bit"
 
 validate:edge+flambda:
-  <<: *validate-template
+  extends: .validate-template
   dependencies:
     - build:edge+flambda
   variables:
@@ -534,7 +528,7 @@ validate:edge+flambda:
     OPAM_VARIANT: "+flambda"
 
 validate:quick:
-  <<: *validate-template
+  extends: .validate-template
   dependencies:
     - build:quick
 
@@ -542,93 +536,93 @@ validate:quick:
 # but not on its ML API
 
 library:ci-bedrock2:
-  <<: *ci-template
+  extends: .ci-template
 
 library:ci-color:
-  <<: *ci-template-flambda
+  extends: .ci-template-flambda
 
 library:ci-compcert:
-  <<: *ci-template-flambda
+  extends: .ci-template-flambda
 
 library:ci-coquelicot:
-  <<: *ci-template
+  extends: .ci-template
 
 library:ci-cross-crypto:
-  <<: *ci-template
+  extends: .ci-template
 
 library:ci-fcsl-pcm:
-  <<: *ci-template
+  extends: .ci-template
 
 library:ci-fiat-crypto:
-  <<: *ci-template-flambda
+  extends: .ci-template-flambda
 
 library:ci-fiat-crypto-legacy:
-  <<: *ci-template-flambda
+  extends: .ci-template-flambda
 
 library:ci-flocq:
-  <<: *ci-template
+  extends: .ci-template
 
 library:ci-corn:
-  <<: *ci-template-flambda
+  extends: .ci-template-flambda
 
 library:ci-geocoq:
-  <<: *ci-template-flambda
+  extends: .ci-template-flambda
 
 library:ci-hott:
-  <<: *ci-template
+  extends: .ci-template
 
 library:ci-iris-lambda-rust:
-  <<: *ci-template-flambda
+  extends: .ci-template-flambda
 
 library:ci-math-comp:
-  <<: *ci-template-flambda
+  extends: .ci-template-flambda
 
 library:ci-sf:
-  <<: *ci-template
+  extends: .ci-template
 
 library:ci-stdlib2:
-  <<: *ci-template-flambda
+  extends: .ci-template-flambda
 
 library:ci-unimath:
-  <<: *ci-template-flambda
+  extends: .ci-template-flambda
 
 library:ci-verdi-raft:
-  <<: *ci-template-flambda
+  extends: .ci-template-flambda
 
 library:ci-vst:
-  <<: *ci-template-flambda
+  extends: .ci-template-flambda
 
 # Plugins are by definition the projects that depend on Coq's ML API
 
 plugin:ci-aac_tactics:
-  <<: *ci-template
+  extends: .ci-template
 
 plugin:ci-bignums:
-  <<: *ci-template
+  extends: .ci-template
 
 plugin:ci-coq_dpdgraph:
-  <<: *ci-template
+  extends: .ci-template
 
 plugin:ci-coqhammer:
-  <<: *ci-template
+  extends: .ci-template
 
 plugin:ci-elpi:
-  <<: *ci-template
+  extends: .ci-template
 
 plugin:ci-equations:
-  <<: *ci-template
+  extends: .ci-template
 
 plugin:ci-fiat_parsers:
-  <<: *ci-template
+  extends: .ci-template
 
 plugin:ci-ltac2:
-  <<: *ci-template
+  extends: .ci-template
 
 plugin:ci-mtac2:
-  <<: *ci-template
+  extends: .ci-template
 
 plugin:ci-paramcoq:
-  <<: *ci-template
+  extends: .ci-template
 
 plugin:plugin-tutorial:
   stage: test
@@ -638,7 +632,7 @@ plugin:plugin-tutorial:
     - make -j "$NJOBS" plugin-tutorial
 
 plugin:ci-quickchick:
-  <<: *ci-template-flambda
+  extends: .ci-template-flambda
 
 plugin:ci-relation-algebra:
-  <<: *ci-template
+  extends: .ci-template
diff --git a/dev/ci/ci-paramcoq.sh b/dev/ci/ci-paramcoq.sh
index c641af2abb..d2e0ee89bf 100755
--- a/dev/ci/ci-paramcoq.sh
+++ b/dev/ci/ci-paramcoq.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download paramcoq
 
-( cd "${CI_BUILD_DIR}/paramcoq" && make && make install )
+( cd "${CI_BUILD_DIR}/paramcoq" && make && make install && cd test-suite && make examples)