aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore2
-rw-r--r--.travis.yml9
-rw-r--r--Makefile2
-rw-r--r--Makefile.build1
-rw-r--r--Makefile.common38
-rw-r--r--Makefile.vofiles40
-rw-r--r--dev/ci/appveyor.sh2
-rw-r--r--dev/doc/changes.md5
-rw-r--r--test-suite/Makefile69
-rw-r--r--test-suite/README.md3
-rw-r--r--test-suite/unit-tests/.merlin6
-rw-r--r--test-suite/unit-tests/clib/inteq.ml13
-rw-r--r--test-suite/unit-tests/clib/unicode_tests.ml15
-rw-r--r--test-suite/unit-tests/src/utest.ml74
-rw-r--r--test-suite/unit-tests/src/utest.mli12
15 files changed, 237 insertions, 54 deletions
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 23b6f7f60..890ee6d7c 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"
@@ -135,7 +135,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:
@@ -167,7 +167,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:
@@ -184,7 +184,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:
@@ -229,6 +229,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.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 eed41fbe7..9493acd1f 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -105,16 +105,12 @@ 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
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/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..ce21ff41c 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,14 @@
# 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
+include ../Makefile.common
+
#######################################################################
# Variables
#######################################################################
@@ -97,7 +102,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 +123,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 +173,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:
@@ -244,6 +253,44 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
} > "$@"
#######################################################################
+# Unit tests
+#######################################################################
+
+OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
+SYSMOD:=-package num,str,unix,dynlink,threads
+
+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_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
+
+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) $(COQCMXS) \
+ $(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/.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
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 01:10:30 +0000