Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 9e43e390 authored by MARCHE Claude's avatar MARCHE Claude

Compilation and make bench work on moloch

parent 57de2a14
......@@ -1604,9 +1604,6 @@ endif
ALTERGODIR=src/trywhy3/alt-ergo
JSOCAMLCW=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.ppx \
-I src/ide
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o -I src/trywhy3 \
-I $(ALTERGODIR)/src/util \
......@@ -1697,6 +1694,16 @@ clean::
CLEANDIRS += src/trywhy3
#########
# why3webserver and full web/js interface
#########
ifeq (@HASJSOFOCAML,yes)
JSOCAMLCW=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.ppx \
-I src/ide
src/ide/why3_js.cmo: src/ide/why3_js.ml lib/why3/why3.cma
$(JSOCAMLCW) $(BFLAGS) -c $<
......@@ -1709,6 +1716,7 @@ src/ide/why3_js.js: src/ide/why3_js.byte
opt: lib/why3/why3.cma bin/why3webserver.opt src/ide/why3_js.js
byte: lib/why3/why3.cma bin/why3webserver.byte src/ide/why3_js.js
endif
########
# bench
......
......@@ -484,6 +484,18 @@ dnl AC_CHECK_PROG(enable_ide,lablgtk2,yes,no) not always available (Win32)
dnl AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true)
# js_of_ocaml
JSOFOCAML=$(ocamlfind query js_of_ocaml)
if test -z "$JSOFCAML"; then
HASJSOFOCAML=no
reason_jsofocaml=" (js_of_ocaml not found)"
else
HASJSOFOCAML=yes
fi
# Coq
enable_coq_support=yes
......@@ -768,6 +780,8 @@ AC_SUBST(enable_ide)
AC_SUBST(LABLGTK2LIB)
AC_SUBST(LABLGTK2PKG)
AC_SUBST(HASJSOFOCAML)
AC_SUBST(META_OCAMLGRAPH)
AC_SUBST(enable_zarith)
......@@ -858,7 +872,8 @@ echo " Library path : $OCAMLLIB"
echo " Native compilation : $enable_native_code"
echo " Profiling : $enable_profiling"
echo "Components"
echo " IDE command : $enable_ide$reason_ide"
echo " GTK IDE : $enable_ide$reason_ide"
echo " Web IDE : $HASJSOFOCAML$reason_jsofocaml"
echo " GMP arithmetic : $enable_zarith$reason_zarith"
echo " Compressed sessions : $enable_zip$reason_zip"
echo " MenhirLib support : $enable_menhirLib$reason_menhirLib"
......
......@@ -96,7 +96,7 @@ let result1 : Call_provers.prover_result =
Call_provers.wait_on_call
(Driver.prove_task ~limit:Call_provers.empty_limit
~command:alt_ergo.Whyconf.command
alt_ergo_driver None task1)
alt_ergo_driver task1)
(* prints Alt-Ergo answer *)
let () = printf "@[On task 1, alt-ergo answers %a@."
......@@ -106,7 +106,7 @@ let result2 : Call_provers.prover_result =
Call_provers.wait_on_call
(Driver.prove_task ~command:alt_ergo.Whyconf.command
~limit:{Call_provers.empty_limit with Call_provers.limit_time = 10}
alt_ergo_driver None task2)
alt_ergo_driver task2)
let () = printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
Call_provers.print_prover_answer result1.Call_provers.pr_answer
......@@ -146,7 +146,7 @@ let result3 =
Call_provers.wait_on_call
(Driver.prove_task ~limit:Call_provers.empty_limit
~command:alt_ergo.Whyconf.command
alt_ergo_driver None task3)
alt_ergo_driver task3)
let () = printf "@[On task 3, alt-ergo answers %a@."
Call_provers.print_prover_result result3
......@@ -177,7 +177,7 @@ let result4 =
Call_provers.wait_on_call
(Driver.prove_task ~limit:Call_provers.empty_limit
~command:alt_ergo.Whyconf.command
alt_ergo_driver None task4)
alt_ergo_driver task4)
let () = printf "@[On task 4, alt-ergo answers %a@."
Call_provers.print_prover_result result4
......
......@@ -35,7 +35,7 @@ type printer_mapping = {
}
type printer_args = {
name_table : name_tables option;
name_table : names_table option;
env : Env.env;
prelude : prelude;
th_prelude : prelude_map;
......
......@@ -36,7 +36,7 @@ type printer_mapping = {
}
type printer_args = {
name_table : name_tables option;
name_table : names_table option;
env : Env.env;
prelude : prelude;
th_prelude : prelude_map;
......
......@@ -345,7 +345,7 @@ let on_tagged_pr t task =
(* Printing tasks *)
type id_decl = (Decl.decl list) Ident.Mid.t
type name_tables = {
type names_table = {
namespace : namespace;
known_map : known_map;
printer : ident_printer;
......@@ -353,6 +353,13 @@ type name_tables = {
id_decl : id_decl;
}
let empty_names_table = {
namespace = empty_ns;
known_map = Mid.empty;
printer = create_ident_printer [];
id_decl = Mid.empty;
}
exception Bad_name_table of string
(* Exception reporting *)
......@@ -367,7 +374,7 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
| NotExclusiveMeta m ->
Format.fprintf fmt "Metaproperty '%s' is not exclusive" m.meta_name
| Bad_name_table s ->
Format.fprintf fmt "Name table associated to task was not generated in %s" s
Format.fprintf fmt "Names table associated to task was not generated in %s" s
| _ -> raise exn)
(* task1 : prefix
......
......@@ -129,14 +129,16 @@ val on_tagged_pr : meta -> task -> Spr.t
(** Printing tasks *)
type id_decl = (Decl.decl list) Ident.Mid.t
type name_tables = {
type names_table = {
namespace : namespace;
known_map : known_map;
printer : ident_printer;
(* Associate an id to a list of declarations in which it is used *)
(* Associate an id to a list of declarations in which it is used *)
id_decl : id_decl;
}
val empty_names_table : names_table
(** Exceptions *)
exception Bad_name_table of string
......
......@@ -335,8 +335,8 @@ let list_transforms_l () =
(** transformations with arguments *)
type trans_with_args = string list -> Env.env -> Task.name_tables -> task trans
type trans_with_args_l = string list -> Env.env -> Task.name_tables -> task tlist
type trans_with_args = string list -> Env.env -> Task.names_table -> task trans
type trans_with_args_l = string list -> Env.env -> Task.names_table -> task tlist
let transforms_with_args = Hstr.create 17
let transforms_with_args_l = Hstr.create 17
......
......@@ -164,8 +164,8 @@ val named : string -> 'a trans -> 'a trans
*)
type trans_with_args = string list -> Env.env -> Task.name_tables -> task trans
type trans_with_args_l = string list -> Env.env -> Task.name_tables -> task tlist
type trans_with_args = string list -> Env.env -> Task.names_table -> task trans
type trans_with_args_l = string list -> Env.env -> Task.names_table -> task tlist
val list_transforms_with_args : unit -> (string * Pp.formatted) list
val list_transforms_with_args_l : unit -> (string * Pp.formatted) list
......@@ -188,5 +188,5 @@ val list_trans : unit -> string list
val apply_transform : string -> Env.env -> task -> task list
(** apply a registered 1-to-1 or a 1-to-n, directly.*)
val apply_transform_args : string -> Env.env -> string list -> Task.name_tables -> task -> task list
val apply_transform_args : string -> Env.env -> string list -> Task.names_table -> task -> task list
(** apply a registered 1-to-1 or a 1-to-n or a trans with args, directly *)
......@@ -46,12 +46,12 @@ val call_on_buffer :
val print_task :
?old : in_channel ->
?cntexample : bool ->
?name_table: Task.name_tables ->
?name_table: Task.names_table ->
driver -> Format.formatter -> Task.task -> unit
val print_theory :
?old : in_channel ->
?name_table: Task.name_tables ->
?name_table: Task.names_table ->
driver -> Format.formatter -> Theory.theory -> unit
(** produce a realization of the given theory using the given driver *)
......@@ -61,7 +61,7 @@ val prove_task :
?cntexample : bool ->
?old : string ->
?inplace : bool ->
?name_table : Task.name_tables ->
?name_table : Task.names_table ->
driver -> Task.task -> Call_provers.prover_call
(** Split the previous function in two simpler functions *)
......@@ -69,7 +69,7 @@ val prepare_task : cntexample:bool -> driver -> Task.task -> Task.task
val print_task_prepared :
?old : in_channel ->
?name_table: Task.name_tables ->
?name_table: Task.names_table ->
driver -> Format.formatter -> Task.task -> Printer.printer_mapping
val prove_task_prepared :
......@@ -77,7 +77,7 @@ val prove_task_prepared :
limit : Call_provers.resource_limit ->
?old : string ->
?inplace : bool ->
?name_table : Task.name_tables ->
?name_table : Task.names_table ->
driver -> Task.task -> Call_provers.prover_call
......
......@@ -435,8 +435,8 @@ let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] IST STRENG VERBOTEN *)
(* forget_all (); *)
let tables = match args.name_table with
| None -> raise (Bad_name_table "why3printer")
| Some tables -> tables in
| None -> empty_names_table (* raise (Bad_name_table "Why3printer.print_task")*)
| Some tables -> tables in
print_prelude fmt args.prelude;
fprintf fmt "theory Task@\n";
print_th_prelude task fmt args.th_prelude;
......@@ -462,8 +462,8 @@ let print_sequent args ?old:_ fmt task =
info := {info_syn = Discriminate.get_syntax_map task;
itp = true};
let tables = match args.name_table with
| None -> raise (Bad_name_table "why3printer")
| Some tables -> tables in
| None -> empty_names_table (* raise (Bad_name_table "Why3printer.print_sequent") *)
| Some tables -> tables in
(* let tables = build_name_tables task in *)
let ut = Task.used_symbols (Task.used_theories task) in
let ld = Task.local_decls task ut in
......
......@@ -30,12 +30,12 @@
*)
val print_ls : Task.name_tables -> Format.formatter -> Term.lsymbol -> unit
val print_tv : Task.name_tables -> Format.formatter -> Ty.tvsymbol -> unit
val print_ts : Task.name_tables -> Format.formatter -> Ty.tysymbol -> unit
val print_forget_vsty : Task.name_tables -> Format.formatter -> Term.vsymbol -> unit
val print_pr : Task.name_tables -> Format.formatter -> Decl.prsymbol -> unit
val print_pat : Task.name_tables -> Format.formatter -> Term.pattern -> unit
val print_ty : Task.name_tables -> Format.formatter -> Ty.ty -> unit
val print_term : Task.name_tables -> Format.formatter -> Term.term -> unit
val print_decl : Task.name_tables -> Format.formatter -> Decl.decl -> unit
val print_ls : Task.names_table -> Format.formatter -> Term.lsymbol -> unit
val print_tv : Task.names_table -> Format.formatter -> Ty.tvsymbol -> unit
val print_ts : Task.names_table -> Format.formatter -> Ty.tysymbol -> unit
val print_forget_vsty : Task.names_table -> Format.formatter -> Term.vsymbol -> unit
val print_pr : Task.names_table -> Format.formatter -> Decl.prsymbol -> unit
val print_pat : Task.names_table -> Format.formatter -> Term.pattern -> unit
val print_ty : Task.names_table -> Format.formatter -> Ty.ty -> unit
val print_term : Task.names_table -> Format.formatter -> Term.term -> unit
val print_decl : Task.names_table -> Format.formatter -> Decl.decl -> unit
......@@ -467,10 +467,10 @@ let build_prover_call c id pr limit callback =
config_pr
~with_steps:Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
let task = Session_itp.get_task c.controller_session id in
let tables = Session_itp.get_tables c.controller_session id in
let table = Session_itp.get_table c.controller_session id in
let call =
Driver.prove_task ?old:None ~cntexample:true ~inplace:false ~command
~limit ?name_table:tables driver task
~limit ?name_table:table driver task
in
let pa = (c.controller_session,id,pr,callback,false,call) in
Queue.push pa prover_tasks_in_progress
......@@ -571,13 +571,13 @@ let schedule_proof_attempt c id pr ~limit ~callback ~notification =
let schedule_transformation_r c id name args ~callback =
let apply_trans () =
let task = get_task c.controller_session id in
let tables = match get_tables c.controller_session id with
| None -> raise (Task.Bad_name_table "schedule_transformation")
| Some tables -> tables in
let table = match get_table c.controller_session id with
| None -> raise (Task.Bad_name_table "Controller_itp.schedule_transformation_r")
| Some table -> table in
begin
try
let subtasks =
Trans.apply_transform_args name c.controller_env args tables task in
Trans.apply_transform_args name c.controller_env args table task in
(* if result is same as input task, consider it as a failure *)
begin
match subtasks with
......
......@@ -68,49 +68,49 @@ let loaded_strategies = ref []
(****** Exception handling *********)
let print_term s id fmt t =
let tables = match (Session_itp.get_tables s id) with
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_term tables fmt t
let print_type s id fmt t =
let tables = match (Session_itp.get_tables s id) with
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_ty tables fmt t
let print_ts s id fmt t =
let tables = match (Session_itp.get_tables s id) with
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_ts tables fmt t
let print_ls s id fmt t =
let tables = match (Session_itp.get_tables s id) with
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_ls tables fmt t
let print_tv s id fmt t =
let tables = match (Session_itp.get_tables s id) with
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_tv tables fmt t
let print_vsty s id fmt t =
let tables = match (Session_itp.get_tables s id) with
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_forget_vsty tables fmt t
let print_pr s id fmt t =
let tables = match (Session_itp.get_tables s id) with
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_pr tables fmt t
let print_pat s id fmt t =
let tables = match (Session_itp.get_tables s id) with
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_pat tables fmt t
......@@ -798,7 +798,7 @@ let get_locations t =
(* -- send the task -- *)
let task_of_id d id =
let task = get_task d.cont.controller_session id in
let tables = get_tables d.cont.controller_session id in
let tables = get_table d.cont.controller_session id in
(* This function also send source locations associated to the task *)
let loc_color_list = get_locations task in
Pp.string_of
......
......@@ -137,7 +137,7 @@ let search_id _cont task args =
type query =
| Qnotask of (Controller_itp.controller -> string list -> string)
| Qtask of (Controller_itp.controller -> Task.name_tables -> string list -> string)
| Qtask of (Controller_itp.controller -> Task.names_table -> string list -> string)
let help_on_queries fmt commands =
let l = Stdlib.Hstr.fold (fun c (h,_) acc -> (c,h)::acc) commands [] in
......@@ -294,10 +294,10 @@ let interp commands_table config cont id s =
| Qnotask f, _ -> Query (f cont args)
| Qtask _, None -> QError "please select a goal first"
| Qtask f, Some id ->
let tables = match Session_itp.get_tables cont.Controller_itp.controller_session id with
| None -> raise (Task.Bad_name_table "interp")
| Some tables -> tables in
let s = try Query (f cont tables args) with
let table = match Session_itp.get_table cont.Controller_itp.controller_session id with
| None -> raise (Task.Bad_name_table "Server_utils.interp")
| Some table -> table in
let s = try Query (f cont table args) with
| Undefined_id s -> QError ("No existing id corresponding to " ^ s)
| Number_of_arguments -> QError "Bad number of arguments"
in s
......
......@@ -17,11 +17,11 @@ exception Number_of_arguments
type query =
| Qnotask of (Controller_itp.controller -> string list -> string)
| Qtask of (Controller_itp.controller -> Task.name_tables -> string list -> string)
| Qtask of (Controller_itp.controller -> Task.names_table -> string list -> string)
val print_id: 'a -> Task.name_tables -> string list -> string
val search_id: 'a -> Task.name_tables -> string list -> string
val print_id: 'a -> Task.names_table -> string list -> string
val search_id: 'a -> Task.names_table -> string list -> string
val list_provers: Controller_itp.controller -> _ -> string
val list_transforms: unit -> (string * Pp.formatted) list
......
......@@ -42,7 +42,7 @@ type proof_attempt_node = {
type proof_node = {
proofn_name : Ident.ident;
proofn_task : Task.task;
proofn_table : Task.name_tables option;
proofn_table : Task.names_table option;
proofn_parent : proof_parent;
proofn_checksum : Termcode.checksum option;
proofn_shape : Termcode.shape;
......@@ -207,7 +207,7 @@ let get_task (s:session) (id:proofNodeID) =
let node = get_proofNode s id in
node.proofn_task
let get_tables (s: session) (id: proofNodeID) =
let get_table (s: session) (id: proofNodeID) =
let node = get_proofNode s id in
node.proofn_table
......@@ -1157,7 +1157,7 @@ let add_registered_transformation s env old_tr goal_id =
Debug.dprintf debug "[merge_theory] trans not found@.";
let task = goal.proofn_task in
let tables = match goal.proofn_table with
| None -> raise (Task.Bad_name_table "add_registered_transformation")
| None -> raise (Task.Bad_name_table "Session_itp.add_registered_transformation")
| Some tables -> tables in
let subgoals = Trans.apply_transform_args old_tr.transf_name env old_tr.transf_args tables task in
graft_transf s goal_id old_tr.transf_name old_tr.transf_args subgoals
......
......@@ -73,7 +73,7 @@ val is_below: session -> any -> any -> bool
type proof_parent = Trans of transID | Theory of theory
val get_task : session -> proofNodeID -> Task.task
val get_tables: session -> proofNodeID -> Task.name_tables option
val get_table : session -> proofNodeID -> Task.names_table option
val get_transformations : session -> proofNodeID -> transID list
val get_proof_attempt_ids :
......
......@@ -50,7 +50,7 @@ type symb =
| Pr of prsymbol
(* [add_unsafe s id tables] Add (s, id) to tables without any checking. *)
let add_unsafe (s: string) (id: symb) (tables: name_tables) : name_tables =
let add_unsafe (s: string) (id: symb) (tables: names_table) : names_table =
match id with
| Ts ty ->
{tables with
......@@ -66,7 +66,7 @@ let add_unsafe (s: string) (id: symb) (tables: name_tables) : name_tables =
}
(* Adds symbols that are introduced to a constructor *)
let constructor_add (cl: constructor list) tables : name_tables =
let constructor_add (cl: constructor list) tables : names_table =
List.fold_left
(fun tables ((ls, cl): constructor) ->
let tables = List.fold_left
......@@ -139,7 +139,7 @@ let rec add_id tables d t =
(* [add d printer tables] Adds all new declaration of symbol inside d to tables.
It uses printer to give them a unique name and also register these new names in printer *)
let add (d: decl) (tables: name_tables): name_tables =
let add (d: decl) (tables: names_table): names_table =
match d.d_node with
| Dtype ty ->
(* only current symbol is new in the declaration (see create_ty_decl) *)
......@@ -188,7 +188,7 @@ let add (d: decl) (tables: name_tables): name_tables =
let tables = add_unsafe s (Pr pr) tables in
add_id tables d t
let build_name_tables task : name_tables =
let build_name_tables task : names_table =
let pr = fresh_printer () in
let km = Task.task_known task in
let empty_decls = Ident.Mid.empty in
......@@ -339,7 +339,7 @@ let rec print_type : type a b. (a, b) trans_typ -> string =
| Topt (s,t) -> "opt [" ^ s ^ "] " ^ print_type t
| Toptbool (s,t) -> "opt [" ^ s ^ "] -> " ^ print_type t
let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> name_tables -> task -> b =
let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> names_table -> task -> b =
fun t f l env tables task ->
match t, l with
| Ttrans, _-> apply f task
......@@ -410,7 +410,7 @@ let wrap_l : type a. (a, task list) trans_typ -> a -> trans_with_args_l =
let wrap : type a. (a, task) trans_typ -> a -> trans_with_args =
fun t f l env tables -> Trans.store (wrap_to_store t f l env tables)
let wrap_any : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> Task.name_tables -> b trans =
let wrap_any : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> Task.names_table -> b trans =
fun t f l env tables -> Trans.store (wrap_to_store t f l env tables)
let wrap_and_register : type a b. desc:Pp.formatted -> string -> (a, b) trans_typ -> a -> unit =
......
......@@ -11,7 +11,7 @@ exception Arg_hyp_not_found of string
(** Pre-processing of tasks, to build unique names for all declared
identifiers of a task.*)
val build_name_tables : Task.task -> Task.name_tables
val build_name_tables : Task.task -> Task.names_table
type (_, _) trans_typ =
| Ttrans : (task Trans.trans, task) trans_typ
......
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