[dune] [test-suite] Support for running the test suite with Dune.

3 files changed, 85 insertions, 0 deletions

diff --git a/test-suite/dune b/test-suite/dune
new file mode 100644
index 0000000000..c5fa0bb14a
--- /dev/null
+++ b/test-suite/dune
@@ -0,0 +1,73 @@
+(rule
+ (targets summary.log)
+ (deps
+   ; File that should be promoted.
+   misc/universes/all_stdlib.v
+   ; Dependencies of the legacy makefile
+   ../Makefile.common
+   ../config/Makefile
+   ; Stuff for the compat script test
+   ../dev/header.ml
+   ../dev/tools/update-compat.py
+   ../doc/stdlib/index-list.html.template
+   (package coq)
+   ; For fake_ide
+   (package coqide-server)
+   (source_tree .))
+   ; Finer-grained dependencies look like this
+   ; ../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: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))))
diff --git a/test-suite/misc/universes/build_all_stdlib.sh b/test-suite/misc/universes/build_all_stdlib.sh
new file mode 100755
index 0000000000..2d2e6f863b
--- /dev/null
+++ b/test-suite/misc/universes/build_all_stdlib.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+echo "Require $(find ../../../theories ../../../plugins -type f -name "*.v" | \
+        sed 's/^.*\/theories\///' | sed 's/^.*\/plugins\///' | sed 's/\.v$//' | sed 's/\//./g') ."
diff --git a/test-suite/misc/universes/dune b/test-suite/misc/universes/dune
new file mode 100644
index 0000000000..58bba300d2
--- /dev/null
+++ b/test-suite/misc/universes/dune
@@ -0,0 +1,8 @@
+(rule
+ (targets all_stdlib.v)
+ (deps
+   (source_tree ../../../theories)
+   (source_tree ../../../plugins))
+ (action
+   (with-outputs-to all_stdlib.v
+    (run ./build_all_stdlib.sh))))