From a2f4a43833a29a5ede5905225b814c33e3a46132 Mon Sep 17 00:00:00 2001
From: Paul Steckler <steck@stecksoft.com>
Date: Fri, 23 Feb 2018 14:23:19 -0500
Subject: add unit tests to test suite

---
 .gitignore                                  |  2 +
 .travis.yml                                 |  9 ++--
 Makefile                                    |  2 +-
 Makefile.common                             |  2 +-
 dev/ci/appveyor.sh                          |  2 +-
 dev/doc/changes.md                          |  5 ++
 test-suite/Makefile                         | 74 ++++++++++++++++++++++++-----
 test-suite/README.md                        |  3 ++
 test-suite/unit-tests/clib/inteq.ml         | 13 +++++
 test-suite/unit-tests/clib/unicode_tests.ml | 15 ++++++
 test-suite/unit-tests/src/utest.ml          | 74 +++++++++++++++++++++++++++++
 test-suite/unit-tests/src/utest.mli         | 12 +++++
 12 files changed, 195 insertions(+), 18 deletions(-)
 create mode 100644 test-suite/unit-tests/clib/inteq.ml
 create mode 100644 test-suite/unit-tests/clib/unicode_tests.ml
 create mode 100644 test-suite/unit-tests/src/utest.ml
 create mode 100644 test-suite/unit-tests/src/utest.mli

diff --git a/.gitignore b/.gitignore
index e2a97b3a1..f1960ba68 100644
--- a/.gitignore
+++ b/.gitignore
@@ -88,6 +88,8 @@ test-suite/coqdoc/Coqdoc.*
 test-suite/coqdoc/index.html
 test-suite/coqdoc/coqdoc.css
 test-suite/output/MExtraction.out
+test-suite/oUnit-anon.cache
+test-suite/unit-tests/**/*.test
 
 # documentation
 
diff --git a/.travis.yml b/.travis.yml
index dbe152b5b..44d24eaa2 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -55,7 +55,7 @@ matrix:
   include:
     - if: NOT (type = pull_request)
       env:
-      - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
+      - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" EXTRA_OPAM="ounit"
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="validate"                           TW="travis_wait"
@@ -156,7 +156,7 @@ matrix:
       env:
       - TEST_TARGET="test-suite"
       - EXTRA_CONF="-coqide opt -with-doc yes"
-      - EXTRA_OPAM="${LABLGTK}"
+      - EXTRA_OPAM="${LABLGTK} ounit"
       before_install: &sphinx-install
       - sudo pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex
       addons:
@@ -188,7 +188,7 @@ matrix:
       - FINDLIB_VER="${FINDLIB_VER_BE}"
       - CAMLP5_VER="${CAMLP5_VER_BE}"
       - EXTRA_CONF="-coqide opt -with-doc yes"
-      - EXTRA_OPAM="${LABLGTK_BE}"
+      - EXTRA_OPAM="${LABLGTK_BE} ounit"
       before_install: *sphinx-install
       addons:
         apt:
@@ -205,7 +205,7 @@ matrix:
       - CAMLP5_VER="${CAMLP5_VER_BE}"
       - NATIVE_COMP="no"
       - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3"
-      - EXTRA_OPAM="${LABLGTK_BE}"
+      - EXTRA_OPAM="${LABLGTK_BE} ounit"
       before_install: *sphinx-install
       addons:
         apt:
@@ -250,6 +250,7 @@ matrix:
       - CAMLP5_VER=".6.17"
       - NATIVE_COMP="no"
       - COQ_DEST="-local"
+      - EXTRA_OPAM="ounit"
       before_install:
       - brew update
       - brew unlink python
diff --git a/Makefile b/Makefile
index 793afb661..f914de5a6 100644
--- a/Makefile
+++ b/Makefile
@@ -58,7 +58,7 @@ FIND_SKIP_DIRS:='(' \
   -name '_build_ci' -o \
   -name '_install_ci' -o \
   -name 'user-contrib' -o \
-  -name 'coq-makefile' -o \
+  -name 'test-suite' -o \
   -name '.opamcache' -o \
   -name '.coq-native' \
 ')' -prune -o
