#
4778f606 |
|
21-Oct-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Delete trailing whitespace in src/
|
#
e032de7e |
|
07-Sep-2018 |
thibault <thibault_gauthier@hotmail.fr> |
conjecturing + parallel translate
|
#
19626c96 |
|
03-Sep-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Promote more Isabelle concurrency code Portable gets slightly richer with make_counter : {inc:int,init:int} -> unit -> int syncref : 'a -> {get:unit->'a, upd : ('a -> 'b * 'a) -> 'b} Under Moscow ML these map to obvious operations on references. Under Poly/ML these map to synchronised variables that are operated on atomically.
|
#
94014c7e |
|
31-Aug-2018 |
thibault <thibault_gauthier@hotmail.fr> |
conjecturing: using gnu parallel instead of parmap
|
#
77f27aac |
|
30-Aug-2018 |
thibault <thibault_gauthier@hotmail.fr> |
conjecturing: integration of eprover calls
|
#
5f7b92b1 |
|
30-Aug-2018 |
thibault <thibault_gauthier@hotmail.fr> |
holyhammer: parallelizable eprover calls
|
#
00240c4d |
|
21-Jul-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
share code between tacticToe and holyHammer + start exp with conjecturing
|
#
6b2d07ed |
|
02-Jul-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: finalizing port of the translation to SML + adding vampire
|
#
769e1d6c |
|
30-Jun-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: evaluation of old and new hammer
|
#
85e6c3a4 |
|
28-Jun-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: fixing unsoundness bug due to different names for the same variable
|
#
a919f854 |
|
28-Jun-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: log functions
|
#
506754eb |
|
27-Jun-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: finishing porting the translation to sml (hh_new function)
|
#
d1a89719 |
|
11-Apr-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
tactictoe: adding create_fof function + improve parallelism
|
#
09ce587a |
|
11-Apr-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
tactictoe: fix many issues in eprover_eval: missing theorems + update_hh_stac + atp problems + eprover_save_flag + omit tactictoe recording
|
#
2b238455 |
|
07-Mar-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
remove trailing white spaces
|
#
94b2e59d |
|
14-Feb-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
tactictoe: interactive recording + examples + readme
|
#
8da85ad6 |
|
18-Jan-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: fix error by matching the changes in hhsPredict
|
#
84da8ccc |
|
11-Jan-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
minimization and prettification shared between tactictoe and holyhammer
|
#
420eb013 |
|
17-Dec-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
removing external predictors
|
#
fbe3aebd |
|
08-Dec-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
tactictoe: reverting back the right print_vartype for first order
|
#
5bc09715 |
|
28-Nov-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
tactictoe: monte carlo wip
|
#
8c60d4f0 |
|
17-Oct-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: exporting theories by adding a filter on write_thyl
|
#
c8fc20a2 |
|
27-Sep-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer signature
|
#
def93c6c |
|
27-Sep-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
tactictoe: online recording (to be fixed)
|
#
cf8b3ea9 |
|
21-Sep-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
tactictoe: interactive recording function
|
#
3124cb7b |
|
19-Sep-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: tactic + pretty-printing
|
#
29673a86 |
|
14-Sep-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix some infelicities in holyhammer build details Trying to build with Moscow ML revealed a dependency on code in tactictoe, so I reordered the directories in the build sequence. But then, tactictoe is only built under Poly/ML anyway. So, I added the [poly] annotation to the holyhammer directories too. Changing the order may then seem unnecessary, but if one was to try to exercise any of the holyhammer code, as part of a regression test for example, then the tactictoe code does need to have been processed and put in sigobj for that to work.
|
#
024705f6 |
|
12-Sep-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
tactictoe: theorems' features IO + orthogonalization of theorems
|
#
6ba144e9 |
|
22-Aug-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: removing scripts + tactictoe: wip+ sharing predictors
|
#
2594d90c |
|
09-Sep-2015 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: updating hh_try function
|
#
9e3aa895 |
|
22-Aug-2015 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyHammer update: provers' binaries now needs to be in PATH + working toward incremental export
|
#
99ba6223 |
|
03-Aug-2015 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer 1.0
|