remove trailing whitespaces

missing tttRecord. signature in tttUnfold code

tnn advice for the value during tactictoe search

more timers + light symweight

regrouping evaluation functions

remove execprefix

alternative theorem predictions

abstracting terms in original tactic

catching errors during term abstraction

abstracting first term in tactics

abstract term wip + fix chainy export missing definitions

updating tactic parser

removing thmlintac and ttt_exl + updating thmdata and tacdata

renaming some flags + readme

explicit timeout during the parsing of tactical strings

comparing with standard search

experiment with extra theorem prediction

reflecting thmlext_flag in evaluation script

splitted theorem predictions

reducing timeout for parsing tactics from 1sec to 10ms

reverting to orthogonalization

remove trailing whitespaces

savestate at the top-level

faster orthogonalization + less verbose debugging information

adding back orthogonalization

simplifying tactictoe/holyhammer/AI debugging scheme

hiding theorem reading trick in holyhammer

adding bash script for extracting statistics

print each search step

parallel instead of sequential savestates

turning off orthogonalization + maximum of 25 child by savestate

fix filtering in parallel evaluation

tactictoe evaluation using savestates

update recording + prettification (parentheses) + eliminate caches + hide outputs explicitly

nicer search recording and parsing for TacticToe

tactictoe search without references

before removing new mcts search

avoiding orthogonalization

reimplementation of let flag

moving some debug information to log_eval

replicate policy behaviour of previous version of TacticToe

new TacticToe search ready for evaulation

inverting order of conjecture

removing dependency to combin leaked by holyhammer

exporting tptp examples

removing metis inclusion as it brings theories as dependencies

enigma for tactictoe: tptp export

ttt_record_thy now include ttt_rewrite_thy in tttUnfold + search status for MCTS

TacticToe missing directory

guessing encapsulating structure namespace

fixes TacticToe recording to handle structure in pred_setTheory

trainling white spaces

tactictoe: more information during recording

removing trailing whitespaces

synthesize: final evaluation

removing num dependencies from aiLib

removing trailing whitespaces + fix cache errors in term generation

more impressive example for tactictoe

tactictoe: handle escape sequence correctly

fix hash function for 32-bit systems

more trailing whitespaces

right attributes for parmap

tactictoe: parallel evaluation

export to TFF0 (wip)

trailing whitespaces

tactictoe: leave a small time before killing thread (fixes recording)

benchmark functions for holyhammer and tactictoe

modifying some filenames

refactored tactictoe: successfully running on the core libraries

tactictoe: loads now after refactoring

finalize holyhammer refactoring, continuing with tactictoe

reinforcement prover: starting to add a cut builder as part of the proof search

Remove TABs from source files (and some trailing w/space)

discontinuing support for asynchronous hammer calls from tactictoe

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.

conjecturing: work in progress

tactictoe: overwrite protection re-enabled

tactictoe: removing unnecessary theory file restoration

tactictoe: flags for random and coverage weights

tactictoe: export ttt_metis_flag

tactictoe: flag to turn off abstraction

tactictoe: abstracting + exporting theorem values for list of theorems

tactictoe: fix unfolding

tactictoe: fixing pattern level

omit recording deep calls: more

omit recording TAC_PROOF when not at the top level

tactictoe: ttt_record_parallel warning

tactictoe: accepting list of theories even if they do not contain ancestors in parallel calls

tactictoe: removing bool and min from parallel calls

tactictoe: adding create_fof function + improve parallelism

tactictoe: avoiding evaluating bool

tactictoe: more flag lifting

tactictoe: fix many issues in eprover_eval: missing theorems + update_hh_stac + atp problems + eprover_save_flag + omit tactictoe recording

tactictoe: term prediction flag

minor in tttUnfold.sml

tactictoe: fix endofline

Fix a bug in tttUnfold + remove trailing whitespace

tactictoe: fixing bug in tttRecord + add back MCTS evaluation as a flag

Tactictoe: training + search time and tactic time as flags

tactictoe: easier recording of standard library

tactictoe: parallel evaluation

tactictoe: fix eval + bug in tttRecord

tactictoe: recording parallel version

tactictoe: update evaluation functions

tactictoe: refractoring

tactictoe: separate rewrite and record

tactictoe: changing how flags work + starting decomposition into recording/training/evaluation.

tactictoe: without Holmake

tactictoe: using buildheap

tactictoe: reverting to e94 commit + adding semicolon fix (untested)

tactictoe: fix a smaller error with DB.fetch

tactictoe: only modifying the name of the theory in new_theory

tactictoe: fixing special case for bool + automatically saving generated scripts for debugging

tactictoe: different name for its theory

tactictoe: check existing export (fix)

remove trailing white spaces

tactictoe: do not try to re-record theories unless ttt_clean_all is called

tactictoe: re-raising the same exception after cleaning

tactictoe: cleaning up .tttsave after an interrupt

tactictoe: special case for core theories

saving and restoring files in case a tactictoe script overwrite them (unlikely)

tactictoe: improved recording mechanism re-using existing Holmakefiles

tactictoe: unquoting before removing comments

tactictoe: renaming hhs prefix to ttt (rebuild necessary)