enabled 'Sudoku' only with 'ISABELLE_FULL_TEST' -- Sudoku is fast enough on modern hardware (within seconds on my MacBook), but it seems to fail on older test machines
authorblanchet
Fri Sep 12 17:51:31 2014 +0200 (2014-09-12)
changeset 58331054e9a9fccad
parent 58330 a016c42d136d
child 58332 be0f5d8d511b
enabled 'Sudoku' only with 'ISABELLE_FULL_TEST' -- Sudoku is fast enough on modern hardware (within seconds on my MacBook), but it seems to fail on older test machines
src/HOL/ROOT
     1.1 --- a/src/HOL/ROOT	Fri Sep 12 17:30:05 2014 +0200
     1.2 +++ b/src/HOL/ROOT	Fri Sep 12 17:51:31 2014 +0200
     1.3 @@ -597,12 +597,13 @@
     1.4      Simps_Case_Conv_Examples
     1.5      ML
     1.6      SAT_Examples
     1.7 -    Sudoku
     1.8      Nominal2_Dummy
     1.9    theories [skip_proofs = false]
    1.10      Meson_Test
    1.11    theories [condition = SVC_HOME]
    1.12      svc_test
    1.13 +  theories [condition = ISABELLE_FULL_TEST]
    1.14 +    Sudoku
    1.15    document_files "root.bib" "root.tex"
    1.16  
    1.17  session "HOL-Isar_Examples" in Isar_Examples = HOL +