Merge PR #9588: [azure] [ci] Build on Windows using Dune.

Reviewed-by: SkySkimmer

3 files changed, 39 insertions, 65 deletions

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