diff --git a/Makefile.common b/Makefile.common
index eed41fbe7..f3b39ff26 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -105,7 +105,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \
 CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
         engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
         parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
-	stm/stm.cma toplevel/toplevel.cma
+        stm/stm.cma toplevel/toplevel.cma
 
 TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
 
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
index 93e7bd99a..c72705c7f 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -5,5 +5,5 @@ tar -xf opam64.tar.xz
 bash opam64/install.sh
 opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c
 eval "$(opam config env)"
-opam install -y ocamlfind camlp5
+opam install -y ocamlfind camlp5 ounit
 cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 6d7c0d368..fb3f751db 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -22,6 +22,11 @@ Proof engine
   should indicate what the canonical form is. An important change is
   the move of `Globnames.global_reference` to `Names.GlobRef.t`.
 
+### Unit testing
+
+  The test suite now allows writing unit tests against OCaml code in the Coq
+  code base. Those unit tests create a dependency on the OUnit test framework.
+
 ## Changes between Coq 8.7 and Coq 8.8
 
 ### Bug tracker
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 2531b8c67..a6e6283bf 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -8,9 +8,6 @@
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
 
-# This is a standalone Makefile to run the test-suite. It can be used
-# outside of the Coq source tree (if BIN is overridden).
-
 # There is one %.v.log target per %.v test file. The target will be
 # filled with the output, timings and status of the test. There is
 # also one target per directory containing %.v files, that runs all
@@ -23,6 +20,13 @@
 # The "run" target runs all tests that have not been run yet. To force
 # all tests to be run, use the "clean" target.
 
+
+###########################################################################
+# Includes
+###########################################################################
+
+include ../config/Makefile
+
 #######################################################################
 # Variables
 #######################################################################
@@ -97,7 +101,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
   coqdoc ssr
 
 # All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile unit-tests
 
 PREREQUISITELOG = prerequisite/admit.v.log			\
   prerequisite/make_local.v.log prerequisite/make_notation.v.log \
@@ -118,13 +122,16 @@ bugs: $(BUGS)
 
 clean:
 	rm -f trace .lia.cache output/MExtraction.out
-	$(SHOW) "RM        <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>"
+	$(SHOW) 'RM        <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>'
 	$(HIDE)find . \( \
-	  -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \
-	\) -print0 | xargs -0 rm -f
-
+	  -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \
+	  \) -print0 | xargs -0 rm -f
+	$(SHOW) 'RM        <**/*.cmx> <**/*.cmi> <**/*.o> <**/*.test>'
+	$(HIDE)find unit-tests \( \
+	  -name '*.cmx' -o -name '*.cmi' -o -name '*.o' -o -name '*.test' \
+	  \) -print0 | xargs -0 rm -f
 distclean: clean
-	$(SHOW) "RM        <**/*.aux>"
+	$(SHOW) 'RM        <**/*.aux>'
 	$(HIDE)find . -name '*.aux' -print0 | xargs -0 rm -f
 
 #######################################################################
@@ -165,12 +172,13 @@ summary:
 	  $(call summary_dir, "Coqwc tests", coqwc); \
 	  $(call summary_dir, "Coq makefile", coq-makefile); \
 	  $(call summary_dir, "Coqdoc tests", coqdoc); \
+	  $(call summary_dir, "Unit tests", unit-tests); \
 	  nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
 	  nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
 	  nb_tests=`expr $$nb_success + $$nb_failure`; \
-	  pourcentage=`expr 100 \* $$nb_success / $$nb_tests`; \
+	  percentage=`expr 100 \* $$nb_success / $$nb_tests`; \
 	  echo; \
-	  echo "$$nb_success tests passed over $$nb_tests, i.e. $$pourcentage %"; \
+	  echo "$$nb_success tests passed over $$nb_tests, i.e. $$percentage %"; \
 	}
 
 summary.log:
