make the Nitpick_Example theory processable even when Kodkodi is not installed;
authorblanchet
Tue Jun 22 12:19:06 2010 +0200 (2010-06-22)
changeset 37495650fae5eea93
parent 37488 a5aa61b7fa74
child 37496 9ae78e12e126
make the Nitpick_Example theory processable even when Kodkodi is not installed;
so that at least the "theory" aspects of it (as opposed to the diagnosis offered by Nitpick) are checked on everybody's machines
src/HOL/Nitpick_Examples/Mini_Nits.thy
src/HOL/Nitpick_Examples/ROOT.ML
src/HOL/Nitpick_Examples/Tests_Nits.thy
     1.1 --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Tue Jun 22 01:21:52 2010 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Tue Jun 22 12:19:06 2010 +0200
     1.3 @@ -14,14 +14,19 @@
     1.4  ML {*
     1.5  exception FAIL
     1.6  
     1.7 -(* int -> term -> string *)
     1.8 +val has_kodkodi = (getenv "KODKODI" <> "")
     1.9 +
    1.10  fun minipick n t =
    1.11    map (fn k => Minipick.kodkod_problem_from_term @{context} (K k) t) (1 upto n)
    1.12    |> Minipick.solve_any_kodkod_problem @{theory}
    1.13 -(* int -> term -> bool *)
    1.14 -fun none n t = (minipick n t = "none" orelse raise FAIL)
    1.15 -fun genuine n t = (minipick n t = "genuine" orelse raise FAIL)
    1.16 -fun unknown n t = (minipick n t = "unknown" orelse raise FAIL)
    1.17 +fun minipick_expect expect n t =
    1.18 +  if has_kodkodi then
    1.19 +    if minipick n t = expect then () else raise FAIL
    1.20 +  else
    1.21 +    ()
    1.22 +val none = minipick_expect "none"
    1.23 +val genuine = minipick_expect "genuine"
    1.24 +val unknown = minipick_expect "unknown"
    1.25  *}
    1.26  
    1.27  ML {* genuine 1 @{prop "x = Not"} *}
     2.1 --- a/src/HOL/Nitpick_Examples/ROOT.ML	Tue Jun 22 01:21:52 2010 +0200
     2.2 +++ b/src/HOL/Nitpick_Examples/ROOT.ML	Tue Jun 22 12:19:06 2010 +0200
     2.3 @@ -5,8 +5,4 @@
     2.4  Nitpick examples.
     2.5  *)
     2.6  
     2.7 -if getenv "KODKODI" = "" then
     2.8 -  ()
     2.9 -else
    2.10 -  setmp_noncritical quick_and_dirty true use_thys
    2.11 -                    ["Nitpick_Examples"];
    2.12 +setmp_noncritical quick_and_dirty true use_thys ["Nitpick_Examples"];
     3.1 --- a/src/HOL/Nitpick_Examples/Tests_Nits.thy	Tue Jun 22 01:21:52 2010 +0200
     3.2 +++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy	Tue Jun 22 12:19:06 2010 +0200
     3.3 @@ -11,6 +11,6 @@
     3.4  imports Main
     3.5  begin
     3.6  
     3.7 -ML {* Nitpick_Tests.run_all_tests () *}
     3.8 +ML {* () |> getenv "KODKODI" <> "" ? Nitpick_Tests.run_all_tests *}
     3.9  
    3.10  end