Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use a soft time limit for E
authorblanchet
Tue, 24 Aug 2010 15:06:47 +0200
changeset 38691 fe5929dacd43
parent 38690 38a926e033ad
child 38692 89d3550d8e16
use a soft time limit for E with a hard limit, "eproof"/"eproof.pl" doesn't show the proof is there's less than 1 second left, yielding "the ATP output is malformed"
src/HOL/Tools/ATP/atp_systems.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 24 14:36:29 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 24 15:06:47 2010 +0200
@@ -136,7 +136,8 @@
   {exec = ("E_HOME", "eproof"),
    required_execs = [],
    arguments = fn _ => fn timeout =>
-     "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
+     "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \
+     \--soft-cpu-limit=" ^
      string_of_int (to_generous_secs timeout),
    has_incomplete_mode = false,
    proof_delims = [tstp_proof_delims],
isabelle