From 9bccbb9f4b60db0a3a4cca2fb47ba62f564a247a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Claude=20March=C3=A9?= Date: Tue, 4 Mar 2014 18:04:29 +0100 Subject: [PATCH] suppression des Makefile.in --- Makefile.in | 2 +- bench/bench | 3 ++- configure.in | 1 - examples/euler001/{Makefile.in => Makefile} | 15 +++++++-------- examples/sudoku/Makefile | 19 +++++++++---------- src/config.sh.in | 15 +++++++++++++++ 6 files changed, 34 insertions(+), 21 deletions(-) rename examples/euler001/{Makefile.in => Makefile} (66%) diff --git a/Makefile.in b/Makefile.in index 56536fbe4..c12ed486a 100644 --- a/Makefile.in +++ b/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 diff --git a/bench/bench b/bench/bench index 99b779a73..378100bb4 100755 --- a/bench/bench +++ b/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 "" diff --git a/configure.in b/configure.in index d26a70cb3..63d326925 100644 --- a/configure.in +++ b/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; diff --git a/examples/euler001/Makefile.in b/examples/euler001/Makefile similarity index 66% rename from examples/euler001/Makefile.in rename to examples/euler001/Makefile index bc35eaba2..21aaa79fc 100644 --- a/examples/euler001/Makefile.in +++ b/examples/euler001/Makefile @@ -1,4 +1,8 @@ +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 - diff --git a/examples/sudoku/Makefile b/examples/sudoku/Makefile index 70d1cb2e2..cd51ac205 100644 --- a/examples/sudoku/Makefile +++ b/examples/sudoku/Makefile @@ -1,4 +1,8 @@ +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 diff --git a/src/config.sh.in b/src/config.sh.in index 5cedee379..577bd3891 100644 --- a/src/config.sh.in +++ b/src/config.sh.in @@ -1,18 +1,23 @@ #!/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 + -- 2.24.1