Commit f0df9560 authored by MARCHE Claude's avatar MARCHE Claude

make bench works without installing even without this stupid option --enablelocal of configure

parent 3a7f4851
......@@ -327,7 +327,7 @@ clean::
bin/whyide.opt $*.why
%.gui: %.mlw bin/whyide.opt
bin/whydb.opt $*.mlw
bin/whyide.opt $*.mlw
install_no_local::
cp -f bin/whyml.@OCAMLBEST@ $(BINDIR)/why3ml
......@@ -392,7 +392,7 @@ install_no_local::
ifeq (@enable_ide@,yes)
IDE_FILES = gconfig scheduler gmain
IDE_FILES = gconfig scheduler db gmain
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
......@@ -401,16 +401,16 @@ IDEMLI = $(addsuffix .mli, $(IDEMODULES))
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
IDECMX = $(addsuffix .cmx, $(IDEMODULES))
$(IDECMO) $(IDECMX): INCLUDES += -I src/ide
$(IDECMO) $(IDECMX): INCLUDES += -I src/ide -I +sqlite3
# build targets
byte: bin/whyide.byte
opt: bin/whyide.opt
bin/whyide.opt bin/whyide.byte: INCLUDES += -thread -I +threads -I +lablgtk2
bin/whyide.opt bin/whyide.byte: INCLUDES += -thread -I +threads -I +lablgtk2 -I +sqlite3
bin/whyide.opt bin/whyide.byte: EXTOBJS += gtkThread
bin/whyide.opt bin/whyide.byte: EXTLIBS += threads lablgtk lablgtksourceview2
bin/whyide.opt bin/whyide.byte: EXTLIBS += threads lablgtk lablgtksourceview2 sqlite3
bin/whyide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
......@@ -441,60 +441,6 @@ install_no_local::
endif
###############
# IDE WITH DB
###############
ifeq (@enable_sql@,yes)
DB_FILES = gconfig scheduler db gdbmain
DBMODULES = $(addprefix src/ide/, $(DB_FILES))
DBML = $(addsuffix .ml, $(DBMODULES))
DBMLI = $(addsuffix .mli, $(DBMODULES))
DBCMO = $(addsuffix .cmo, $(DBMODULES))
DBCMX = $(addsuffix .cmx, $(DBMODULES))
$(DBCMO) $(DBCMX): INCLUDES += -I src/ide -I +sqlite3
# build targets
byte: bin/whydb.byte
opt: bin/whydb.opt
bin/whydb.opt bin/whydb.byte: INCLUDES += -thread -I +threads -I +lablgtk2 -I +sqlite3
bin/whydb.opt bin/whydb.byte: EXTOBJS += gtkThread
bin/whydb.opt bin/whydb.byte: EXTLIBS += threads lablgtk lablgtksourceview2 sqlite3
bin/whydb.opt: src/why.cmxa $(PGMCMX) $(DBCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
bin/whydb.byte: src/why.cma $(PGMCMO) $(DBCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
# depend and clean targets
include .depend.db
.depend.db:
$(OCAMLDEP) -slash -I src -I src/ide $(DBML) $(DBMLI) > $@
depend: .depend.db
clean::
rm -f src/ide/*.cm[iox] src/ide/*.o
rm -f src/ide/*.annot src/ide/*~
rm -f bin/whydb.byte bin/whydb.opt
rm -f .depend.db
install_no_local::
cp -f bin/whydb.@OCAMLBEST@ $(BINDIR)/why3db
endif
##############
# Coq plugin
......
......@@ -2,8 +2,11 @@
# auto bench for why
(* Useless in this script ?
export WHY3LIB=lib
export WHY3DATA=.
*)
export WHY3LOADPATH=theories
pgm=$1
pgml=$2
......@@ -16,6 +19,9 @@ goods () {
# running Why
if ! $pgm $2 $f > /dev/null 2>&1; then
echo "why FAILED"
echo "env: WHY3DATA='$WHY3DATA'"
echo "invocation: $pgm $2 $f"
echo "result:"
$pgm $2 $f
exit 1
fi
......
......@@ -72,10 +72,6 @@ AC_ARG_ENABLE(ide,
[ --enable-ide enable Why3 IDE],,
enable_ide=yes)
AC_ARG_ENABLE(sql,
[ --enable-sql enable Why3 IDE + SQL],,
enable_sql=yes)
# dynlink
AC_ARG_ENABLE(plugins,
......@@ -256,14 +252,26 @@ fi
# checking for lablgtk2
if test "$enable_ide" = yes ; then
#AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_ide=no)
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtk.cma,,enable_ide=no)
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtksourceview2.cma,,enable_ide=no)
if test "$enable_ide" = no; then
AC_MSG_WARN("Lib lablgtk2 not found, IDE disabled.)
reason_ide=" (lablgtk2 not found)"
else
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtksourceview2.cma,,enable_ide=no)
if test "$enable_ide" = no; then
AC_MSG_WARN("Lib lablgtksourceview2 not found, IDE disabled.)
reason_ide=" (lablgtksourceview2 not found)"
fi
fi
fi
# checking for sqlite3
if test "$enable_sql" = yes ; then
AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_sql=no)
if test "$enable_ide" = yes ; then
AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_ide=no)
if test "$enable_ide" = no; then
AC_MSG_WARN("Lib sqlite3 not found, IDE disabled.)
reason_ide=" (sqlite3 not found)"
fi
fi
......@@ -276,11 +284,13 @@ dnl AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true)
if test "$enable_coq_support" = no; then
enable_coq_support=no
AC_MSG_WARN(coq support disabled)
reason_coq_support=" (disabled by user)"
else
AC_CHECK_PROG(COQC,coqc,coqc,no)
if test "$COQC" = no ; then
enable_coq_support=no
AC_MSG_WARN(Cannot find coqc.)
reason_coq_support=" (coqc not found)"
else
COQLIB=`$COQC -where | sed -e 's|\\\|/|g' -e 's| |\\ |g'`
AC_MSG_CHECKING(Coq version)
......@@ -289,18 +299,26 @@ else
case $COQVERSION in
8.*|trunk)
enable_coq_support=yes
AC_MSG_RESULT($COQVERSION);;
AC_MSG_RESULT($COQVERSION)
;;
*)
enable_coq_support=no
AC_MSG_WARN(You need Coq 8.x or later; Coq discarded);;
AC_MSG_WARN(You need Coq 8.x or later; Coq discarded)
reason_coq_support=" (need version 8.x or later)"
;;
esac
fi
fi
if test "$enable_coq_support" = yes; then
AC_CHECK_FILE($COQLIB/kernel/term.cmi,,enable_coq_support=no)
if test "$enable_coq_support" = no; then
reason_coq_support=" ($COQLIB/kernel/term.cmi not found)"
fi
fi
if test "$CAMLP5O" = no; then
enable_coq_support=no
reason_coq_support=" ($CAMLP5O not found)"
fi
# hypothesis_selection
......@@ -353,7 +371,6 @@ dnl AC_SUBST(OCAMLWEB)
AC_SUBST(CAMLP5O)
AC_SUBST(enable_ide)
AC_SUBST(enable_sql)
AC_SUBST(enable_plugins)
AC_SUBST(DYNLINK)
......@@ -392,10 +409,9 @@ echo "-----------------------------------------"
echo "OCaml version : $OCAMLVERSION"
echo "OCaml library path : $OCAMLLIB"
echo "Verbose make : $enable_verbose_make"
echo "Why IDE : $enable_ide"
echo "Why IDE with database : $enable_sql"
echo "Why IDE : $enable_ide $reason_ide"
echo "Why plugins : $enable_plugins"
echo "Coq support : $enable_coq_support"
echo "Coq plugin support : $enable_coq_support $reason_coq_support"
if test "$enable_coq_support" = "yes" ; then
echo " Version : $COQVERSION"
echo " Lib : $COQLIB"
......
......@@ -18,7 +18,7 @@ the alt-ergo prover to check them
let config = Whyconf.read_config None
let main = Whyconf.get_main config
let env = Env.create_env (Lexer.retrieve main.Whyconf.loadpath)
let env = Env.create_env (Lexer.retrieve (Whyconf.loadpath main))
let provers = Whyconf.get_provers config
......
......@@ -48,12 +48,15 @@ type config_prover = {
}
type main = {
private_libdir : string;
private_datadir : string;
loadpath : string list;
timelimit : int;
private_libdir : string; (* "/usr/local/lib/why/" *)
private_datadir : string; (* "/usr/local/share/why/" *)
loadpath : string list; (* "/usr/local/lib/why/theories" *)
timelimit : int; (* default prover time limit in seconds
(0 unlimited) *)
memlimit : int;
(* default prover memory limit in megabytes (0 unlimited)*)
running_provers_max : int;
(* max number of running prover processes *)
}
let libdir m =
......@@ -63,9 +66,29 @@ let libdir m =
let datadir m =
try
Sys.getenv "WHY3DATA"
let d = Sys.getenv "WHY3DATA" in
(*
eprintf "[Info] datadir set using WHY3DATA='%s'@." d;
*)
d
with Not_found -> m.private_datadir
let loadpath m =
try
let d = Sys.getenv "WHY3LOADPATH" in
(*
eprintf "[Info] loadpath set using WHY3LOADPATH='%s'@." d;
*)
[d]
with Not_found -> m.loadpath
let timelimit m = m.timelimit
let memlimit m = m.memlimit
let running_provers_max m = m.running_provers_max
let set_limits m time mem running =
{ m with timelimit = time; memlimit = mem; running_provers_max = running }
type config = {
conf_file : string; (* "/home/innocent_user/.why.conf" *)
config : Rc.t ;
......
......@@ -29,20 +29,15 @@ type config_prover = {
editor : string; (* Interative theorem prover *)
}
type main = {
private_libdir : string; (* "/usr/local/lib/why/" *)
private_datadir : string; (* "/usr/local/share/why/" *)
loadpath : string list; (* "/usr/local/lib/why/theories" *)
timelimit : int; (* default prover time limit in seconds
(0 unlimited) *)
memlimit : int;
(* default prover memory limit in megabytes (0 unlimited)*)
running_provers_max : int;
(* max number of running prover processes *)
}
type main
val libdir: main -> string
val datadir: main -> string
val loadpath: main -> string list
val timelimit: main -> int
val memlimit: main -> int
val running_provers_max: main -> int
val set_limits: main -> int -> int -> int -> main
type config
(** A configuration linked to an rc file. Whyconf gives access to
......
......@@ -101,10 +101,10 @@ let load_config config =
window_width = ide.ide_window_width;
tree_width = ide.ide_tree_width;
task_height = ide.ide_task_height;
time_limit = main.Whyconf.timelimit;
mem_limit = main.Whyconf.memlimit;
time_limit = Whyconf.timelimit main;
mem_limit = Whyconf.memlimit main;
verbose = ide.ide_verbose;
max_running_processes = main.Whyconf.running_provers_max;
max_running_processes = Whyconf.running_provers_max main;
(*
provers = Mstr.fold (get_prover_data env) provers [];
*)
......@@ -131,11 +131,9 @@ let save_config t =
} acc in
let config = t.config in
let config = set_main config
{ (get_main config) with
timelimit = t.time_limit;
memlimit = t.mem_limit;
running_provers_max = t.max_running_processes;
} in
(set_limits (get_main config)
t.time_limit t.mem_limit t.max_running_processes)
in
let ide = empty_section in
let ide = set_int ide "window_height" t.window_height in
let ide = set_int ide "window_width" t.window_width in
......
This diff is collapsed.
This diff is collapsed.
......@@ -295,9 +295,9 @@ let () =
in
let main = get_main config in
opt_loadpath := List.rev_append !opt_loadpath main.loadpath;
if !opt_timelimit = None then opt_timelimit := Some main.timelimit;
if !opt_memlimit = None then opt_memlimit := Some main.memlimit;
opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main);
if !opt_timelimit = None then opt_timelimit := Some (Whyconf.timelimit main);
if !opt_memlimit = None then opt_memlimit := Some (Whyconf.memlimit main);
begin match !opt_prover with
| Some s ->
let prover = try Mstr.find s (get_provers config) with
......
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