HOL-SPARK .prv files are subject to system option spark_prv;
authorwenzelm
Wed Mar 25 13:31:47 2015 +0100 (2015-03-25)
changeset 59810e749a0f2f401
parent 59809 87641097d0f3
child 59811 6b0d9e8ac227
HOL-SPARK .prv files are subject to system option spark_prv;
tuned;
etc/components
src/HOL/ROOT
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/SPARK/etc/options
     1.1 --- a/etc/components	Wed Mar 25 11:39:52 2015 +0100
     1.2 +++ b/etc/components	Wed Mar 25 13:31:47 2015 +0100
     1.3 @@ -4,6 +4,7 @@
     1.4  src/HOL/Mirabelle
     1.5  src/HOL/Mutabelle
     1.6  src/HOL/Library/Sum_of_Squares
     1.7 +src/HOL/SPARK
     1.8  src/HOL/Tools
     1.9  src/HOL/Tools/ATP
    1.10  src/HOL/TPTP
     2.1 --- a/src/HOL/ROOT	Wed Mar 25 11:39:52 2015 +0100
     2.2 +++ b/src/HOL/ROOT	Wed Mar 25 13:31:47 2015 +0100
     2.3 @@ -824,7 +824,7 @@
     2.4    theories SPARK
     2.5  
     2.6  session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
     2.7 -  options [document = false]
     2.8 +  options [document = false, spark_prv = false]
     2.9    theories
    2.10      "Gcd/Greatest_Common_Divisor"
    2.11  
    2.12 @@ -877,7 +877,7 @@
    2.13      "RIPEMD-160/rmd/s_r.siv"
    2.14  
    2.15  session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
    2.16 -  options [show_question_marks = false]
    2.17 +  options [show_question_marks = false, spark_prv = false]
    2.18    theories
    2.19      Example_Verification
    2.20      VC_Principles
     3.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Mar 25 11:39:52 2015 +0100
     3.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Mar 25 13:31:47 2015 +0100
     3.3 @@ -953,29 +953,33 @@
     3.4    | x => x);
     3.5  
     3.6  fun close incomplete thy =
     3.7 -  thy |>
     3.8 -  VCs.map (fn
     3.9 -      {pfuns, type_map, env = SOME {vcs, path, ...}} =>
    3.10 +  thy |> VCs.map (fn {pfuns, type_map, env} =>
    3.11 +    (case env of
    3.12 +      NONE => error "No SPARK environment is currently open"
    3.13 +    | SOME {vcs, path, ...} =>
    3.14          let
    3.15            val (proved, unproved) = partition_vcs vcs;
    3.16            val _ = Thm.join_proofs (maps (#2 o snd) proved);
    3.17 -          val (proved', proved'') = List.partition (fn (_, (_, thms, _, _)) =>
    3.18 -            exists (#oracle o Thm.peek_status) thms) proved
    3.19 -        in
    3.20 -          (if null unproved then ()
    3.21 -           else (if incomplete then warning else error)
    3.22 -             (Pretty.string_of (pp_open_vcs unproved));
    3.23 -           if null proved' then ()
    3.24 -           else warning (Pretty.string_of (pp_vcs
    3.25 +          val (proved', proved'') =
    3.26 +            List.partition (fn (_, (_, thms, _, _)) =>
    3.27 +              exists (#oracle o Thm.peek_status) thms) proved;
    3.28 +          val _ =
    3.29 +            if null unproved then ()
    3.30 +            else (if incomplete then warning else error) (Pretty.string_of (pp_open_vcs unproved));
    3.31 +          val _ =
    3.32 +            if null proved' then ()
    3.33 +            else warning (Pretty.string_of (pp_vcs
    3.34               "The following VCs are not marked as proved \
    3.35               \because their proofs contain oracles:" proved'));
    3.36 -           File.write (Path.ext "prv" path)
    3.37 -             (implode (map (fn (s, _) => snd (strip_number s) ^
    3.38 -                " -- proved by " ^ Distribution.version ^ "\n") proved''));
    3.39 -           {pfuns = pfuns, type_map = type_map, env = NONE})
    3.40 -        end
    3.41 -    | _ => error "No SPARK environment is currently open") |>
    3.42 -  Sign.parent_path;
    3.43 +          val prv_path = Path.ext "prv" path;
    3.44 +          val _ =
    3.45 +            if File.exists prv_path orelse Options.default_bool @{system_option spark_prv} then
    3.46 +              File.write prv_path
    3.47 +               (implode (map (fn (s, _) => snd (strip_number s) ^
    3.48 +                  " -- proved by " ^ Distribution.version ^ "\n") proved''))
    3.49 +            else ();
    3.50 +        in {pfuns = pfuns, type_map = type_map, env = NONE} end))
    3.51 +  |> Sign.parent_path;
    3.52  
    3.53  
    3.54  (** set up verification conditions **)
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/SPARK/etc/options	Wed Mar 25 13:31:47 2015 +0100
     4.3 @@ -0,0 +1,6 @@
     4.4 +(* :mode=isabelle-options: *)
     4.5 +
     4.6 +section "HOL-SPARK"
     4.7 +
     4.8 +option spark_prv : bool = true
     4.9 +  -- "produce proof review file after 'spark_end'"