@@ -243,6 +251,50 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
+#######################################################################
+# Unit tests
+#######################################################################
+
+OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
+SYSMOD:=-package num,str,unix,dynlink,threads
+
+COQSRCDIRS=-I $(LIB)/clib -I $(LIB)/lib -I $(LIB)/kernel -I $(LIB)/kernel/byterun \
+-I $(LIB)/library -I $(LIB)/engine -I $(LIB)/pretyping -I $(LIB)/interp \
+-I $(LIB)/proofs -I $(LIB)/parsing -I $(LIB)/printing -I $(LIB)/tactics -I $(LIB)/vernac \
+-I $(LIB)/stm -I $(LIB)/toplevel
+
+# ML files from unit-test framework, not containing tests
+UNIT_SRCFILES=$(shell find ./unit-tests/src -name *.ml)
+UNIT_ALLMLFILES:=$(shell find ./unit-tests -name *.ml)
+UNIT_MLFILES:=$(filter-out $(UNIT_SRCFILES),$(UNIT_ALLMLFILES))
+UNIT_LOGFILES:=$(patsubst %.ml,%.ml.log,$(UNIT_MLFILES))
+
+UNIT_CMXS=utest.cmx
+
+# this is same link order as CORECMA in Makefile.common in Coq root dir
+COQCMXAS=clib.cmxa lib.cmxa kernel.cmxa library.cmxa engine.cmxa pretyping.cmxa \
+ interp.cmxa proofs.cmxa parsing.cmxa printing.cmxa tactics.cmxa vernac.cmxa stm.cmxa toplevel.cmxa
+
+unit-tests/src/utest.cmx : unit-tests/src/utest.ml unit-tests/src/utest.cmi
+	$(SHOW) 'OCAMLOPT  $<'
+	$(HIDE)$(OCAMLOPT) -c -I unit-tests/src -package oUnit $<
+unit-tests/src/utest.cmi : unit-tests/src/utest.mli
+	$(SHOW) 'OCAMLOPT  $<'
+	$(HIDE)$(OCAMLOPT) -package oUnit $<
+
+$(UNIT_LOGFILES) : unit-tests/src/utest.cmx
+
+unit-tests: $(UNIT_LOGFILES)
+
+# Build executable, run it to generate log file
+unit-tests/%.ml.log: unit-tests/%.ml
+	$(SHOW) 'TEST      $<'
+	$(HIDE)$(OCAMLOPT) -linkall -linkpkg -cclib -lcoqrun \
+		   $(SYSMOD) -package camlp5.gramlib,oUnit  \
+	     -I unit-tests/src $(COQSRCDIRS) $(COQCMXAS) \
+	     $(UNIT_CMXS) $< -o $<.test;
+	$(HIDE)./$<.test
+
 #######################################################################
 # Other generic tests
 #######################################################################
diff --git a/test-suite/README.md b/test-suite/README.md
index 1d1195646..4572c98cf 100644
--- a/test-suite/README.md
+++ b/test-suite/README.md
@@ -73,3 +73,6 @@ When you fix a bug, you should usually add a regression test here as well.
 The error "(bug seems to be opened, please check)" when running `make test-suite` means that a test in `bugs/closed` failed to compile.
 
 There are also output tests in `test-suite/output` which consist of a `.v` file and a `.out` file with the expected output.
