Commit df8c5de4 authored by MARCHE Claude's avatar MARCHE Claude

running_prover_max in conf file

parent a76db8e8
......@@ -292,21 +292,21 @@ $(IDECMO) $(IDECMX) $(addsuffix .cmx, $(IDEMAIN)) $(addsuffix .cmo, $(IDEMAIN)):
src/ide/gmain.cmo src/ide/gmain.cmx: INCLUDES += -I +lablgtk2
ifeq (@enable_ide@,yes)
byte: bin/gwhy.byte
opt: bin/gwhy.opt
byte: bin/whyide.byte
opt: bin/whyide.opt
endif
bin/gwhy.opt bin/gwhy.byte: INCLUDES = -thread -I +lablgtk2
bin/whyide.opt bin/whyide.byte: INCLUDES = -thread -I +lablgtk2
# -I +sqlite3
bin/gwhy.opt: src/why.cmxa $(PGMCMX) $(IDECMX) src/ide/gmain.cmx
bin/whyide.opt: src/why.cmxa $(PGMCMX) $(IDECMX) src/ide/gmain.cmx
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx $^
$(STRIP) $@
# sqlite3.cmxa
bin/gwhy.byte: src/why.cma $(PGMCMO) $(IDECMO) src/ide/gmain.cmo
bin/whyide.byte: src/why.cma $(PGMCMO) $(IDECMO) src/ide/gmain.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
lablgtk.cma lablgtksourceview2.cma gtkThread.cmo $^
......@@ -324,75 +324,9 @@ depend: .depend.ide
clean::
rm -f src/ide/*.cm[iox] src/ide/*.o
rm -f src/ide/*.annot src/ide/*~
rm -f bin/gwhy.byte bin/gwhy.opt
rm -f bin/whyide.byte bin/whyide.opt
rm -f .depend.ide
###############
# rust prover
###############
MNG_FILES = db scheduler
MNG_MAIN_FILES = test gmanager
MNGMODULES = $(addprefix src/manager/, $(MNG_FILES))
MNGMAINS = $(addprefix src/manager/, $(MNG_MAIN_FILES))
MNGML = $(addsuffix .ml, $(MNGMODULES))
MNGMLI = $(addsuffix .mli, $(MNGMODULES))
MNGCMO = $(addsuffix .cmo, $(MNGMODULES))
MNGCMX = $(addsuffix .cmx, $(MNGMODULES))
MNGMAINML = $(addsuffix .ml, $(MNGMAINS))
$(MNGCMO) $(MNGCMX) $(addsuffix .cmx, $(MNGMAINS)) $(addsuffix .cmo, $(MNGMAINS)): INCLUDES = -thread -I src/manager -I +sqlite3 -I +threads
src/manager/gmanager.cmo src/manager/gmanager.cmx: INCLUDES += -I +lablgtk2
ifeq (@enable_rust_prover@,yes)
byte: bin/manager-test.byte bin/why-ide.byte
opt: bin/manager-test.opt bin/why-ide.opt
endif
bin/manager-test.opt bin/manager-test.byte: INCLUDES = -thread -I +sqlite3
bin/manager-test.opt: src/why.cmxa $(MNGCMX) src/manager/test.cmx
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa sqlite3.cmxa $^
$(STRIP) $@
bin/manager-test.byte: src/why.cma $(MNGCMO) src/manager/test.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma sqlite3.cma $^
bin/why-ide.opt bin/why-ide.byte: INCLUDES = -thread -I +sqlite3 -I +lablgtk2
bin/why-ide.opt: src/why.cmxa $(PGMCMX) $(MNGCMX) src/manager/gmanager.cmx
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx sqlite3.cmxa $^
$(STRIP) $@
bin/why-ide.byte: src/why.cma $(PGMCMO) $(MNGCMO) src/manager/gmanager.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
lablgtk.cma lablgtksourceview2.cma gtkThread.cmo sqlite3.cma $^
# depend and clean targets
include .depend.manager
.depend.manager:
$(OCAMLDEP) -slash -I src -I src/manager $(MNGML) $(MNGMLI) $(MNGMAINML) > $@
depend: .depend.manager
clean::
rm -f src/manager/*.cm[iox] src/manager/*.o
rm -f src/manager/*.annot src/manager/*~
rm -f bin/manager.byte bin/manager.opt
rm -f .depend.manager
##############
# Coq plugin
##############
......@@ -588,15 +522,15 @@ install::
## install: install-binary install-lib install-man
##
## BINARYFILES = $(BINARY) bin/why-ide.$(OCAMLBEST)
## BINARYFILES = $(BINARY) bin/whyide.$(OCAMLBEST)
##
## # install-binary should not depend on $(BINARYFILES); otherwise it
## # enforces the compilation of why-ide, even when lablgtk2 is not installed
## # enforces the compilation of whyide, even when lablgtk2 is not installed
## install-binary:
## mkdir -p $(BINDIR)
## cp -f $(BINARY) $(BINDIR)/why$(EXE)
## if test -f bin/why-ide.$(OCAMLBEST); then \
## cp -f bin/why-ide.$(OCAMLBEST) $(BINDIR)/why-ide-bin$(EXE); \
## if test -f bin/whyide.$(OCAMLBEST); then \
## cp -f bin/whyide.$(OCAMLBEST) $(BINDIR)/whyide-bin$(EXE); \
## fi
##
## install-lib:
......@@ -638,12 +572,12 @@ install::
## cp lib/mizar/why.miz @MIZARLIB@/mml
## cp lib/mizar/dict/why.voc @MIZARLIB@/mml/dict
##
## local-install: $(BINARY) $(WHYCONFIG) $(JESSIE) bin/why-ide.$(OCAMLBEST) byte bin/why-ide.byte
## local-install: $(BINARY) $(WHYCONFIG) $(JESSIE) bin/whyide.$(OCAMLBEST) byte bin/whyide.byte
## cp $(BINARY) $$HOME/bin/why
## cp $(WHYCONFIG) $$HOME/bin/why
## cp $(JESSIE) $$HOME/bin/jessie
## if test -f bin/why-ide.$(OCAMLBEST); then \
## cp -f bin/why-ide.$(OCAMLBEST) $$HOME/bin/why-ide; \
## if test -f bin/whyide.$(OCAMLBEST); then \
## cp -f bin/whyide.$(OCAMLBEST) $$HOME/bin/whyide; \
## fi
##
## local: install
......@@ -770,7 +704,7 @@ dep: depend
# FTP = $(WWW)/download
# WWWKRAKATOA = /users/www-perso/projets/krakatoa
#
# FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/why-ide.sh \
# FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/whyide.sh \
# mix/*.ml* \
# version.sh Version Makefile.in configure.in configure .depend .depend.coq \
# config/check_ocamlgraph.ml \
......
......@@ -100,7 +100,8 @@ type config = {
loadpath : string list; (* "/usr/local/share/why/theories" *)
timelimit : int option; (* default prover time limit in seconds *)
memlimit : int option; (* default prover memory limit in megabytes *)
provers : config_prover Mstr.t; (* indexed by short identifiers *)
running_provers_max : int option; (* max number of running prover processes *)
provers : config_prover Mstr.t; (* indexed by short identifiers *)
}
let to_string key = function
......@@ -157,11 +158,13 @@ let load_main dirname main al =
let lp = ref [] in
let tl = ref None in
let ml = ref None in
let rp = ref None in
let load (key, value) = match key with
| "library" ->
lp := absolute_filename dirname (to_string key value) :: !lp
| "timelimit" -> set_int key tl value
| "memlimit" -> set_int key ml value
| "running_provers_max" -> set_int key rp value
| _ -> error (UnknownField key)
in
List.iter load al;
......@@ -169,6 +172,7 @@ let load_main dirname main al =
loadpath = List.rev !lp;
timelimit = !tl;
memlimit = !ml;
running_provers_max = !rp;
provers = Mstr.empty }
let read_config conf_file =
......@@ -191,6 +195,7 @@ let read_config conf_file =
loadpath = [];
timelimit = None;
memlimit = None;
running_provers_max = None;
provers = Mstr.empty }
in
let provers = ref Mstr.empty in
......@@ -218,6 +223,7 @@ let save_config config =
List.iter (fprintf fmt "library = \"%s\"@\n") config.loadpath;
Util.option_iter (fprintf fmt "timelimit = %d@\n") config.timelimit;
Util.option_iter (fprintf fmt "memlimit = %d@\n") config.memlimit;
Util.option_iter (fprintf fmt "running_provers_max = %d@\n") config.running_provers_max;
fprintf fmt "@.";
let print_prover name prover =
fprintf fmt "[prover %s]@\n" name;
......
......@@ -32,6 +32,7 @@ type config = {
loadpath : string list; (* "/usr/local/share/why/theories" *)
timelimit : int option; (* default prover time limit in seconds *)
memlimit : int option; (* default prover memory limit in megabytes *)
running_provers_max : int option; (* max number of running prover processes *)
provers : config_prover Mstr.t; (* indexed by short identifiers *)
}
......
......@@ -53,7 +53,9 @@ let timelimit =
(* TODO: put that in config file *)
let window_width = 1024
let window_height = 768
(*
let font_name = "Monospace 10"
*)
let split = ref false
......@@ -230,9 +232,6 @@ module Ide_goals = struct
let view_status_column =
GTree.view_column ~title:"Status"
(*
~renderer:(icon_renderer, ["stock_id", status_column])
*)
~renderer:(image_renderer, ["pixbuf", status_column])
()
......@@ -360,9 +359,6 @@ let iconname_timeout = "clock32"
let iconname_failure = "bug32"
let iconname_yes = "accept32"
let iconname_no = "delete32"
(*
let iconname_down = "play32"
*)
let image_default = ref (image ~size:32 iconname_default)
let image_scheduled = ref !image_default
......@@ -374,9 +370,6 @@ let image_timeout = ref !image_default
let image_failure = ref !image_default
let image_yes = ref !image_default
let image_no = ref !image_default
(*
let image_down = ref !image_default
*)
let resize_images size =
image_default := image ~size iconname_default;
......@@ -389,9 +382,6 @@ let resize_images size =
image_failure := image ~size iconname_failure;
image_yes := image ~size iconname_yes;
image_no := image ~size iconname_no
(*
image_down := image ~size iconname_down
*)
let () = resize_images 16
......@@ -403,11 +393,15 @@ let image_of_result = function
| Scheduler.Unknown -> !image_unknown
| Scheduler.HighFailure -> !image_failure
(*
let count = ref 0
*)
let () =
begin
Scheduler.async := GtkThread.async;
match config.running_provers_max with
| None -> ()
| Some n ->
if n >= 1 then Scheduler.maximum_running_proofs := n
end
let () = Scheduler.async := GtkThread.async
let prover_on_all_goals ~(model:GTree.tree_store) ~(view:GTree.view) p () =
Ident.Hid.iter
......@@ -419,10 +413,6 @@ let prover_on_all_goals ~(model:GTree.tree_store) ~(view:GTree.view) p () =
let prover_row = model#append ~parent:row () in
model#set ~row:prover_row ~column:Ide_goals.name_column ("prover: " ^name);
view#expand_row (model#get_path row);
(*
incr count;
let c = !count in
*)
let callback result time =
(*
printf "Scheduled task #%d: status set to %a@." c
......@@ -556,6 +546,6 @@ let () =
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/gwhy.opt"
compile-command: "unset LANG; make -C ../.. bin/whyide.opt"
End:
*)
......@@ -21,7 +21,12 @@
open Why
val async: ((unit->unit)->unit->unit) ref
(** async f () should call [f ()] *)
(** async f () should call [f ()] asynchronously, in a suitable way
for the current user interface (e.g. GtkThread.async) *)
val maximum_running_proofs: int ref
(** bound on the number of prover processes running in parallel.
default is 2 *)
type proof_attempt_status =
| Scheduled (** external proof attempt is scheduled *)
......
......@@ -266,6 +266,7 @@ let () =
loadpath = [];
timelimit = None;
memlimit = None;
running_provers_max = None;
provers = Mstr.empty }
in
......
[main]
library = "theories"
timelimit = 2
running_provers_max = 2
[prover alt-ergo]
name = "Alt-Ergo"
......
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