Commit ba0f7e79 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

filenames

parent f0df9560
......@@ -80,9 +80,10 @@ driver = "drivers/tptp.drv"
[ATP verit]
name = "veriT"
exec = "veriT"
exec = "verit"
version_switch = "--proof-format-and-exit"
version_regexp = "verit \\([^ \n\r]+\\) -"
version_switch = "--help"
version_regexp = "Version: \\([^ \n\r]+\\)"
command = "why3-cpulimit %t %m %e %f 2>&1"
driver = "drivers/verit.drv"
......
......@@ -66,7 +66,7 @@ let () =
let conf_file_doesnt_exist = not (Sys.file_exists conf_file) in
if conf_file_doesnt_exist then
printf "Config file %s doesn't exist, \
so autodection is automatically triggered@." conf_file;
so autodetection is automatically triggered@." conf_file;
let config =
if !auto || conf_file_doesnt_exist
then Autodetection.run_auto_detection config
......
......@@ -114,7 +114,7 @@ let detect_prover main acc data =
(fun acc com ->
let out = Filename.temp_file "out" "" in
let cmd = sprintf "%s %s" com data.version_switch in
let c = sprintf "(%s) > %s" cmd out in
let c = sprintf "(%s) > %s 2>&1" cmd out in
eprintf "Run : %s@." c;
let ret = Sys.command c in
if ret <> 0 then
......@@ -126,12 +126,10 @@ let detect_prover main acc data =
let s =
try
let ch = open_in out in
Sysutil.channel_contents ch
(* let s = ref (input_line ch) in *)
(* while !s = "" do s := input_line ch done; *)
(* close_in ch; *)
(* Sys.remove out; *)
(* !s *)
let c = Sysutil.channel_contents ch in
close_in ch;
Sys.remove out;
c
with Not_found | End_of_file -> ""
in
let re = Str.regexp data.version_regexp in
......
......@@ -1588,6 +1588,8 @@ let edit_selected_row p =
let file = Driver.file_of_task driver
(Filename.concat project_dir fn) tn t
in
(* TODO: ne pas le changer mais le retuiliser
s'il existe deja! en principe peut venir de la base de donnees *)
a.Model.edited_as <- file;
let old_status = a.Model.status in
Helpers.set_proof_status ~obsolete:false a Scheduler.Running 0.0;
......
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