Store why3-cpulimit and why3-call-pvs in libdir.

As a side effect, provers-detection-data.conf no longer needs to be preprocessed.

.gitignore

@@ -31,12 +31,6 @@ why3.conf
 /why3regtests.out
 /META
 
-# /lib/why3/
-/lib/why3/META
-/lib/why3/why3.cm*
-/lib/why3/why3.a
-/lib/why3/why3.o
-
 # /bench/
 /bench/programs/good/booleans/
 /bench/programs/good/exceptions/
@@ -56,8 +50,6 @@ why3.conf
 /bin/why3ide.byte
 /bin/why3ide.opt
 /bin/why3ide
-/bin/why3-cpulimit
-/bin/why3-cpulimit.exe
 /bin/why3config.byte
 /bin/why3config.opt
 /bin/why3config
@@ -114,8 +106,17 @@ why3.conf
 /doc/apidoc/
 /doc/stdlibdoc/
 
+# /lib
+/lib/why3-cpulimit
+/lib/why3-cpulimit.exe
+
+# /lib/why3/
+/lib/why3/META
+/lib/why3/why3.cm*
+/lib/why3/why3.a
+/lib/why3/why3.o
+
 # /share/
-/share/provers-detection-data.conf
 /share/emacs/semantic.cache
 
 # /src/
