[azure] [ci] Build on Windows using Dune.

We may want to keep the make-based and Dune job, however the
make-based setup is tested by the INRIA workers so it may not be
needed.

In order for some test to run well, we always run in Dune with an
absolute path. The easiest way to get a portable absolute path is to
use OCaml itself so we introduce a small executable to do that.

While we are at it, we do some cleanup of the test-suite `dune` file,
in particular we remove useless comments, set `--no-buffer` so results
can be seen in real time, and recognize the `NJOBS` variable as we
have moved to a Dune version that supports env vars.

9 files changed, 49 insertions, 75 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b3dc1fa896..c3627862e3 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -154,7 +154,7 @@ after_script:
     - BIN=$(readlink -f ../_install_ci/bin)/
     - LIB=$(readlink -f ../_install_ci/lib/coq)/
     - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH"
-    - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" COQFLAGS="${COQFLAGS}" all
+    - make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" COQFLAGS="${COQFLAGS}" all
   artifacts:
     name: "$CI_JOB_NAME.logs"
     when: on_failure
diff --git a/Makefile.dune b/Makefile.dune
index e3a8a30bc2..29f6fed974 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -76,7 +76,7 @@ quickopt: voboot
 	dune build $(DUNEOPT) $(QUICKOPT_TARGETS)
 
 test-suite: voboot
-	dune runtest $(DUNEOPT)
+	dune runtest --no-buffer $(DUNEOPT)
 
 refman-html: voboot
 	dune build @refman-html
diff --git a/dev/ci/azure-build.sh b/dev/ci/azure-build.sh
index c0030c566f..04c7d5db91 100755
--- a/dev/ci/azure-build.sh
+++ b/dev/ci/azure-build.sh
@@ -4,6 +4,4 @@ set -e -x
 
 cd $(dirname $0)/../..
 
-./configure -local
-make -j 2 byte
-make -j 2 world
+make -f Makefile.dune coq coqide-server
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh
index 8a1e36659c..9448a03f4f 100755
--- a/dev/ci/azure-opam.sh
+++ b/dev/ci/azure-opam.sh
@@ -10,4 +10,4 @@ bash opam64/install.sh
 
 opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $OPAM_VARIANT --disable-sandboxing
 eval "$(opam env)"
-opam install -y num ocamlfind ounit
+opam install -y num ocamlfind dune ounit
diff --git a/dev/ci/azure-test.sh b/dev/ci/azure-test.sh
index 8813245e5a..80a3d2e083 100755
--- a/dev/ci/azure-test.sh
+++ b/dev/ci/azure-test.sh
@@ -4,6 +4,5 @@ set -e -x
 
 #NB: if we make test-suite from the main makefile we get environment
 #too large for exec error
-cd $(dirname $0)/../../test-suite
-make -j 2 clean
-make -j 2 PRINT_LOGS=1
+cd $(dirname $0)/../../
+make -f Makefile.dune test-suite
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 03bfc5ffac..5582503d89 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -34,20 +34,24 @@ include ../Makefile.common
 
 # Default value when called from a freshly compiled Coq, but can be
 # easily overridden
-LIB := ..
+
 BIN := $(shell cd ..; pwd)/bin/
 COQFLAGS?=
 
-coqc_boot := $(BIN)coqc -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestSuite $(COQFLAGS)
-coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS)
-coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
+ifeq ($(COQLIB),)
+  # This method of setting `pwd` won't work on win32 OCaml
+  COQLIB := $(shell cd ..; pwd)
+endif
+export COQLIB
+
+coqc := $(BIN)coqc -q -R prerequisite TestSuite $(COQFLAGS)
+coqchk := $(BIN)coqchk -R prerequisite TestSuite
 coqdoc := $(BIN)coqdoc
-coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestSuite
-coqtopbyte := $(BIN)coqtop.byte
+coqtop := $(BIN)coqtop -q -test-mode -R prerequisite TestSuite
+coqtopbyte := $(BIN)coqtop.byte -q
 
-coqc_interactive := $(coqc) -async-proofs-cache force
-coqc_boot_interactive := $(coqc_boot) -async-proofs-cache force
-coqdep := $(BIN)coqdep -coqlib $(LIB)
+coqc_interactive := $(coqc) -test-mode -async-proofs-cache force
+coqdep := $(BIN)coqdep
 
 VERBOSE?=
 SHOW := $(if $(VERBOSE),@true,@echo)
@@ -398,7 +402,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
 	  output=$*.out.real; \
