diff --git a/etc/options b/etc/options --- a/etc/options +++ b/etc/options @@ -1,377 +1,375 @@ (* :mode=isabelle-options: *) section "Document Preparation" option browser_info : bool = false -- "generate theory browser information" option document : string = "" -- "build document in given format: pdf, dvi, false" option document_output : string = "" -- "document output directory" option document_variants : string = "document" -- "alternative document variants (separated by colons)" option document_tags : string = "" -- "default command tags (separated by commas)" option document_bibliography : bool = false -- "explicitly enable use of bibtex (default: according to presence of root.bib)" option document_preprocessor : string = "" -- "document preprocessor: executable relative to document output directory" option document_build : string = "lualatex" -- "document build engine (e.g. lualatex, pdflatex, build)" option document_logo : string = "" -- "generate named instance of Isabelle logo (underscore means unnamed variant)" option thy_output_display : bool = false -- "indicate output as multi-line display-style material" option thy_output_break : bool = false -- "control line breaks in non-display material" option thy_output_cartouche : bool = false -- "indicate if the output should be delimited as cartouche" option thy_output_quotes : bool = false -- "indicate if the output should be delimited via double quotes" option thy_output_margin : int = 76 -- "right margin / page width for printing of display material" option thy_output_indent : int = 0 -- "indentation for pretty printing of display material" option thy_output_source : bool = false -- "print original source text rather than internal representation" option thy_output_source_cartouche : bool = false -- "print original source text rather than internal representation, preserve cartouches" option thy_output_modes : string = "" -- "additional print modes for document output (separated by commas)" section "Prover Output" option show_types : bool = false -- "show type constraints when printing terms" option show_sorts : bool = false -- "show sort constraints when printing types" option show_brackets : bool = false -- "show extra brackets when printing terms/types" option show_question_marks : bool = true -- "show leading question mark of schematic variables" option show_consts : bool = false -- "show constants with types when printing proof state" option show_main_goal : bool = false -- "show main goal when printing proof state" option goals_limit : int = 10 -- "maximum number of subgoals to be printed" option names_long : bool = false -- "show fully qualified names" option names_short : bool = false -- "show base names only" option names_unique : bool = true -- "show partially qualified names, as required for unique name resolution" option eta_contract : bool = true -- "print terms in eta-contracted form" option print_mode : string = "" -- "additional print modes for prover output (separated by commas)" section "Parallel Processing and Timing" public option threads : int = 0 -- "maximum number of worker threads for prover process (0 = hardware max.)" option threads_trace : int = 0 -- "level of tracing information for multithreading" option threads_stack_limit : real = 0.25 -- "maximum stack size for worker threads (in giga words, 0 = unlimited)" public option parallel_limit : int = 0 -- "approximative limit for parallel tasks (0 = unlimited)" public option parallel_print : bool = true -- "parallel and asynchronous printing of results" public option parallel_proofs : int = 1 -- "level of parallel proof checking: 0, 1, 2" option parallel_subproofs_threshold : real = 0.01 -- "lower bound of timing estimate for forked nested proofs (seconds)" -option parallel_presentation : bool = true - -- "parallel theory presentation" option command_timing_threshold : real = 0.1 -- "default threshold for persistent command timing (seconds)" public option timeout_scale : real = 1.0 -- "scale factor for timeout in Isabelle/ML and session build" section "Detail of Proof Checking" option record_proofs : int = -1 -- "set level of proofterm recording: 0, 1, 2, negative means unchanged" option quick_and_dirty : bool = false -- "if true then some tools will OMIT some proofs" option skip_proofs : bool = false -- "skip over proofs (implicit 'sorry')" option strict_facts : bool = false -- "force lazy facts when defined in context" section "Global Session Parameters" option condition : string = "" -- "required environment variables for subsequent theories (separated by commas)" option timeout : real = 0 -- "timeout for session build job (seconds > 0)" option timeout_build : bool = true -- "observe timeout for session build" option process_output_limit : int = 100 -- "build process output limit (in million characters, 0 = unlimited)" option process_output_tail : int = 40 -- "build process output tail shown to user (in lines, 0 = unlimited)" option profiling : string = "" -- "ML profiling (possible values: time, allocations)" option system_log : string = "" -- "output for system messages (log file or \"-\" for console progress)" option system_heaps : bool = false -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS" section "ML System" option ML_print_depth : int = 20 -- "ML print depth for toplevel pretty-printing" public option ML_exception_trace : bool = false -- "ML exception trace for toplevel command execution" public option ML_exception_debugger : bool = false -- "ML debugger exception trace for toplevel command execution" public option ML_debugger : bool = false -- "ML debugger instrumentation for newly compiled code" public option ML_system_64 : bool = false -- "ML system for 64bit platform is used if possible (change requires restart)" public option ML_process_policy : string = "" -- "ML process command prefix (process policy)" section "PIDE Build" option pide_reports : bool = true -- "report PIDE markup" option build_pide_reports : bool = true -- "report PIDE markup in batch build" section "Editor Session" public option editor_load_delay : real = 0.5 -- "delay for file load operations (new buffers etc.)" public option editor_input_delay : real = 0.2 -- "delay for user input (text edits, cursor movement etc.)" public option editor_generated_input_delay : real = 1.0 -- "delay for machine-generated input that may outperform user edits" public option editor_output_delay : real = 0.1 -- "delay for prover output (markup, common messages etc.)" public option editor_consolidate_delay : real = 2.0 -- "delay to consolidate status of command evaluation (execution forks)" public option editor_prune_delay : real = 15 -- "delay to prune history (delete old versions)" option editor_prune_size : int = 0 -- "retained size of pruned history (delete old versions)" public option editor_update_delay : real = 0.5 -- "delay for physical GUI updates" public option editor_reparse_limit : int = 10000 -- "maximum amount of reparsed text outside perspective" public option editor_tracing_messages : int = 1000 -- "initial number of tracing messages for each command transaction (0: unbounded)" public option editor_chart_delay : real = 3.0 -- "delay for chart repainting" public option editor_continuous_checking : bool = true -- "continuous checking of proof document (visible and required parts)" public option editor_output_state : bool = false -- "implicit output of proof state" option editor_execution_delay : real = 0.02 -- "delay for start of execution process after document update (seconds)" option editor_syslog_limit : int = 100 -- "maximum amount of buffered syslog messages" public option editor_presentation : bool = false -- "dynamic presentation while editing" section "Headless Session" option headless_consolidate_delay : real = 15 -- "delay to consolidate status of command evaluation (execution forks)" option headless_prune_delay : real = 60 -- "delay to prune history (delete old versions)" option headless_check_delay : real = 0.5 -- "delay for theory status check during PIDE processing (seconds)" option headless_check_limit : int = 0 -- "maximum number of theory status checks (0 = unlimited)" option headless_nodes_status_delay : real = -1 -- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)" option headless_watchdog_timeout : real = 600 -- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)" option headless_commit_cleanup_delay : real = 60 -- "delay for cleanup of already imported theories (seconds, 0 = disabled)" option headless_load_limit : real = 5.0 -- "limit in MB for loaded theory files (0 = unlimited)" section "Miscellaneous Tools" public option find_theorems_limit : int = 40 -- "limit of displayed results" public option find_theorems_tactic_limit : int = 5 -- "limit of tactic search for 'solves' criterion" section "Completion" public option completion_limit : int = 40 -- "limit for completion within the formal context" public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store" -- "glob patterns to ignore in file-system path completion (separated by colons)" section "Spell Checker" public option spell_checker : bool = true -- "enable spell-checker for prose words within document text, comments etc." public option spell_checker_dictionary : string = "en" -- "spell-checker dictionary name" public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment" -- "included markup elements for spell-checker (separated by commas)" public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text" -- "excluded markup elements for spell-checker (separated by commas)" section "Secure Shell" option ssh_config_dir : string = "$HOME/.ssh" -- "SSH configuration directory" option ssh_config_file : string = "$HOME/.ssh/config" -- "main SSH configuration file" option ssh_identity_files : string = "$HOME/.ssh/id_dsa:$HOME/.ssh/id_ecdsa:$HOME/.ssh/id_rsa" -- "possible SSH identity files (separated by colons)" option ssh_compression : bool = true -- "enable SSH compression" option ssh_connect_timeout : real = 60 -- "SSH connection timeout (seconds)" option ssh_alive_interval : real = 30 -- "time interval to keep SSH server connection alive (seconds)" option ssh_alive_count_max : int = 3 -- "maximum number of messages to keep SSH server connection alive" section "Phabricator" option phabricator_version_arcanist : string = "7af9846f994a8d0a1fc89af996e3ddd81f01765e" -- "repository version for arcanist" option phabricator_version_phabricator : string = "2afedad61c5181bb4f832cea27b9b59df19f3fd5" -- "repository version for phabricator" section "Theory Export" option export_theory : bool = false -- "export theory content to Isabelle/Scala" option export_standard_proofs : bool = false -- "export standardized proof terms to Isabelle/Scala (not scalable)" option export_proofs : bool = false -- "export proof terms to Isabelle/Scala" option prune_proofs : bool = false -- "prune proof terms after export (do not store in Isabelle/ML)" section "Theory update" option update_inner_syntax_cartouches : bool = false -- "update inner syntax (types, terms, etc.) to use cartouches" option update_mixfix_cartouches : bool = false -- "update mixfix templates to use cartouches instead of double quotes" option update_control_cartouches : bool = false -- "update antiquotations to use control symbol with cartouche argument" option update_path_cartouches : bool = false -- "update file-system paths to use cartouches" section "Build Database" option build_database_server : bool = false option build_database_user : string = "" option build_database_password : string = "" option build_database_name : string = "" option build_database_host : string = "" option build_database_port : int = 0 option build_database_ssh_host : string = "" option build_database_ssh_user : string = "" option build_database_ssh_port : int = 0 section "Build Log Database" option build_log_database_user : string = "" option build_log_database_password : string = "" option build_log_database_name : string = "" option build_log_database_host : string = "" option build_log_database_port : int = 0 option build_log_ssh_host : string = "" option build_log_ssh_user : string = "" option build_log_ssh_port : int = 0 option build_log_history : int = 30 -- "length of relevant history (in days)" option build_log_transaction_size : int = 1 -- "number of log files for each db update" section "Isabelle/Scala/ML system channel" option system_channel_address : string = "" option system_channel_password : string = "" diff --git a/src/HOL/ROOT b/src/HOL/ROOT --- a/src/HOL/ROOT +++ b/src/HOL/ROOT @@ -1,1210 +1,1211 @@ chapter HOL session HOL (main) = Pure + description " Classical Higher-order Logic. " options [strict_facts] sessions Tools theories Main (global) Complex_Main (global) document_theories Tools.Code_Generator document_files "root.bib" "root.tex" session "HOL-Examples" in Examples = HOL + description " Notable Examples in Isabelle/HOL. " sessions "HOL-Computational_Algebra" theories Adhoc_Overloading_Examples Ackermann Cantor Coherent Commands Drinker Groebner_Examples Iff_Oracle Induction_Schema Knaster_Tarski "ML" Peirce Records Seq Sqrt document_files "root.bib" "root.tex" session "HOL-Proofs" (timing) in Proofs = Pure + description " HOL-Main with explicit proof terms. " options [quick_and_dirty = false, record_proofs = 2, parallel_limit = 500] sessions "HOL-Library" theories "HOL-Library.Realizers" session "HOL-Library" (main timing) in Library = HOL + description " Classical Higher-order Logic -- batteries included. " theories Library (*conflicting type class instantiations and dependent applications*) Finite_Lattice List_Lexorder List_Lenlexorder Prefix_Order Product_Lexorder Product_Order Subseq_Order (*conflicting syntax*) Datatype_Records (*data refinements and dependent applications*) AList_Mapping Code_Binary_Nat Code_Prolog Code_Real_Approx_By_Float Code_Target_Numeral Code_Target_Numeral_Float DAList DAList_Multiset RBT_Mapping RBT_Set (*printing modifications*) OptionalSugar (*prototypic tools*) Predicate_Compile_Quickcheck (*legacy tools*) Old_Datatype Old_Recdef Realizers Refute document_files "root.bib" "root.tex" session "HOL-Analysis" (main timing) in Analysis = HOL + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Library" "HOL-Combinatorics" "HOL-Computational_Algebra" theories Analysis document_files "root.tex" "root.bib" session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] theories Complex_Analysis document_files "root.tex" "root.bib" session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" + theories Approximations Metric_Arith_Examples session "HOL-Homology" (timing) in Homology = "HOL-Analysis" + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Algebra" theories Homology document_files "root.tex" session "HOL-Combinatorics" (main timing) in "Combinatorics" = "HOL" + sessions "HOL-Library" theories Combinatorics document_files "root.tex" session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" + theories Computational_Algebra (*conflicting type class instantiations and dependent applications*) Field_as_Ring session "HOL-Real_Asymp" in Real_Asymp = HOL + sessions "HOL-Decision_Procs" theories Real_Asymp Real_Asymp_Approx Real_Asymp_Examples session "HOL-Real_Asymp-Manual" in "Real_Asymp/Manual" = "HOL-Real_Asymp" + theories Real_Asymp_Doc document_files (in "~~/src/Doc") "iman.sty" "extra.sty" "isar.sty" document_files "root.tex" "style.sty" session "HOL-Hahn_Banach" in Hahn_Banach = HOL + description " Author: Gertrud Bauer, TU Munich The Hahn-Banach theorem for real vector spaces. This is the proof of the Hahn-Banach theorem for real vectorspaces, following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach theorem is one of the fundamental theorems of functional analysis. It is a conclusion of Zorn's lemma. Two different formaulations of the theorem are presented, one for general real vectorspaces and its application to normed vectorspaces. The theorem says, that every continous linearform, defined on arbitrary subspaces (not only one-dimensional subspaces), can be extended to a continous linearform on the whole vectorspace. " sessions "HOL-Analysis" theories Hahn_Banach document_files "root.bib" "root.tex" session "HOL-Induct" in Induct = HOL + description " Examples of (Co)Inductive Definitions. Comb proves the Church-Rosser theorem for combinators (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz). Mutil is the famous Mutilated Chess Board problem (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz). PropLog proves the completeness of a formalization of propositional logic (see http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz). Exp demonstrates the use of iterated inductive definitions to reason about mutually recursive relations. " sessions "HOL-Library" theories [quick_and_dirty] Common_Patterns theories Nested_Datatype QuoDataType QuoNestedDataType Term SList ABexp Infinitely_Branching_Tree Ordinals Sigma_Algebra Comb PropLog Com document_files "root.tex" session "HOL-IMP" (timing) in IMP = "HOL-Library" + options [document_variants = document] theories BExp ASM Finite_Reachable Denotational Compiler2 Poly_Types Sec_Typing Sec_TypingT Def_Init_Big Def_Init_Small Fold Live Live_True Hoare_Examples Hoare_Sound_Complete VCG Hoare_Total VCG_Total_EX VCG_Total_EX2 Collecting1 Collecting_Examples Abs_Int_Tests Abs_Int1_parity Abs_Int1_const Abs_Int3 Procs_Dyn_Vars_Dyn Procs_Stat_Vars_Dyn Procs_Stat_Vars_Stat C_like OO document_files "root.bib" "root.tex" session "HOL-IMPP" in IMPP = HOL + description \ Author: David von Oheimb Copyright 1999 TUM IMPP -- An imperative language with procedures. This is an extension of IMP with local variables and mutually recursive procedures. For documentation see "Hoare Logic for Mutual Recursion and Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). \ theories EvenOdd session "HOL-Data_Structures" (timing) in Data_Structures = HOL + options [document_variants = document] sessions "HOL-Number_Theory" theories [document = false] Less_False theories Sorting Balance Tree_Map Interval_Tree AVL_Map AVL_Bal_Set AVL_Bal2_Set Height_Balanced_Tree RBT_Set2 RBT_Map Tree23_Map Tree23_of_List Tree234_Map Brother12_Map AA_Map Set2_Join_RBT Array_Braun Trie_Fun Trie_Map Tries_Binary Queue_2Lists Heaps Leftist_Heap Binomial_Heap Selection document_files "root.tex" "root.bib" session "HOL-Import" in Import = HOL + theories HOL_Light_Maps theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" + description " Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity. " sessions "HOL-Algebra" theories Number_Theory document_files "root.tex" session "HOL-Hoare" in Hoare = HOL + description " Verification of imperative programs (verification conditions are generated automatically from pre/post conditions and loop invariants). " theories Examples ExamplesAbort ExamplesTC Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation document_files "root.bib" "root.tex" session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL + description " Verification of shared-variable imperative programs a la Owicki-Gries. (verification conditions are generated automatically). " theories Hoare_Parallel document_files "root.bib" "root.tex" session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" + sessions "HOL-Number_Theory" "HOL-Data_Structures" "HOL-Examples" theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Code_Lazy_Test Code_Test_PolyML Code_Test_Scala theories [condition = ISABELLE_GHC] Code_Test_GHC theories [condition = ISABELLE_MLTON] Code_Test_MLton theories [condition = ISABELLE_OCAMLFIND] Code_Test_OCaml theories [condition = ISABELLE_SMLNJ] Code_Test_SMLNJ session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" + description " Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Testing Metis and Sledgehammer. " sessions "HOL-Decision_Procs" theories Abstraction Big_O Binary_Tree Clausification Message Proxies Tarski Trans_Closure Sets session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL + description " Author: Jasmin Blanchette, TU Muenchen Copyright 2009 " options [kodkod_scala] sessions "HOL-Library" theories [quick_and_dirty] Nitpick_Examples session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" + description " Author: Clemens Ballarin, started 24 September 1999, and many others The Isabelle Algebraic Library. " sessions "HOL-Cardinals" "HOL-Combinatorics" theories (* Orders and Lattices *) Galois_Connection (* Knaster-Tarski theorem and Galois connections *) (* Groups *) FiniteProduct (* Product operator for commutative groups *) Sylow (* Sylow's theorem *) Bij (* Automorphism Groups *) Multiplicative_Group Zassenhaus (* The Zassenhaus lemma *) (* Rings *) Divisibility (* Rings *) IntRing (* Ideals and residue classes *) UnivPoly (* Polynomials *) (* Main theory *) Algebra document_files "root.bib" "root.tex" session "HOL-Auth" (timing) in Auth = HOL + description " A new approach to verifying authentication protocols. " sessions "HOL-Library" directories "Smartcard" "Guard" theories Auth_Shared Auth_Public "Smartcard/Auth_Smartcard" "Guard/Auth_Guard_Shared" "Guard/Auth_Guard_Public" document_files "root.tex" session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" + description " Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Verifying security protocols using Chandy and Misra's UNITY formalism. " directories "Simple" "Comp" theories (*Basic meta-theory*) UNITY_Main (*Simple examples: no composition*) "Simple/Deadlock" "Simple/Common" "Simple/Network" "Simple/Token" "Simple/Channel" "Simple/Lift" "Simple/Mutex" "Simple/Reach" "Simple/Reachability" (*Verifying security protocols using UNITY*) "Simple/NSP_Bad" (*Example of composition*) "Comp/Handshake" (*Universal properties examples*) "Comp/Counter" "Comp/Counterc" "Comp/Priority" "Comp/TimerArray" "Comp/Progress" "Comp/Alloc" "Comp/AllocImpl" "Comp/Client" (*obsolete*) ELT document_files "root.tex" session "HOL-Unix" in Unix = HOL + options [print_mode = "no_brackets,no_type_brackets"] sessions "HOL-Library" theories Unix document_files "root.bib" "root.tex" session "HOL-ZF" in ZF = HOL + sessions "HOL-Library" theories MainZF Games document_files "root.tex" session "HOL-Imperative_HOL" (timing) in Imperative_HOL = HOL + options [print_mode = "iff,no_brackets"] sessions "HOL-Library" directories "ex" theories Imperative_HOL_ex document_files "root.bib" "root.tex" session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" + description " Various decision procedures, typically involving reflection. " directories "ex" theories Decision_Procs session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + sessions "HOL-Examples" theories Hilbert_Classical Proof_Terms XML_Data session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" + description " Examples for program extraction in Higher-Order Logic. " options [quick_and_dirty = false] sessions "HOL-Computational_Algebra" theories Greatest_Common_Divisor Warshall Higman_Extraction Pigeonhole Euclid document_files "root.bib" "root.tex" session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" + description \ Lambda Calculus in de Bruijn's Notation. This session defines lambda-calculus terms with de Bruijn indixes and proves confluence of beta, eta and beta+eta. The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html). \ options [print_mode = "no_brackets", quick_and_dirty = false] sessions "HOL-Library" theories Eta StrongNorm Standardization WeakNorm document_files "root.bib" "root.tex" session "HOL-Prolog" in Prolog = HOL + description " Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) A bare-bones implementation of Lambda-Prolog. This is a simple exploratory implementation of Lambda-Prolog in HOL, including some minimal examples (in Test.thy) and a more typical example of a little functional language and its type system. " theories Test Type session "HOL-MicroJava" (timing) in MicroJava = HOL + description " Formalization of a fragment of Java, together with a corresponding virtual machine and a specification of its bytecode verifier and a lightweight bytecode verifier, including proofs of type-safety. " sessions "HOL-Library" "HOL-Eisbach" directories "BV" "Comp" "DFA" "J" "JVM" theories MicroJava document_files "introduction.tex" "root.bib" "root.tex" session "HOL-NanoJava" in NanoJava = HOL + description " Hoare Logic for a tiny fragment of Java. " theories Example document_files "root.bib" "root.tex" session "HOL-Bali" (timing) in Bali = HOL + sessions "HOL-Library" theories AxExample AxSound AxCompl Trans TypeSafe document_files "root.tex" session "HOL-IOA" in IOA = HOL + description \ Author: Tobias Nipkow and Konrad Slind and Olaf Müller Copyright 1994--1996 TU Muenchen The meta-theory of I/O-Automata in HOL. This formalization has been significantly changed and extended, see HOLCF/IOA. There are also the proofs of two communication protocols which formerly have been here. @inproceedings{Nipkow-Slind-IOA, author={Tobias Nipkow and Konrad Slind}, title={{I/O} Automata in {Isabelle/HOL}}, booktitle={Proc.\ TYPES Workshop 1994}, publisher=Springer, series=LNCS, note={To appear}} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz and @inproceedings{Mueller-Nipkow, author={Olaf M\"uller and Tobias Nipkow}, title={Combining Model Checking and Deduction for {I/O}-Automata}, booktitle={Proc.\ TACAS Workshop}, organization={Aarhus University, BRICS report}, year=1995} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz \ theories Solve session "HOL-Lattice" in Lattice = HOL + description " Author: Markus Wenzel, TU Muenchen Basic theory of lattices and orders. " theories CompleteLattice document_files "root.tex" session "HOL-ex" (timing) in ex = "HOL-Number_Theory" + description " Miscellaneous examples for Higher-Order Logic. " theories Antiquote Argo_Examples Arith_Examples Ballot BinEx Birthday_Paradox Bit_Lists Bubblesort CTL Cartouche_Examples Case_Product Chinese Classical Code_Binary_Nat_examples Code_Lazy_Demo Code_Timing Coercion_Examples Computations Conditional_Parametricity_Examples Cubic_Quartic Datatype_Record_Examples Dedekind_Real Erdoes_Szekeres Eval_Examples Executable_Relation Execute_Choice Functions Function_Growth Gauge_Integration Guess HarmonicSeries Hebrew Hex_Bin_Examples IArray_Examples Intuitionistic Join_Theory Lagrange List_to_Set_Comprehension_Examples LocaleTest2 MergeSort MonoidGroup Multiquote NatSum Normalization_by_Evaluation PER Parallel_Example Peano_Axioms Perm_Fragments PresburgerEx Primrec Pythagoras Quicksort Radix_Sort Reflection_Examples Refute_Examples Residue_Ring Rewrite_Examples SOS SOS_Cert Serbian Set_Comprehension_Pointfree_Examples Set_Theory Simproc_Tests Simps_Case_Conv_Examples Sketch_and_Explore Sorting_Algorithms_Examples Specifications_with_bundle_mixins Sqrt_Script Sudoku Sum_of_Powers Tarski Termination ThreeDivides Transfer_Debug Transfer_Int_Nat Transitive_Closure_Table_Ex Tree23 Triangular_Numbers Unification While_Combinator_Example veriT_Preprocessing theories [skip_proofs = false] SAT_Examples Meson_Test session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" + description " Miscellaneous Isabelle/Isar examples. " options [quick_and_dirty] sessions "HOL-Hoare" theories Structured_Statements Basic_Logic Expr_Compiler Fibonacci Group Group_Context Group_Notepad Hoare_Ex Mutilated_Checkerboard Puzzle Summation document_files "root.bib" "root.tex" session "HOL-Eisbach" in Eisbach = HOL + description \ The Eisbach proof method language and "match" method. \ sessions FOL "HOL-Analysis" theories Eisbach Tests Examples Examples_FOL Example_Metric session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL + description " Verification of the SET Protocol. " sessions "HOL-Library" theories SET_Protocol document_files "root.tex" session "HOL-Matrix_LP" in Matrix_LP = HOL + description " Two-dimensional matrices and linear programming. " sessions "HOL-Library" directories "Compute_Oracle" theories Cplex document_files "root.tex" session "HOL-TLA" in TLA = HOL + description " Lamport's Temporal Logic of Actions. " theories TLA session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" + theories Inc session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" + theories DBuffer session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" + theories MemoryImplementation session "HOL-TPTP" in TPTP = HOL + description " Author: Jasmin Blanchette, TU Muenchen Author: Nik Sultana, University of Cambridge Copyright 2011 TPTP-related extensions. " sessions "HOL-Library" theories ATP_Theory_Export MaSh_Eval TPTP_Interpret THF_Arith TPTP_Proof_Reconstruction theories ATP_Problem_Import session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" + sessions "HOL-Combinatorics" theories Probability document_files "root.tex" session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" + theories Dining_Cryptographers Koepf_Duermuth_Countermeasure Measure_Not_CCC session "HOL-Nominal" in Nominal = HOL + sessions "HOL-Library" theories Nominal session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" + theories Class3 CK_Machine Compile Contexts Crary CR_Takahashi CR Fsub Height Lambda_mu Lam_Funs LocalWeakening Pattern SN SOS Standardization Support Type_Preservation Weakening W theories [quick_and_dirty] VC_Condition session "HOL-Cardinals" (timing) in Cardinals = HOL + description " Ordinals and Cardinals, Full Theories. " theories Cardinals Bounded_Set document_files "intro.tex" "root.tex" "root.bib" session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" + description " (Co)datatype Examples. " directories "Derivation_Trees" theories Compat Lambda_Term Process TreeFsetI "Derivation_Trees/Gram_Lang" "Derivation_Trees/Parallel_Composition" Koenig Lift_BNF Milner_Tofte Stream_Processor Cyclic_List Free_Idempotent_Monoid Regex_ACI Regex_ACIDZ TLList FAE_Sequence Misc_Codatatype Misc_Datatype Misc_Primcorec Misc_Primrec Datatype_Simproc_Tests session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" + description " Corecursion Examples. " directories "Tests" theories LFilter Paper_Examples Stream_Processor "Tests/Simple_Nesting" "Tests/Iterate_GPV" theories [quick_and_dirty] "Tests/GPV_Bare_Bones" "Tests/Merge_D" "Tests/Merge_Poly" "Tests/Misc_Mono" "Tests/Misc_Poly" "Tests/Small_Concrete" "Tests/Stream_Friends" "Tests/TLList_Friends" "Tests/Type_Class" session "HOL-Statespace" in Statespace = HOL + theories [skip_proofs = false] StateSpaceEx document_files "root.tex" session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" + description " Nonstandard analysis. " theories Nonstandard_Analysis document_files "root.tex" session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" + theories NSPrimes session "HOL-Mirabelle-ex" in "Tools/Mirabelle" = HOL + description "Some arbitrary small test case for Mirabelle." - options [timeout = 60, mirabelle_actions = "arith"] + options [timeout = 60, + mirabelle_theories = "HOL-Analysis.Inner_Product", mirabelle_actions = "arith"] sessions "HOL-Analysis" theories "HOL-Analysis.Inner_Product" session "HOL-SMT_Examples" (timing) in SMT_Examples = HOL + options [quick_and_dirty] sessions "HOL-Library" theories Boogie SMT_Examples SMT_Word_Examples SMT_Examples_Verit SMT_Tests_Verit theories [condition = Z3_INSTALLED] SMT_Tests session "HOL-SPARK" in "SPARK" = HOL + sessions "HOL-Library" theories SPARK session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" + directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt" theories "Gcd/Greatest_Common_Divisor" "Liseq/Longest_Increasing_Subsequence" "RIPEMD-160/F" "RIPEMD-160/Hash" "RIPEMD-160/K_L" "RIPEMD-160/K_R" "RIPEMD-160/R_L" "RIPEMD-160/Round" "RIPEMD-160/R_R" "RIPEMD-160/S_L" "RIPEMD-160/S_R" "Sqrt/Sqrt" export_files (in ".") "*:**.prv" session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" + options [show_question_marks = false] sessions "HOL-Library" "HOL-SPARK-Examples" theories Example_Verification VC_Principles Reference Complex_Types document_theories "HOL-SPARK-Examples.Greatest_Common_Divisor" document_files "complex_types.ads" "complex_types_app.adb" "complex_types_app.ads" "Gcd.adb" "Gcd.ads" "intro.tex" "loop_invariant.adb" "loop_invariant.ads" "root.bib" "root.tex" "Simple_Gcd.adb" "Simple_Gcd.ads" session "HOL-Mutabelle" in Mutabelle = HOL + sessions "HOL-Library" theories MutabelleExtra session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL + sessions "HOL-Library" theories Quickcheck_Examples Quickcheck_Lattice_Examples Completeness Quickcheck_Interfaces Quickcheck_Nesting_Example theories [condition = ISABELLE_GHC] Hotel_Example Quickcheck_Narrowing_Examples session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" + description " Author: Cezary Kaliszyk and Christian Urban " theories DList Quotient_FSet Quotient_Int Quotient_Message Lift_FSet Lift_Set Lift_Fun Quotient_Rat Lift_DList Int_Pow Lifting_Code_Dt_Test session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL + sessions "HOL-Library" theories Examples Predicate_Compile_Tests Predicate_Compile_Quickcheck_Examples Specialisation_Examples IMP_1 IMP_2 (* FIXME since 21-Jul-2011 Hotel_Example_Small_Generator *) IMP_3 IMP_4 theories [condition = ISABELLE_SWIPL] Code_Prolog_Examples Context_Free_Grammar_Example Hotel_Example_Prolog Lambda_Example List_Examples theories [condition = ISABELLE_SWIPL, quick_and_dirty] Reg_Exp_Example session "HOL-Types_To_Sets" in Types_To_Sets = HOL + description " Experimental extension of Higher-Order Logic to allow translation of types to sets. " directories "Examples" theories Types_To_Sets "Examples/Prerequisites" "Examples/Finite" "Examples/T2_Spaces" "Examples/Unoverload_Def" "Examples/Linear_Algebra_On" session HOLCF (main timing) in HOLCF = HOL + description " Author: Franz Regensburger Author: Brian Huffman HOLCF -- a semantic extension of HOL by the LCF logic. " sessions "HOL-Library" theories HOLCF (global) document_files "root.tex" session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF + theories Domain_ex Fixrec_ex New_Domain document_files "root.tex" session "HOLCF-Library" in "HOLCF/Library" = HOLCF + theories HOLCF_Library HOL_Cpo session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF + description " IMP -- A WHILE-language and its Semantics. This is the HOLCF-based denotational semantics of a simple WHILE-language. " sessions "HOL-IMP" theories HoareEx document_files "isaverbatimwrite.sty" "root.tex" "root.bib" session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" + description " Miscellaneous examples for HOLCF. " theories Dnat Dagstuhl Focus_ex Fix2 Hoare Concurrency_Monad Loop Powerdomain_ex Domain_Proofs Letrec Pattern_Match session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" + description \ FOCUS: a theory of stream-processing functions Isabelle/HOLCF. For introductions to FOCUS, see "The Design of Distributed Systems - An Introduction to FOCUS" http://www4.in.tum.de/publ/html.php?e=2 "Specification and Refinement of a Buffer of Length One" http://www4.in.tum.de/publ/html.php?e=15 "Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321 \ theories Fstreams FOCUS Buffer_adm session IOA (timing) in "HOLCF/IOA" = HOLCF + description " Author: Olaf Müller Copyright 1997 TU München A formalization of I/O automata in HOLCF. The distribution contains simulation relations, temporal logic, and an abstraction theory. Everything is based upon a domain-theoretic model of finite and infinite sequences. " theories Abstraction session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA + description " Author: Olaf Müller The Alternating Bit Protocol performed in I/O-Automata: combining IOA with Model Checking. Theory Correctness contains the proof of the abstraction from unbounded channels to finite ones. File Check.ML contains a simple ModelChecker prototype checking Spec against the finite version of the ABP-protocol. " theories Correctness Spec session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA + description " Author: Tobias Nipkow & Konrad Slind A network transmission protocol, performed in the I/O automata formalization by Olaf Müller. " theories Overview Correctness session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA + description " Author: Olaf Müller Memory storage case study. " theories Correctness session "IOA-ex" in "HOLCF/IOA/ex" = IOA + description " Author: Olaf Müller " theories TrivEx TrivEx2 diff --git a/src/HOL/Tools/Mirabelle/mirabelle.ML b/src/HOL/Tools/Mirabelle/mirabelle.ML --- a/src/HOL/Tools/Mirabelle/mirabelle.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle.ML @@ -1,257 +1,268 @@ (* Title: HOL/Mirabelle/Tools/mirabelle.ML Author: Jasmin Blanchette and Sascha Boehme, TU Munich Author: Makarius *) signature MIRABELLE = sig (*core*) val print_name: string -> string val print_properties: Properties.T -> string type context = {index: int, tag: string, arguments: Properties.T, timeout: Time.time, theory: theory} type command = {name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state} val theory_action: binding -> (context -> command list -> XML.body) -> theory -> theory val log_command: command -> XML.body -> XML.tree val log_report: Properties.T -> XML.body -> XML.tree val print_exn: exn -> string val command_action: binding -> (context -> command -> string) -> theory -> theory (*utility functions*) val can_apply : Time.time -> (Proof.context -> int -> tactic) -> Proof.state -> bool val theorems_in_proof_term : theory -> thm -> thm list val theorems_of_sucessful_proof: Toplevel.state -> thm list val get_argument : (string * string) list -> string * string -> string val get_int_argument : (string * string) list -> string * int -> int val get_bool_argument : (string * string) list -> string * bool -> bool val cpu_time : ('a -> 'b) -> 'a -> 'b * int end structure Mirabelle : MIRABELLE = struct (** Mirabelle core **) (* concrete syntax *) val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords \<^theory>); val print_name = Token.print_name keywords; val print_properties = Token.print_properties keywords; fun read_actions str = Token.read_body keywords (Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params)) (Symbol_Pos.explode0 str); (* actions *) type command = {name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}; type context = {index: int, tag: string, arguments: Properties.T, timeout: Time.time, theory: theory}; structure Data = Theory_Data ( type T = (context -> command list -> XML.body) Name_Space.table; val empty = Name_Space.empty_table "mirabelle_action"; val extend = I; val merge = Name_Space.merge_tables; ); fun theory_action binding action thy = let val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming); in thy |> Data.map (#2 o Name_Space.define context true (binding, action)) end; (* log content *) fun log_action name arguments = XML.Elem (("action", (Markup.nameN, name) :: arguments), [XML.Text (print_name name ^ (if null arguments then "" else " " ^ print_properties arguments))]); fun log_command ({name, pos, ...}: command) body = XML.Elem (("command", (Markup.nameN, name) :: Position.properties_of pos), body); fun log_report props body = XML.Elem (("report", props), body); (* apply actions *) fun apply_action index name arguments timeout commands thy = let val action = #2 (Name_Space.check (Context.Theory thy) (Data.get thy) (name, Position.none)); val tag = "#" ^ Value.print_int index ^ " " ^ name ^ ": "; val context = {index = index, tag = tag, arguments = arguments, timeout = timeout, theory = thy}; val export_body = action context commands; val export_head = log_action name arguments; val export_name = Path.binding0 (Path.basic "mirabelle" + Path.basic (Value.print_int index)); in if null export_body then () else Export.export thy export_name (export_head :: export_body) end; fun print_exn exn = (case exn of Timeout.TIMEOUT _ => "timeout" | ERROR msg => "error: " ^ msg | exn => "exception:\n" ^ General.exnMessage exn); fun command_action binding action = let fun apply context command = let val s = action context command handle exn => if Exn.is_interrupt exn then Exn.reraise exn else #tag context ^ print_exn exn; in if s = "" then NONE else SOME (log_command command [XML.Text s]) end; in theory_action binding (map_filter o apply) end; (* theory line range *) local val theory_name = Scan.many1 (Symbol_Pos.symbol #> (fn s => Symbol.not_eof s andalso s <> "[")) >> Symbol_Pos.content; val line = Symbol_Pos.scan_nat >> (Symbol_Pos.content #> Value.parse_nat); val end_line = Symbol_Pos.$$ ":" |-- line; val range = Symbol_Pos.$$ "[" |-- line -- Scan.option end_line --| Symbol_Pos.$$ "]"; in fun read_theory_range str = (case Scan.read Symbol_Pos.stopper (theory_name -- Scan.option range) (Symbol_Pos.explode0 str) of SOME res => res | NONE => error ("Malformed specification of theory line range: " ^ quote str)); end; fun check_theories strs = let val theories = map read_theory_range strs; fun get_theory name = if null theories then SOME NONE else get_first (fn (a, b) => if a = name then SOME b else NONE) theories; fun check_line NONE _ = false | check_line _ NONE = true | check_line (SOME NONE) _ = true | check_line (SOME (SOME (line, NONE))) (SOME i) = line <= i | check_line (SOME (SOME (line, SOME end_line))) (SOME i) = line <= i andalso i <= end_line; fun check_pos range = check_line range o Position.line_of; in check_pos o get_theory end; +fun check_session qualifier thy_name (_: Position.T) = + Resources.theory_qualifier thy_name = qualifier; + (* presentation hook *) val whitelist = ["apply", "by", "proof"]; val _ = - Theory.setup (Thy_Info.add_presentation (fn context => fn thy => + Build.add_hook (fn qualifier => fn loaded_theories => let - val {options, adjust_pos, segments, ...} = context; - val mirabelle_timeout = Options.seconds options \<^system_option>\mirabelle_timeout\; - val mirabelle_stride = Options.int options \<^system_option>\mirabelle_stride\; - val mirabelle_actions = Options.string options \<^system_option>\mirabelle_actions\; - val mirabelle_theories = Options.string options \<^system_option>\mirabelle_theories\; + val mirabelle_timeout = Options.default_seconds \<^system_option>\mirabelle_timeout\; + val mirabelle_stride = Options.default_int \<^system_option>\mirabelle_stride\; + val mirabelle_actions = Options.default_string \<^system_option>\mirabelle_actions\; + val mirabelle_theories = Options.default_string \<^system_option>\mirabelle_theories\; val actions = (case read_actions mirabelle_actions of SOME actions => actions | NONE => error ("Failed to parse mirabelle_actions: " ^ quote mirabelle_actions)); - val check = check_theories (space_explode "," mirabelle_theories); - val commands = - segments - |> map_index (fn (n, {command = tr, prev_state = st, state = st', ...}) => - if n mod mirabelle_stride = 0 then - let - val name = Toplevel.name_of tr; - val pos = adjust_pos (Toplevel.pos_of tr); - in - if can (Proof.assert_backward o Toplevel.proof_of) st andalso - member (op =) whitelist name andalso - check (Context.theory_long_name thy) pos - then SOME {name = name, pos = pos, pre = Toplevel.proof_of st, post = st'} - else NONE - end - else NONE) - |> map_filter I; + val check = + if mirabelle_theories = "" then check_session qualifier + else check_theories (space_explode "," mirabelle_theories); - fun apply (i, (name, arguments)) () = - apply_action (i + 1) name arguments mirabelle_timeout commands thy; - in if null commands then () else fold_index apply actions () end)); + fun theory_commands (thy, segments) = + let + val commands = segments + |> map_index (fn (n, {command = tr, prev_state = st, state = st', ...}) => + if n mod mirabelle_stride = 0 then + let + val name = Toplevel.name_of tr; + val pos = Toplevel.pos_of tr; + in + if can (Proof.assert_backward o Toplevel.proof_of) st andalso + member (op =) whitelist name andalso + check (Context.theory_long_name thy) pos + then SOME {name = name, pos = pos, pre = Toplevel.proof_of st, post = st'} + else NONE + end + else NONE) + |> map_filter I; + in if null commands then NONE else SOME (thy, commands) end; + + fun app_actions (thy, commands) = + (actions, ()) |-> fold_index (fn (index, (name, arguments)) => fn () => + apply_action (index + 1) name arguments mirabelle_timeout commands thy); + in + if null actions then () + else List.app app_actions (map_filter theory_commands loaded_theories) + end); (* Mirabelle utility functions *) fun can_apply time tac st = let val {context = ctxt, facts, goal} = Proof.goal st; val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt); in (case try (Timeout.apply time (Seq.pull o full_tac)) goal of SOME (SOME _) => true | _ => false) end; local fun fold_body_thms f = let fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) => fn (x, seen) => if Inttab.defined seen i then (x, seen) else let val name = Proofterm.thm_node_name thm_node; val prop = Proofterm.thm_node_prop thm_node; val body = Future.join (Proofterm.thm_node_body thm_node); val (x', seen') = app (n + (if name = "" then 0 else 1)) body (x, Inttab.update (i, ()) seen); in (x' |> n = 0 ? f (name, prop, body), seen') end); in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end; in fun theorems_in_proof_term thy thm = let val all_thms = Global_Theory.all_thms_of thy true; fun collect (s, _, _) = if s <> "" then insert (op =) s else I; fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE; fun resolve_thms names = map_filter (member_of names) all_thms; in resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) end; end; fun theorems_of_sucessful_proof st = (case try Toplevel.proof_of st of NONE => [] | SOME prf => theorems_in_proof_term (Proof.theory_of prf) (#goal (Proof.goal prf))); fun get_argument arguments (key, default) = the_default default (AList.lookup (op =) arguments key); fun get_int_argument arguments (key, default) = (case Option.map Int.fromString (AList.lookup (op =) arguments key) of SOME (SOME i) => i | SOME NONE => error ("bad option: " ^ key) | NONE => default); fun get_bool_argument arguments (key, default) = (case Option.map Bool.fromString (AList.lookup (op =) arguments key) of SOME (SOME i) => i | SOME NONE => error ("bad option: " ^ key) | NONE => default); fun cpu_time f x = let val ({cpu, ...}, y) = Timing.timing f x in (y, Time.toMilliseconds cpu) end; end diff --git a/src/HOL/Tools/Mirabelle/mirabelle.scala b/src/HOL/Tools/Mirabelle/mirabelle.scala --- a/src/HOL/Tools/Mirabelle/mirabelle.scala +++ b/src/HOL/Tools/Mirabelle/mirabelle.scala @@ -1,272 +1,272 @@ /* Title: HOL/Tools/Mirabelle/mirabelle.scala Author: Makarius Isabelle/Scala front-end for Mirabelle. */ package isabelle.mirabelle import isabelle._ object Mirabelle { /* actions and options */ def action_names(): List[String] = { val Pattern = """Mirabelle action: "(\w+)".*""".r (for { file <- File.find_files(Path.explode("~~/src/HOL/Tools/Mirabelle").file, pred = _.getName.endsWith(".ML")) line <- split_lines(File.read(file)) name <- line match { case Pattern(a) => Some(a) case _ => None } } yield name).sorted } def sledgehammer_options(): List[String] = { val Pattern = """val .*K *= *"(.*)" *\(\*(.*)\*\)""".r split_lines(File.read(Path.explode("~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML"))). flatMap(line => line match { case Pattern(a, b) => Some (a + b) case _ => None }) } /* exported log content */ object Log { def export_name(index: Int, theory: String = ""): String = Export.compound_name(theory, "mirabelle/" + index) val separator = "\n------------------\n" sealed abstract class Entry { def print: String } case class Action(name: String, arguments: Properties.T, body: XML.Body) extends Entry { def print: String = "action: " + XML.content(body) + separator } case class Command(name: String, position: Properties.T, body: XML.Body) extends Entry { def print: String = "\n" + print_head + separator + Pretty.string_of(body) def print_head: String = { val line = Position.Line.get(position) val offset = Position.Offset.get(position) val loc = line.toString + ":" + offset.toString "at " + loc + " (" + name + "):" } } case class Report(result: Properties.T, body: XML.Body) extends Entry { override def print: String = "\n" + separator + Pretty.string_of(body) } def entry(export_name: String, xml: XML.Tree): Entry = xml match { case XML.Elem(Markup("action", (Markup.NAME, name) :: props), body) => Action(name, props, body) case XML.Elem(Markup("command", (Markup.NAME, name) :: props), body) => Command(name, props.filter(Markup.position_property), body) case XML.Elem(Markup("report", props), body) => Report(props, body) case _ => error("Malformed export " + quote(export_name) + "\nbad XML: " + xml) } } /* main mirabelle */ def mirabelle( options: Options, actions: List[String], output_dir: Path, theories: List[String] = Nil, selection: Sessions.Selection = Sessions.Selection.empty, progress: Progress = new Progress, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, numa_shuffling: Boolean = false, max_jobs: Int = 1, verbose: Boolean = false): Build.Results = { require(!selection.requirements) progress.echo("Building required heaps ...") val build_results0 = Build.build(options, build_heap = true, selection = selection.copy(requirements = true), progress = progress, dirs = dirs, select_dirs = select_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = verbose) if (build_results0.ok) { val build_options = - options + "timeout_build=false" + "parallel_presentation=false" + + options + "timeout_build=false" + ("mirabelle_actions=" + actions.mkString(";")) + ("mirabelle_theories=" + theories.mkString(",")) progress.echo("Running Mirabelle ...") val build_results = Build.build(build_options, clean_build = true, selection = selection, progress = progress, dirs = dirs, select_dirs = select_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = verbose) if (build_results.ok) { val structure = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs) val store = Sessions.store(build_options) using(store.open_database_context())(db_context => { var seen_theories = Set.empty[String] for { session <- structure.imports_selection(selection).iterator session_hierarchy = structure.hierarchy(session) theories <- db_context.input_database(session)((db, a) => Some(store.read_theories(db, a))) theory <- theories if !seen_theories(theory) index <- 1 to actions.length export <- db_context.read_export(session_hierarchy, theory, Log.export_name(index)) body = export.uncompressed_yxml if body.nonEmpty } { seen_theories += theory val export_name = Log.export_name(index, theory = theory) val log = body.map(Log.entry(export_name, _)) val log_dir = Isabelle_System.make_directory(output_dir + Path.basic(theory)) val log_file = log_dir + Path.basic("mirabelle" + index).log progress.echo("Writing " + log_file) File.write(log_file, terminate_lines(log.map(_.print))) } }) } build_results } else build_results0 } /* Isabelle tool wrapper */ val default_output_dir: Path = Path.explode("mirabelle") val isabelle_tool = Isabelle_Tool("mirabelle", "testing tool for automated proof tools", Scala_Project.here, args => { val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) var actions: List[String] = Nil var base_sessions: List[String] = Nil var select_dirs: List[Path] = Nil var numa_shuffling = false var output_dir = default_output_dir var theories: List[String] = Nil var exclude_session_groups: List[String] = Nil var all_sessions = false var dirs: List[Path] = Nil var session_groups: List[String] = Nil var max_jobs = 1 var options = Options.init(opts = build_options) var verbose = false var exclude_sessions: List[String] = Nil val default_stride = options.int("mirabelle_stride") val default_timeout = options.seconds("mirabelle_timeout") val getopts = Getopts(""" Usage: isabelle mirabelle [OPTIONS] [SESSIONS ...] Options are: -A ACTION add to list of actions -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -N cyclic shuffling of NUMA CPU nodes (performance tuning) -O DIR output directory for log files (default: """ + default_output_dir + """) -T THEORY theory restriction: NAME or NAME[LINE:END_LINE] -X NAME exclude sessions from group NAME and all descendants -a select all sessions -d DIR include session directory -g NAME select session group NAME -j INT maximum number of parallel jobs (default 1) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -s INT run actions on every nth goal (default """ + default_stride + """) -t SECONDS timeout for each action (default """ + default_timeout + """) -v verbose -x NAME exclude session NAME and all descendants Apply the given actions at all theories and proof steps of the specified sessions. The absence of theory restrictions (option -T) means to check all theories fully. Otherwise only the named theories are checked. Each ACTION is either of the form NAME or NAME [OPTION, ...] following Isabelle/Isar outer syntax. Available actions are:""" + action_names().mkString("\n ", "\n ", "") + """ For the ACTION "sledgehammer", the following OPTIONs are available:""" + sledgehammer_options().mkString("\n ", "\n ", "\n"), "A:" -> (arg => actions = actions ::: List(arg)), "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "N" -> (_ => numa_shuffling = true), "O:" -> (arg => output_dir = Path.explode(arg)), "T:" -> (arg => theories = theories ::: List(arg)), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), "a" -> (_ => all_sessions = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "g:" -> (arg => session_groups = session_groups ::: List(arg)), "j:" -> (arg => max_jobs = Value.Int.parse(arg)), "o:" -> (arg => options = options + arg), "s:" -> (arg => options = options + ("mirabelle_stride=" + arg)), "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) val sessions = getopts(args) if (actions.isEmpty) getopts.usage() val progress = new Console_Progress(verbose = verbose) val start_date = Date.now() if (verbose) { progress.echo("Started at " + Build_Log.print_date(start_date)) } val results = progress.interrupt_handler { mirabelle(options, actions, output_dir, theories = theories, selection = Sessions.Selection( all_sessions = all_sessions, base_sessions = base_sessions, exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions, session_groups = session_groups, sessions = sessions), progress = progress, dirs = dirs, select_dirs = select_dirs, numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling), max_jobs = max_jobs, verbose = verbose) } val end_date = Date.now() val elapsed_time = end_date.time - start_date.time if (verbose) { progress.echo("\nFinished at " + Build_Log.print_date(end_date)) } val total_timing = results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _). copy(elapsed = elapsed_time) progress.echo(total_timing.message_resources) sys.exit(results.rc) }) } diff --git a/src/Pure/Thy/thy_info.ML b/src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML +++ b/src/Pure/Thy/thy_info.ML @@ -1,467 +1,455 @@ (* Title: Pure/Thy/thy_info.ML Author: Makarius Global theory info database, with auto-loading according to theory and file dependencies, and presentation of theory documents. *) signature THY_INFO = sig type presentation_context = {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, segments: Document_Output.segment list} val adjust_pos_properties: presentation_context -> Position.T -> Properties.T val apply_presentation: presentation_context -> theory -> unit val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory val get_names: unit -> string list val lookup_theory: string -> theory option val get_theory: string -> theory val master_directory: string -> Path.T val remove_thy: string -> unit - val use_theories: Options.T -> string -> (string * Position.T) list -> unit + val use_theories: Options.T -> string -> (string * Position.T) list -> + (theory * Document_Output.segment list) list val use_thy: string -> unit val script_thy: Position.T -> string -> theory -> theory val register_thy: theory -> unit val finish: unit -> unit end; structure Thy_Info: THY_INFO = struct (** theory presentation **) (* hook for consolidated theory *) type presentation_context = {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, segments: Document_Output.segment list}; fun adjust_pos_properties (context: presentation_context) pos = Position.offset_properties_of (#adjust_pos context pos) @ Position.id_properties_of pos; structure Presentation = Theory_Data ( type T = ((presentation_context -> theory -> unit) * stamp) list; val empty = []; val extend = I; fun merge data : T = Library.merge (eq_snd op =) data; ); -fun sequential_presentation options = - not (Options.bool options \<^system_option>\parallel_presentation\); - fun apply_presentation (context: presentation_context) thy = - Par_List.map' - {name = "apply_presentation", sequential = sequential_presentation (#options context)} - (fn (f, _) => f context thy) (Presentation.get thy) - |> ignore; + ignore (Par_List.map (fn (f, _) => f context thy) (Presentation.get thy)); fun add_presentation f = Presentation.map (cons (f, stamp ())); val _ = - Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => + Theory.setup (add_presentation (fn {options, segments, ...} => fn thy => if exists (Toplevel.is_skipped_proof o #state) segments then () else let val body = Document_Output.present_thy options thy segments; in if Options.string options "document" = "false" then () else let val thy_name = Context.theory_name thy; val latex = Latex.isabelle_body thy_name body; in Export.export thy \<^path_binding>\document/latex\ latex end end)); (** thy database **) (* messages *) val show_path = space_implode " via " o map quote; fun cycle_msg names = "Cyclic dependency of " ^ show_path names; (* derived graph operations *) fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); fun new_entry name parents entry = String_Graph.new_node (name, entry) #> add_deps name parents; (* global thys *) type deps = {master: (Path.T * SHA1.digest), (*master dependencies for thy file*) imports: (string * Position.T) list}; (*source specification of imports (partially qualified)*) fun make_deps master imports : deps = {master = master, imports = imports}; fun master_dir_deps (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d); local val global_thys = Synchronized.var "Thy_Info.thys" (String_Graph.empty: (deps option * theory option) String_Graph.T); in fun get_thys () = Synchronized.value global_thys; fun change_thys f = Synchronized.change global_thys f; end; fun get_names () = String_Graph.topological_order (get_thys ()); (* access thy *) fun lookup thys name = try (String_Graph.get_node thys) name; fun lookup_thy name = lookup (get_thys ()) name; fun get thys name = (case lookup thys name of SOME thy => thy | NONE => error ("Theory loader: nothing known about theory " ^ quote name)); fun get_thy name = get (get_thys ()) name; (* access deps *) val lookup_deps = Option.map #1 o lookup_thy; val master_directory = master_dir_deps o #1 o get_thy; (* access theory *) fun lookup_theory name = (case lookup_thy name of SOME (_, SOME theory) => SOME theory | _ => NONE); fun get_theory name = (case lookup_theory name of SOME theory => theory | _ => error ("Theory loader: undefined entry for theory " ^ quote name)); val get_imports = Resources.imports_of o get_theory; (** thy operations **) (* remove *) fun remove name thys = (case lookup thys name of NONE => thys | SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name) | SOME _ => let val succs = String_Graph.all_succs thys [name]; val _ = writeln ("Theory loader: removing " ^ commas_quote succs); in fold String_Graph.del_node succs thys end); val remove_thy = change_thys o remove; (* update *) fun update deps theory thys = let val name = Context.theory_long_name theory; val parents = map Context.theory_long_name (Theory.parents_of theory); val thys' = remove name thys; val _ = map (get thys') parents; in new_entry name parents (SOME deps, SOME theory) thys' end; fun update_thy deps theory = change_thys (update deps theory); (* scheduling loader tasks *) datatype result = - Result of {theory: theory, exec_id: Document_ID.exec, - present: (unit -> unit) option, commit: unit -> unit}; + Result of + {theory: theory, + exec_id: Document_ID.exec, + present: unit -> presentation_context option, + commit: unit -> unit}; fun theory_result theory = - Result {theory = theory, exec_id = Document_ID.none, present = NONE, commit = I}; + Result + {theory = theory, + exec_id = Document_ID.none, + present = K NONE, + commit = I}; fun result_theory (Result {theory, ...}) = theory; -fun result_present (Result {present, ...}) = present; fun result_commit (Result {commit, ...}) = commit; -fun join_theory (Result {theory, exec_id, ...}) = - let - val _ = Execution.join [exec_id]; - val res = Exn.capture Thm.consolidate_theory theory; - val exns = maps Task_Queue.group_status (Execution.peek exec_id); - in res :: map Exn.Exn exns end; +fun consolidate_theory (Exn.Exn exn) = [Exn.Exn exn] + | consolidate_theory (Exn.Res (Result {theory, exec_id, ...})) = + let + val _ = Execution.join [exec_id]; + val res = Exn.capture Thm.consolidate_theory theory; + val exns = maps Task_Queue.group_status (Execution.peek exec_id); + in res :: map Exn.Exn exns end; + +fun present_theory (Exn.Exn exn) = [Exn.Exn exn] + | present_theory (Exn.Res (Result {theory, present, ...})) = + (case present () of + NONE => [] + | SOME (context as {segments, ...}) => + [Exn.capture (fn () => (apply_presentation context theory; (theory, segments))) ()]); + datatype task = Task of string list * (theory list -> result) | Finished of theory; -fun task_finished (Task _) = false - | task_finished (Finished _) = true; - -fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents; +val schedule_theories = Thread_Attributes.uninterruptible (fn _ => fn tasks => + let + fun join_parents deps name parents = + (case map #1 (filter (not o can Future.join o #2) deps) of + [] => map (result_theory o Future.join o the o AList.lookup (op =) deps) parents + | bad => + error ("Failed to load theory " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")")); -val schedule_seq = - String_Graph.schedule (fn deps => fn (_, task) => - (case task of - Task (parents, body) => - let - val result = body (task_parents deps parents); - val _ = Par_Exn.release_all (join_theory result); - val _ = (case result_present result of NONE => () | SOME present => present ()); - val _ = result_commit result (); - in result_theory result end - | Finished thy => thy)) #> ignore; - -val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks => - let val futures = tasks |> String_Graph.schedule (fn deps => fn (name, task) => (case task of Task (parents, body) => - (singleton o Future.forks) - {name = "theory:" ^ name, group = NONE, - deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true} - (fn () => - (case filter (not o can Future.join o #2) deps of - [] => body (map (result_theory o Future.join) (task_parents deps parents)) - | bad => - error - ("Failed to load theory " ^ quote name ^ - " (unresolved " ^ commas_quote (map #1 bad) ^ ")"))) + if Multithreading.max_threads () > 1 then + (singleton o Future.forks) + {name = "theory:" ^ name, group = NONE, + deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true} + (fn () => body (join_parents deps name parents)) + else + Future.value_result (Exn.capture (fn () => body (join_parents deps name parents)) ()) | Finished theory => Future.value (theory_result theory))); - val results1 = futures - |> maps (fn future => - (case Future.join_result future of - Exn.Res result => join_theory result - | Exn.Exn exn => [Exn.Exn exn])); + val results1 = futures |> maps (consolidate_theory o Future.join_result); - val results2 = futures - |> map_filter (Option.mapPartial result_present o Exn.get_res o Future.join_result) - |> Par_List.map' - {name = "present", sequential = sequential_presentation (Options.default ())} - (fn present => Exn.capture present ()); + val present_results = futures |> maps (present_theory o Future.join_result); + val results2 = (map o Exn.map_res) (K ()) present_results; val results3 = futures |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ()); - (* FIXME avoid global Execution.reset (!??) *) val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ())); val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4); - in () end); + in Par_Exn.release_all present_results end); (* eval theory *) fun eval_thy options master_dir header text_pos text parents = let val (name, _) = #name header; val keywords = fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents (Keyword.add_keywords (#keywords header) Keyword.empty_keywords); val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text); val elements = Thy_Element.parse_elements keywords spans; val text_id = Position.copy_id text_pos Position.none; fun init () = Resources.begin_theory master_dir header parents; fun excursion () = let fun element_result span_elem (st, _) = let fun prepare span = let val tr = Position.setmp_thread_data text_id (fn () => Command.read_span keywords st master_dir init span) (); in Toplevel.timing (Resources.last_timing tr) tr end; val elem = Thy_Element.map_element prepare span_elem; val (results, st') = Toplevel.element_result keywords elem st; val pos' = Toplevel.pos_of (Thy_Element.last_element elem); in (results, (st', pos')) end; val (results, (end_state, end_pos)) = fold_map element_result elements (Toplevel.init_toplevel (), Position.none); val thy = Toplevel.end_theory end_pos end_state; in (results, thy) end; val (results, thy) = cond_timeit true ("theory " ^ quote name) excursion; - fun present () = + fun present () : presentation_context = let val segments = (spans ~~ maps Toplevel.join_results results) |> map (fn (span, (st, tr, st')) => {span = span, prev_state = st, command = tr, state = st'}); - val context: presentation_context = - {options = options, file_pos = text_pos, adjust_pos = I, segments = segments}; - in apply_presentation context thy end; + in {options = options, file_pos = text_pos, adjust_pos = I, segments = segments} end; in (thy, present) end; (* require_thy -- checking database entries wrt. the file-system *) local fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; fun load_thy options initiators deps text (name, header_pos) keywords parents = let val {master = (thy_path, _), imports} = deps; val dir = Path.dir thy_path; val exec_id = Document_ID.make (); val id = Document_ID.print exec_id; val put_id = Position.put_id id; val _ = Execution.running Document_ID.none exec_id [] orelse raise Fail ("Failed to register execution: " ^ id); val text_pos = put_id (Path.position thy_path); val text_props = Position.properties_of text_pos; val _ = remove_thy name; val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) [XML.blob [text]]; val _ = Position.setmp_thread_data (Position.id_only id) (fn () => (parents, map #2 imports) |> ListPair.app (fn (thy, pos) => Context_Position.reports_global thy [(put_id pos, Theory.get_markup thy)])) (); val timing_start = Timing.start (); val header = Thy_Header.make (name, put_id header_pos) imports keywords; val (theory, present) = eval_thy options dir header text_pos text (if name = Context.PureN then [Context.the_global_context ()] else parents); val timing_result = Timing.result timing_start; val timing_props = [Markup.theory_timing, (Markup.nameN, name)]; val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) [] fun commit () = update_thy deps theory; - in Result {theory = theory, exec_id = exec_id, present = SOME present, commit = commit} end; + in Result {theory = theory, exec_id = exec_id, present = SOME o present, commit = commit} end; fun check_thy_deps dir name = (case lookup_deps name of SOME NONE => (true, NONE, Position.none, get_imports name, []) | NONE => let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end | SOME (SOME {master, ...}) => let val {master = master', text = text', theory_pos = theory_pos', imports = imports', keywords = keywords'} = Resources.check_thy dir name; val deps' = SOME (make_deps master' imports', text'); val current = #2 master = #2 master' andalso (case lookup_theory name of NONE => false | SOME theory => Resources.loaded_files_current theory); in (current, deps', theory_pos', imports', keywords') end); +fun task_finished (Task _) = false + | task_finished (Finished _) = true; + in fun require_thys options initiators qualifier dir strs tasks = fold_map (require_thy options initiators qualifier dir) strs tasks |>> forall I and require_thy options initiators qualifier dir (s, require_pos) tasks = let val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s; in (case try (String_Graph.get_node tasks) theory_name of SOME task => (task_finished task, tasks) | NONE => let val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators); val (current, deps, theory_pos, imports, keywords) = check_thy_deps master_dir theory_name handle ERROR msg => cat_error msg ("The error(s) above occurred for theory " ^ quote theory_name ^ Position.here require_pos ^ required_by "\n" initiators); val qualifier' = Resources.theory_qualifier theory_name; val dir' = dir + master_dir_deps (Option.map #1 deps); val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports; val (parents_current, tasks') = require_thys options (theory_name :: initiators) qualifier' dir' imports tasks; val all_current = current andalso parents_current; val task = if all_current then Finished (get_theory theory_name) else (case deps of NONE => raise Fail "Malformed deps" | SOME (dep, text) => Task (parents, load_thy options initiators dep text (theory_name, theory_pos) keywords)); val tasks'' = new_entry theory_name parents task tasks'; in (all_current, tasks'') end) end; end; (* use theories *) fun use_theories options qualifier imports = - let val (_, tasks) = require_thys options [] qualifier Path.current imports String_Graph.empty - in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end; + schedule_theories (#2 (require_thys options [] qualifier Path.current imports String_Graph.empty)); fun use_thy name = - use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)]; + ignore (use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)]); (* toplevel scripting -- without maintaining database *) fun script_thy pos txt thy = let val trs = Outer_Syntax.parse_text thy (K thy) pos txt; val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs); val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ()); in Toplevel.end_theory end_pos end_state end; (* register theory *) fun register_thy theory = let val name = Context.theory_long_name theory; val {master, ...} = Resources.check_thy (Resources.master_directory theory) name; val imports = Resources.imports_of theory; in change_thys (fn thys => let val thys' = remove name thys; val _ = writeln ("Registering theory " ^ quote name); in update (make_deps master imports) theory thys' end) end; (* finish all theories *) fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry))); end; fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name); diff --git a/src/Pure/Tools/build.ML b/src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML +++ b/src/Pure/Tools/build.ML @@ -1,99 +1,120 @@ (* Title: Pure/Tools/build.ML Author: Makarius Build Isabelle sessions. *) -structure Build: sig end = +signature BUILD = +sig + type hook = string -> (theory * Document_Output.segment list) list -> unit + val add_hook: hook -> unit +end; + +structure Build: BUILD = struct (* session timing *) fun session_timing f x = let val start = Timing.start (); val y = f x; val timing = Timing.result start; val threads = string_of_int (Multithreading.max_threads ()); val props = [("threads", threads)] @ Markup.timing_properties timing; val _ = Output.protocol_message (Markup.session_timing :: props) []; in y end; (* build theories *) +type hook = string -> (theory * Document_Output.segment list) list -> unit; + +local + val hooks = Synchronized.var "Build.hooks" ([]: hook list); +in + +fun add_hook hook = Synchronized.change hooks (cons hook); + +fun apply_hooks qualifier loaded_theories = + Synchronized.value hooks + |> List.app (fn hook => hook qualifier loaded_theories); + +end; + + fun build_theories qualifier (options, thys) = let val condition = space_explode "," (Options.string options "condition"); val conds = filter_out (can getenv_strict) condition; - in - if null conds then - (Options.set_default options; - Isabelle_Process.init_options (); - Future.fork I; - (Thy_Info.use_theories options qualifier - |> - (case Options.string options "profiling" of - "" => I - | "time" => profile_time - | "allocations" => profile_allocations - | bad => error ("Bad profiling option: " ^ quote bad)) - |> Unsynchronized.setmp print_mode - (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) - else - Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ - " (undefined " ^ commas conds ^ ")\n") - end; + val loaded_theories = + if null conds then + (Options.set_default options; + Isabelle_Process.init_options (); + Future.fork I; + (Thy_Info.use_theories options qualifier + |> + (case Options.string options "profiling" of + "" => I + | "time" => profile_time + | "allocations" => profile_allocations + | bad => error ("Bad profiling option: " ^ quote bad)) + |> Unsynchronized.setmp print_mode + (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) + else + (Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ + " (undefined " ^ commas conds ^ ")\n"); []) + in apply_hooks qualifier loaded_theories end; (* build session *) val _ = Protocol_Command.define "build_session" (fn [resources_yxml, args_yxml] => let val _ = Resources.init_session_yxml resources_yxml; val (session_name, theories) = YXML.parse_body args_yxml |> let open XML.Decode; val position = Position.of_properties o properties; in pair string (list (pair Options.decode (list (pair string position)))) end; val _ = Session.init session_name; fun build () = let val res1 = theories |> (List.app (build_theories session_name) |> session_timing |> Exn.capture); val res2 = Exn.capture Session.finish (); val _ = Resources.finish_session_base (); val _ = Par_Exn.release_all [res1, res2]; val _ = if session_name = Context.PureN then Theory.install_pure (Thy_Info.get_theory Context.PureN) else (); in () end; fun exec e = if can Theory.get_pure () then Isabelle_Thread.fork {name = "build_session", stack_limit = Isabelle_Thread.stack_limit (), interrupts = false} e |> ignore else e (); in exec (fn () => (Future.interruptible_task (fn () => (build (); (0, []))) () handle exn => ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"]))) |> let open XML.Encode in pair int (list string) end |> single |> Output.protocol_message Markup.build_session_finished) end | _ => raise Match); end;