1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
Description: put internal executables away in /usr/libexec
Author: Julien Puydt
Forwarded: https://github.com/lukaszcz/coqhammer/issues/139
--- coq-hammer.orig/src/plugin/opt.ml
+++ coq-hammer/src/plugin/opt.ml
@@ -128,7 +128,7 @@
in
declare_bool_option gdopt
-let predict_path = ref "predict"
+let predict_path = ref "/usr/libexec/coq-hammer/predict"
let _ =
let gdopt=
--- coq-hammer.orig/src/plugin/provers.ml
+++ coq-hammer/src/plugin/provers.ml
@@ -172,7 +172,7 @@
let tmt = string_of_int !Opt.atp_timelimit in
let tmt2 = string_of_int (!Opt.atp_timelimit + 1) in
let cmd =
- "htimeout " ^ tmt2 ^ " eprover -s --cpu-limit=" ^ tmt ^ " --auto-schedule -R --print-statistics -p --tstp-format \"" ^ infile ^ "\" 2>/dev/null | grep \"file[(]'\\|# SZS\" > \"" ^ outfile ^ "\""
+ "/usr/libexec/coq-hammer/htimeout " ^ tmt2 ^ " eprover -s --cpu-limit=" ^ tmt ^ " --auto-schedule -R --print-statistics -p --tstp-format \"" ^ infile ^ "\" 2>/dev/null | grep \"file[(]'\\|# SZS\" > \"" ^ outfile ^ "\""
in
invoke_prover "eprover" cmd outfile
|
