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

Reviewed-by: SkySkimmer

12 files changed, 64 insertions, 90 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/CoqMakefile.in b/tools/CoqMakefile.in
index f8f10b34ae..bd9d8c9221 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -187,7 +187,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
 COQMAKEFILE_VERSION:=@COQ_VERSION@
 
-COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)")
+COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
 
 CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS)
 
@@ -216,9 +216,9 @@ endif
 
 concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2))
 
-COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib)
-COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib)
-COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop)
+COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/user-contrib)
+COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)/user-contrib)
+COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop)
 
 # Files #######################################################################
 #
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 4f01a6bd87..68281d6481 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -123,9 +123,10 @@ let read_whole_file s =
 let quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'" else s
 
 let generate_makefile oc conf_file local_file args project =
+  let coqlib = Envars.coqlib () in
   let makefile_template =
-    let template = "/tools/CoqMakefile.in" in
-    Envars.coqlib () ^ template in
+    let template = Filename.concat "tools" "CoqMakefile.in" in
+    Filename.concat coqlib template in
   let s = read_whole_file makefile_template in
   let s = List.fold_left
     (* We use global_substitute to avoid running into backslash issues due to \1 etc. *)
@@ -260,7 +261,7 @@ let generate_conf_doc oc { defs; q_includes; r_includes } =
          eprintf "Warning: in %s\n" destination;
          destination
       end else "$(INSTALLDEFAULTROOT)"
-    else String.concat "/" gcd in
+    else String.concat Filename.dir_sep gcd in
   Printf.fprintf oc "COQMF_INSTALLCOQDOCROOT = %s\n" (quote root)
 
 let generate_conf_defs oc { defs; extra_args } =
@@ -343,15 +344,13 @@ let chop_prefix p f =
   let len_f = String.length f in
   String.sub f len_p (len_f - len_p)
 
-let clean_path p =
-  Str.global_replace (Str.regexp_string "//") "/" p
-
 let destination_of { ml_includes; q_includes; r_includes; } file =
   let file_dir = CUnix.canonical_path_name (Filename.dirname file) in
   let includes = q_includes @ r_includes in
   let mk_destination logic canonical_path =
-    clean_path (physical_dir_of_logical_dir logic ^ "/" ^
-                chop_prefix canonical_path file_dir ^ "/") in
+    Filename.concat
+      (physical_dir_of_logical_dir logic)
+      (chop_prefix canonical_path file_dir) in
   let candidates =
     CList.map_filter (fun {thing={ canonical_path }, logic} ->
       if is_prefix canonical_path file_dir then
@@ -368,8 +367,9 @@ let destination_of { ml_includes; q_includes; r_includes; } file =
      with
         | [{thing={ canonical_path }, logic}], {thing={ canonical_path = p }} ->
             let destination =
-              clean_path (physical_dir_of_logical_dir logic ^ "/" ^
-                          chop_prefix p file_dir ^ "/") in
+              Filename.concat
+                (physical_dir_of_logical_dir logic)
+                (chop_prefix p file_dir) in
             Printf.printf "%s" (quote destination)
         | _ -> () (* skip *)
         | exception Not_found -> () (* skip *)
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 ""
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index e1d35e537b..74a089510e 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -11,7 +11,7 @@
 open Util
 open Pp
 
-let ( / ) s1 s2 = s1 ^ "/" ^ s2
+let ( / ) s1 s2 = Filename.concat s1 s2
 
 let set_debug () =
   let () = Backtrace.record_backtrace true in