Commit ba81184b authored by MARCHE Claude's avatar MARCHE Claude

bench, extraction Ocaml: also generates doc

parent 9226102c
......@@ -107,7 +107,15 @@ extract_and_run () {
if BENCH=yes make -C $1 > /dev/null 2>&1; then
echo -n "execute... "
if $1/main.opt $3 > /dev/null 2>&1; then
echo "ok"
echo -n "doc... "
if BENCH=yes make -C $1 doc > /dev/null 2>&1; then
echo "ok"
else
echo "documentation failed!"
echo BENCH=yes make -C $1 doc
BENCH=yes make -C $1 doc
exit 1
fi
else
echo "execution failed!"
echo $1/main.opt $3
......
......@@ -32,6 +32,10 @@ all: $(MAIN).$(OCAMLBEST)
extract: $(ML)
doc:
$(WHY3) doc ../euler001.mlw
$(WHY3) session html .
$(MAIN).byte: $(CMO) $(MAIN).cmo
ocamlc $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ $^
......
......@@ -5,7 +5,11 @@ ifeq ($(BENCH),yes)
WHY3=../../bin/why3
WHY3SHARE=../../share
else
WHY3=$(BINDIR)/why3
ifeq ($(BINDIR),)
WHY3=why3
else
WHY3=$(BINDIR)/why3
endif
WHY3SHARE=$(shell $(WHY3) --print-datadir)
endif
......@@ -29,8 +33,8 @@ all: $(MAIN).opt
extract: $(ML)
doc:
$(WHY3)doc ../sudoku.mlw
$(WHY3)session html ../sudoku.mlw
$(WHY3) doc ../sudoku.mlw
$(WHY3) session html .
$(MAIN).byte: $(CMO) $(MAIN).cmo
ocamlc -g $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ $^
......
......@@ -5,7 +5,11 @@ ifeq ($(BENCH),yes)
WHY3=../../bin/why3
WHY3SHARE=../../share
else
WHY3=$(BINDIR)/why3
ifeq ($(BINDIR),)
WHY3=why3
else
WHY3=$(BINDIR)/why3
endif
WHY3SHARE=$(shell $(WHY3) --print-datadir)
endif
......@@ -28,6 +32,10 @@ all: $(MAIN).$(OCAMLBEST)
extract: $(ML)
doc:
$(WHY3) doc ../vstte10_max_sum.mlw
$(WHY3) session html .
$(MAIN).byte: $(CMO) $(MAIN).cmo
ocamlc $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ $^
......
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