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, 12 Sep 2014 17:51:31 +0200
changeset 58331 054e9a9fccad
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
--- a/src/HOL/ROOT	Fri Sep 12 17:30:05 2014 +0200
+++ b/src/HOL/ROOT	Fri Sep 12 17:51:31 2014 +0200
@@ -597,12 +597,13 @@
     Simps_Case_Conv_Examples
     ML
     SAT_Examples
-    Sudoku
     Nominal2_Dummy
   theories [skip_proofs = false]
     Meson_Test
   theories [condition = SVC_HOME]
     svc_test
+  theories [condition = ISABELLE_FULL_TEST]
+    Sudoku
   document_files "root.bib" "root.tex"
 
 session "HOL-Isar_Examples" in Isar_Examples = HOL +