improved bench for extraction

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
 }

examples/euler001/Makefile.in

 
-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

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