From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 .gitlab-ci.yml | 86 ++++++++++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 75 insertions(+), 11 deletions(-)

(limited to '.gitlab-ci.yml')

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 799f5b14..b936401a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -9,12 +9,13 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-v8.8-V2018-09-20"
+  CACHEKEY: "bionic_coq-v8.9-V2018-10-22"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
   # Used to select special compiler switches such as flambda, 32bits, etc...
   OPAM_VARIANT: ""
+  GIT_DEPTH: "10"
 
 docker-boot:
   stage: docker
@@ -37,11 +38,11 @@ docker-boot:
 before_script:
   - cat /proc/{cpu,mem}info || true
   - ls -a # figure out if artifacts are around
-  - printenv | sort
+  - printenv -0 | sort -z | tr '\0' '\n'
   - declare -A switch_table
   - switch_table=( ["base"]="$COMPILER" ["edge"]="$COMPILER_EDGE" )
-  - opam switch -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT"
-  - eval $(opam config env)
+  - opam switch set -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT"
+  - eval $(opam env)
   - opam list
   - opam config list
 
@@ -60,23 +61,28 @@ after_script:
     paths:
       - _install_ci
       - config/Makefile
+      - config/coq_config.py
       - test-suite/misc/universes/all_stdlib.v
     expire_in: 1 week
   script:
     - set -e
 
+    - echo 'start:coq.clean'
+    - make clean # ensure that `make clean` works on a fresh clone
+    - echo 'end:coq.clean'
+
     - echo 'start:coq.config'
     - ./configure -warn-error yes -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE"
     - echo 'end:coq.config'
 
     - echo 'start:coq.build'
     - make -j "$NJOBS" byte
-    - make -j "$NJOBS"
+    - make -j "$NJOBS" world $EXTRA_TARGET
     - make test-suite/misc/universes/all_stdlib.v
     - echo 'end:coq:build'
 
     - echo 'start:coq.install'
-    - make install
+    - make install install-byte $EXTRA_INSTALL
     - make install-byte
     - cp bin/fake_ide _install_ci/bin/
     - echo 'end:coq.install'
@@ -88,6 +94,19 @@ 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
+  stage: test
+  dependencies:
+    - not-a-real-job
+  script:
+    - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/" COQBOOT=no'
+    - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= refman
+    - make install-doc-sphinx
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - _install_ci/share/doc/coq/
+
 # set dependencies when using
 .test-suite-template: &test-suite-template
   stage: test
@@ -155,12 +174,15 @@ after_script:
     - call dev/ci/gitlab.bat
   only:
     variables:
-      - $WINDOWS == "enabled"
+      - $WINDOWS =~ /enabled/
 
 build:base:
   <<: *build-template
   variables:
-    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes"
+    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
+    # coqdoc for stdlib, until we know how to build it from installed Coq
+    EXTRA_TARGET: "stdlib"
+    EXTRA_INSTALL: "install-doc-stdlib-html install-doc-printable"
 
 # no coqide for 32bit: libgtk installation problems
 build:base+32bit:
@@ -225,6 +247,42 @@ pkg:nix:
     paths:
       - nix-build-coq.drv-0/*/test-suite/logs
 
+build:macOS:
+  stage: build
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - _build
+    expire_in: 1 week
+  tags:
+    - macOS
+  dependencies: []
+  before_script: []
+  script:
+    - dev/build/osx/make-macos-dmg.sh
+  variables:
+    NJOBS: "2"
+  only:
+    variables:
+      - $MACOS == "enabled"
+
+doc:refman:
+  <<: *doc-template
+  dependencies:
+    - build:base
+
+doc:ml-api:
+  stage: test
+  dependencies:
+    - build:edge
+  script:
+    - ./configure -warn-error yes -prefix "$(pwd)/_install_ci"
+    - make mli-doc source-doc # ml-doc [broken in 4.07.0]
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - dev/ocamldoc
+
 test-suite:base:
   <<: *test-suite-template
   dependencies:
@@ -297,6 +355,9 @@ ci-coq-dpdgraph:
 ci-coquelicot:
   <<: *ci-template
 
+ci-cross-crypto:
+  <<: *ci-template
+
 ci-elpi:
   <<: *ci-template
 
@@ -336,12 +397,15 @@ ci-ltac2:
 ci-math-comp:
   <<: *ci-template-flambda
 
-ci-quickchick:
-  <<: *ci-template-flambda
-
 ci-mtac2:
   <<: *ci-template
 
+ci-pidetop:
+  <<: *ci-template
+
+ci-quickchick:
+  <<: *ci-template-flambda
+
 ci-sf:
   <<: *ci-template
 
-- 
cgit v1.2.3