Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 4a6dca53 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

restore a working web interface

parent e774556b
......@@ -20,7 +20,7 @@ let log s = ignore (Firebug.console ## log (Js.string s))
let get_opt o = Js.Opt.get o (fun () -> assert false)
let check_def s o =
Js.Optdef.get o (fun () -> log ("Object " ^ s ^ " is undefined or null");
Js.Optdef.get o (fun () -> log ("ERROR in check_def(): object " ^ s ^ " is undefined or null");
assert false)
let get_global ident =
......@@ -61,7 +61,7 @@ let getElement cast id =
getElement_exn cast id
with
Not_found ->
log ("Element " ^ id ^ " does not exist or has invalid type");
log ("ERROR in getElement(): element " ^ id ^ " does not exist or has invalid type");
assert false
(**********)
......@@ -82,7 +82,8 @@ module PE = struct
let log_print_msg = print "why3-msg"
let error_print_msg s =
error_container ##. innerHTML := Js.string s
error_container ##. innerHTML := Js.string s;
log_print_msg s
(* TODO remove this *)
let printAnswer s = log_print_msg s
......@@ -341,9 +342,9 @@ let sendRequest r =
let onreadystatechange () =
if xhr ##. readyState == XmlHttpRequest.DONE then
if xhr ##. status == 200 then
PE.printAnswer (readBody xhr)
PE.printAnswer ("Http request '" ^ r ^ "' returned " ^ readBody xhr)
else
PE.printAnswer ("Erreur " ^ string_of_int (xhr ##. status)) in
PE.printAnswer ("Http request '" ^ r ^ "' failed with status " ^ string_of_int (xhr ##. status)) in
xhr ## overrideMimeType (Js.string "text/json");
let _ = xhr ## _open (Js.string "GET")
(Js.string ("http://localhost:6789/request?"^r)) Js._true in
......@@ -626,10 +627,15 @@ let getNotification2 () =
if xhr ##. status == 200 then
let r = readBody xhr in
let nl =
try Json_util.parse_list_notification r with e ->
log (Printexc.to_string e ^ " " ^ r); [] in
try Json_util.parse_list_notification r
with e ->
log ("ERROR in getNotification2: Json_util.parse_list_notification raised " ^ Printexc.to_string e ^
" on the following notification: " ^ r); []
in
(* TODO: make a nicer log *)
if nl != [] then
PE.printAnswer ("r = |" ^ r ^ "|");
(**)
interpNotifications nl
else
()
......
......@@ -44,14 +44,14 @@ let convert_infos (i: global_information) =
let convert_prover_answer (pa: prover_answer) =
match pa with
| Valid -> String "Valid"
| Invalid -> String "Invalid"
| Timeout -> String "Timeout"
| OutOfMemory -> String "OutOfMemory"
| StepLimitExceeded -> String "StepLimitExceeded"
| Unknown _ -> String "Unknown"
| Failure _ -> String "Failure"
| HighFailure -> String "HighFailure"
| Valid -> "Valid",""
| Invalid -> "Invalid",""
| Timeout -> "Timeout",""
| OutOfMemory -> "OutOfMemory",""
| StepLimitExceeded -> "StepLimitExceeded",""
| Unknown(s,_) -> "Unknown",s
| Failure s -> "Failure",s
| HighFailure -> "HighFailure",""
let convert_limit (l: Call_provers.resource_limit) =
Record (convert_record
......@@ -70,13 +70,16 @@ let convert_model (m: Model_parser.model) =
(* TODO pr_model should have a different format *)
let convert_proof_result (pr: prover_result) =
Record (convert_record
["pr_answer", convert_prover_answer pr.pr_answer;
"pr_status", convert_unix_process pr.pr_status;
"pr_output", String pr.pr_output;
"pr_time", Float pr.pr_time;
"pr_steps", Int pr.pr_steps;
"pr_model", convert_model pr.pr_model])
let (a,s) = convert_prover_answer pr.pr_answer in
Record
(convert_record
["pr_answer", String a;
"pr_answer_arg", String s;
"pr_status", convert_unix_process pr.pr_status;
"pr_output", String pr.pr_output;
"pr_time", Float pr.pr_time;
"pr_steps", Int pr.pr_steps;
"pr_model", convert_model pr.pr_model])
let convert_proof_attempt (pas: proof_attempt_status) =
Record (match pas with
......@@ -482,47 +485,65 @@ let parse_node_type_from_json j =
| String "NProofAttempt" -> NProofAttempt
| _ -> raise NotNodeType
exception NotProverAnswer
let parse_prover_answer j =
match j with
| String "Valid" -> Valid
| String "Invalid" -> Invalid
| String "Timeout" -> Timeout
| String "OutOfMemory" -> OutOfMemory
| String "StepLimitExceeded" -> StepLimitExceeded
| String "Unknown" -> raise NotProverAnswer (* TODO *)
| String "Failure" -> raise NotProverAnswer (* TODO *)
| String "HighFailure" -> HighFailure
| _ -> raise NotProverAnswer
exception NotUnixProcess
let parse_unix_process j =
let parse_prover_answer a d =
match a with
| "Valid" -> Valid
| "Invalid" -> Invalid
| "Timeout" -> Timeout
| "OutOfMemory" -> OutOfMemory
| "StepLimitExceeded" -> StepLimitExceeded
| "Unknown" -> Unknown (d,None)
| "Failure" -> Failure d
| "HighFailure" -> HighFailure
| _ -> HighFailure
let parse_unix_process j arg =
match j with
| String "WEXITED" -> Unix.WEXITED 0 (* TODO dummy value *)
| String "WSIGNALED" -> Unix.WSIGNALED 0 (* TODO dummy value *)
| String "WSTOPPED" -> Unix.WSTOPPED 0 (* TODO dummy value *)
| _ -> raise NotUnixProcess
exception NotProverResult
| "WEXITED" -> Unix.WEXITED arg (* TODO dummy value *)
| "WSIGNALED" -> Unix.WSIGNALED arg (* TODO dummy value *)
| "WSTOPPED" -> Unix.WSTOPPED arg (* TODO dummy value *)
| _ -> Unix.WSIGNALED (-1) (* default, should never happen *)
let parse_prover_result j =
try
let pr_answer = get_field j "pr_answer" in
let pr_status_unix = get_field j "pr_status" in
let pr_output = get_string (get_field j "pr_output") in
let pr_time = get_float (get_field j "pr_time") in
let pr_steps = get_int (get_field j "pr_steps") in
let pr_model = get_string (get_field j "pr_model") in
{pr_answer = parse_prover_answer pr_answer;
pr_status = parse_unix_process pr_status_unix;
pr_output = pr_output;
pr_time = pr_time;
pr_steps = pr_steps;
pr_model = Obj.magic pr_model} (* TODO pr_model is a string, should be model *)
with
| _ -> raise NotProverResult
let pr_answer =
let arg =
try get_string (get_field j "pr_answer_arg")
with Not_found -> ""
in
try parse_prover_answer (get_string (get_field j "pr_answer")) arg
with Not_found -> HighFailure
in
let pr_status_unix =
let arg =
try get_int (get_field j "pr_status_arg")
with Not_found -> (-1)
in
try parse_unix_process (get_string (get_field j "pr_status")) arg
with Not_found -> Unix.WSIGNALED (-1)
in
let pr_output =
try get_string (get_field j "pr_output")
with Not_found -> ""
in
let pr_time =
try get_float (get_field j "pr_time")
with Not_found -> -1.0
in
let pr_steps =
try get_int (get_field j "pr_steps")
with Not_found -> -1
in
let _pr_model =
try get_string (get_field j "pr_model")
with Not_found -> ""
in
{ pr_answer = pr_answer;
pr_status = pr_status_unix;
pr_output = pr_output;
pr_time = pr_time;
pr_steps = pr_steps;
pr_model = Model_parser.default_model (* pr_model *)}
(* TODO pr_model is a string, should be model *)
exception NotProofAttempt
......
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