+
+There are unit tests of OCaml code in `test-suite/unit-tests`. These tests are contained in `.ml` files, and rely on the `OUnit`
+unit-test framework, as described at http://ounit.forge.ocamlcore.org/.  Use `make unit-tests' in the unit-tests directory to run them.
diff --git a/test-suite/unit-tests/clib/inteq.ml b/test-suite/unit-tests/clib/inteq.ml
new file mode 100644
index 000000000..c07ec293f
--- /dev/null
+++ b/test-suite/unit-tests/clib/inteq.ml
@@ -0,0 +1,13 @@
+open Utest
+
+let eq0 = mk_bool_test "clib-inteq0"
+            "Int.equal on 0"
+            (Int.equal 0 0)
+
+let eq42 = mk_bool_test "clib-inteq42"
+             "Int.equal on 42"
+             (Int.equal 42 42)
+
+let tests = [ eq0; eq42 ]
+
+let _ = run_tests __FILE__ tests
diff --git a/test-suite/unit-tests/clib/unicode_tests.ml b/test-suite/unit-tests/clib/unicode_tests.ml
new file mode 100644
index 000000000..9ae405977
--- /dev/null
+++ b/test-suite/unit-tests/clib/unicode_tests.ml
@@ -0,0 +1,15 @@
+open Utest
+
+let unicode0 = mk_eq_test "clib-unicode0"
+                 "split_at_first_letter, first letter is character"
+                 None
+                 (Unicode.split_at_first_letter "ident")
+
+let unicode1 = mk_eq_test "clib-unicode1"
+                 "split_at_first_letter, first letter not character"
+                 (Some ("__","ident"))
+                 (Unicode.split_at_first_letter "__ident")
+
+let tests = [ unicode0; unicode1 ]
+
+let _ = run_tests __FILE__ tests
diff --git a/test-suite/unit-tests/src/utest.ml b/test-suite/unit-tests/src/utest.ml
new file mode 100644
index 000000000..069e6a4bf
--- /dev/null
+++ b/test-suite/unit-tests/src/utest.ml
@@ -0,0 +1,74 @@
+open OUnit
+
+(* general case to build a test *)
+let mk_test nm test = nm >: test
+
+(* common cases for building tests *)
+let mk_eq_test nm descr expected actual =
+  mk_test nm (TestCase (fun _ -> assert_equal ~msg:descr expected actual))
+
+let mk_bool_test nm descr actual =
+  mk_test nm (TestCase (fun _ -> assert_bool descr actual))
+
+let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "\n%!") oc)
+
+(* given test result, print message, return success boolean *)
+let logger out_ch result =
+  let cprintf s = cfprintf out_ch s in
+  match result with
+  | RSuccess path ->
+     cprintf "TEST SUCCEEDED: %s" (string_of_path path);
+     true
+  | RError (path,msg)
+  | RFailure (path,msg) ->
+     cprintf "TEST FAILED: %s (%s)" (string_of_path path) msg;
+     false
+  | RSkip (path,msg)
+  | RTodo (path,msg) ->
+     cprintf "TEST DID NOT SUCCEED: %s (%s)" (string_of_path path) msg;
+     false
+
+(* run one OUnit test case, return successes, no. of tests *)
+(* notionally one test, which might be a TestList *)
+let run_one logit test =
+  let rec process_results rs =
+    match rs with
+      [] -> (0,0)
+    | (r::rest) ->
+       let succ = if logit r then 1 else 0 in
+       let succ_results,tot_results = process_results rest in
+       (succ + succ_results,tot_results + 1)
+  in
+  let results = perform_test (fun _ -> ()) test in
+  process_results results
+
+(* run list of OUnit test cases, log results *)
+let run_tests ml_fn tests =
+  let log_fn = ml_fn ^ ".log" in
+  let out_ch = open_out log_fn in
+  let cprintf s = cfprintf out_ch s in
+  let ceprintf s = cfprintf stderr s in
+  let logit = logger out_ch in
+  let rec run_some tests succ tot =
+    match tests with
+      [] -> (succ,tot)
+    | (t::ts) ->
+       let succ_one,tot_one = run_one logit t in
+       run_some ts (succ + succ_one) (tot + tot_one)
+  in
+  (* format for test-suite summary to find status
+     success if all tests succeeded, else failure
+   *)
+  let succ,tot = run_some tests 0 0 in
+  cprintf
+      "*** Ran %d tests, with %d successes and %d failures ***"
+      tot succ (tot - succ);
+  if succ = tot then
+    cprintf
+      "==========> SUCCESS <==========\n    %s...Ok" ml_fn
+  else begin
+    cprintf
+      "==========> FAILURE <==========\n    %s...Error!" ml_fn;
+    ceprintf "FAILED    %s.log" ml_fn
+  end;
+  close_out out_ch
diff --git a/test-suite/unit-tests/src/utest.mli b/test-suite/unit-tests/src/utest.mli
new file mode 100644
index 000000000..70928228b
--- /dev/null
+++ b/test-suite/unit-tests/src/utest.mli
@@ -0,0 +1,12 @@
+(** give a name to a unit test *)
+val mk_test : string -> OUnit.test -> OUnit.test
+
+(** simple ways to build a test *)
+val mk_eq_test : string -> string -> 'a -> 'a -> OUnit.test
+val mk_bool_test : string -> string -> bool -> OUnit.test
+
+(** run unit tests *)
+(* the string argument should be the name of the .ml file
+   containing the tests; use __FILE__ for that purpose.
+ *)
+val run_tests : string -> OUnit.test list -> unit
-- 
cgit v1.2.3


