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

attempt to solve the issue with metis Unknown/Timeout

parent d3dfe8ec
...@@ -216,7 +216,10 @@ exec = "metis" ...@@ -216,7 +216,10 @@ exec = "metis"
version_switch = "-v" version_switch = "-v"
version_regexp = "metis \\([^ \n,]+\\)" version_regexp = "metis \\([^ \n,]+\\)"
version_ok = "2.3" version_ok = "2.3"
command = "%l/why3-cpulimit %T %m -s %e --time-limit %t %f" # %U means 2*timelimit+1. Required because Metis tends to
# react very slowly to the time limit given, hence answers
# oscillate between Timeout and Unknown
command = "%l/why3-cpulimit %U %m -s %e --time-limit %t %f"
driver = "drivers/metis.drv" driver = "drivers/metis.drv"
[ATP metitarski] [ATP metitarski]
......
...@@ -140,13 +140,14 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ...@@ -140,13 +140,14 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
| "f" -> use_stdin := false; fin | "f" -> use_stdin := false; fin
| "t" -> on_timelimit := true; string_of_int timelimit | "t" -> on_timelimit := true; string_of_int timelimit
| "T" -> string_of_int (succ timelimit) | "T" -> string_of_int (succ timelimit)
| "U" -> string_of_int (2 * timelimit + 1)
| "m" -> string_of_int memlimit | "m" -> string_of_int memlimit
(* FIXME: libdir and datadir can be changed in the configuration file (* FIXME: libdir and datadir can be changed in the configuration file
Should we pass them as additional arguments? Or would it be better Should we pass them as additional arguments? Or would it be better
to prepare the command line in a separate function? *) to prepare the command line in a separate function? *)
| "l" -> Config.libdir | "l" -> Config.libdir
| "d" -> Config.datadir | "d" -> Config.datadir
| _ -> failwith "unknown specifier, use %%f, %%t, %%m, %%l, or %%d" | _ -> failwith "unknown specifier, use %%, %f, %t, %T, %U, %m, %l, or %d"
in in
let subst s = let subst s =
try try
......
Supports Markdown
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