On Wed, 2014-05-07 at 15:41 +0200, Makarius wrote: > How about ~~/src/HOL/ex/Sudoko.thy? It formally depends on ZCHAFF_HOME, > so it is rarely run in practice. Does it now make sense to remove that > condition in the ROOT file? What is tested in this theory anyway? The > 'refute' / 'oops' sequences seem to be relatively soft in their > requirements.
The theory demonstrates how Isabelle can be used as an efficient Sudoku solver. zChaff is still clearly superior to the internal solver (< 1s vs. > 60s for some problems in this theory). But the worst that should happen with the internal solver are timeouts within Refute. I suppose if you don't mind burning a few cycles, the condition in ROOT could be dropped. Moreover, it is merely a historic accident that the theory is based on Refute. I tried switching to Nitpick just now, but I ran into a minor issue that I'll raise in a separate thread. Best, Tjark _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
