Skip to content

why3
why3
Commit 7707e9ec authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files
Options

Support realizations compiled afterward (fixes issue #75). 

Why3 now looks for a %l/{coq,pvs}/version file to check which version of a
prover was used to compile realizations. In particular, there is no longer
any Config.compile_time_support variable set once and for all.
parent fc53feba
Hide whitespace changes
Inline Side-by-side
Showing with 64 additions and 45 deletions
.gitignore
View file @ 7707e9ec
......@@ -157,10 +157,12 @@ why3.conf
/src/coq-tactic/why3tac.ml
# Coq
/lib/coq/version
# PVS
.pvscontext
orphaned-proofs.prf
/lib/pvs/version
/lib/pvs/*/*.summary
pvsbin/
......
Makefile.in
View file @ 7707e9ec
......@@ -162,7 +162,9 @@ endif
.PHONY: install-bin install-data uninstall-bin uninstall-data
.PHONY: install-bash install-emacs install-framac
.PHONY: uninstall-bash uninstall-emacs uninstall-framac
.PHONY: install-coq-tactic install-coq install-pvs install-isabelle
.PHONY: coq install-coq-tactic install-coq install-coq-data
.PHONY: pvs install-pvs install-pvs-data
.PHONY: install-isabelle
.PHONY: plugins plugins.byte plugins.opt
CLEANDIRS =
......@@ -1006,6 +1008,9 @@ endif
# Coq realizations
####################
lib/coq/version: lib/coq/version.in config.status
./config.status chmod --file $@
COQVERSIONSPECIFIC=
COQVERSIONSPECIFICTARGETS=$(addprefix lib/coq/, $(COQVERSIONSPECIFIC))
......@@ -1146,6 +1151,7 @@ ifeq (@enable_coq_libs@,yes)
install-coq:
$(MKDIR_P) $(LIBDIR)/why3/coq
$(INSTALL_DATA) lib/coq/version $(LIBDIR)/why3/coq/
$(INSTALL_DATA) lib/coq/BuiltIn.vo lib/coq/HighOrd.vo $(LIBDIR)/why3/coq/
$(MKDIR_P) $(LIBDIR)/why3/coq/int
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/
......@@ -1190,7 +1196,9 @@ COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
$(SHOW) 'Coqdep $<'
$(HIDE)$(COQDEP) -R lib/coq Why3 $< $(TOTARGET)
all: $(COQVO)
coq: $(COQVO)
all: coq
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq"
......@@ -1209,9 +1217,11 @@ endif
all: drivers/coq-realizations.aux
install-data::
install-coq-data:
$(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
install-data:: install-coq-data
clean::
rm -f drivers/coq-realizations.aux
......@@ -1219,6 +1229,9 @@ clean::
# PVS realizations
####################
lib/pvs/version: lib/pvs/version.in config.status
./config.status chmod --file $@
ifeq (@enable_pvs_libs@,yes)
PVSLIBS_INT_FILES = Int Abs MinMax ComputerDivision EuclideanDivision
......@@ -1259,6 +1272,8 @@ drivers/pvs-realizations.aux: Makefile
) > $@
install-pvs:
$(MKDIR_P) $(LIBDIR)/why3/pvs
$(INSTALL_DATA) lib/pvs/version $(LIBDIR)/why3/pvs/
$(MKDIR_P) $(LIBDIR)/why3/pvs/int
$(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_INT)) $(LIBDIR)/why3/pvs/int/
$(INSTALL_DATA) $(addsuffix .prf, $(PVSLIBS_INT)) $(LIBDIR)/why3/pvs/int/
......@@ -1284,10 +1299,12 @@ drivers/pvs-realizations.aux: Makefile
$(SHOW) 'Generate $@'
$(HIDE)echo "(* generated automatically at compilation time *)" > $@
install-data::
endif
install-pvs-data:
$(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
endif
install-data:: install-pvs-data
all: drivers/pvs-realizations.aux
......
configure.in
View file @ 7707e9ec
......@@ -643,9 +643,7 @@ fi
if test "$enable_coq_support" = no; then
enable_coq_tactic=no
enable_coq_libs=no
COMPILETIMECOQ=
else
COMPILETIMECOQ="\\\"Coq\\\", \\\"$COQVERSION\\\"; "
COQVERSION=
fi
if test "$enable_coq_tactic" = yes; then
......@@ -720,9 +718,7 @@ fi
if test "$enable_pvs_support" = no; then
enable_pvs_libs=no
COMPILETIMEPVS=
else
COMPILETIMEPVS="\\\"PVS\\\", \\\"$PVSVERSION\\\"; "
PVSVERSION=
fi
# Isabelle
......@@ -901,12 +897,11 @@ AC_SUBST(COQC)
AC_SUBST(COQDEP)
AC_SUBST(COQLIB)
AC_SUBST(COQPPLIBS)
AC_SUBST(COMPILETIMECOQ)
AC_SUBST(COQVERSION)
AC_SUBST(enable_pvs_libs)
AC_SUBST(PVS)
AC_SUBST(PVSVERSION)
AC_SUBST(COMPILETIMEPVS)
AC_SUBST(enable_isabelle_libs)
AC_SUBST(ISABELLE)
......@@ -948,11 +943,13 @@ AC_CONFIG_FILES(Makefile src/config.sh doc/version.tex)
AC_CONFIG_FILES(lib/why3/META)
AC_CONFIG_FILES(.merlin)
AC_CONFIG_FILES(src/jessie/Makefile)
AC_CONFIG_FILES(lib/coq/version lib/pvs/version)
AC_CONFIG_COMMANDS([chmod],
chmod a-w Makefile src/config.sh doc/version.tex;
chmod a-w lib/why3/META;
chmod a-w .merlin;
chmod a-w src/jessie/Makefile;
chmod a-w lib/coq/version lib/pvs/version;
chmod u+x src/config.sh)
AC_OUTPUT
......
lib/why3-call-pvs
View file @ 7707e9ec
#!/bin/sh
if test -z "$PVS_LIBRARY_PATH"; then
export PVS_LIBRARY_PATH=$1/pvs
export PVS_LIBRARY_PATH=$1
else
export PVS_LIBRARY_PATH=$1/pvs:$PVS_LIBRARY_PATH
export PVS_LIBRARY_PATH=$1:$PVS_LIBRARY_PATH
fi
shift
exec "$@"
share/provers-detection-data.conf
View file @ 7707e9ec
......@@ -524,7 +524,7 @@ driver = "mathematica"
# Coq 8.6: do not limit memory
[ITP coq]
name = "Coq"
compile_time_support = true
support_library = "%l/coq/version"
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
......@@ -539,7 +539,7 @@ editor = "coqide"
# Coq 8.5: do not limit memory
[ITP coq]
name = "Coq"
compile_time_support = true
support_library = "%l/coq/version"
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
......@@ -553,7 +553,7 @@ editor = "coqide"
[ITP coq]
name = "Coq"
compile_time_support = true
support_library = "%l/coq/version"
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
......@@ -565,13 +565,13 @@ editor = "coqide"
[ITP pvs]
name = "PVS"
compile_time_support = true
support_library = "%l/pvs/version"
exec = "pvs"
version_switch = "-version"
version_regexp = "PVS Version \\([^ \n]+\\)"
version_ok = "6.0"
version_bad = "^[0-5]\..+$"
command = "%l/why3-call-pvs %l proveit -f %f"
command = "%l/why3-call-pvs %l/pvs proveit -f %f"
driver = "pvs"
in_place = true
editor = "pvs"
......
src/config.sh.in
View file @ 7707e9ec
......@@ -27,8 +27,6 @@ let version = \"@VERSION@\"
let libdir = $libdir
let datadir = $datadir
let localdir = $localdir
let compile_time_support = [ @COMPILETIMECOQ@ @COMPILETIMEPVS@ ]
" > $config
echo "
......
src/driver/autodetection.ml
View file @ 7707e9ec
......@@ -57,7 +57,7 @@ type prover_autodetection_data =
prover_id : string;
prover_name : string;
prover_altern : string;
compile_time_support : bool;
support_library : string;
execs : string list;
version_switch : string;
version_regexp : string;
......@@ -77,7 +77,7 @@ type prover_autodetection_data =
let prover_keys =
let add acc k = Sstr.add k acc in
List.fold_left add Sstr.empty
["name";"compile_time_support";
["name";"support_library";
"exec";"version_switch";"version_regexp";
"version_ok";"version_old";"version_bad";"command"; "command_steps";
"editor";"driver";"in_place";"message";"alternative";"use_at_auto_level"]
......@@ -89,8 +89,7 @@ let load_prover kind (id,section) =
prover_id = id;
prover_name = get_string section "name";
prover_altern = get_string section ~default:"" "alternative";
compile_time_support =
get_bool section ~default:false "compile_time_support";
support_library = get_string section ~default:"" "support_library";
execs = get_stringl section "exec";
version_switch = get_string section ~default:"" "version_switch";
version_regexp = get_string section ~default:"" "version_regexp";
......@@ -394,6 +393,30 @@ let generate_auto_strategies config =
(add_strategy
(add_strategy config split) auto0) auto1) auto2
let check_support_library data ver =
let cmd_regexp = Str.regexp "%\\(.\\)" in
let replace s = match Str.matched_group 1 s with
| "l" -> Config.libdir
| "d" -> Config.datadir
| c -> c in
let sl = Str.global_substitute cmd_regexp replace data.support_library in
try
let f = open_in sl in
let support_ver = input_line f in
close_in f;
if support_ver = ver then true
else begin
eprintf
"Found prover %s version %s, but Why3 was compiled with support for version %s@."
data.prover_name ver support_ver;
false
end
with Sys_error _ | Not_found ->
eprintf
"Found prover %s version %s, but Why3 wasn't compiled with support for it@."
data.prover_name ver;
false
let detect_exec env data acc exec_name =
let s = ask_prover_version env exec_name data.version_switch in
match s with
......@@ -420,25 +443,7 @@ let detect_exec env data acc exec_name =
else
(* check if this prover needs compile-time support *)
let missing_compile_time_support =
if data.compile_time_support then
try
let compile_time_ver =
List.assoc data.prover_name Config.compile_time_support
in
if compile_time_ver <> ver then begin
eprintf
"Found prover %s version %s, but Why3 was compiled with support for version %s@."
data.prover_name ver compile_time_ver;
true
end
else
false
with Not_found ->
eprintf
"Found prover %s version %s, but Why3 wasn't compiled with support for it@."
data.prover_name ver;
true
else false
data.support_library <> "" && not (check_support_library data ver)
in
if missing_compile_time_support then
(known_version env exec_name; acc)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment