Skip to content

GitLab

why3
why3
Commit 4dfefc95 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files
Options

Move check_realization.sh from nightly to bench.

parent 1be275ca
Hide whitespace changes
Inline Side-by-side
Showing with 4 additions and 3 deletions
Makefile.in
View file @ 4dfefc95
...@@ -1589,6 +1589,7 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \ ...@@ -1589,6 +1589,7 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
# 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@" bash bench/bench ".@OCAMLBEST@"
@echo ""
@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; fi $(MAKE) test-coq-tactic; fi
......
bench/bench
View file @ 4dfefc95
...@@ -254,3 +254,6 @@ list_stuff --list-formats ...@@ -254,3 +254,6 @@ list_stuff --list-formats
list_stuff --list-metas list_stuff --list-metas
list_stuff --list-debug-flags list_stuff --list-debug-flags
echo "" echo ""
echo "=== Checking realizations ==="
exec bench/check_realizations.sh
misc/nightly-bench.sh
View file @ 4dfefc95
...@@ -137,9 +137,6 @@ else ...@@ -137,9 +137,6 @@ else
echo "Counterexample regression tests succeeded. " >> $REPORT echo "Counterexample regression tests succeeded. " >> $REPORT
fi fi
# check realizations
misc/check-realizations.sh >> $REPORT
# replay proofs # replay proofs
examples/regtests.sh &> $OUT examples/regtests.sh &> $OUT
if test "$?" != "0" ; then if test "$?" != "0" ; then
......
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