77 reconstruct: proof_data -> thm } |
77 reconstruct: proof_data -> thm } |
78 |
78 |
79 |
79 |
80 (* SMT options *) |
80 (* SMT options *) |
81 |
81 |
82 val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" 30 |
82 val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30) |
83 |
83 |
84 fun with_timeout ctxt f x = |
84 fun with_timeout ctxt f x = |
85 TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x |
85 TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x |
86 handle TimeLimit.TimeOut => raise SMT "timeout" |
86 handle TimeLimit.TimeOut => raise SMT "timeout" |
87 |
87 |
88 val (trace, setup_trace) = Attrib.config_bool "smt_trace" false |
88 val (trace, setup_trace) = Attrib.config_bool "smt_trace" (K false) |
89 |
89 |
90 fun trace_msg ctxt f x = |
90 fun trace_msg ctxt f x = |
91 if Config.get ctxt trace then tracing (f x) else () |
91 if Config.get ctxt trace then tracing (f x) else () |
92 |
92 |
93 |
93 |
94 (* SMT certificates *) |
94 (* SMT certificates *) |
95 |
95 |
96 val (record, setup_record) = Attrib.config_bool "smt_record" true |
96 val (record, setup_record) = Attrib.config_bool "smt_record" (K true) |
97 |
97 |
98 structure Certificates = Generic_Data |
98 structure Certificates = Generic_Data |
99 ( |
99 ( |
100 type T = Cache_IO.cache option |
100 type T = Cache_IO.cache option |
101 val empty = NONE |
101 val empty = NONE |