@@ -209,4 +210,4 @@ pvsbin/
 /src/jessie/ptests_local_config.ml
 /src/jessie/tests/basic/result/*.log
 /src/jessie/tests/demo/result/*.log
-/trash
\ No newline at end of file
+/trash

Makefile.in

@@ -1061,19 +1061,20 @@ endif
 # tools
 #######
 
-TOOLS = bin/why3-cpulimit$(EXE)
+TOOLS = lib/why3-cpulimit$(EXE)
 
 byte opt: $(TOOLS)
 
-bin/why3-cpulimit$(EXE): src/tools/@CPULIMIT@.c
+lib/why3-cpulimit$(EXE): src/tools/@CPULIMIT@.c
 	$(CC) -Wall -o $@ $^
 
 clean::
-	rm -f bin/why3-cpulimit$(EXE) src/tools/*~
+	rm -f lib/why3-cpulimit$(EXE) src/tools/*~
 
 install_no_local::
-	cp -f bin/why3-cpulimit$(EXE) $(BINDIR)/why3-cpulimit$(EXE)
-	cp -f bin/why3-call-pvs $(BINDIR)/why3-call-pvs
+	mkdir -p $(LIBDIR)/why3
+	cp -f lib/why3-cpulimit$(EXE) $(LIBDIR)/why3/why3-cpulimit$(EXE)
+	cp -f lib/why3-call-pvs $(LIBDIR)/why3/why3-call-pvs
 
 #########
 # why3doc
@@ -1534,7 +1535,7 @@ DISTRIB_FILES = Version Makefile.in configure.in configure \
       modules/*.mlw \
       lib/coq/*.v lib/coq/*/*.v lib/coq-tactic/*.v \
       lib/pvs/*/*.pvs lib/pvs/*/*.prf \
-      share/provers-detection-data.conf.in \
+      share/provers-detection-data.conf \
       share/why3session.dtd \
       share/javascript/*.js share/javascript/*.css \
       share/javascript/themes/default/*.gif \
@@ -1661,16 +1662,10 @@ clean::
 doc/version.tex: doc/version.tex.in config.status
 	./config.status chmod --file $@
 
-share/provers-detection-data.conf: share/provers-detection-data.conf.in config.status
-	./config.status chmod --file $@
-
-# We want it to be always up-ot-date
-Makefile : share/provers-detection-data.conf
-
 config.status: configure Version
 	./config.status --recheck
 
-opt byte: lib/why3/META share/provers-detection-data.conf
+opt byte: lib/why3/META
 
 lib/why3/META: lib/why3/META.in config.status
 	./config.status chmod --file $@

configure.in

@@ -579,10 +579,8 @@ fi
 
 if test "$enable_local" = no; then
    LOCALDIR=''
-   LOCALBIN=''
 else
    LOCALDIR="${PWD}"
-   LOCALBIN="${PWD}/bin/"
 fi
 
 #For the META
@@ -667,7 +665,6 @@ AC_SUBST(FRAMAC_LIBDIR)
 
 AC_SUBST(enable_local)
 AC_SUBST(LOCALDIR)
-AC_SUBST(LOCALBIN)
 
 AC_SUBST(enable_relocation)
 
@@ -677,7 +674,7 @@ dnl AC_SUBST(PDFVIEWER)
 # Finally create the Makefile from Makefile.in
 dnl AC_OUTPUT(Makefile)
 AC_CONFIG_FILES(Makefile src/config.sh doc/version.tex)
-AC_CONFIG_FILES(share/provers-detection-data.conf lib/why3/META)
+AC_CONFIG_FILES(lib/why3/META)
 AC_CONFIG_FILES(src/jessie/Makefile)
 AC_CONFIG_COMMANDS([chmod],
 chmod a-w Makefile src/config.sh doc/version.tex;

share/provers-detection-data.conf.in → share/provers-detection-data.conf

@@ -11,7 +11,7 @@ version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
 version_ok  = "0.95.1"
 version_old = "0.95"
 version_old = "0.95-dev"
-command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -timelimit %t %f"
+command = "%l/why3-cpulimit %T %m -s %e -timelimit %t %f"
 driver = "drivers/alt_ergo.drv"
 editor = "altgr-ergo"
 
@@ -29,7 +29,7 @@ version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
 version_ok  = "0.95.1"
 version_old = "0.95"
 version_old = "0.95-dev"
-command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -timelimit %t -model %f"
+command = "%l/why3-cpulimit %T %m -s %e -timelimit %t -model %f"
 driver = "drivers/alt_ergo_model.drv"
 editor = "altgr-ergo"
 
@@ -40,7 +40,7 @@ exec = "alt-ergo-0.94"
 version_switch = "-version"
 version_regexp = "\\([0-9.]+\\)"
 version_old = "0.94"
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
+command = "%l/why3-cpulimit %t %m -s %e %f"
 driver = "drivers/alt_ergo_0.94.drv"
 editor = "altgr-ergo"
 
@@ -53,7 +53,7 @@ version_switch = "-version"
 version_regexp = "\\([0-9.]+\\)"
 version_old = "^0\.93\..+$"
 version_old = "0.93"
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
+command = "%l/why3-cpulimit %t %m -s %e %f"
 driver = "drivers/alt_ergo_0.93.drv"
 
 [ATP alt-ergo]
@@ -74,7 +74,7 @@ version_old = "0.92"
 version_old = "0.91"
 version_old = "0.9"
 version_old = "0.8"
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
+command = "%l/why3-cpulimit %t %m -s %e %f"
 driver = "drivers/alt_ergo_0.92.drv"
 
 # CVC4 version 1.x
@@ -90,7 +90,7 @@ version_ok  = "1.0"
 version_ok  = "1.1"
 version_ok  = "1.2"
 driver = "drivers/cvc4.drv"
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e --lang=smt2 %f"
+command = "%l/why3-cpulimit %t %m -s %e --lang=smt2 %f"
 
 # CVC3 versions 2.4.x
 [ATP cvc3]
@@ -103,7 +103,7 @@ version_regexp = "This is CVC3 version \\([^ \n]+\\)"
 version_ok  = "2.4.1"
 version_old = "2.4"
 # the -timeout option is unreliable in CVC3 2.4.1
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -seed 42 %f"
+command = "%l/why3-cpulimit %t %m -s %e -seed 42 %f"
 driver = "drivers/cvc3.drv"
 
 # CVC3 versions 2.x
@@ -117,7 +117,7 @@ version_regexp = "This is CVC3 version \\([^ \n]+\\)"
 version_old = "2.2"
 version_old = "2.1"
 # we pass time 0 to why3-cpulimit to avoid race
-command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e  -seed 42 -timeout %t %f"
+command = "%l/why3-cpulimit %T %m -s %e  -seed 42 -timeout %t %f"
 driver = "drivers/cvc3.drv"
 
 [ATP yices]
@@ -131,7 +131,7 @@ version_old = "^1\.0\.3[0-7]$"
 version_old = "^1\.0\.2[5-9]$"
 version_old = "^1\.0\.2[0-4]$"
 version_old = "^1\.0\.1\.*$"
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e"
+command = "%l/why3-cpulimit %t %m -s %e"
 driver = "drivers/yices.drv"
 
 [ATP yices2]
@@ -141,7 +141,7 @@ exec = "yices-2.0.4"
 version_switch = "--version"
 version_regexp = "[Yices ]*\\([^ \n]+\\)\."
 version_ok = "^2\.0\.4"
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e"
+command = "%l/why3-cpulimit %t %m -s %e"
 driver = "drivers/yices.drv"
 
 [ATP eprover]
@@ -156,7 +156,7 @@ version_ok  = "1.6"
 version_old = "1.5"
 version_old = "1.4"
 # we pass time 0 to why3-cpulimit to avoid race
-command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
+command = "%l/why3-cpulimit %T %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
 driver = "drivers/eprover.drv"
 
 [ATP gappa]
@@ -171,7 +171,7 @@ version_regexp = "Gappa \\([^ \n]*\\)"
 version_ok = "^1\.0\..+$"
 version_ok = "^0\.1[4-8]\..+$"
 version_old = "^0\.1[1-3]\..+$"
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
+command = "%l/why3-cpulimit %t %m -s %e -Eprecision=70"
 driver = "drivers/gappa.drv"
 
 [ATP mathsat]
@@ -181,7 +181,7 @@ exec = "mathsat-5.2.2"
 version_switch = "-version"
 version_regexp = "MathSAT5 version \\([^ \n]+\\)"
 version_ok  = "5.2.2"
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -input=smt2 -model -random_seed=80 %f"
+command = "%l/why3-cpulimit %t %m -s %e -input=smt2 -model -random_seed=80 %f"
 driver = "drivers/mathsat.drv"
 
 [ATP simplify]
@@ -194,7 +194,7 @@ version_switch = "-version"
 version_regexp = "Simplify version \\([^ \n,]+\\)"
 version_old = "1.5.5"
 version_old = "1.5.4"
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
+command = "%l/why3-cpulimit %t %m -s %e %f"
 driver = "drivers/simplify.drv"
 
 [ATP metis]
@@ -203,7 +203,7 @@ exec = "metis"
 version_switch = "-v"
 version_regexp = "metis \\([^ \n,]+\\)"
 version_ok = "2.3"
-command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e --time-limit %t %f"
+command = "%l/why3-cpulimit %T %m -s %e --time-limit %t %f"
 driver = "drivers/metis.drv"
 
 [ATP metitarski]
@@ -212,7 +212,7 @@ exec = "metit"
 version_switch = "-v"
 version_regexp = "MetiTarski \\([^ \n,]+\\)"
 version_ok = "2.2"
-command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e --time %t %f"
+command = "%l/why3-cpulimit %T %m -s %e --time %t %f"
 driver = "drivers/metitarski.drv"
 
 [ATP spass]
@@ -222,7 +222,7 @@ exec = "SPASS-3.7"
 version_switch = " | grep 'SPASS V'"
 version_regexp = "SPASS V \\([^ \n\t]+\\)"
 version_ok = "3.7"
-command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
+command = "%l/why3-cpulimit %T %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
 driver = "drivers/spass.drv"
 
 [ATP spass]
@@ -232,7 +232,7 @@ exec = "SPASS-3.8ds"
 version_switch = " | grep 'SPASS[^ \\n\\t]* V'"
 version_regexp = "SPASS[^ \n\t]* V \\([^ \n\t]+\\)"
 version_ok = "3.8ds"
-command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -Isabelle=1 -PGiven=0 -TimeLimit=%t %f"
+command = "%l/why3-cpulimit %T %m -s %e -Isabelle=1 -PGiven=0 -TimeLimit=%t %f"
 driver = "drivers/spass_types.drv"
 
 [ATP vampire]
@@ -242,7 +242,7 @@ exec = "vampire-0.6"
 version_switch = "--version"
 version_regexp = "Vampire \\([0-9.]+\\)"
 # we pass time 0 to why3-cpulimit to avoid race
-command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -t %t"
+command = "%l/why3-cpulimit %T %m -s %e -t %t"
 driver = "drivers/vampire.drv"
 version_ok = "0.6"
 
@@ -251,7 +251,7 @@ name = "Princess"
 exec = "princess"
 # version_switch = "-h"
 version_regexp = "(CASC version \\([0-9-]+\\))"
-command = "'@LOCALBIN@why3-cpulimit' %T 0 -s %e -timeout=%t %f"
+command = "%l/why3-cpulimit %T 0 -s %e -timeout=%t %f"
 driver = "drivers/princess.drv"
 version_ok = "2013-05-13"
 
@@ -261,7 +261,7 @@ exec = "beagle"
 exec = "beagle-0.4.1"
 # version_switch = "-h"
 version_regexp = "version \\([0-9.]+\\)"
-command = "'@LOCALBIN@why3-cpulimit' %t 0 -s %e %f"
+command = "%l/why3-cpulimit %t 0 -s %e %f"
 driver = "drivers/beagle.drv"
 version_ok = "0.4.1"
 
@@ -271,7 +271,7 @@ exec = "veriT"
 exec = "verit"
 version_switch = "--help"
 version_regexp = "Version: \\([^ \n\r]+\\)"
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
+command = "%l/why3-cpulimit %t %m -s %e %f"
 driver = "drivers/verit.drv"
 
 [ATP z3]
@@ -292,7 +292,7 @@ version_old = "4.1.2"
 version_old = "4.1.1"
 version_old = "4.0"
 driver = "drivers/z3.drv"
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 %f"
+command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 %f"
 
 [ATP z3]
 name = "Z3"
@@ -307,7 +307,7 @@ version_old = "3.1"
 version_old = "3.0"
 driver = "drivers/z3.drv"
 # the -T is unreliable in Z3 3.2
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 %f"
+command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 %f"
 
 [ATP z3]
 name = "Z3"
@@ -321,7 +321,7 @@ version_regexp = "Z3 version \\([^ \n\r]+\\)"
 version_old = "^2\.2.+$"
 version_old = "^2\.1[6-9]$"
 driver = "drivers/z3.drv"
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 \
+command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 \
 PHASE_SELECTION=0 \
 RESTART_STRATEGY=0 \
 RESTART_FACTOR=1.5 \
@@ -352,7 +352,7 @@ version_regexp = "Z3 version \\([^ \n\r]+\\)"
 version_old = "^2\.1[0-5]$"
 version_old = "^2\.[0-9]$"
 version_old = "1.3"
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt %f"
+command = "%l/why3-cpulimit %t %m -s %e -smt %f"
 driver = "drivers/z3_smtv1.drv"
 
 [ATP zenon]
@@ -362,7 +362,7 @@ exec = "zenon-0.7.1"
 version_switch = "-v"
 version_regexp = "zenon version \\([^ \n\t]+\\)"
 version_ok = "0.7.1"
-command = "'@LOCALBIN@why3-cpulimit' %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f"
+command = "%l/why3-cpulimit %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f"
 driver = "drivers/zenon.drv"
 
 [ATP iprover]
@@ -372,7 +372,7 @@ exec = "iprover-0.8.1"
 version_switch = " | grep iProver"
 version_regexp = "iProver v\\([^ \n\t]+\\)"
 version_ok = "0.8.1"
-command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e --fof true --out_options none \
+command = "%l/why3-cpulimit %T %m -s %e --fof true --out_options none \
 --time_out_virtual %t --clausifier /usr/bin/env --clausifier_options \
 \"eprover --cnf --tstp-format \" %f"
 driver = "drivers/iprover.drv"
@@ -384,7 +384,7 @@ version_switch = "-run \"Exit[]\""
 version_regexp = "Mathematica \\([0-9.]+\\)"
 version_ok = "8.0"
 version_ok = "7.0"
-command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -noprompt < %f"
+command = "%l/why3-cpulimit %t %m -s %e -noprompt < %f"
 driver = "drivers/mathematica.drv"
 
 [ITP coq]
@@ -395,7 +395,7 @@ version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
 version_ok = "8.4pl2"
 version_ok = "8.4pl1"
 version_ok = "8.4"
-command = "'@LOCALBIN@why3-cpulimit' 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
+command = "%l/why3-cpulimit 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
 driver = "drivers/coq_8_4.drv"
 editor = "coqide"
 
@@ -409,7 +409,7 @@ version_ok = "8.3pl3"
 version_ok = "8.3pl2"
 version_ok = "8.3pl1"
 version_ok = "8.3"
-command = "'@LOCALBIN@why3-cpulimit' 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
+command = "%l/why3-cpulimit 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
 driver = "drivers/coq.drv"
 editor = "coqide"
 
@@ -420,14 +420,14 @@ version_switch = "-version"
 version_regexp = "PVS Version \\([^ \n]+\\)"
 version_ok = "6.0"
 version_bad = "^[0-5]\..+$"
-command = "'@LOCALBIN@why3-cpulimit' 0 %m -s @LOCALBIN@why3-call-pvs %l proveit -f %f"
+command = "%l/why3-cpulimit 0 %m -s %l/why3-call-pvs %l proveit -f %f"
 driver = "drivers/pvs.drv"
 in_place = true
 editor = "pvs"
 
 [editor pvs]
 name = "PVS"
-command = "@LOCALBIN@why3-call-pvs %l pvs %f"
+command = "%l/why3-call-pvs %l pvs %f"
 
 [editor coqide]
 name = "CoqIDE"

src/driver/call_provers.ml

@@ -132,7 +132,6 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
                  ?(cleanup=false) ?(inplace=false) fin =
 
   let arglist = Cmdline.cmdline_split command in
-  let command = List.hd arglist in
   let use_stdin = ref true in
   let on_timelimit = ref false in
   let cmd_regexp = Str.regexp "%\\(.\\)" in
@@ -158,6 +157,7 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
       raise e
   in
   let arglist = List.map subst arglist in
+  let command = List.hd arglist in
   Debug.dprintf debug "@[<hov 2>Call_provers: command is: %a@]@."
     (Pp.print_list Pp.space pp_print_string) arglist;
   let argarray = Array.of_list arglist in