Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
use a soft time limit for E
authorblanchet
Tue, 24 Aug 2010 15:06:47 +0200
changeset 38930fe5929dacd43
parent 38929 38a926e033ad
child 38931 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 
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 24 14:36:29 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 24 15:06:47 2010 +0200
     1.3 @@ -136,7 +136,8 @@
     1.4    {exec = ("E_HOME", "eproof"),
     1.5     required_execs = [],
     1.6     arguments = fn _ => fn timeout =>
     1.7 -     "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
     1.8 +     "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \
     1.9 +     \--soft-cpu-limit=" ^
    1.10       string_of_int (to_generous_secs timeout),
    1.11     has_incomplete_mode = false,
    1.12     proof_delims = [tstp_proof_delims],
wneuper/isa