diff --git a/bench/bench b/bench/bench index c5e01a1ccbedf9c3117e9c92cce95e2af05b9120..116e3b2e05c1fa3c66d224c2aea785ea97b041db 100755 --- a/bench/bench +++ b/bench/bench @@ -81,19 +81,29 @@ execute () { extract_and_run () { echo -n "$1... " rm -f $1/$2 - if make -C $1 > /dev/null 2>&1; then - if $1/main.opt $3 > /dev/null 2>&1; then - echo "ok" - else - echo "execution failed!" - echo $1/main.opt $3 - $1/main.opt $3 - exit 1 - fi + echo -n "extract... " + if make -C $1 extract > /dev/null 2>&1; then + echo -n "compile... " + if make -C $1 > /dev/null 2>&1; then + echo -n "execute... " + if $1/main.opt $3 > /dev/null 2>&1; then + echo "ok" + else + echo "execution failed!" + echo $1/main.opt $3 + $1/main.opt $3 + exit 1 + fi + else + echo "compilation failed!" + echo make -C $1 + make -C $1 + exit 1 + fi else - echo "extract or compilation failed!" - echo make -C $1 - make -C $1 + echo "extract failed!" + echo make -C $1 extract + make -C $1 extract exit 1 fi } diff --git a/examples/euler001/Makefile.in b/examples/euler001/Makefile.in index 289e8db3b0b8d6b534761dac9086220fa47be112..31758ad634c46e158ca914b0457a8da864ccc348 100644 --- a/examples/euler001/Makefile.in +++ b/examples/euler001/Makefile.in @@ -1,30 +1,32 @@ -OBJ=euler001__Euler001 main +MAIN=main +OBJ=euler001__Euler001 +ML = $(addsuffix .ml, $(OBJ)) CMO = $(addsuffix .cmo, $(OBJ)) CMX = $(addsuffix .cmx, $(OBJ)) -NAME=main - OCAMLOPT=ocamlopt -noassert -inline 1000 INCLUDE=@BIGINTINCLUDE@ -I ../../lib/why3 -all: $(NAME).@OCAMLBEST@ +all: $(MAIN).@OCAMLBEST@ + +extract: $(ML) -$(NAME).byte: $(CMO) +$(MAIN).byte: $(CMO) $(MAIN).cmo ocamlc $(INCLUDE) @BIGINTLIB@.cma why3extract.cma -o $@ $^ -$(NAME).opt: $(CMX) +$(MAIN).opt: $(CMX) $(MAIN).cmx $(OCAMLOPT) $(INCLUDE) @BIGINTLIB@.cmxa why3extract.cmxa -o $@ $^ -main.cmx: euler001__Euler001.cmx +$(MAIN).cmx: $(CMX) -euler001__Euler001.ml: ../euler001.mlw +$(ML): ../euler001.mlw ../../bin/why3 -E ocaml ../euler001.mlw -o . %.cmx: %.ml - ocamlopt $(INCLUDE) -annot -c $< + $(OCAMLOPT) $(INCLUDE) -annot -c $< %.cmo: %.ml ocamlc $(INCLUDE) -annot -c $< @@ -33,8 +35,7 @@ euler001__Euler001.ml: ../euler001.mlw ocamlc $(INCLUDE) -annot -c $< clean:: - rm -f *.cm[xio] *.o *.annot $(NAME).opt - rm -f euler001__*.ml euler001__*.ml.bak + rm -f $(ML) *.cm[xio] *.o *.annot $(MAIN).opt $(MAIN).byte Makefile: Makefile.in ../../config.status cd ../.. ; ./config.status chmod --file examples/euler001/Makefile diff --git a/examples/sudoku/Makefile b/examples/sudoku/Makefile index 3fd9740ab2d5c38fd98d443671dfeb02c38ef477..0f40c2fa4be0e56b0cf706a291a08c4e1efbbcab 100644 --- a/examples/sudoku/Makefile +++ b/examples/sudoku/Makefile @@ -15,6 +15,8 @@ OCAMLOPT = ocamlopt -noassert -inline 1000 all: $(MAIN).opt +extract: $(ML) + doc: ../../bin/why3doc ../sudoku.mlw ../../bin/why3session html ../sudoku.mlw @@ -40,5 +42,5 @@ $(ML): ../sudoku.mlw ocamlc $(WHY3) -annot -g -c $< clean:: - rm -f $(ML) *.cm[xio] $(MAIN).opt + rm -f $(ML) *.cm[xio] $(MAIN).opt $(MAIN).byte