1 files changed, 14 insertions, 51 deletions
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}"))))