From 565a30614c6df16466f66cac1e517f9202612709 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 17 Feb 2019 01:03:12 +0100
Subject: [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.
---
 test-suite/dune | 65 +++++++++++++--------------------------------------------
 1 file changed, 14 insertions(+), 51 deletions(-)

(limited to 'test-suite/dune')

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}"))))
-- 
cgit v1.2.3