Wed, 18 Dec 2013 16:50:14 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 16 Dec 2013 23:36:54 +0100 |
blanchet |
fixed source of 'Subscript' exception
|
file |
diff |
annotate
|
Tue, 19 Nov 2013 18:34:04 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 17 Oct 2013 20:49:19 +0200 |
blanchet |
generate a comment storing the goal nickname in "learn_prover"
|
file |
diff |
annotate
|
Thu, 17 Oct 2013 01:10:08 +0200 |
blanchet |
if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice
|
file |
diff |
annotate
|
Wed, 09 Oct 2013 15:58:02 +0200 |
blanchet |
run relevance filter only once for ATPs and SMT solvers, since it should now yield the same results anyway
|
file |
diff |
annotate
|
Fri, 04 Oct 2013 16:51:26 +0200 |
blanchet |
more thorough spying
|
file |
diff |
annotate
|
Fri, 04 Oct 2013 16:11:19 +0200 |
blanchet |
more Sledgehammer spying -- record fact indices
|
file |
diff |
annotate
|
Fri, 04 Oct 2013 11:12:28 +0200 |
blanchet |
more parallelism in blocking mode
|
file |
diff |
annotate
|
Tue, 24 Sep 2013 11:02:42 +0200 |
blanchet |
encode goal digest in spying log (to detect duplicates)
|
file |
diff |
annotate
|
Tue, 24 Sep 2013 09:12:09 +0200 |
blanchet |
made SML/NJ happy
|
file |
diff |
annotate
|
Mon, 23 Sep 2013 14:53:43 +0200 |
blanchet |
tuned spying
|
file |
diff |
annotate
|
Mon, 23 Sep 2013 14:53:43 +0200 |
blanchet |
added "spy" option to Sledgehammer
|
file |
diff |
annotate
|
Wed, 11 Sep 2013 22:20:44 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 23 Aug 2013 15:07:32 +0200 |
blanchet |
eliminated some needless MaSh features
|
file |
diff |
annotate
|
Sat, 17 Aug 2013 19:13:28 +0200 |
wenzelm |
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
|
file |
diff |
annotate
|
Sat, 17 Aug 2013 12:13:53 +0200 |
wenzelm |
more direct sledgehammer configuration via mode = Normal_Result and output_result;
|
file |
diff |
annotate
|
Tue, 13 Aug 2013 11:34:56 +0200 |
blanchet |
added flag for jEdit/PIDE asynchronous mode
|
file |
diff |
annotate
|
Thu, 08 Aug 2013 14:24:21 +0200 |
wenzelm |
dockable window for Sledgehammer, based on asynchronous/parallel query operation;
|
file |
diff |
annotate
|
Sat, 13 Jul 2013 13:25:42 +0200 |
wenzelm |
more explicit Markup.information for messages produced by "auto" tools;
|
file |
diff |
annotate
|
Tue, 09 Jul 2013 18:44:59 +0200 |
smolkas |
moved code -> easier debugging
|
file |
diff |
annotate
|
Tue, 28 May 2013 08:52:41 +0200 |
blanchet |
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
|
file |
diff |
annotate
|
Fri, 24 May 2013 16:43:37 +0200 |
blanchet |
improved handling of free variables' types in Isar proofs
|
file |
diff |
annotate
|
Fri, 17 May 2013 11:35:52 +0200 |
wenzelm |
tuned signature -- emphasize thread creation here;
|
file |
diff |
annotate
|
Wed, 15 May 2013 17:43:42 +0200 |
blanchet |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
file |
diff |
annotate
|
Tue, 23 Apr 2013 16:30:30 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Tue, 19 Feb 2013 17:01:06 +0100 |
blanchet |
avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
tuned data structure
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread through fact triple component from which used facts come, for accurate index output
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
more precise output of selected facts
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
simplified SMT solver code in Sledgehammer
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
eliminated needless speed optimization -- and simplified code quite a bit
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
|
file |
diff |
annotate
|
Tue, 15 Jan 2013 20:51:30 +0100 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
Mon, 14 Jan 2013 10:32:33 +0100 |
blanchet |
run Sledgehammer provers in parallel in "try"
|
file |
diff |
annotate
|
Sun, 13 Jan 2013 21:42:38 +0100 |
blanchet |
tuned message
|
file |
diff |
annotate
|
Sat, 05 Jan 2013 22:31:31 +0100 |
blanchet |
increased hard timeout -- minimization can take time
|
file |
diff |
annotate
|
Wed, 02 Jan 2013 10:54:36 +0100 |
blanchet |
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
|
file |
diff |
annotate
|
Wed, 02 Jan 2013 10:41:53 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Sat, 15 Dec 2012 19:57:12 +0100 |
blanchet |
thread no timeout properly
|
file |
diff |
annotate
|
Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
Thu, 18 Oct 2012 13:19:44 +0200 |
blanchet |
refactor code
|
file |
diff |
annotate
|
Fri, 14 Sep 2012 18:12:41 +0200 |
wenzelm |
clarified markup names;
|
file |
diff |
annotate
|
Tue, 14 Aug 2012 13:20:59 +0200 |
blanchet |
be less aggressive at kicking out chained facts
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
faster maximal node computation
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learn from SMT proofs when they can be minimized by Metis
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
name tuning
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed ML structures
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
learn from minimized ATP proofs
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
use async manager to manage MaSh learners to make sure they get killed cleanly
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
centrally construct expensive data structures
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
renamed Sledgehammer options
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
more code rationalization in relevance filter
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
systematize lazy names in relevance filter
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
rationalize relevance filter, slowing moving code from Iter to MaSh
|
file |
diff |
annotate
|
Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
|
file |
diff |
annotate
|