From 107e42b0776a0979e522e82654435d9f2bea7a80 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 16 May 2018 09:49:55 +0200
Subject: unit tests: add .merlin

---
 test-suite/unit-tests/.merlin | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test-suite/unit-tests/.merlin

diff --git a/test-suite/unit-tests/.merlin b/test-suite/unit-tests/.merlin
new file mode 100644
index 000000000..b2279de74
--- /dev/null
+++ b/test-suite/unit-tests/.merlin
@@ -0,0 +1,6 @@
+REC
+
+S **
+B **
+
+PKG oUnit
-- 
cgit v1.2.3


From d0243311634a8d6fa77fb2d0bb36eab96186a605 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 16 May 2018 20:36:34 +0200
Subject: Modify make system to include Makefile.common in the test suite

---
 Makefile.build      |  1 +
 Makefile.common     | 36 ------------------------------------
 Makefile.vofiles    | 40 ++++++++++++++++++++++++++++++++++++++++
 test-suite/Makefile | 21 ++++++++-------------
 4 files changed, 49 insertions(+), 49 deletions(-)
 create mode 100644 Makefile.vofiles

diff --git a/Makefile.build b/Makefile.build
index ffe605757..179ca28b6 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -89,6 +89,7 @@ byte: coqbyte coqide-byte pluginsbyte printers
 MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
 
 include Makefile.common
+include Makefile.vofiles
 include Makefile.doc      ## provides the 'documentation' rule
 include Makefile.checker
 include Makefile.ide      ## provides the 'coqide' rule
diff --git a/Makefile.common b/Makefile.common
index f3b39ff26..9493acd1f 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -111,10 +111,6 @@ TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
 
 GRAMMARCMA:=grammar/grammar.cma
 
-# modules known by the toplevel of Coq
-
-OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib))
-
 ###########################################################################
 # plugins object files
 ###########################################################################
@@ -163,40 +159,8 @@ PLUGINSOPT:=$(PLUGINSCMO:.cmo=.cmxs)
 LINKCMO:=$(CORECMA) $(STATICPLUGINS)
 LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx)
 
-###########################################################################
-# vo files
-###########################################################################
-
-THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v"))
-PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v"))
-ALLVO := $(THEORIESVO) $(PLUGINSVO)
-VFILES := $(ALLVO:.vo=.v)
-
-## More specific targets
-
-THEORIESLIGHTVO:= \
- $(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO))
-
 ALLSTDLIB := test-suite/misc/universes/all_stdlib
 
-# convert a (stdlib) filename into a module name:
-# remove .vo, replace theories and plugins by Coq, and replace slashes by dots
-vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
-
-ALLMODS:=$(call vo_to_mod,$(ALLVO))
-
-
-# Converting a stdlib filename into native compiler filenames
-# Used for install targets
-vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*)))))
-
-vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o)))))
-
-GLOBFILES:=$(ALLVO:.vo=.glob)
-LIBFILES:=$(ALLVO) $(call vo_to_cm,$(ALLVO)) \
-	    $(call vo_to_obj,$(ALLVO)) \
-	    $(VFILES) $(GLOBFILES)
-
 # For emacs:
 # Local Variables:
 # mode: makefile
diff --git a/Makefile.vofiles b/Makefile.vofiles
new file mode 100644
index 000000000..fc902c4a8
--- /dev/null
+++ b/Makefile.vofiles
@@ -0,0 +1,40 @@
+
+# This file calls [find] and as such is not suitable for inclusion in
+# the test suite Makefile, unlike Makefile.common.
+
+###########################################################################
+# vo files
+###########################################################################
+
+THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v"))
+PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v"))
+ALLVO := $(THEORIESVO) $(PLUGINSVO)
+VFILES := $(ALLVO:.vo=.v)
+
+## More specific targets
+
+THEORIESLIGHTVO:= \
+ $(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO))
+
+# convert a (stdlib) filename into a module name:
+# remove .vo, replace theories and plugins by Coq, and replace slashes by dots
+vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
+
+ALLMODS:=$(call vo_to_mod,$(ALLVO))
+
+
+# Converting a stdlib filename into native compiler filenames
+# Used for install targets
+vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*)))))
+
+vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o)))))
+
+GLOBFILES:=$(ALLVO:.vo=.glob)
+LIBFILES:=$(ALLVO) $(call vo_to_cm,$(ALLVO)) \
+	    $(call vo_to_obj,$(ALLVO)) \
+	    $(VFILES) $(GLOBFILES)
+
+# For emacs:
+# Local Variables:
+# mode: makefile
+# End:
diff --git a/test-suite/Makefile b/test-suite/Makefile
index a6e6283bf..ce21ff41c 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -26,6 +26,7 @@
 ###########################################################################
 
 include ../config/Makefile
