HOL icon indicating copy to clipboard operation
HOL copied to clipboard

Tactictoe selftests seem to fail.

Open ordinarymath opened this issue 1 month ago • 1 comments

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 []

ordinarymath avatar Dec 03 '25 04:12 ordinarymath

https://github.com/HOL-Theorem-Prover/HOL/issues/1541 is probably the cause of this breakage

ordinarymath avatar Dec 03 '25 05:12 ordinarymath