Commit 85074baf authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

bench: typecheck the gallery before extraction/execution

I know that extraction and execution are much more fun than
the boring "can we even parse WhyML at all?" question, but
you see, if our parsing/typechecking is broken, then the fun
stuff is broken, too. And I really prefer to get the error
messages about the typechecking being broken from the typechecking
part of the bench, and not from the test-api or extraction part.
Merci pour votre compréhension.
parent e63151cf
...@@ -1601,8 +1601,8 @@ CLEANDIRS += src/trywhy3 ...@@ -1601,8 +1601,8 @@ CLEANDIRS += src/trywhy3
.PHONY: bench test .PHONY: bench test
bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
share/Makefile.config share/Makefile.config bin/why3extract.@OCAMLBEST@
# temporarily disabled dependency: bin/why3extract bash bench/bench ".@OCAMLBEST@"
$(MAKE) test-api-logic.@OCAMLBEST@ $(MAKE) test-api-logic.@OCAMLBEST@
# $(MAKE) test-api-mlw-tree.@OCAMLBEST@ # $(MAKE) test-api-mlw-tree.@OCAMLBEST@
# $(MAKE) test-api-mlw.@OCAMLBEST@ # $(MAKE) test-api-mlw.@OCAMLBEST@
...@@ -1611,7 +1611,6 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \ ...@@ -1611,7 +1611,6 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
# desactivé car requiert findlib # desactivé car requiert findlib
# if test -d examples/runstrat ; then \ # if test -d examples/runstrat ; then \
# $(MAKE) test-runstrat.@OCAMLBEST@ ; fi # $(MAKE) test-runstrat.@OCAMLBEST@ ; fi
bash bench/bench ".@OCAMLBEST@"
@if test "@enable_coq_tactic@" = "yes"; then \ @if test "@enable_coq_tactic@" = "yes"; then \
echo "=== checking the Coq tactic ==="; \ echo "=== checking the Coq tactic ==="; \
$(MAKE) test-coq-tactic.@OCAMLBEST@; fi $(MAKE) test-coq-tactic.@OCAMLBEST@; fi
......
...@@ -169,10 +169,6 @@ list_stuff () { ...@@ -169,10 +169,6 @@ list_stuff () {
fi fi
} }
echo "=== Checking invalid goals ==="
invalid_goals bench/invalid
echo ""
echo "=== Checking theories ===" echo "=== Checking theories ==="
goods theories --type-only # FIXME remove --type-only goods theories --type-only # FIXME remove --type-only
echo "" echo ""
...@@ -193,6 +189,33 @@ bads bench/typing/bad --type-only ...@@ -193,6 +189,33 @@ bads bench/typing/bad --type-only
bads bench/programs/bad-typing --type-only bads bench/programs/bad-typing --type-only
echo "" echo ""
echo "=== Checking good files ==="
goods bench/typing/good
goods bench/programs/good
goods examples/bts
goods examples/tests
goods examples/tests-provers
goods examples/check-builtin
goods examples/logic
goods examples
goods examples/foveoos11-cm
goods examples/WP_revisited
goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
goods examples/bitvectors "-L examples/bitvectors"
goods examples/avl "-L examples/avl"
goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication"
goods examples/double_wp "-L examples/double_wp"
goods examples/in_progress
echo ""
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""
echo "=== Checking invalid goals ==="
invalid_goals bench/invalid
echo ""
echo "=== Checking execution ===" echo "=== Checking execution ==="
execute examples/euler001.mlw Euler001.bench execute examples/euler001.mlw Euler001.bench
execute examples/euler002.mlw Solve.bench execute examples/euler002.mlw Solve.bench
...@@ -225,7 +248,7 @@ execute examples/vstte10_queens.mlw NQueens.test8 ...@@ -225,7 +248,7 @@ execute examples/vstte10_queens.mlw NQueens.test8
echo "" echo ""
echo "=== Extraction to Ocaml ===" echo "=== Checking extraction to OCaml ==="
extract_and_run examples/euler001 euler001.ml 1000000 extract_and_run examples/euler001 euler001.ml 1000000
extract_and_run examples/gcd gcd.ml 6 15 extract_and_run examples/gcd gcd.ml 6 15
extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml
...@@ -234,31 +257,6 @@ extract_and_run examples/defunctionalization defunctionalization.ml ...@@ -234,31 +257,6 @@ extract_and_run examples/defunctionalization defunctionalization.ml
extract_and_run examples/sudoku sudoku.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6 extract_and_run examples/sudoku sudoku.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6
echo "" echo ""
echo "=== Checking good files ==="
goods bench/typing/good
goods bench/programs/good
goods examples/bts
goods examples/tests
goods examples/tests-provers
goods examples/check-builtin
goods examples/logic
goods examples
goods examples/foveoos11-cm
goods examples/WP_revisited
goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
goods examples/bitvectors "-L examples/bitvectors"
goods examples/avl "-L examples/avl"
goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication"
goods examples/double_wp "-L examples/double_wp"
goods examples/in_progress
echo ""
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""
echo "=== Checking --list-* ===" echo "=== Checking --list-* ==="
list_stuff --list-transforms list_stuff --list-transforms
list_stuff --list-printers list_stuff --list-printers
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment