--- a/NEWS Mon Oct 01 12:19:55 2018 +0200
+++ b/NEWS Mon Oct 01 12:41:35 2018 +0200
@@ -47,6 +47,12 @@
* Sledgehammer: The URL for SystemOnTPTP, which is used by remote
provers, has been updated.
+* Session HOL-SPARK: .prv files are no longer written to the
+file-system, but exported to the session database. Results may be
+retrieved with the "isabelle export" command-line tool like this:
+
+ isabelle export -x "*:**.prv" HOL-SPARK-Examples
+
*** ML ***
--- a/src/HOL/ROOT Mon Oct 01 12:19:55 2018 +0200
+++ b/src/HOL/ROOT Mon Oct 01 12:41:35 2018 +0200
@@ -857,7 +857,6 @@
SPARK
session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
- options [spark_prv = false]
theories
"Gcd/Greatest_Common_Divisor"
"Liseq/Longest_Increasing_Subsequence"
@@ -873,7 +872,7 @@
"Sqrt/Sqrt"
session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
- options [show_question_marks = false, spark_prv = false]
+ options [show_question_marks = false]
sessions
"HOL-SPARK-Examples"
theories
--- a/src/HOL/SPARK/Tools/spark_commands.ML Mon Oct 01 12:19:55 2018 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Mon Oct 01 12:41:35 2018 +0200
@@ -13,13 +13,13 @@
val ([{src_path, lines = vc_lines, pos = vc_pos, ...}: Token.file,
{lines = fdl_lines, pos = fdl_pos, ...},
{lines = rls_lines, pos = rls_pos, ...}], thy') = files thy;
- val base = fst (Path.split_ext (File.full_path (Resources.master_directory thy') src_path));
+ val path = fst (Path.split_ext src_path);
in
SPARK_VCs.set_vcs
(snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines)))
(Fdl_Parser.parse_rules rls_pos (cat_lines rls_lines))
(snd (Fdl_Parser.parse_vcs header vc_pos (cat_lines vc_lines)))
- base prfx thy'
+ path prfx thy'
end;
fun add_proof_fun_cmd pf thy =
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Mon Oct 01 12:19:55 2018 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Mon Oct 01 12:41:35 2018 +0200
@@ -973,11 +973,9 @@
\because their proofs contain oracles:" proved'));
val prv_path = Path.ext "prv" path;
val _ =
- if File.exists prv_path orelse Options.default_bool \<^system_option>\<open>spark_prv\<close> then
- File.write prv_path
- (implode (map (fn (s, _) => snd (strip_number s) ^
- " -- proved by " ^ Distribution.version ^ "\n") proved''))
- else ();
+ Export.export thy (Path.implode prv_path)
+ [implode (map (fn (s, _) => snd (strip_number s) ^
+ " -- proved by " ^ Distribution.version ^ "\n") proved'')];
in {pfuns = pfuns, type_map = type_map, env = NONE} end))
|> Sign.parent_path;
--- a/src/HOL/SPARK/etc/options Mon Oct 01 12:19:55 2018 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-(* :mode=isabelle-options: *)
-
-section "HOL-SPARK"
-
-option spark_prv : bool = true
- -- "produce proof review file after 'spark_end'"