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 fa238e35 authored by MARCHE Claude's avatar MARCHE Claude

In case of syntax/type errors at start-up, show the file and error

parent 78faa9df
......@@ -5,135 +5,135 @@
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="1" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../isqrt.mlw" expanded="true">
<theory name="Square" sum="266e4aaa701863bb290853e7ea871e14" expanded="true">
<goal name="sqr_non_neg" expl="">
<file name="../isqrt.mlw" proved="true">
<theory name="Square" proved="true" sum="266e4aaa701863bb290853e7ea871e14">
<goal name="sqr_non_neg" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="sqr_increasing" expl="">
<goal name="sqr_increasing" proved="true">
<proof prover="1" timelimit="5" memlimit="4000"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="sqr_sum" expl="">
<goal name="sqr_sum" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
</theory>
<theory name="Simple" sum="3299c34521b97079c507d438bc082f60" expanded="true">
<goal name="WP_parameter isqrt" expl="VC for isqrt">
<transf name="split_goal_wp">
<goal name="WP_parameter isqrt.1" expl="loop invariant init">
<theory name="Simple" proved="true" sum="9253a56173520e899153b3f344520525">
<goal name="WP_parameter isqrt" expl="VC for isqrt" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter isqrt.0" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt.2" expl="loop invariant init">
<goal name="WP_parameter isqrt.1" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt.3" expl="loop invariant init">
<goal name="WP_parameter isqrt.2" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt.4" expl="loop invariant preservation">
<goal name="WP_parameter isqrt.3" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt.5" expl="loop invariant preservation">
<goal name="WP_parameter isqrt.4" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt.6" expl="loop invariant preservation">
<goal name="WP_parameter isqrt.5" expl="loop invariant preservation" proved="true">
<proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.00" steps="15"/></proof>
</goal>
<goal name="WP_parameter isqrt.7" expl="loop variant decrease">
<goal name="WP_parameter isqrt.6" expl="loop variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="WP_parameter isqrt.8" expl="postcondition">
<goal name="WP_parameter isqrt.7" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter main" expl="VC for main">
<goal name="WP_parameter main" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
</theory>
<theory name="NewtonMethod" sum="b7e1ed0d2b8beabaab444b31c5339896" expanded="true">
<goal name="WP_parameter sqrt" expl="VC for sqrt" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter sqrt.1" expl="postcondition">
<theory name="NewtonMethod" proved="true" sum="b3c07fdcf48d4ec7b7eec7ecc14c2ff2">
<goal name="WP_parameter sqrt" expl="VC for sqrt" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter sqrt.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="WP_parameter sqrt.2" expl="postcondition">
<goal name="WP_parameter sqrt.1" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="WP_parameter sqrt.3" expl="loop invariant init">
<goal name="WP_parameter sqrt.2" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter sqrt.4" expl="loop invariant init">
<goal name="WP_parameter sqrt.3" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="WP_parameter sqrt.5" expl="loop invariant init">
<goal name="WP_parameter sqrt.4" expl="loop invariant init" proved="true">
<proof prover="1" timelimit="5" memlimit="4000"><result status="valid" time="1.21"/></proof>
</goal>
<goal name="WP_parameter sqrt.6" expl="loop invariant init">
<goal name="WP_parameter sqrt.5" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter sqrt.7" expl="loop invariant init">
<goal name="WP_parameter sqrt.6" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="12"/></proof>
</goal>
<goal name="WP_parameter sqrt.8" expl="assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter sqrt.8.1" expl="VC for sqrt">
<goal name="WP_parameter sqrt.7" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter sqrt.7.0" expl="VC for sqrt" proved="true">
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.2" expl="VC for sqrt">
<goal name="WP_parameter sqrt.7.1" expl="VC for sqrt" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.3" expl="VC for sqrt">
<goal name="WP_parameter sqrt.7.2" expl="VC for sqrt" proved="true">
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.4" expl="VC for sqrt">
<goal name="WP_parameter sqrt.7.3" expl="VC for sqrt" proved="true">
<proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.5" expl="VC for sqrt">
<goal name="WP_parameter sqrt.7.4" expl="VC for sqrt" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.6" expl="VC for sqrt">
<goal name="WP_parameter sqrt.7.5" expl="VC for sqrt" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.7" expl="VC for sqrt">
<goal name="WP_parameter sqrt.7.6" expl="VC for sqrt" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.8" expl="VC for sqrt">
<goal name="WP_parameter sqrt.7.7" expl="VC for sqrt" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.9" expl="VC for sqrt">
<goal name="WP_parameter sqrt.7.8" expl="VC for sqrt" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sqrt.9" expl="loop invariant preservation">
<goal name="WP_parameter sqrt.8" expl="loop invariant preservation" proved="true">
<proof prover="7"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter sqrt.10" expl="loop invariant preservation">
<goal name="WP_parameter sqrt.9" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sqrt.11" expl="loop invariant preservation">
<goal name="WP_parameter sqrt.10" expl="loop invariant preservation" proved="true">
<proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter sqrt.12" expl="loop invariant preservation">
<goal name="WP_parameter sqrt.11" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sqrt.13" expl="loop invariant preservation">
<goal name="WP_parameter sqrt.12" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sqrt.14" expl="loop variant decrease">
<goal name="WP_parameter sqrt.13" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sqrt.15" expl="assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter sqrt.15.1" expl="VC for sqrt">
<goal name="WP_parameter sqrt.14" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter sqrt.14.0" expl="VC for sqrt" proved="true">
<proof prover="7" timelimit="5" memlimit="4000"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sqrt.15.2" expl="VC for sqrt">
<goal name="WP_parameter sqrt.14.1" expl="VC for sqrt" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sqrt.16" expl="postcondition">
<goal name="WP_parameter sqrt.15" expl="postcondition" proved="true">
<proof prover="1" timelimit="5" memlimit="4000"><result status="valid" time="0.01"/></proof>
<proof prover="7" timelimit="5" memlimit="4000"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -1105,10 +1105,13 @@ let scroll_to_loc ~force_tab_switch loc_of_goal =
try
let (n, v, _, _) = get_source_view_table f in
if force_tab_switch then
(Debug.dprintf debug "tab switch to page %d@." n;
notebook#goto_page n);
begin
Debug.dprintf debug "tab switch to page %d@." n;
notebook#goto_page n;
end;
move_to_line ~yalign:0.0 v l
with Nosourceview _ -> ()
with Nosourceview _ ->
Debug.dprintf debug "scroll_to_loc: no source know for file %s@." f
(* Erase the colors and apply the colors given by l (which come from the task)
to appropriate source files *)
......@@ -1457,7 +1460,7 @@ let treat_message_notification msg = match msg with
(* TODO find a new color *)
scroll_to_loc ~force_tab_switch:true (Some (loc,0));
color_loc ~color:Goal_color loc;
print_message ~kind:1 ~mark:"Parse_Or_Type_Error]" "%s" s
print_message ~kind:1 ~mark:"Parse_Or_Type_Error" "%s" s
end
| File_Saved f ->
begin
......
......@@ -634,33 +634,25 @@ end
let f = Sysutil.relativize_filename (Session_itp.get_dir s) f in
Loc.user_position f l b e
(* Reload_files that is used even if the controller is not correct. It can
be incorrect and end up in a correct state. *)
let reload_files cont ~use_shapes =
try let _ = reload_files cont ~use_shapes in true with
let capture_parse_or_type_errors f cont =
try let _ = f cont in None with
| Loc.Located (loc, e) ->
let loc = relativize_location cont.controller_session loc in
let s = Format.asprintf "%a at %a@."
Exn_printer.exn_printer e Loc.report_position loc in
P.notify (Message (Parse_Or_Type_Error (loc, s)));
false
Some (loc, s)
| e ->
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
P.notify (Message (Parse_Or_Type_Error (Loc.dummy_position, s)));
false
Some (Loc.dummy_position, s)
(* Reload_files that is used even if the controller is not correct. It can
be incorrect and end up in a correct state. *)
let reload_files cont ~use_shapes =
capture_parse_or_type_errors (reload_files ~use_shapes) cont
let add_file cont ?format fname =
try add_file cont ?format fname; true with
| Loc.Located (loc, e) ->
let loc = relativize_location cont.controller_session loc in
let s = Format.asprintf "%a at %a@."
Exn_printer.exn_printer e Loc.report_position loc in
P.notify (Message (Parse_Or_Type_Error (loc, s)));
false
| e ->
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
P.notify (Message (Parse_Or_Type_Error (Loc.dummy_position, s)));
false
capture_parse_or_type_errors (fun c -> add_file c ?format fname) cont
(* ----------------------------------- ------------------------------------- *)
......@@ -932,11 +924,14 @@ end
| None ->
if (Sys.file_exists f) then
begin
let b = add_file cont f in
if b then
let file = get_file cont.controller_session fn in
send_new_subtree_from_file file;
read_and_send (file_name file)
match add_file cont f with
| None ->
let file = get_file cont.controller_session fn in
send_new_subtree_from_file file;
read_and_send (file_name file)
| Some(loc,s) ->
read_and_send fn;
P.notify (Message (Parse_Or_Type_Error(loc,s)))
end
else
P.notify (Message (Open_File_Error ("File not found: " ^ f)))
......@@ -989,15 +984,15 @@ end
P.notify (Initialized infos);
load_files_session ();
Debug.dprintf debug "reloading source files@.";
let b = reload_files d.cont ~use_shapes in
if b then
begin
(* Send the tree *)
reset_and_send_the_whole_tree ();
(* After initial sending, we don't check anymore that there is a need to
let x = reload_files d.cont ~use_shapes in
reset_and_send_the_whole_tree ();
(* After initial sending, we don't check anymore that there is a need to
focus on a specific node. *)
get_focused_label := None
end
get_focused_label := None;
match x with
| None -> ()
| Some(loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,s)))
(* ----------------- Schedule proof attempt -------------------- *)
......@@ -1205,12 +1200,12 @@ end
let _old_focus = !focused_node in
unfocus ();
clear_tables ();
let b = reload_files d.cont ~use_shapes:true in
if b then
begin
match reload_files d.cont ~use_shapes:true with
| None ->
(* TODO: try to restore the previous focus : focused_node := old_focus; *)
reset_and_send_the_whole_tree ()
end
reset_and_send_the_whole_tree ()
| Some(loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,s)))
let replay_session () : unit =
let d = get_server_data () 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