+include ../Makefile.common
 
 #######################################################################
 # Variables
@@ -258,31 +259,25 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
 OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
 SYSMOD:=-package num,str,unix,dynlink,threads
 
-COQSRCDIRS=-I $(LIB)/clib -I $(LIB)/lib -I $(LIB)/kernel -I $(LIB)/kernel/byterun \
--I $(LIB)/library -I $(LIB)/engine -I $(LIB)/pretyping -I $(LIB)/interp \
--I $(LIB)/proofs -I $(LIB)/parsing -I $(LIB)/printing -I $(LIB)/tactics -I $(LIB)/vernac \
--I $(LIB)/stm -I $(LIB)/toplevel
+COQSRCDIRS:=$(addprefix -I $(LIB)/,$(CORESRCDIRS))
+COQCMXS:=$(addprefix $(LIB)/,$(LINKCMX))
 
 # ML files from unit-test framework, not containing tests
-UNIT_SRCFILES=$(shell find ./unit-tests/src -name *.ml)
+UNIT_SRCFILES:=$(shell find ./unit-tests/src -name *.ml)
 UNIT_ALLMLFILES:=$(shell find ./unit-tests -name *.ml)
 UNIT_MLFILES:=$(filter-out $(UNIT_SRCFILES),$(UNIT_ALLMLFILES))
 UNIT_LOGFILES:=$(patsubst %.ml,%.ml.log,$(UNIT_MLFILES))
 
 UNIT_CMXS=utest.cmx
 
-# this is same link order as CORECMA in Makefile.common in Coq root dir
-COQCMXAS=clib.cmxa lib.cmxa kernel.cmxa library.cmxa engine.cmxa pretyping.cmxa \
- interp.cmxa proofs.cmxa parsing.cmxa printing.cmxa tactics.cmxa vernac.cmxa stm.cmxa toplevel.cmxa
-
-unit-tests/src/utest.cmx : unit-tests/src/utest.ml unit-tests/src/utest.cmi
+unit-tests/src/utest.cmx: unit-tests/src/utest.ml unit-tests/src/utest.cmi
 	$(SHOW) 'OCAMLOPT  $<'
 	$(HIDE)$(OCAMLOPT) -c -I unit-tests/src -package oUnit $<
-unit-tests/src/utest.cmi : unit-tests/src/utest.mli
+unit-tests/src/utest.cmi: unit-tests/src/utest.mli
 	$(SHOW) 'OCAMLOPT  $<'
 	$(HIDE)$(OCAMLOPT) -package oUnit $<
 
-$(UNIT_LOGFILES) : unit-tests/src/utest.cmx
+$(UNIT_LOGFILES): unit-tests/src/utest.cmx
 
 unit-tests: $(UNIT_LOGFILES)
 
@@ -291,7 +286,7 @@ unit-tests/%.ml.log: unit-tests/%.ml
 	$(SHOW) 'TEST      $<'
 	$(HIDE)$(OCAMLOPT) -linkall -linkpkg -cclib -lcoqrun \
 		   $(SYSMOD) -package camlp5.gramlib,oUnit  \
-	     -I unit-tests/src $(COQSRCDIRS) $(COQCMXAS) \
+	     -I unit-tests/src $(COQSRCDIRS) $(COQCMXS) \
 	     $(UNIT_CMXS) $< -o $<.test;
 	$(HIDE)./$<.test
 
-- 
cgit v1.2.3