-	  $(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \
+	  $(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \
 	    | grep -v "Welcome to Coq" \
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
@@ -437,7 +441,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
 	  echo $(call log_intro,$<); \
 	  tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
 	  tmpexpected=`mktemp /tmp/coqcheck.XXXXXX`; \
-	  $(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \
+	  $(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \
 	    | grep -v "Welcome to Coq" \
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
@@ -492,7 +496,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
 	  true "extract effective user time"; \
-	  res=`$(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \
+	  res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \
 	  R=$$?; times; \
 	  if [ $$R != 0 ]; then \
 	    echo $(log_failure); \
@@ -556,7 +560,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG)
 	  echo $(call log_intro,$<); \
 	  export BIN="$(BIN)"; \
 	  export coqc="$(coqc)"; \
-	  export coqtop="$(coqc_boot)"; \
+	  export coqtop="$(coqc)"; \
 	  export coqdep="$(coqdep)"; \
 	  export coqtopbyte="$(coqtopbyte)"; \
 	  "$<" 2>&1; R=$$?; times; \
@@ -578,7 +582,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
 	@echo "TEST      $<"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off $(call get_coq_prog_args,"$<")" 2>&1; \
+	  $(BIN)fake_ide "$<" "-q -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off $(call get_coq_prog_args,"$<")" 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
diff --git a/test-suite/dune b/test-suite/dune
index eae072553a..9efc1e2dc1 100644
--- a/test-suite/dune
+++ b/test-suite/dune
@@ -1,3 +1,13 @@
+; The easiest way to generate a portable absolute path is to use OCaml
+; itself to print it
+(executable
+ (name ocaml_pwd)
+ (modules ocaml_pwd))
+
+(rule
+ (targets libpath.inc)
+ (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe ../../install/%{context_name}/lib/coq/ ))))
+
 (rule
  (targets summary.log)
  (deps
@@ -14,60 +24,13 @@
    ; For fake_ide
    (package coqide-server)
    (source_tree .))
-   ; Finer-grained dependencies look like this
+   ; Finer-grained dependencies would look like this and be generated
+   ; by coqdep; that would allow tests to be run incrementally.
    ; ../tools/CoqMakefile.in
    ; ../theories/Init/Prelude.vo
-   ; ../theories/Arith/Arith.vo
-   ; ../theories/Arith/Compare.vo
-   ; ../theories/PArith/PArith.vo
-   ; ../theories/QArith/QArith.vo
-   ; ../theories/QArith/Qcanon.vo
-   ; ../theories/ZArith/ZArith.vo
-   ; ../theories/ZArith/Zwf.vo
-   ; ../theories/Sets/Ensembles.vo
-   ; ../theories/Numbers/Natural/Peano/NPeano.vo
-   ; ../theories/Numbers/Cyclic/Int31/Cyclic31.vo
-   ; ../theories/FSets/FMaps.vo
-   ; ../theories/FSets/FSets.vo
-   ; ../theories/MSets/MSets.vo
-   ; ../theories/Compat/Coq87.vo
-   ; ../theories/Compat/Coq88.vo
-   ; ../theories/Relations/Relations.vo
-   ; ../theories/Unicode/Utf8.vo
-   ; ../theories/Program/Program.vo
-   ; ../theories/Classes/EquivDec.vo
-   ; ../theories/Classes/DecidableClass.vo
-   ; ../theories/Classes/SetoidClass.vo
-   ; ../theories/Classes/RelationClasses.vo
-   ; ../theories/Logic/Classical.vo
-   ; ../theories/Logic/Hurkens.vo
-   ; ../theories/Logic/ClassicalFacts.vo
-   ; ../theories/Reals/Reals.vo
-   ; ../theories/Lists/Streams.vo
-   ; ../plugins/micromega/Lia.vo
-   ; ../plugins/micromega/Lqa.vo
-   ; ../plugins/micromega/Psatz.vo
-   ; ../plugins/micromega/MExtraction.vo
-   ; ../plugins/nsatz/Nsatz.vo
-   ; ../plugins/omega/Omega.vo
-   ; ../plugins/ssr/ssrbool.vo
-   ; ../plugins/derive/Derive.vo
-   ; ../plugins/funind/Recdef.vo
-   ; ../plugins/extraction/Extraction.vo
-   ; ../plugins/extraction/ExtrOcamlNatInt.vo
-   ; coqtop
-   ; coqtop.opt
-   ; coqidetop.opt
-   ; coqqueryworker.opt
-   ; coqtacticworker.opt
-   ; coqproofworker.opt
-   ; coqc
-   ; coqchk
-   ; coqdoc
+   ; %{bin:coqc}
    ; %{bin:coq_makefile}
    ; %{bin:fake_ide}
  (action
   (progn
-   ; XXX: we will allow to set the NJOBS variable in a future Dune
-   ; version, either by using an env var or by letting Dune set `-j`
-   (run make -j 2 BIN= PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}))))
+   (bash "make -j %{env:NJOBS=2} BIN= COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}"))))
diff --git a/test-suite/ocaml_pwd.ml b/test-suite/ocaml_pwd.ml
new file mode 100644
index 0000000000..10ca52a4a9
--- /dev/null
+++ b/test-suite/ocaml_pwd.ml
@@ -0,0 +1,7 @@
+let _ =
+  let ch_dir = Sys.argv.(1) in
+  Sys.chdir ch_dir;
+  let dir = Sys.getcwd () in
+  (* Needed for windows *)
+  let dir = Filename.quote dir in
+  Format.printf "%s%!" dir
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 0d3fb77551..5dd6cc6c83 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -79,14 +79,17 @@ let use_suffix prefix suffix =
 
 (** A weaker analog of the function in Envars *)
 
+let getenv_else s dft = try Sys.getenv s with Not_found -> dft ()
+
 let guess_coqlib () =
+  getenv_else "COQLIB" (fun () ->
   let file = "theories/Init/Prelude.vo" in
   let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
   let prefix = Filename.dirname coqbin in
   let coqlib = use_suffix prefix Coq_config.coqlibsuffix in
   if Sys.file_exists (coqlib / file) then coqlib else
   if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / file)
-  then Coq_config.coqlib else prefix
+  then Coq_config.coqlib else prefix)
 
 let header_trailer = ref true
 let header_file = ref ""