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

8 files changed, 111 insertions, 2 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 6169c7e7e4..e829b517d7 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -321,6 +321,19 @@ test-suite:edge+flambda:
     OPAM_SWITCH: edge
     OPAM_VARIANT: "+flambda"
 
+test-suite:egde:dune:dev:
+  stage: test
+  dependencies:
+    - build:egde:dune:dev
+  script: make -f Makefile.dune test-suite
+  variables:
+    OPAM_SWITCH: edge
+  artifacts:
+    name: "$CI_JOB_NAME.logs"
+    when: on_failure
+    paths:
+      - _build/default/test-suite/logs
+
 validate:base:
   <<: *validate-template
   dependencies:
diff --git a/Makefile.dune b/Makefile.dune
index d9c1452cae..298a27c93e 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -1,7 +1,7 @@
 # -*- mode: makefile -*-
 # Dune Makefile for Coq
 
-.PHONY: voboot states world watch release apidoc ocheck ireport clean help
+.PHONY: help voboot states world watch test-suite release apidoc ocheck ireport clean
 
 # use DUNEOPT=--display=short for a more verbose build
 # DUNEOPT=--display=short
@@ -13,6 +13,7 @@ help:
 	@echo "  - states:  build a minimal functional coqtop"
 	@echo "  - world:   build all binaries and libraries"
 	@echo "  - watch:   build all binaries and libraries [continuous build]"
+	@echo "  - test-suite: run Coq's test suite"
 	@echo "  - release: build Coq in release mode"
 	@echo "  - apidoc:  build ML API documentation"
 	@echo "  - ocheck:  build for all supported OCaml versions [requires OPAM]"
@@ -33,6 +34,9 @@ world: voboot
 watch: voboot
 	dune build $(DUNEOPT) @install -w
 
+test-suite: voboot
+	dune $(DUNEOPT) runtest
+
 release: voboot
 	dune build $(DUNEOPT) -p coq
 
diff --git a/config/dune b/config/dune
index ce87a7816d..cc993b97c9 100644
--- a/config/dune
+++ b/config/dune
@@ -7,7 +7,7 @@
 ; Dune doesn't use configure's output, but it is still necessary for
 ; some Coq files to work; will be fixed in the future.
 (rule
- (targets coq_config.ml)
+ (targets coq_config.ml Makefile)
  (mode fallback)
  (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX))
  (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no))))
diff --git a/dune b/dune
index 240550cf94..4e78a2fe3f 100644
--- a/dune
+++ b/dune
@@ -29,3 +29,8 @@
  (targets revision)
  (deps (:rev-script dev/tools/make_git_revision.sh))
  (action (with-stdout-to revision (run %{rev-script}))))
+
+; Use summary.log as the target
+(alias
+ (name runtest)
+ (deps test-suite/summary.log))
diff --git a/ide/dune b/ide/dune
index 037b0fcc9e..70a1709f37 100644
--- a/ide/dune
+++ b/ide/dune
@@ -10,6 +10,8 @@
 
 (executable
  (name fake_ide)
+ (public_name fake_ide)
+ (package coqide-server)
  (modules fake_ide)
  (libraries coqide-server.protocol coqide-server.core))
 
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))))