suppression des Makefile.in

Makefile.in

@@ -1923,7 +1923,7 @@ src/config.sh: src/config.sh.in config.status
 
 src/util/config.ml: src/config.sh
 	$(if $(QUIET),@echo 'Generate $@' &&) \
-	    LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
+	    BINDIR=$(BINDIR) LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
 
 clean::
 	rm -f src/util/config.ml src/config.ml

bench/bench

@@ -183,7 +183,8 @@ execute examples/vstte10_queens.mlw NQueens.test8
 echo ""
 
 echo "=== Extraction to Ocaml ==="
-extract_and_run examples/euler001 euler001__Euler001.ml 1000000
+extract_and_run examples/euler001 euler001__*.ml 1000000
+extract_and_run examples/vstte10_max_sum vstte10_max_sum__*.ml
 extract_and_run examples/sudoku sudoku__*.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6
 echo ""
 

configure.in

@@ -765,7 +765,6 @@ dnl AC_OUTPUT(Makefile)
 AC_CONFIG_FILES(Makefile src/config.sh doc/version.tex)
 AC_CONFIG_FILES(lib/why3/META)
 AC_CONFIG_FILES(src/jessie/Makefile)
-AC_CONFIG_FILES(examples/euler001/Makefile)
 AC_CONFIG_COMMANDS([chmod],
 chmod a-w Makefile src/config.sh doc/version.tex;
 chmod a-w lib/why3/META;

examples/euler001/Makefile.in → examples/euler001/Makefile

 
+WHY3SHARE=$(shell ../../bin/why3 --print-datadir)
+
+include $(WHY3SHARE)/Makefile.config
+
 MAIN=main
 OBJ=euler001__Euler001
 
@@ -8,17 +12,15 @@ CMX = $(addsuffix .cmx, $(OBJ))
 
 OCAMLOPT=ocamlopt -noassert -inline 1000
 
-INCLUDE=@BIGINTINCLUDE@ -I ../../lib/why3
-
-all: $(MAIN).@OCAMLBEST@
+all: $(MAIN).$(OCAMLBEST)
 
 extract: $(ML)
 
 $(MAIN).byte: $(CMO)  $(MAIN).cmo
-	ocamlc $(INCLUDE) @BIGINTLIB@.cma why3extract.cma -o $@ $^
+	ocamlc $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ $^
 
 $(MAIN).opt: $(CMX)  $(MAIN).cmx
-	$(OCAMLOPT) $(INCLUDE) @BIGINTLIB@.cmxa why3extract.cmxa -o $@ $^
+	$(OCAMLOPT) $(INCLUDE) $(BIGINTLIB).cmxa why3extract.cmxa -o $@ $^
 
 $(MAIN).cmx: $(CMX)
 
@@ -38,6 +40,3 @@ clean::
 	rm -f $(ML) *.cm[xio] *.o *.annot $(MAIN).opt $(MAIN).byte
 	rm -f why3__*.ml* euler001__*.ml* int__*.ml*
 
-Makefile: Makefile.in ../../config.status
-	cd ../.. ; ./config.status chmod --file examples/euler001/Makefile
-

examples/sudoku/Makefile

 
+WHY3SHARE=$(shell ../../bin/why3 --print-datadir)
+
+include $(WHY3SHARE)/Makefile.config
+
 MAIN = main
 OBJ = sudoku__Grid sudoku__TheClassicalSudokuGrid sudoku__Solver
 
@@ -6,11 +10,6 @@ ML  = $(addsuffix .ml, $(OBJ))
 CMO = $(addsuffix .cmo, $(OBJ))
 CMX = $(addsuffix .cmx, $(OBJ))
 
-
-ZARITH = $(shell ocamlfind query -i-format zarith)
-NUMLIB = zarith
-WHY3   = -I ../../lib/why3
-
 OCAMLOPT = ocamlopt -noassert -inline 1000
 
 all: $(MAIN).opt
@@ -22,10 +21,10 @@ doc:
 	../../bin/why3session html ../sudoku.mlw
 
 $(MAIN).byte: $(CMO) $(MAIN).cmo
-	ocamlc -g $(ZARITH) $(WHY3) $(NUMLIB).cma why3extract.cma -o $@ $^
+	ocamlc -g $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ $^
 
 $(MAIN).opt: $(CMX) $(MAIN).cmx
-	$(OCAMLOPT) $(ZARITH) $(WHY3) $(NUMLIB).cmxa why3extract.cmxa -o $@ $^
+	$(OCAMLOPT) $(INCLUDE) $(BIGINTLIB).cmxa why3extract.cmxa -o $@ $^
 
 $(MAIN).cmx: $(CMX)
 
@@ -33,13 +32,13 @@ $(ML): ../sudoku.mlw
 	../../bin/why3 -E ocaml32 ../sudoku.mlw -o .
 
 %.cmx: %.ml
-	$(OCAMLOPT) $(WHY3) -annot -c $<
+	$(OCAMLOPT) $(INCLUDE) -annot -c $<
 
 %.cmo: %.ml
-	ocamlc $(WHY3) -annot -g -c $<
+	ocamlc $(INCLUDE) -annot -g -c $<
 
 %.cmi: %.mli
-	ocamlc $(WHY3) -annot -g -c $<
+	ocamlc $(INCLUDE) -annot -g -c $<
 
 clean::
 	rm -f $(ML) *.annot *.o *.cm[xio] $(MAIN).opt $(MAIN).byte

src/config.sh.in

 #!/bin/sh
 
 config=src/util/config.ml
+makefileconfig=share/Makefile.config
 
+bindir="\"$BINDIR\""
 libdir="\"$LIBDIR/why3\""
 datadir="\"$DATADIR/why3\""
 localdir="None"
 
 if [ "@enable_relocation@" = "yes" ]; then
+    bindir='Filename.concat (Filename.dirname
+        (Filename.dirname Sys.executable_name)) "bin"'
     libdir='Filename.concat (Filename.concat (Filename.dirname
         (Filename.dirname Sys.executable_name)) "lib") "why3"'
     datadir='Filename.concat (Filename.concat (Filename.dirname
         (Filename.dirname Sys.executable_name)) "share") "why3"'
     localdir="None"
 elif [ "@enable_local@" = "yes" ]; then
+    bindir="\"@LOCALDIR@/bin\""
     libdir="\"@LOCALDIR@/lib\""
     datadir="\"@LOCALDIR@/share\""
     localdir="Some \"@LOCALDIR@\""
@@ -28,3 +33,13 @@ let localdir  = $localdir
 
 let compile_time_support = [ @COMPILETIMECOQ@ @COMPILETIMEPVS@ ]
 " > $config
+
+echo "
+BINDIR      = $bindir
+LIBDIR      = $libdir
+DATADIR     = $datadir
+OCAMLBEST   = @OCAMLBEST@
+BIGINTLIB   = @BIGINTLIB@
+INCLUDE     = @BIGINTINCLUDE@ -I $libdir/why3
+" > $makefileconfig
+