Commit d72aa5b9 authored by MARCHE Claude's avatar MARCHE Claude

compilation

parent e4e484d3
......@@ -257,9 +257,11 @@ $(MNGCMO) $(MNGCMX): src/why.cmi
#byte: bin/manager.byte
#opt: bin/manager.opt
bin/manager.opt bin/manager.byte: INCLUDES = -I +sqlite3
bin/manager.opt: src/why.cmxa $(MNGCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) sqlite3.cma $^
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) sqlite3.cmxa $^
$(STRIP) $@
bin/manager.byte: src/why.cma $(MNGCMO)
......@@ -303,12 +305,15 @@ byte: bin/whyide.byte
opt: bin/whyide.opt
endif
bin/whyide.opt bin/whyide.byte: INCLUDES = -I +lablgtk2 -I +threads
bin/whyide.opt: src/why.cmxa $(IDE_CMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx $^
$(STRIP) $@
bin/whyide.byte: src/why.cma $(IDE_CMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
......
......@@ -438,6 +438,7 @@ let call_prover_on_file ?debug ?timeout drv filename =
Call_provers.on_file ?debug ?timeout drv.drv_prover filename
let call_prover_on_formatter ?debug ?timeout ?filename drv ib =
Call_provers.on_formatter ?debug ?timeout ?filename drv.drv_prover ib
let call_prover_on_buffer ?debug ?timeout ?filename drv ib =
Call_provers.on_buffer ?debug ?timeout ?filename drv.drv_prover ib
......
......@@ -19,7 +19,7 @@ let current () =
let default_busyfn (db:Sqlite3.db) =
let default_busyfn (_db:Sqlite3.db) =
print_endline "WARNING: busy";
(* Thread.delay (Random.float 1.) *)
ignore (Unix.select [] [] [] (Random.float 1.))
......@@ -274,15 +274,15 @@ module Loc = struct
let f () = if !first then (first := false; " WHERE ") else " AND "
in
let q = match id with
| None -> q | Some b -> q ^ (f()) ^ "loc.id=?" in
| None -> q | Some _b -> q ^ (f()) ^ "loc.id=?" in
let q = match file with
| None -> q | Some b -> q ^ (f()) ^ "loc.file=?" in
| None -> q | Some _b -> q ^ (f()) ^ "loc.file=?" in
let q = match line with
| None -> q | Some b -> q ^ (f()) ^ "loc.line=?" in
| None -> q | Some _b -> q ^ (f()) ^ "loc.line=?" in
let q = match start with
| None -> q | Some b -> q ^ (f()) ^ "loc.start=?" in
| None -> q | Some _b -> q ^ (f()) ^ "loc.start=?" in
let q = match stop with
| None -> q | Some b -> q ^ (f()) ^ "loc.stop=?" in
| None -> q | Some _b -> q ^ (f()) ^ "loc.stop=?" in
let q = match custom_where with
| "",_ -> q | w,_ -> q ^ (f()) ^ "(" ^ w ^ ")" in
let sql =
......@@ -717,7 +717,7 @@ module Goal = struct
end
*)
let from_id db id : goal =
let from_id _db _id : goal =
assert false
(*
let sql="SELECT goal.id, goal.task_checksum, goal.parent_id, goal.name, goal.pos_id, goal.proved, goal_pos.id, goal_pos.file, goal_pos.line, goal_pos.start, goal_pos.stop, goal_parent.id, goal_parent.name, goal_parent.obsolete FROM goal LEFT JOIN transf AS goal_parent ON (goal_parent.id = goal.parent_id) LEFT JOIN loc AS goal_pos ON (goal_pos.id = goal.pos_id) " ^ q in
......@@ -1083,15 +1083,15 @@ let root_goals () =
exception AlreadyAttempted
let try_prover ~timelimit:int ?memlimit:int (g : goal) (d: prover_data) : unit =
let try_prover ~timelimit:_int ?memlimit:_int (_g : goal) (_d: prover_data) : unit =
assert false (* TODO *)
let add_transformation (g : goal) (t : transf) : unit =
let add_transformation (_g : goal) (_t : transf) : unit =
assert false (* TODO *)
let add_or_replace_task (name : string) (t : Why.Task.task) : unit =
let add_or_replace_task (_name : string) (_t : Why.Task.task) : unit =
assert false (* TODO *)
let read_db_from_file (file : string) : goal list =
let read_db_from_file (_file : string) : goal list =
assert false (* TODO *)
......@@ -3,8 +3,8 @@ open Format
open Why
let autodetection () =
Whyconf.set_loadpath [Filename.concat Config.datadir "theories"];
(*
Whyconf.set_loadpath [Filename.concat Config.datadir "theories"];
Whyconf.set_driverpath (Filename.concat Config.datadir "drivers");
*)
Whyconf.add_driver_config "Alt-Ergo 0.9" "alt_ergo.drv" "alt-ergo";
......@@ -63,8 +63,8 @@ let rec report fmt = function
fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_short
| Driver.Error e ->
Driver.report fmt e
| Dynlink_compat.Dynlink.Error e ->
fprintf fmt "Dynlink : %s" (Dynlink_compat.Dynlink.error_message e)
| Config.Dynlink.Error e ->
fprintf fmt "Dynlink : %s" (Config.Dynlink.error_message e)
| e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
......@@ -81,7 +81,7 @@ let m : Why.Theory.theory Why.Theory.Mnm.t =
let do_task tname (th : Why.Theory.theory) (task : Why.Task.task) : unit =
let do_task tname (_th : Why.Theory.theory) (task : Why.Task.task) : unit =
(*
if !opt_prove then begin
let res = Driver.call_prover ~debug:!opt_debug ?timeout drv task in
......
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