HOL
HOL copied to clipboard
Tactictoe selftests seem to fail.
Despite the tests not failing the output log seems like they are
ttt_rewrite_thy: ConseqConv
path/to/hol/src/quantHeuristics/ConseqConvScript.sml
6 proofs recognized
ttt_rewrite_thy time: 0.0164
ttt_record_thy: ConseqConv
path/to/hol/src/quantHeuristics/ConseqConvScript.sml
cp: cannot stat 'path/to/hol/src/quantHeuristics/ConseqConvTheory.sml': No such file or directory
cp: cannot stat 'path/to/hol/src/quantHeuristics/ConseqConvTheory.dat': No such file or directory
cp: cannot stat 'path/to/hol/src/quantHeuristics/ConseqConvTheory.uo': No such file or directory
cp: cannot stat 'path/to/hol/src/quantHeuristics/ConseqConvTheory.ui': No such file or directory
cp: cannot stat 'path/to/hol/src/quantHeuristics/ConseqConvTheory.sml.tttsave': No such file or directory
rm: cannot remove 'path/to/hol/src/quantHeuristics/ConseqConvTheory.sml.tttsave': No such file or directory
cp: cannot stat 'path/to/hol/src/quantHeuristics/ConseqConvTheory.dat.tttsave': No such file or directory
rm: cannot remove 'path/to/hol/src/quantHeuristics/ConseqConvTheory.dat.tttsave': No such file or directory
cp: cannot stat 'path/to/hol/src/quantHeuristics/ConseqConvTheory.uo.tttsave': No such file or directory
rm: cannot remove 'path/to/hol/src/quantHeuristics/ConseqConvTheory.uo.tttsave': No such file or directory
cp: cannot stat 'path/to/hol/src/quantHeuristics/ConseqConvTheory.ui.tttsave': No such file or directory
rm: cannot remove 'path/to/hol/src/quantHeuristics/ConseqConvTheory.ui.tttsave': No such file or directory
ttt_record_thy time: 9.6284
Missing tactic data: indexedLists quantHeuristics ind_type divides While cv reduce one sum option quotient pair combin sat normalForms relation marker num prim_rec arithmetic numeral basicSize numpair pred_set list rich_list patternMatches hol
Run tttUnfold.ttt_record ()
Loading 6 tactic calls in 0.0 seconds
METIS_TAC []
https://github.com/HOL-Theorem-Prover/HOL/issues/1541 is probably the cause of this breakage