bench extraction should work even if -disable-local and not installed

bench/bench

@@ -82,9 +82,9 @@ extract_and_run () {
     echo -n "$1... "
     rm -f $1/$2
     echo -n "extract... "
-    if make -C $1 extract > /dev/null 2>&1; then
+    if BENCH=yes make -C $1 extract > /dev/null 2>&1; then
         echo -n "compile... "
-        if make -C $1 > /dev/null 2>&1; then
+        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"
@@ -96,14 +96,14 @@ extract_and_run () {
            fi
         else
             echo "compilation failed!"
-            echo make -C $1
-            make -C $1
+            echo BENCH=yes make -C $1
+            BENCH=yes make -C $1
             exit 1
         fi
     else
         echo "extract failed!"
-        echo make -C $1 extract
-        make -C $1 extract
+        echo BENCH=yes make -C $1 extract
+        BENCH=yes make -C $1 extract
         exit 1
     fi
 }

examples/euler001/Makefile

 
-WHY3SHARE=$(shell ../../bin/why3 --print-datadir)
+BENCH ?= no
+
+ifeq ($(BENCH),yes)
+  WHY3=../../bin/why3
+  WHY3SHARE=../../share
+else
+  WHY3=$(BINDIR)/why3
+  WHY3SHARE=$(shell $WHY3 --print-datadir)
+endif
 
 include $(WHY3SHARE)/Makefile.config
 
@@ -25,7 +33,7 @@ $(MAIN).opt: $(CMX)  $(MAIN).cmx
 $(MAIN).cmx: $(CMX)
 
 $(ML): ../euler001.mlw
-	../../bin/why3 -E ocaml32 ../euler001.mlw -o .
+	$(WHY3) -E ocaml32 ../euler001.mlw -o .
 
 %.cmx: %.ml
 	$(OCAMLOPT) $(INCLUDE) -annot -c $<

examples/sudoku/Makefile

 
-WHY3SHARE=$(shell ../../bin/why3 --print-datadir)
+BENCH ?= no
+
+ifeq ($(BENCH),yes)
+  WHY3=../../bin/why3
+  WHY3SHARE=../../share
+else
+  WHY3=$(BINDIR)/why3
+  WHY3SHARE=$(shell $WHY3 --print-datadir)
+endif
 
 include $(WHY3SHARE)/Makefile.config
 
@@ -17,8 +25,8 @@ all: $(MAIN).opt
 extract: $(ML)
 
 doc:
-	../../bin/why3doc ../sudoku.mlw
-	../../bin/why3session html ../sudoku.mlw
+	$(WHY3)doc ../sudoku.mlw
+	$(WHY3)session html ../sudoku.mlw
 
 $(MAIN).byte: $(CMO) $(MAIN).cmo
 	ocamlc -g $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ $^
@@ -29,7 +37,7 @@ $(MAIN).opt: $(CMX) $(MAIN).cmx
 $(MAIN).cmx: $(CMX)
 
 $(ML): ../sudoku.mlw
-	../../bin/why3 -E ocaml32 ../sudoku.mlw -o .
+	$(WHY3) -E ocaml32 ../sudoku.mlw -o .
 
 %.cmx: %.ml
 	$(OCAMLOPT) $(INCLUDE) -annot -c $<

examples/vstte10_max_sum/Makefile

 
-WHY3SHARE=$(shell ../../bin/why3 --print-datadir)
+BENCH ?= no
+
+ifeq ($(BENCH),yes)
+  WHY3=../../bin/why3
+  WHY3SHARE=../../share
+else
+  WHY3=$(BINDIR)/why3
+  WHY3SHARE=$(shell $WHY3 --print-datadir)
+endif
 
 include $(WHY3SHARE)/Makefile.config
 
@@ -12,7 +20,7 @@ CMX = $(addsuffix .cmx, $(OBJ))
 
 OCAMLOPT=ocamlopt -noassert -inline 1000
 
-all: $(MAIN).opt
+all: $(MAIN).$(OCAMLBEST)
 
 extract: $(ML)
 
@@ -25,7 +33,7 @@ $(MAIN).opt: $(CMX)  $(MAIN).cmx
 $(MAIN).cmx: $(CMX)
 
 $(ML): ../vstte10_max_sum.mlw
-	../../bin/why3 -E ocaml32 ../vstte10_max_sum.mlw -o .
+	$(WHY3) -E ocaml32 ../vstte10_max_sum.mlw -o .
 
 %.cmx: %.ml
 	$(OCAMLOPT) $(INCLUDE) -annot -c $<