# HG changeset patch # User wenzelm # Date 1343159321 -7200 # Node ID 6f2bcc0a16e067d55b8d63a3399e4714a5adab86 # Parent 1959baa226321b1342bd803ad1931eb02cb7742d# Parent e06ea2327cc5aeb2dd90fc862ca8f22fbede5461 merged diff -r 1959baa22632 -r 6f2bcc0a16e0 etc/options --- a/etc/options Tue Jul 24 12:36:59 2012 +0200 +++ b/etc/options Tue Jul 24 21:48:41 2012 +0200 @@ -1,24 +1,30 @@ (* :mode=isabelle-options: *) declare browser_info : bool = false +declare browser_info_remote : string = "" -declare document : bool = true -declare document_format : string = pdf -declare document_variants : string = document +declare document : string = "" +declare document_variants : string = "outline=/proof,/ML" declare document_graph : bool = false +declare document_dump : string = "" +declare document_dump_only : bool = false +declare no_document : bool = false -declare threads_limit : int = 1 +declare threads : int = 0 declare threads_trace : int = 0 -declare parallel_proofs : int = 1 +declare parallel_proofs : int = 2 declare parallel_proofs_threshold : int = 100 declare print_mode : string = "" -declare proofs : int = 0 +declare proofs : int = 1 declare quick_and_dirty : bool = false -declare timing : bool = false -declare verbose : bool = false - declare condition : string = "" +declare show_question_marks : bool = true + +declare names_long : bool = false +declare names_short : bool = false +declare names_unique : bool = true + diff -r 1959baa22632 -r 6f2bcc0a16e0 etc/settings --- a/etc/settings Tue Jul 24 12:36:59 2012 +0200 +++ b/etc/settings Tue Jul 24 21:48:41 2012 +0200 @@ -67,11 +67,15 @@ ### -### Batch sessions (cf. isabelle usedir) +### Batch sessions ### +#cf. isabelle usedir ISABELLE_USEDIR_OPTIONS="-M max -p 1 -q 2 -v true -V outline=/proof,/ML" +#cf. isabelle build +ISABELLE_BUILD_OPTIONS="" + ### ### Document preparation (cf. isabelle latex/document) diff -r 1959baa22632 -r 6f2bcc0a16e0 lib/Tools/build --- a/lib/Tools/build Tue Jul 24 12:36:59 2012 +0200 +++ b/lib/Tools/build Tue Jul 24 21:48:41 2012 +0200 @@ -9,6 +9,17 @@ PRG="$(basename "$0")" +function show_settings() +{ + local PREFIX="$1" + echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\"" + echo + echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\"" + echo "${PREFIX}ML_HOME=\"$ML_HOME\"" + echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\"" + echo "${PREFIX}ML_OPTIONS=\"$ML_OPTIONS\"" +} + function usage() { echo @@ -19,18 +30,14 @@ echo " -b build target images" echo " -d DIR additional session directory with ROOT file" echo " -j INT maximum number of jobs (default 1)" - echo " -l list sessions only" + echo " -n no build -- test dependencies only" echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)" echo " -s system build mode: produce output in ISABELLE_HOME" + echo " -t inner session timing" echo " -v verbose" echo echo " Build and manage Isabelle sessions, depending on implicit" - echo " ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\"" - echo - echo " ML_PLATFORM=\"$ML_PLATFORM\"" - echo " ML_HOME=\"$ML_HOME\"" - echo " ML_SYSTEM=\"$ML_SYSTEM\"" - echo " ML_OPTIONS=\"$ML_OPTIONS\"" + show_settings " " echo exit 1 } @@ -52,14 +59,15 @@ ALL_SESSIONS=false BUILD_IMAGES=false MAX_JOBS=1 -LIST_ONLY=false +NO_BUILD=false SYSTEM_MODE=false +TIMING=false VERBOSE=false declare -a MORE_DIRS=() eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)" -while getopts "abd:j:lo:sv" OPT +while getopts "abd:j:no:stv" OPT do case "$OPT" in a) @@ -75,8 +83,8 @@ check_number "$OPTARG" MAX_JOBS="$OPTARG" ;; - l) - LIST_ONLY="true" + n) + NO_BUILD="true" ;; o) BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG" @@ -84,6 +92,9 @@ s) SYSTEM_MODE="true" ;; + t) + TIMING="true" + ;; v) VERBOSE="true" ;; @@ -100,6 +111,26 @@ [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } -exec "$ISABELLE_TOOL" java isabelle.Build \ - "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$SYSTEM_MODE" "$VERBOSE" \ - "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" +if [ "$NO_BUILD" = false ]; then + echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" + + if [ "$VERBOSE" = true ]; then + show_settings "" + echo + fi + . "$ISABELLE_HOME/lib/scripts/timestart.bash" +fi + +"$ISABELLE_TOOL" java isabelle.Build \ + "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" \ + "$VERBOSE" "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" +RC="$?" + +if [ "$NO_BUILD" = false ]; then + echo -n "Finished at "; date + + . "$ISABELLE_HOME/lib/scripts/timestop.bash" + echo "$TIMES_REPORT" +fi + +exit "$RC" diff -r 1959baa22632 -r 6f2bcc0a16e0 lib/scripts/getsettings --- a/lib/scripts/getsettings Tue Jul 24 12:36:59 2012 +0200 +++ b/lib/scripts/getsettings Tue Jul 24 21:48:41 2012 +0200 @@ -51,6 +51,10 @@ #platform source "$ISABELLE_HOME/lib/scripts/isabelle-platform" +if [ -z "$ISABELLE_PLATFORM" ]; then + echo 1>&2 "Failed to determine hardware and operating system type!" + exit 2 +fi #Isabelle distribution identifier -- filled in automatically! ISABELLE_ID="" diff -r 1959baa22632 -r 6f2bcc0a16e0 lib/scripts/isabelle-platform --- a/lib/scripts/isabelle-platform Tue Jul 24 12:36:59 2012 +0200 +++ b/lib/scripts/isabelle-platform Tue Jul 24 21:48:41 2012 +0200 @@ -4,17 +4,17 @@ # # NOTE: The ML system or JVM may have their own idea about the platform! -ISABELLE_PLATFORM="unknown-platform" +ISABELLE_PLATFORM32="" ISABELLE_PLATFORM64="" case $(uname -s) in Linux) case $(uname -m) in i?86) - ISABELLE_PLATFORM=x86-linux + ISABELLE_PLATFORM32=x86-linux ;; x86_64) - ISABELLE_PLATFORM=x86-linux + ISABELLE_PLATFORM32=x86-linux ISABELLE_PLATFORM64=x86_64-linux ;; esac @@ -22,47 +22,32 @@ Darwin) case $(uname -m) in i?86) - ISABELLE_PLATFORM=x86-darwin + ISABELLE_PLATFORM32=x86-darwin if [ "$(sysctl -n hw.optional.x86_64 2>/dev/null)" = 1 ]; then ISABELLE_PLATFORM64=x86_64-darwin fi ;; x86_64) - ISABELLE_PLATFORM=x86-darwin + ISABELLE_PLATFORM32=x86-darwin ISABELLE_PLATFORM64=x86_64-darwin ;; - Power* | power* | ppc) - ISABELLE_PLATFORM=ppc-darwin - ;; esac ;; CYGWIN_NT*) case $(uname -m) in i?86 | x86_64) - ISABELLE_PLATFORM=x86-cygwin - ;; - esac - ;; - SunOS) - case $(uname -r) in - 5.*) - case $(uname -p) in - sparc) - ISABELLE_PLATFORM=sparc-solaris - ;; - i?86 | x86_64) - ISABELLE_PLATFORM=x86-solaris - ;; - esac + ISABELLE_PLATFORM32=x86-cygwin ;; esac ;; *BSD) case $(uname -m) in i?86 | x86_64) - ISABELLE_PLATFORM=x86-linux + ISABELLE_PLATFORM32=x86-linux #cf. BSD Linux Binary Compatibility ;; esac ;; esac +ISABELLE_PLATFORM="$ISABELLE_PLATFORM32" + diff -r 1959baa22632 -r 6f2bcc0a16e0 src/CCL/ROOT --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/CCL/ROOT Tue Jul 24 21:48:41 2012 +0200 @@ -0,0 +1,23 @@ +session CCL! in "." = Pure + + description {* + Author: Martin Coen, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + + Classical Computational Logic based on First-Order Logic. + + A computational logic for an untyped functional language with + evaluation to weak head-normal form. + *} + options [document = false] + theories Wfd Fix + +session ex = CCL + + description {* + Author: Martin Coen, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + + Examples for Classical Computational Logic. + *} + options [document = false] + theories Nat List Stream Flag + diff -r 1959baa22632 -r 6f2bcc0a16e0 src/CCL/Set.thy --- a/src/CCL/Set.thy Tue Jul 24 12:36:59 2012 +0200 +++ b/src/CCL/Set.thy Tue Jul 24 21:48:41 2012 +0200 @@ -1,7 +1,7 @@ header {* Extending FOL by a modified version of HOL set theory *} theory Set -imports FOL +imports "~~/src/FOL/FOL" begin declare [[eta_contract]] diff -r 1959baa22632 -r 6f2bcc0a16e0 src/CTT/ROOT --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/CTT/ROOT Tue Jul 24 21:48:41 2012 +0200 @@ -0,0 +1,17 @@ +session CTT! in "." = Pure + + description {* + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1991 University of Cambridge + *} + options [document = false] + theories Main + +session ex = CTT + + description {* + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1991 University of Cambridge + + Examples for Constructive Type Theory. + *} + options [document = false] + theories Typechecking Elimination Equality Synthesis diff -r 1959baa22632 -r 6f2bcc0a16e0 src/Cube/ROOT --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Cube/ROOT Tue Jul 24 21:48:41 2012 +0200 @@ -0,0 +1,10 @@ +session Cube! in "." = Pure + + description {* + Author: Tobias Nipkow + Copyright 1992 University of Cambridge + + The Lambda-Cube a la Barendregt. + *} + options [document = false] + theories Example + diff -r 1959baa22632 -r 6f2bcc0a16e0 src/FOL/ROOT --- a/src/FOL/ROOT Tue Jul 24 12:36:59 2012 +0200 +++ b/src/FOL/ROOT Tue Jul 24 21:48:41 2012 +0200 @@ -1,4 +1,4 @@ -session FOL! (10) in "." = Pure + +session FOL! in "." = Pure + description "First-Order Logic with Natural Deduction" options [proofs = 2] theories FOL diff -r 1959baa22632 -r 6f2bcc0a16e0 src/FOLP/ROOT --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/FOLP/ROOT Tue Jul 24 21:48:41 2012 +0200 @@ -0,0 +1,32 @@ +session FOLP! in "." = Pure + + description {* + Author: Martin Coen, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + + Modifed version of FOL that contains proof terms. + + Presence of unknown proof term means that matching does not behave as expected. + *} + options [document = false] + theories FOLP + +session ex = FOLP + + description {* + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + + Examples for First-Order Logic. + *} + options [document = false] + theories + Intro + Nat + Foundation + If + Intuitionistic + Classical + Propositional_Int + Quantifiers_Int + Propositional_Cla + Quantifiers_Cla + diff -r 1959baa22632 -r 6f2bcc0a16e0 src/HOL/Decision_Procs/ex/Approximation_Ex.thy --- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Tue Jul 24 12:36:59 2012 +0200 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Tue Jul 24 21:48:41 2012 +0200 @@ -1,7 +1,7 @@ (* Author: Johannes Hoelzl 2009 *) theory Approximation_Ex -imports Complex_Main "~~/src/HOL/Decision_Procs/Approximation" +imports Complex_Main "../Approximation" begin text {* diff -r 1959baa22632 -r 6f2bcc0a16e0 src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy --- a/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy Tue Jul 24 12:36:59 2012 +0200 +++ b/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy Tue Jul 24 21:48:41 2012 +0200 @@ -3,7 +3,7 @@ header {* Some examples demonstrating the comm-ring method *} theory Commutative_Ring_Ex -imports Commutative_Ring +imports "../Commutative_Ring" begin lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243" diff -r 1959baa22632 -r 6f2bcc0a16e0 src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy --- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Tue Jul 24 12:36:59 2012 +0200 +++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Tue Jul 24 21:48:41 2012 +0200 @@ -3,7 +3,7 @@ header {* Examples for Ferrante and Rackoff's quantifier elimination procedure *} theory Dense_Linear_Order_Ex -imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" +imports "../Dense_Linear_Order" begin lemma diff -r 1959baa22632 -r 6f2bcc0a16e0 src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Tue Jul 24 12:36:59 2012 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Tue Jul 24 21:48:41 2012 +0200 @@ -3,7 +3,7 @@ header "Denotational Abstract Interpretation" theory Abs_Int_den0_fun -imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step +imports "~~/src/HOL/ex/Interpretation_with_Defs" "../Big_Step" begin subsection "Orderings" diff -r 1959baa22632 -r 6f2bcc0a16e0 src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Tue Jul 24 12:36:59 2012 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Tue Jul 24 21:48:41 2012 +0200 @@ -5,7 +5,7 @@ theory Abs_Int0_ITP imports "~~/src/HOL/ex/Interpretation_with_Defs" "~~/src/HOL/Library/While_Combinator" - Collecting + "../Collecting" begin subsection "Orderings" diff -r 1959baa22632 -r 6f2bcc0a16e0 src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Tue Jul 24 12:36:59 2012 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Tue Jul 24 21:48:41 2012 +0200 @@ -1,7 +1,7 @@ (* Author: Tobias Nipkow *) theory Abs_Int1_const_ITP -imports Abs_Int1_ITP Abs_Int_Tests +imports Abs_Int1_ITP "../Abs_Int_Tests" begin subsection "Constant Propagation" diff -r 1959baa22632 -r 6f2bcc0a16e0 src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Tue Jul 24 12:36:59 2012 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Tue Jul 24 21:48:41 2012 +0200 @@ -1,7 +1,7 @@ (* Author: Tobias Nipkow *) theory Abs_Int2_ITP -imports Abs_Int1_ITP Vars +imports Abs_Int1_ITP "../Vars" begin instantiation prod :: (preord,preord) preord diff -r 1959baa22632 -r 6f2bcc0a16e0 src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Tue Jul 24 12:36:59 2012 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Tue Jul 24 21:48:41 2012 +0200 @@ -1,7 +1,7 @@ (* Author: Tobias Nipkow *) theory Abs_Int2_ivl_ITP -imports Abs_Int2_ITP Abs_Int_Tests +imports Abs_Int2_ITP "../Abs_Int_Tests" begin subsection "Interval Analysis" diff -r 1959baa22632 -r 6f2bcc0a16e0 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jul 24 12:36:59 2012 +0200 +++ b/src/HOL/IsaMakefile Tue Jul 24 21:48:41 2012 +0200 @@ -57,6 +57,7 @@ HOL-Mutabelle \ HOL-NanoJava \ HOL-Nitpick_Examples \ + HOL-NSA-Examples \ HOL-Number_Theory \ HOL-Old_Number_Theory \ HOL-Quickcheck_Examples \ diff -r 1959baa22632 -r 6f2bcc0a16e0 src/HOL/NSA/Examples/NSPrimes.thy --- a/src/HOL/NSA/Examples/NSPrimes.thy Tue Jul 24 12:36:59 2012 +0200 +++ b/src/HOL/NSA/Examples/NSPrimes.thy Tue Jul 24 21:48:41 2012 +0200 @@ -23,10 +23,10 @@ choicefun :: "'a set => 'a" where "choicefun E = (@x. \X \ Pow(E) -{{}}. x : X)" -consts injf_max :: "nat => ('a::{order} set) => 'a" -primrec +primrec injf_max :: "nat => ('a::{order} set) => 'a" +where injf_max_zero: "injf_max 0 E = choicefun E" - injf_max_Suc: "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})" +| injf_max_Suc: "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})" lemma dvd_by_all: "\M. \N. 0 < N & (\m. 0 < m & (m::nat) <= M --> m dvd N)" diff -r 1959baa22632 -r 6f2bcc0a16e0 src/HOL/ROOT --- a/src/HOL/ROOT Tue Jul 24 12:36:59 2012 +0200 +++ b/src/HOL/ROOT Tue Jul 24 21:48:41 2012 +0200 @@ -2,7 +2,7 @@ description {* Classical Higher-order Logic *} options [document_graph] theories Complex_Main - files "document/root.tex" "document/root.bib" + files "document/root.bib" "document/root.tex" session "HOL-Base"! in "." = Pure + description {* Raw HOL base, with minimal tools *} @@ -19,11 +19,744 @@ options [document = false] theories Main -session "HOL-Proofs"! (2) in "." = Pure + +session "HOL-Proofs"! (4) in "." = Pure + description {* HOL-Main with proof terms *} options [document = false, proofs = 2, parallel_proofs = 0] theories Main +session Library = HOL + + description {* Classical Higher-order Logic -- batteries included *} + theories + Library + List_Prefix + List_lexord + Sublist_Order + Product_Lattice + Code_Char_chr + Code_Char_ord + Code_Integer + Efficient_Nat + (*"Code_Prolog" FIXME*) + Code_Real_Approx_By_Float + Target_Numeral + files "document/root.bib" "document/root.tex" + +session Hahn_Banach = HOL + + description {* + Author: Gertrud Bauer, TU Munich + + The Hahn-Banach theorem for real vector spaces. + *} + options [document_graph] + theories Hahn_Banach + files "document/root.bib" "document/root.tex" + +session Induct = HOL + + theories [quick_and_dirty] + Common_Patterns + theories + QuoDataType + QuoNestedDataType + Term + SList + ABexp + Tree + Ordinals + Sigma_Algebra + Comb + PropLog + Com + files "document/root.tex" + +session IMP = HOL + + options [document_graph] + theories [document = false] + "~~/src/HOL/ex/Interpretation_with_Defs" + "~~/src/HOL/Library/While_Combinator" + "~~/src/HOL/Library/Char_ord" + "~~/src/HOL/Library/List_lexord" + theories + BExp + ASM + Small_Step + Denotation + Comp_Rev + Poly_Types + Sec_Typing + Sec_TypingT + Def_Ass_Sound_Big + Def_Ass_Sound_Small + Live + Live_True + Hoare_Examples + VC + HoareT + Collecting1 + Collecting_list + Abs_Int_Tests + Abs_Int1_parity + Abs_Int1_const + Abs_Int3 + "Abs_Int_ITP/Abs_Int1_parity_ITP" + "Abs_Int_ITP/Abs_Int1_const_ITP" + "Abs_Int_ITP/Abs_Int3_ITP" + "Abs_Int_Den/Abs_Int_den2" + Procs_Dyn_Vars_Dyn + Procs_Stat_Vars_Dyn + Procs_Stat_Vars_Stat + C_like + OO + Fold + files "document/root.bib" "document/root.tex" + +session IMPP = HOL + + description {* + Author: David von Oheimb + Copyright 1999 TUM + *} + options [document = false] + theories EvenOdd + +session Import = HOL + + options [document_graph] + theories HOL_Light_Maps + theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import + +session Number_Theory = HOL + + options [document = false] + theories Number_Theory + +session Old_Number_Theory = HOL + + options [document_graph] + theories [document = false] + "~~/src/HOL/Library/Infinite_Set" + "~~/src/HOL/Library/Permutation" + theories + Fib + Factorization + Chinese + WilsonRuss + WilsonBij + Quadratic_Reciprocity + Primes + Pocklington + files "document/root.tex" + +session Hoare = HOL + + theories Hoare + files "document/root.bib" "document/root.tex" + +session Hoare_Parallel = HOL + + options [document_graph] + theories Hoare_Parallel + files "document/root.bib" "document/root.tex" + +session Codegenerator_Test = "HOL-Library" + + options [document = false, document_graph = false, browser_info = false] + theories Generate Generate_Pretty + +session Metis_Examples = HOL + + description {* + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen + + Testing Metis and Sledgehammer. + *} + options [document = false] + theories + Abstraction + Big_O + Binary_Tree + Clausification + Message + Proxies + Tarski + Trans_Closure + Sets + +session Nitpick_Examples = HOL + + description {* + Author: Jasmin Blanchette, TU Muenchen + Copyright 2009 + *} + options [document = false] + theories [quick_and_dirty] Nitpick_Examples + +session Algebra = HOL + + description {* + Author: Clemens Ballarin, started 24 September 1999 + + The Isabelle Algebraic Library. + *} + options [document_graph] + theories [document = false] + (* Preliminaries from set and number theory *) + "~~/src/HOL/Library/FuncSet" + "~~/src/HOL/Old_Number_Theory/Primes" + "~~/src/HOL/Library/Binomial" + "~~/src/HOL/Library/Permutation" + theories + (*** New development, based on explicit structures ***) + (* Groups *) + FiniteProduct (* Product operator for commutative groups *) + Sylow (* Sylow's theorem *) + Bij (* Automorphism Groups *) + + (* Rings *) + Divisibility (* Rings *) + IntRing (* Ideals and residue classes *) + UnivPoly (* Polynomials *) + theories [document = false] + (*** Old development, based on axiomatic type classes ***) + "abstract/Abstract" (*The ring theory*) + "poly/Polynomial" (*The full theory*) + files "document/root.bib" "document/root.tex" + +session Auth = HOL + + options [document_graph] + theories + Auth_Shared + Auth_Public + "Smartcard/Auth_Smartcard" + "Guard/Auth_Guard_Shared" + "Guard/Auth_Guard_Public" + files "document/root.tex" + +session UNITY = HOL + + description {* + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1998 University of Cambridge + + Verifying security protocols using UNITY. + *} + options [document_graph] + theories [document = false] "../Auth/Public" + 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" + files "document/root.tex" + +session Unix = HOL + + options [print_mode = "no_brackets,no_type_brackets"] + theories Unix + files "document/root.bib" "document/root.tex" + +session ZF = HOL + + description {* *} + theories MainZF Games + files "document/root.tex" + +session Imperative_HOL = HOL + + description {* *} + options [document_graph, print_mode = "iff,no_brackets"] + theories [document = false] + "~~/src/HOL/Library/Countable" + "~~/src/HOL/Library/Monad_Syntax" + "~~/src/HOL/Library/Code_Natural" + "~~/src/HOL/Library/LaTeXsugar" + theories Imperative_HOL_ex + files "document/root.bib" "document/root.tex" + +session Decision_Procs = HOL + + options [document = false] + theories Decision_Procs + +session ex in "Proofs/ex" = "HOL-Proofs" + + options [document = false, proofs = 2, parallel_proofs = 0] + theories Hilbert_Classical + +session Extraction in "Proofs/Extraction" = "HOL-Proofs" + + description {* Examples for program extraction in Higher-Order Logic *} + options [proofs = 2, parallel_proofs = 0] + theories [document = false] + "~~/src/HOL/Library/Efficient_Nat" + "~~/src/HOL/Library/Monad_Syntax" + "~~/src/HOL/Number_Theory/Primes" + "~~/src/HOL/Number_Theory/UniqueFactorization" + "~~/src/HOL/Library/State_Monad" + theories + Greatest_Common_Divisor + Warshall + Higman_Extraction + Pigeonhole + Euclid + files "document/root.bib" "document/root.tex" + +session Lambda in "Proofs/Lambda" = "HOL-Proofs" + + options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0] + theories [document = false] + "~~/src/HOL/Library/Code_Integer" + theories + Eta + StrongNorm + Standardization + WeakNorm + files "document/root.bib" "document/root.tex" + +session Prolog = HOL + + description {* + Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) + *} + options [document = false] + theories Test Type + +session MicroJava = HOL + + options [document_graph] + theories [document = false] "~~/src/HOL/Library/While_Combinator" + theories MicroJava + files + "document/introduction.tex" + "document/root.bib" + "document/root.tex" + +session NanoJava = HOL + + options [document_graph] + theories Example + files "document/root.bib" "document/root.tex" + +session Bali = HOL + + options [document_graph] + theories + AxExample + AxSound + AxCompl + Trans + files "document/root.tex" + +session IOA = HOL + + description {* + Author: Tobias Nipkow & Konrad Slind + Copyright 1994 TU Muenchen + + The meta theory of I/O-Automata. + + @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 + *} + options [document = false] + theories Solve + +session Lattice = HOL + + description {* + Author: Markus Wenzel, TU Muenchen + + Basic theory of lattices and orders. + *} + theories CompleteLattice + files "document/root.tex" + +session ex = HOL + + description {* Miscellaneous examples for Higher-Order Logic. *} + theories [document = false] + "~~/src/HOL/Library/State_Monad" + Code_Nat_examples + "~~/src/HOL/Library/FuncSet" + Eval_Examples + Normalization_by_Evaluation + Hebrew + Chinese + Serbian + "~~/src/HOL/Library/FinFun_Syntax" + theories + Iff_Oracle + Coercion_Examples + Numeral_Representation + Higher_Order_Logic + Abstract_NAT + Guess + Binary + Fundefs + Induction_Schema + LocaleTest2 + Records + While_Combinator_Example + MonoidGroup + BinEx + Hex_Bin_Examples + Antiquote + Multiquote + PER + NatSum + ThreeDivides + Intuitionistic + CTL + Arith_Examples + BT + Tree23 + MergeSort + Lagrange + Groebner_Examples + MT + Unification + Primrec + Tarski + Classical + Set_Theory + Meson_Test + Termination + Coherent + PresburgerEx + ReflectionEx + Sqrt + Sqrt_Script + Transfer_Ex + Transfer_Int_Nat + HarmonicSeries + Refute_Examples + Landau + Execute_Choice + Summation + Gauge_Integration + Dedekind_Real + Quicksort + Birthday_Paradox + List_to_Set_Comprehension_Examples + Seq + Simproc_Tests + Executable_Relation + FinFunPred + Set_Comprehension_Pointfree_Tests + Parallel_Example + theories SVC_Oracle + theories [condition = SVC_HOME] svc_test + theories [condition = ZCHAFF_HOME] + (*requires zChaff (or some other reasonably fast SAT solver)*) + Sudoku +(* FIXME +(*requires a proof-generating SAT solver (zChaff or MiniSAT)*) +(*global side-effects ahead!*) +try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *) +*) + files "document/root.bib" "document/root.tex" + +session Isar_Examples = HOL + + description {* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *} + theories [document = false] + "~~/src/HOL/Library/Lattice_Syntax" + "../Number_Theory/Primes" + theories + Basic_Logic + Cantor + Drinker + Expr_Compiler + Fibonacci + Group + Group_Context + Group_Notepad + Hoare_Ex + Knaster_Tarski + Mutilated_Checkerboard + Nested_Datatype + Peirce + Puzzle + Summation + files + "document/root.bib" + "document/root.tex" + "document/style.tex" + +session SET_Protocol = HOL + + options [document_graph] + theories [document = false] "~~/src/HOL/Library/Nat_Bijection" + theories SET_Protocol + files "document/root.tex" + +session Matrix_LP = HOL + + options [document_graph] + theories Cplex + files "document/root.tex" + +session TLA! = HOL + + description {* The Temporal Logic of Actions *} + options [document = false] + theories TLA + +session Inc in "TLA/Inc" = TLA + + options [document = false] + theories Inc + +session Buffer in "TLA/Buffer" = TLA + + options [document = false] + theories DBuffer + +session Memory in "TLA/Memory" = TLA + + options [document = false] + theories MemoryImplementation + +session TPTP = HOL + + description {* + Author: Jasmin Blanchette, TU Muenchen + Author: Nik Sultana, University of Cambridge + Copyright 2011 + + TPTP-related extensions. + *} + options [document = false] + theories + ATP_Theory_Export + MaSh_Eval + MaSh_Export + TPTP_Interpret + THF_Arith + theories [proofs = 0] (* FIXME !? *) + ATP_Problem_Import + +session Multivariate_Analysis = HOL + + options [document_graph] + theories + Multivariate_Analysis + Determinants + files + "Integration.certs" + "document/root.tex" + +session "HOL-Probability"! in "Probability" = "HOL-Multivariate_Analysis" + + options [document_graph] + theories [document = false] + "~~/src/HOL/Library/Countable" + "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits" + "~~/src/HOL/Library/Permutation" + theories + Probability + "ex/Dining_Cryptographers" + "ex/Koepf_Duermuth_Countermeasure" + files "document/root.tex" + +session Nominal (2) = HOL + + options [document = false] + theories Nominal + +session Examples in "Nominal/Examples" = "HOL-Nominal" + + options [document = false] + theories Nominal_Examples + theories [quick_and_dirty] VC_Condition + +session Word = HOL + + options [document_graph] + theories Word + files "document/root.bib" "document/root.tex" + +session Examples in "Word/Examples" = "HOL-Word" + + options [document = false] + theories WordExamples + +session Statespace = HOL + + theories StateSpaceEx + files "document/root.tex" + +session NSA = HOL + + options [document_graph] + theories Hypercomplex + files "document/root.tex" + +session Examples in "NSA/Examples" = "HOL-NSA" + + options [document = false] + theories NSPrimes + +session Mirabelle = HOL + + options [document = false] + theories Mirabelle_Test +(* FIXME + @cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case +*) + +session SMT_Examples = "HOL-Word" + + options [document = false, quick_and_dirty] + theories + SMT_Tests + SMT_Examples + SMT_Word_Examples + files + "SMT_Examples.certs" + "SMT_Tests.certs" + +session "HOL-Boogie"! in "Boogie" = "HOL-Word" + + options [document = false] + theories Boogie + (* FIXME files!?! *) + +session Examples in "Boogie/Examples" = "HOL-Boogie" + + options [document = false] + theories + Boogie_Max_Stepwise + Boogie_Max + Boogie_Dijkstra + VCC_Max + files + "Boogie_Dijkstra.certs" + "Boogie_Max.certs" + "VCC_Max.certs" + +session "HOL-SPARK"! in "SPARK" = "HOL-Word" + + options [document = false] + theories SPARK + +session Examples in "SPARK/Examples" = "HOL-SPARK" + + options [document = false] + 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" + files + "Gcd/greatest_common_divisor/g_c_d.fdl" + "Gcd/greatest_common_divisor/g_c_d.rls" + "Gcd/greatest_common_divisor/g_c_d.siv" + "Liseq/liseq/liseq_length.fdl" + "Liseq/liseq/liseq_length.rls" + "Liseq/liseq/liseq_length.siv" + "RIPEMD-160/rmd/f.fdl" + "RIPEMD-160/rmd/f.rls" + "RIPEMD-160/rmd/f.siv" + "RIPEMD-160/rmd/hash.fdl" + "RIPEMD-160/rmd/hash.rls" + "RIPEMD-160/rmd/hash.siv" + "RIPEMD-160/rmd/k_l.fdl" + "RIPEMD-160/rmd/k_l.rls" + "RIPEMD-160/rmd/k_l.siv" + "RIPEMD-160/rmd/k_r.fdl" + "RIPEMD-160/rmd/k_r.rls" + "RIPEMD-160/rmd/k_r.siv" + "RIPEMD-160/rmd/r_l.fdl" + "RIPEMD-160/rmd/r_l.rls" + "RIPEMD-160/rmd/r_l.siv" + "RIPEMD-160/rmd/round.fdl" + "RIPEMD-160/rmd/round.rls" + "RIPEMD-160/rmd/round.siv" + "RIPEMD-160/rmd/r_r.fdl" + "RIPEMD-160/rmd/r_r.rls" + "RIPEMD-160/rmd/r_r.siv" + "RIPEMD-160/rmd/s_l.fdl" + "RIPEMD-160/rmd/s_l.rls" + "RIPEMD-160/rmd/s_l.siv" + "RIPEMD-160/rmd/s_r.fdl" + "RIPEMD-160/rmd/s_r.rls" + "RIPEMD-160/rmd/s_r.siv" + +session Manual in "SPARK/Manual" = "HOL-SPARK" + + options [show_question_marks = false] + theories + Example_Verification + VC_Principles + Reference + Complex_Types + files + "complex_types_app/initialize.fdl" + "complex_types_app/initialize.rls" + "complex_types_app/initialize.siv" + "document/complex_types.ads" + "document/complex_types_app.adb" + "document/complex_types_app.ads" + "document/Gcd.adb" + "document/Gcd.ads" + "document/intro.tex" + "document/loop_invariant.adb" + "document/loop_invariant.ads" + "document/root.bib" + "document/root.tex" + "document/Simple_Gcd.adb" + "document/Simple_Gcd.ads" + "loop_invariant/proc1.fdl" + "loop_invariant/proc1.rls" + "loop_invariant/proc1.siv" + "loop_invariant/proc2.fdl" + "loop_invariant/proc2.rls" + "loop_invariant/proc2.siv" + "simple_greatest_common_divisor/g_c_d.fdl" + "simple_greatest_common_divisor/g_c_d.rls" + "simple_greatest_common_divisor/g_c_d.siv" + +session Mutabelle = HOL + + options [document = false] + theories MutabelleExtra + +session Quickcheck_Examples = HOL + + options [document = false] + theories Quickcheck_Examples (* FIXME *) + +session Quotient_Examples = HOL + + description {* + Author: Cezary Kaliszyk and Christian Urban + *} + options [document = false] + theories + DList + FSet + Quotient_Int + Quotient_Message + Lift_FSet + Lift_Set + Lift_RBT + Lift_Fun + Quotient_Rat + Lift_DList + +session Predicate_Compile_Examples = HOL + + options [document = false] + theories (* FIXME *) + Examples + Predicate_Compile_Tests + Specialisation_Examples + session HOLCF! (3) = HOL + description {* Author: Franz Regensburger @@ -35,6 +768,111 @@ theories [document = false] "~~/src/HOL/Library/Nat_Bijection" "~~/src/HOL/Library/Countable" - theories Plain_HOLCF Fixrec HOLCF + theories + Plain_HOLCF + Fixrec + HOLCF + files "document/root.tex" + +session Tutorial in "HOLCF/Tutorial" = HOLCF + + theories + Domain_ex + Fixrec_ex + New_Domain + files "document/root.tex" + +session Library in "HOLCF/Library" = HOLCF + + options [document = false] + theories HOLCF_Library + +session IMP in "HOLCF/IMP" = HOLCF + + options [document = false] + theories HoareEx files "document/root.tex" +session ex in "HOLCF/ex" = HOLCF + + description {* Misc HOLCF examples *} + options [document = false] + theories + Dnat + Dagstuhl + Focus_ex + Fix2 + Hoare + Concurrency_Monad + Loop + Powerdomain_ex + Domain_Proofs + Letrec + Pattern_Match + +session FOCUS in "HOLCF/FOCUS" = HOLCF + + options [document = false] + theories + Fstreams + FOCUS + Buffer_adm + +session IOA! in "HOLCF/IOA" = HOLCF + + description {* + Author: Olaf Mueller + + Formalization of a semantic model of I/O-Automata. + *} + options [document = false] + theories "meta_theory/Abstraction" + +session ABP in "HOLCF/IOA/ABP" = IOA + + description {* + Author: Olaf Mueller + + The Alternating Bit Protocol performed in I/O-Automata. + *} + options [document = false] + theories Correctness + +session 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 Mueller. + *} + options [document = false] + theories Correctness + +session Storage in "HOLCF/IOA/Storage" = IOA + + description {* + Author: Olaf Mueller + + Memory storage case study. + *} + options [document = false] + theories Correctness + +session ex in "HOLCF/IOA/ex" = IOA + + description {* + Author: Olaf Mueller + *} + options [document = false] + theories + TrivEx + TrivEx2 + +session Datatype_Benchmark = HOL + + description {* Some rather large datatype examples (from John Harrison). *} + options [document = false] + theories [condition = ISABELLE_BENCHMARK] + (* FIXME Toplevel.timing := true; *) + Brackin + Instructions + SML + Verilog + +session Record_Benchmark = HOL + + description {* Some benchmark on large record. *} + options [document = false] + theories [condition = ISABELLE_BENCHMARK] + (* FIXME Toplevel.timing := true; *) + Record_Benchmark + diff -r 1959baa22632 -r 6f2bcc0a16e0 src/LCF/LCF.thy --- a/src/LCF/LCF.thy Tue Jul 24 12:36:59 2012 +0200 +++ b/src/LCF/LCF.thy Tue Jul 24 21:48:41 2012 +0200 @@ -6,7 +6,7 @@ header {* LCF on top of First-Order Logic *} theory LCF -imports FOL +imports "~~/src/FOL/FOL" begin text {* This theory is based on Lawrence Paulson's book Logic and Computation. *} diff -r 1959baa22632 -r 6f2bcc0a16e0 src/LCF/ROOT --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LCF/ROOT Tue Jul 24 21:48:41 2012 +0200 @@ -0,0 +1,22 @@ +session LCF! in "." = Pure + + description {* + Author: Tobias Nipkow + Copyright 1992 University of Cambridge + *} + options [document = false] + theories LCF + +session ex = LCF + + description {* + Author: Tobias Nipkow + Copyright 1991 University of Cambridge + + Some examples from Lawrence Paulson's book Logic and Computation. + *} + options [document = false] + theories + Ex1 + Ex2 + Ex3 + Ex4 + diff -r 1959baa22632 -r 6f2bcc0a16e0 src/Pure/General/exn.scala --- a/src/Pure/General/exn.scala Tue Jul 24 12:36:59 2012 +0200 +++ b/src/Pure/General/exn.scala Tue Jul 24 21:48:41 2012 +0200 @@ -31,11 +31,19 @@ private val runtime_exception = Class.forName("java.lang.RuntimeException") - def message(exn: Throwable): String = - if (exn.getClass == runtime_exception) { + def user_message(exn: Throwable): Option[String] = + if (exn.isInstanceOf[java.io.IOException]) { + val msg = exn.getMessage + Some(if (msg == null) "I/O error" else "I/O error: " + msg) + } + else if (exn.getClass == runtime_exception) { val msg = exn.getMessage - if (msg == null) "Error" else msg + Some(if (msg == null) "Error" else msg) } - else exn.toString + else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString) + else None + + def message(exn: Throwable): String = + user_message(exn) getOrElse exn.toString } diff -r 1959baa22632 -r 6f2bcc0a16e0 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Tue Jul 24 12:36:59 2012 +0200 +++ b/src/Pure/General/path.scala Tue Jul 24 21:48:41 2012 +0200 @@ -96,8 +96,16 @@ new Path(norm_elems(explode_elems(raw_elems) ++ roots)) } + def is_ok(str: String): Boolean = + try { explode(str); true } catch { case ERROR(_) => false } + def split(str: String): List[Path] = space_explode(':', str).filterNot(_.isEmpty).map(explode) + + + /* encode */ + + val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode)) } diff -r 1959baa22632 -r 6f2bcc0a16e0 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Tue Jul 24 12:36:59 2012 +0200 +++ b/src/Pure/IsaMakefile Tue Jul 24 21:48:41 2012 +0200 @@ -188,11 +188,12 @@ Syntax/syntax_phases.ML \ Syntax/syntax_trans.ML \ Syntax/term_position.ML \ + System/build.ML \ System/invoke_scala.ML \ - System/build.ML \ System/isabelle_process.ML \ System/isabelle_system.ML \ System/isar.ML \ + System/options.ML \ System/session.ML \ System/system_channel.ML \ Thy/html.ML \ diff -r 1959baa22632 -r 6f2bcc0a16e0 src/Pure/Isar/parse.scala --- a/src/Pure/Isar/parse.scala Tue Jul 24 12:36:59 2012 +0200 +++ b/src/Pure/Isar/parse.scala Tue Jul 24 21:48:41 2012 +0200 @@ -60,7 +60,10 @@ def text: Parser[String] = atom("text", _.is_text) def ML_source: Parser[String] = atom("ML source", _.is_text) def doc_source: Parser[String] = atom("document source", _.is_text) - def path: Parser[String] = atom("file name/path specification", _.is_name) + def path: Parser[String] = + atom("file name/path specification", tok => tok.is_name && Path.is_ok(tok.content)) + def theory_name: Parser[String] = + atom("theory name", tok => tok.is_name && Thy_Load.is_ok(tok.content)) private def tag_name: Parser[String] = atom("tag name", tok => diff -r 1959baa22632 -r 6f2bcc0a16e0 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Jul 24 12:36:59 2012 +0200 +++ b/src/Pure/ROOT.ML Tue Jul 24 21:48:41 2012 +0200 @@ -103,6 +103,7 @@ use "context.ML"; use "context_position.ML"; use "config.ML"; +use "System/options.ML"; (* inner syntax *) diff -r 1959baa22632 -r 6f2bcc0a16e0 src/Pure/System/build.ML --- a/src/Pure/System/build.ML Tue Jul 24 12:36:59 2012 +0200 +++ b/src/Pure/System/build.ML Tue Jul 24 21:48:41 2012 +0200 @@ -12,18 +12,64 @@ structure Build: BUILD = struct +local + +fun use_thys options = + Thy_Info.use_thys + |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs") + |> Unsynchronized.setmp print_mode + (space_explode "," (Options.string options "print_mode") @ print_mode_value ()) + |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs") + |> Unsynchronized.setmp Goal.parallel_proofs_threshold + (Options.int options "parallel_proofs_threshold") + |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace") + |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads") + |> (case Options.string options "document" of "" => true | "false" => true | _ => false) ? + Present.no_document + |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty") + |> Unsynchronized.setmp Printer.show_question_marks_default + (Options.bool options "show_question_marks") + |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long") + |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short") + |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique"); + +fun use_theories (options, thys) = + let val condition = space_explode "," (Options.string options "condition") in + (case filter_out (can getenv_strict) condition of + [] => use_thys options thys + | conds => + Output.physical_stderr ("Ignoring theories " ^ commas_quote thys ^ + " (undefined " ^ commas conds ^ ")\n")) + end; + +in + fun build args_file = let - val (save, (parent, (name, theories))) = + val (save, (options, (timing, (verbose, (browser_info, (parent_base_name, + (name, (base_name, theories)))))))) = File.read (Path.explode args_file) |> YXML.parse_body |> - let open XML.Decode in pair bool (pair string (pair string (list string))) end; + let open XML.Decode in + pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string + (pair string (pair string ((list (pair Options.decode (list string))))))))))) + end; - val _ = Session.init false parent name; (* FIXME reset!? *) - val _ = Thy_Info.use_thys theories; + val _ = + Session.init save false + (Options.bool options "browser_info") browser_info + (Options.string options "document") + (Options.bool options "document_graph") + (space_explode ":" (Options.string options "document_variants")) + parent_base_name base_name + (not (Options.bool options "document_dump_only"), Options.string options "document_dump") + (Options.string options "browser_info_remote") + verbose; + val _ = Session.with_timing name timing (List.app use_theories) theories; val _ = Session.finish (); - val _ = if save then () else quit (); in () end handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1); end; + +end; diff -r 1959baa22632 -r 6f2bcc0a16e0 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Tue Jul 24 12:36:59 2012 +0200 +++ b/src/Pure/System/build.scala Tue Jul 24 21:48:41 2012 +0200 @@ -42,8 +42,10 @@ /* Info */ sealed case class Info( + base_name: String, dir: Path, parent: Option[String], + parent_base_name: Option[String], description: String, options: Options, theories: List[(Options, List[Path])], @@ -115,7 +117,7 @@ private case class Session_Entry( name: String, - reset: Boolean, + this_name: Boolean, order: Int, path: Option[String], parent: Option[String], @@ -140,7 +142,6 @@ val session_entry: Parser[Session_Entry] = { val session_name = atom("session name", _.is_name) - val theory_name = atom("theory name", _.is_name) val option = name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) } @@ -187,16 +188,19 @@ try { if (entry.name == "") error("Bad session name") - val full_name = + val (full_name, parent_base_name) = if (is_pure(entry.name)) { if (entry.parent.isDefined) error("Illegal parent session") - else entry.name + else (entry.name, None: Option[String]) } else entry.parent match { case Some(parent_name) if queue1.defined(parent_name) => - if (entry.reset) entry.name - else parent_name + "-" + entry.name + val full_name = + if (entry.this_name) entry.name + else parent_name + "-" + entry.name + val parent_base_name = Some(queue1(parent_name).base_name) + (full_name, parent_base_name) case _ => error("Bad parent session") } @@ -208,14 +212,17 @@ val key = Session.Key(full_name, entry.order) + val session_options = options ++ entry.options + val theories = - entry.theories.map({ case (opts, thys) => (options ++ opts, thys.map(Path.explode(_))) }) + entry.theories.map({ case (opts, thys) => + (session_options ++ opts, thys.map(Path.explode(_))) }) val files = entry.files.map(Path.explode(_)) val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString) val info = - Session.Info(dir + path, entry.parent, - entry.description, options ++ entry.options, theories, files, digest) + Session.Info(entry.name, dir + path, entry.parent, parent_base_name, + entry.description, session_options, theories, files, digest) queue1 + (key, info) } @@ -279,6 +286,10 @@ /** build **/ + private def echo(msg: String) { java.lang.System.out.println(msg) } + private def sleep(): Unit = Thread.sleep(500) + + /* dependencies */ sealed case class Node( @@ -290,7 +301,7 @@ def sources(name: String): List[(Path, SHA1.Digest)] = deps(name).sources } - def dependencies(queue: Session.Queue): Deps = + def dependencies(verbose: Boolean, queue: Session.Queue): Deps = Deps((Map.empty[String, Node] /: queue.topological_order)( { case (deps, (name, info)) => val preloaded = @@ -300,6 +311,8 @@ } val thy_info = new Thy_Info(new Thy_Load(preloaded)) + if (verbose) echo("Checking " + name) + val thy_deps = thy_info.dependencies( info.theories.map(_._2).flatten. @@ -318,7 +331,12 @@ } thy :: uses }).flatten ::: info.files.map(file => info.dir + file) - val sources = all_files.par.map(p => (p, SHA1.digest(p))).toList + val sources = + try { all_files.map(p => (p, SHA1.digest(p))) } + catch { + case ERROR(msg) => + error(msg + "\nThe error(s) above occurred in session " + quote(name)) + } deps + (name -> Node(loaded_theories, sources)) })) @@ -340,9 +358,23 @@ def join: (String, String, Int) = { val res = result.join; args_file.delete; res } } - private def start_job(name: String, info: Session.Info, output: Option[String]): Job = + private def start_job(name: String, info: Session.Info, output: Option[String], + options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job = { + // global browser info dir + if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile) + { + browser_info.file.mkdirs() + File.copy(Path.explode("~~/lib/logo/isabelle.gif"), + browser_info + Path.explode("isabelle.gif")) + File.write(browser_info + Path.explode("index.html"), + File.read(Path.explode("~~/lib/html/library_index_header.template")) + + File.read(Path.explode("~~/lib/html/library_index_content.template")) + + File.read(Path.explode("~~/lib/html/library_index_footer.template"))) + } + val parent = info.parent.getOrElse("") + val parent_base_name = info.parent_base_name.getOrElse("") val cwd = info.dir.file val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output.getOrElse("")) @@ -371,8 +403,10 @@ val args_xml = { import XML.Encode._ - pair(bool, pair(string, pair(string, list(string))))( - output.isDefined, (parent, (name, info.theories.map(_._2).flatten.map(_.implode)))) + pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string, + pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))( + (output.isDefined, (options, (timing, (verbose, (browser_info, (parent_base_name, + (name, (info.base_name, info.theories))))))))) } new Job(cwd, env, script, YXML.string_of_body(args_xml)) } @@ -380,33 +414,18 @@ /* build */ - private def echo(msg: String) { java.lang.System.out.println(msg) } - private def sleep(): Unit = Thread.sleep(500) - def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int, - list_only: Boolean, system_mode: Boolean, verbose: Boolean, + no_build: Boolean, system_mode: Boolean, timing: Boolean, verbose: Boolean, more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int = { val options = (Options.init() /: more_options)(_.define_simple(_)) val queue = find_sessions(options, all_sessions, sessions, more_dirs) - val deps = dependencies(queue) + val deps = dependencies(verbose, queue) val (output_dir, browser_info) = if (system_mode) (Path.explode("~~/heaps/$ML_IDENTIFIER"), Path.explode("~~/browser_info")) else (Path.explode("$ISABELLE_OUTPUT"), Path.explode("$ISABELLE_BROWSER_INFO")) - // prepare browser info dir - if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile) - { - browser_info.file.mkdirs() - File.copy(Path.explode("~~/lib/logo/isabelle.gif"), - browser_info + Path.explode("isabelle.gif")) - File.write(browser_info + Path.explode("index.html"), - File.read(Path.explode("~~/lib/html/library_index_header.template")) + - File.read(Path.explode("~~/lib/html/library_index_content.template")) + - File.read(Path.explode("~~/lib/html/library_index_footer.template"))) - } - // prepare log dir val log_dir = output_dir + Path.explode("log") log_dir.file.mkdirs() @@ -444,8 +463,7 @@ else if (running.size < (max_jobs max 1)) { pending.dequeue(running.isDefinedAt(_)) match { case Some((name, info)) => - if (list_only) { - echo(name + " in " + info.dir) + if (no_build) { loop(pending - name, running, results + (name -> 0)) } else if (info.parent.map(results(_)).forall(_ == 0)) { @@ -454,7 +472,7 @@ Some(Isabelle_System.standard_path(output_dir + Path.basic(name))) else None echo((if (output.isDefined) "Building " else "Running ") + name + " ...") - val job = start_job(name, info, output) + val job = start_job(name, info, output, info.options, timing, verbose, browser_info) loop(pending, running + (name -> job), results) } else { @@ -467,7 +485,13 @@ else { sleep(); loop(pending, running, results) } } - (0 /: loop(queue, Map.empty, Map.empty))({ case (rc1, (_, rc2)) => rc1 max rc2 }) + val results = loop(queue, Map.empty, Map.empty) + val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 }) + if (rc != 0) { + val unfinished = (for ((name, r) <- results.iterator if r != 0) yield name).toList.sorted + echo("Unfinished session(s): " + commas(unfinished)) + } + rc } @@ -481,11 +505,12 @@ Properties.Value.Boolean(all_sessions) :: Properties.Value.Boolean(build_images) :: Properties.Value.Int(max_jobs) :: - Properties.Value.Boolean(list_only) :: + Properties.Value.Boolean(no_build) :: Properties.Value.Boolean(system_mode) :: + Properties.Value.Boolean(timing) :: Properties.Value.Boolean(verbose) :: Command_Line.Chunks(more_dirs, options, sessions) => - build(all_sessions, build_images, max_jobs, list_only, system_mode, + build(all_sessions, build_images, max_jobs, no_build, system_mode, timing, verbose, more_dirs.map(Path.explode), options, sessions) case _ => error("Bad arguments:\n" + cat_lines(args)) } diff -r 1959baa22632 -r 6f2bcc0a16e0 src/Pure/System/options.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/options.ML Tue Jul 24 21:48:41 2012 +0200 @@ -0,0 +1,76 @@ +(* Title: Pure/System/options.ML + Author: Makarius + +Stand-alone options with external string representation. +*) + +signature OPTIONS = +sig + type T + val empty: T + val bool: T -> string -> bool + val int: T -> string -> int + val real: T -> string -> real + val string: T -> string -> string + val declare: {name: string, typ: string, value: string} -> T -> T + val decode: XML.body -> T +end; + +structure Options: OPTIONS = +struct + +(* representation *) + +val boolT = "bool"; +val intT = "int"; +val realT = "real"; +val stringT = "string"; + +datatype T = Options of {typ: string, value: string} Symtab.table; + +val empty = Options Symtab.empty; + + +(* get *) + +fun get T parse (Options tab) name = + (case Symtab.lookup tab name of + SOME {typ, value} => + if typ = T then + (case parse value of + SOME x => x + | NONE => + error ("Malformed value for option " ^ quote name ^ " : " ^ T ^ " =\n" ^ quote value)) + else error ("Ill-typed option " ^ quote name ^ " : " ^ typ ^ " vs. " ^ T) + | NONE => error ("Unknown option " ^ quote name)); + +val bool = get boolT Bool.fromString; +val int = get intT Int.fromString; +val real = get realT Real.fromString; +val string = get stringT SOME; + + +(* declare *) + +fun declare {name, typ, value} (Options tab) = + let + val check_value = + if typ = boolT then ignore oo bool + else if typ = intT then ignore oo int + else if typ = realT then ignore oo real + else if typ = stringT then ignore oo string + else error ("Unknown type for option " ^ quote name ^ " : " ^ quote typ); + val options' = Options (Symtab.update_new (name, {typ = typ, value = value}) tab) + handle Symtab.DUP _ => error ("Duplicate declaration of option " ^ quote name); + val _ = check_value options' name; + in options' end; + + +(* decode *) + +fun decode body = + fold (declare o (fn (name, typ, value) => {name = name, typ = typ, value = value})) + (let open XML.Decode in list (triple string string string) end body) empty; + +end; + diff -r 1959baa22632 -r 6f2bcc0a16e0 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Tue Jul 24 12:36:59 2012 +0200 +++ b/src/Pure/System/options.scala Tue Jul 24 21:48:41 2012 +0200 @@ -79,6 +79,11 @@ } options } + + + /* encode */ + + val encode: XML.Encode.T[Options] = (options => options.encode) } @@ -177,7 +182,7 @@ case "int" => Options.Int case "real" => Options.Real case "string" => Options.String - case _ => error("Malformed type for option " + quote(name) + " : " + quote(typ_name)) + case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name)) } (new Options(options + (name -> Options.Opt(typ, value, description)))).check_value(name) } @@ -209,4 +214,14 @@ case i => define(str.substring(0, i), str.substring(i + 1)) } } + + + /* encode */ + + def encode: XML.Body = + { + import XML.Encode.{string => str, _} + list(triple(str, str, str))( + options.toList.map({ case (name, opt) => (name, opt.typ.print, opt.value) })) + } } diff -r 1959baa22632 -r 6f2bcc0a16e0 src/Pure/System/session.ML --- a/src/Pure/System/session.ML Tue Jul 24 12:36:59 2012 +0200 +++ b/src/Pure/System/session.ML Tue Jul 24 21:48:41 2012 +0200 @@ -9,11 +9,13 @@ val id: unit -> string list val name: unit -> string val welcome: unit -> string - val init: bool -> string -> string -> unit + val finish: unit -> unit + val init: bool -> bool -> bool -> string -> string -> bool -> string list -> + string -> string -> bool * string -> string -> bool -> unit + val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b val use_dir: string -> string -> bool -> string list -> bool -> bool -> string -> string -> bool -> string list -> string -> string -> bool * string -> string -> int -> bool -> bool -> int -> int -> int -> int -> unit - val finish: unit -> unit end; structure Session: SESSION = @@ -63,9 +65,9 @@ end; -(* init *) +(* init_name *) -fun init reset parent name = +fun init_name reset parent name = if not (member (op =) (! session) parent) orelse not (! session_finished) then error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) else (add_path reset name; session_finished := false); @@ -94,26 +96,32 @@ fun dumping (_, "") = NONE | dumping (cp, path) = SOME (cp, Path.explode path); +fun with_timing _ false f x = f x + | with_timing item true f x = + let + val start = Timing.start (); + val y = f x; + val timing = Timing.result start; + val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) + |> Real.fmt (StringCvt.FIX (SOME 2)); + val _ = + Output.physical_stderr ("Timing " ^ item ^ " (" ^ + string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^ + Timing.message timing ^ ", factor " ^ factor ^ ")\n"); + in y end; + +fun init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose = + (init_name reset parent name; + Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants + (path ()) name (dumping dump) (get_rpath rpath) verbose + (map Thy_Info.get_theory (Thy_Info.get_names ()))); + fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent name dump rpath level timing verbose max_threads trace_threads parallel_proofs parallel_proofs_threshold = ((fn () => - (init reset parent name; - Present.init build info info_path doc doc_graph doc_variants (path ()) name - (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ())); - if timing then - let - val start = Timing.start (); - val _ = use root; - val timing = Timing.result start; - val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) - |> Real.fmt (StringCvt.FIX (SOME 2)); - val _ = - Output.physical_stderr ("Timing " ^ item ^ " (" ^ - string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^ - Timing.message timing ^ ", factor " ^ factor ^ ")\n"); - in () end - else use root; + (init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose; + with_timing item timing use root; finish ())) |> Unsynchronized.setmp Proofterm.proofs level |> Unsynchronized.setmp print_mode (modes @ print_mode_value ()) diff -r 1959baa22632 -r 6f2bcc0a16e0 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Tue Jul 24 12:36:59 2012 +0200 +++ b/src/Pure/Thy/thy_header.scala Tue Jul 24 21:48:41 2012 +0200 @@ -46,7 +46,6 @@ val header: Parser[Thy_Header] = { val file_name = atom("file name", _.is_name) - val theory_name = atom("theory name", _.is_name) val keyword_kind = atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) } diff -r 1959baa22632 -r 6f2bcc0a16e0 src/Pure/Thy/thy_load.scala --- a/src/Pure/Thy/thy_load.scala Tue Jul 24 12:36:59 2012 +0200 +++ b/src/Pure/Thy/thy_load.scala Tue Jul 24 21:48:41 2012 +0200 @@ -13,6 +13,10 @@ object Thy_Load { def thy_path(path: Path): Path = path.ext("thy") + + def is_ok(str: String): Boolean = + try { thy_path(Path.explode(str)); true } + catch { case ERROR(_) => false } } diff -r 1959baa22632 -r 6f2bcc0a16e0 src/Pure/library.scala --- a/src/Pure/library.scala Tue Jul 24 12:36:59 2012 +0200 +++ b/src/Pure/library.scala Tue Jul 24 21:48:41 2012 +0200 @@ -24,11 +24,7 @@ object ERROR { def apply(message: String): Throwable = new RuntimeException(message) - def unapply(exn: Throwable): Option[String] = - exn match { - case e: RuntimeException => Some(Exn.message(e)) - case _ => None - } + def unapply(exn: Throwable): Option[String] = Exn.user_message(exn) } def error(message: String): Nothing = throw ERROR(message) diff -r 1959baa22632 -r 6f2bcc0a16e0 src/Sequents/ROOT --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ROOT Tue Jul 24 21:48:41 2012 +0200 @@ -0,0 +1,32 @@ +session Sequents! in "." = Pure + + description {* + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1991 University of Cambridge + + Classical Sequent Calculus based on Pure Isabelle. + *} + options [document = false] + theories + LK + ILL + ILL_predlog + Washing + Modal0 + T + S4 + S43 + +session LK = Sequents + + description {* + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + + Examples for Classical Logic. + *} + options [document = false] + theories + Propositional + Quantifiers + Hard_Quantifiers + Nat + diff -r 1959baa22632 -r 6f2bcc0a16e0 src/ZF/ROOT --- a/src/ZF/ROOT Tue Jul 24 12:36:59 2012 +0200 +++ b/src/ZF/ROOT Tue Jul 24 21:48:41 2012 +0200 @@ -1,4 +1,4 @@ -session ZF! (10) in "." = FOL + +session ZF! in "." = Pure + description {* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge @@ -8,7 +8,9 @@ This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson. *} options [document_graph] - theories Main Main_ZFC + theories + Main + Main_ZFC files "document/root.tex" session AC = ZF + @@ -19,8 +21,17 @@ Proofs of AC-equivalences, due to Krzysztof Grabczewski. *} options [document_graph] - theories WO6_WO1 WO1_WO7 AC7_AC9 WO1_AC AC15_WO6 - WO2_AC16 AC16_WO4 AC17_AC1 AC18_AC19 DC + theories + WO6_WO1 + WO1_WO7 + AC7_AC9 + WO1_AC + AC15_WO6 + WO2_AC16 + AC16_WO4 + AC17_AC1 + AC18_AC19 + DC files "document/root.tex" "document/root.bib" session Coind = ZF + @@ -39,6 +50,7 @@ Jacob Frost, A Case Study of Co_induction in Isabelle Report, Computer Lab, University of Cambridge (1995). *} + options [document = false] theories ECR session Constructible = ZF + @@ -61,6 +73,7 @@ Glynn Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993. *} + options [document = false] theories Equiv files "document/root.tex" "document/root.bib" @@ -108,6 +121,7 @@ Gerard Huet. Residual Theory in Lambda-Calculus: A Formal Development. J. Functional Programming 4(3) 1994, 371-394. *} + options [document = false] theories Confluence session UNITY = ZF + @@ -117,6 +131,7 @@ ZF/UNITY proofs. *} + options [document = false] theories (*Simple examples: no composition*) Mutex @@ -134,6 +149,7 @@ Miscellaneous examples for Zermelo-Fraenkel Set Theory. *} + options [document = false] theories misc Ring (*abstract algebra*) diff -r 1959baa22632 -r 6f2bcc0a16e0 src/ZF/ZF.thy --- a/src/ZF/ZF.thy Tue Jul 24 12:36:59 2012 +0200 +++ b/src/ZF/ZF.thy Tue Jul 24 21:48:41 2012 +0200 @@ -6,7 +6,7 @@ header{*Zermelo-Fraenkel Set Theory*} theory ZF -imports FOL +imports "~~/src/FOL/FOL" begin declare [[eta_contract = false]]