added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
authorwenzelm
Sun Apr 09 20:17:00 2017 +0200 (2017-04-09)
changeset 654489bc3b57c1fa7
parent 65447 fae6051ec192
child 65449 c82e63b11b8b
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
NEWS
etc/options
src/HOL/Proofs.thy
src/HOL/ROOT
src/Pure/System/isabelle_process.ML
     1.1 --- a/NEWS	Sun Apr 09 19:56:52 2017 +0200
     1.2 +++ b/NEWS	Sun Apr 09 20:17:00 2017 +0200
     1.3 @@ -166,6 +166,14 @@
     1.4  ISABELLE_PLATFORM64.
     1.5  
     1.6  
     1.7 +*** System ***
     1.8 +
     1.9 +* System option "record_proofs" allows to change the global
    1.10 +Proofterm.proofs variable for a session. Regular values are are 0, 1, 2;
    1.11 +a negative value means the current state in the ML heap image remains
    1.12 +unchanged.
    1.13 +
    1.14 +
    1.15  
    1.16  New in Isabelle2016-1 (December 2016)
    1.17  -------------------------------------
     2.1 --- a/etc/options	Sun Apr 09 19:56:52 2017 +0200
     2.2 +++ b/etc/options	Sun Apr 09 20:17:00 2017 +0200
     2.3 @@ -82,6 +82,8 @@
     2.4  
     2.5  section "Detail of Proof Checking"
     2.6  
     2.7 +option record_proofs : int = -1
     2.8 +  -- "set level of proofterm recording: 0, 1, 2, negative means unchanged"
     2.9  option quick_and_dirty : bool = false
    2.10    -- "if true then some tools will OMIT some proofs"
    2.11  option skip_proofs : bool = false
     3.1 --- a/src/HOL/Proofs.thy	Sun Apr 09 19:56:52 2017 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,8 +0,0 @@
     3.4 -theory Proofs
     3.5 -imports Pure
     3.6 -begin
     3.7 -
     3.8 -ML "Proofterm.proofs := 2"
     3.9 -
    3.10 -end
    3.11 -
     4.1 --- a/src/HOL/ROOT	Sun Apr 09 19:56:52 2017 +0200
     4.2 +++ b/src/HOL/ROOT	Sun Apr 09 20:17:00 2017 +0200
     4.3 @@ -18,8 +18,7 @@
     4.4    description {*
     4.5      HOL-Main with explicit proof terms.
     4.6    *}
     4.7 -  options [document = false, quick_and_dirty = false, parallel_proofs = 0]
     4.8 -  theories Proofs (*sequential change of global flag!*)
     4.9 +  options [document = false, quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
    4.10    theories "~~/src/HOL/Library/Old_Datatype"
    4.11    files
    4.12      "Tools/Quickcheck/Narrowing_Engine.hs"
     5.1 --- a/src/Pure/System/isabelle_process.ML	Sun Apr 09 19:56:52 2017 +0200
     5.2 +++ b/src/Pure/System/isabelle_process.ML	Sun Apr 09 20:17:00 2017 +0200
     5.3 @@ -219,6 +219,8 @@
     5.4    Multithreading.trace := Options.default_int "threads_trace";
     5.5    Multithreading.max_threads_update (Options.default_int "threads");
     5.6    Goal.parallel_proofs := Options.default_int "parallel_proofs";
     5.7 +  let val proofs = Options.default_int "record_proofs"
     5.8 +  in if proofs < 0 then () else Proofterm.proofs := proofs end;
     5.9    Printer.show_markup_default := false);
    5.10  
    5.11  fun init_options_interactive () =