diff options
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | .travis.yml | 9 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | Makefile.common | 2 | ||||
| -rw-r--r-- | dev/ci/appveyor.sh | 2 | ||||
| -rw-r--r-- | dev/doc/changes.md | 5 | ||||
| -rw-r--r-- | test-suite/Makefile | 74 | ||||
| -rw-r--r-- | test-suite/README.md | 3 | ||||
| -rw-r--r-- | test-suite/unit-tests/clib/inteq.ml | 13 | ||||
| -rw-r--r-- | test-suite/unit-tests/clib/unicode_tests.ml | 15 | ||||
| -rw-r--r-- | test-suite/unit-tests/src/utest.ml | 74 | ||||
| -rw-r--r-- | test-suite/unit-tests/src/utest.mli | 12 |
12 files changed, 195 insertions, 18 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 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 @@ -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: @@ -244,6 +252,50 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v } > "$@" ####################################################################### +# 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 |