diff options
author | Paul Steckler <steck@stecksoft.com> | 2018-02-23 14:23:19 -0500 |
---|---|---|
committer | Gaƫtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-16 13:28:10 +0200 |
commit | a2f4a43833a29a5ede5905225b814c33e3a46132 (patch) | |
tree | bb2bd38286a6d51451df109e476862ab75ca65de /test-suite | |
parent | 3f480c993311d19b152deb6bb4dc561188d76fc7 (diff) |
add unit tests to test suite
Diffstat (limited to 'test-suite')
-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 |
6 files changed, 180 insertions, 11 deletions
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 |