# HG changeset patch # User huffman # Date 1230154760 28800 # Node ID c3d1f87a3cb03d2eeef2130490d00bf0961b8203 # Parent 5eff800a695f1ac1f7aa26dbf50895d2271aa87d# Parent bad036eb71c4a364415c5ee159919c173cc5a394 merged. diff -r 5eff800a695f -r c3d1f87a3cb0 Admin/MacOS/README --- a/Admin/MacOS/README Wed Dec 24 13:29:49 2008 -0800 +++ b/Admin/MacOS/README Wed Dec 24 13:39:20 2008 -0800 @@ -6,3 +6,12 @@ * CocoaDialog http://cocoadialog.sourceforge.net/ * Platypus http://www.sveinbjorn.org/platypus + +* AppHack 1.1 http://www.sveinbjorn.org/apphack + + Manual setup: + File type: "Isabelle theory" + Icon: "theory.icns" + "Editor" + Suffixes: "thy" + diff -r 5eff800a695f -r c3d1f87a3cb0 Admin/MacOS/mk --- a/Admin/MacOS/mk Wed Dec 24 13:29:49 2008 -0800 +++ b/Admin/MacOS/mk Wed Dec 24 13:39:20 2008 -0800 @@ -16,4 +16,4 @@ -c "$THIS/script" \ -o None \ -f "$COCOADIALOG_APP" \ - Isabelle.app + "$PWD/Isabelle.app" diff -r 5eff800a695f -r c3d1f87a3cb0 Admin/build --- a/Admin/build Wed Dec 24 13:29:49 2008 -0800 +++ b/Admin/build Wed Dec 24 13:39:20 2008 -0800 @@ -7,7 +7,7 @@ #paranoia setting for sunbroy PATH="/usr/local/dist/DIR/j2sdk1.5.0/bin:$PATH" -PATH="/home/scala/scala/bin:$PATH" +PATH="/home/scala/current/bin:$PATH" ## directory layout diff -r 5eff800a695f -r c3d1f87a3cb0 NEWS --- a/NEWS Wed Dec 24 13:29:49 2008 -0800 +++ b/NEWS Wed Dec 24 13:39:20 2008 -0800 @@ -42,6 +42,11 @@ ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any Isabelle distribution. +* Proofs of fully specified statements are run in parallel on +multi-core systems. A speedup factor of 2-3 can be expected on a +regular 4-core machine, if the initial heap space is made reasonably +large (cf. Poly/ML option -H). [Poly/ML 5.2.1 or later] + * The Isabelle System Manual (system) has been updated, with formally checked references as hyperlinks. @@ -55,8 +60,8 @@ * Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML interface instead. -* There is a new lexical item "float" with syntax ["-"] digit+ "." digit+, -without spaces. +* There is a new syntactic category "float_const" for signed decimal +fractions (e.g. 123.45 or -123.45). *** Pure *** @@ -391,6 +396,14 @@ *** ML *** +* High-level support for concurrent ML programming, see +src/Pure/Cuncurrent. The data-oriented model of "future values" is +particularly convenient to organize independent functional +computations. The concept of "synchronized variables" provides a +higher-order interface for components with shared state, avoiding the +delicate details of mutexes and condition variables. [Poly/ML 5.2.1 +or later] + * Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm to 'a -> thm, while results are always tagged with an authentic oracle name. The Isar command 'oracle' is now polymorphic, no argument type @@ -860,8 +873,8 @@ print_mode_active, PrintMode.setmp etc. INCOMPATIBILITY. * Functions system/system_out provide a robust way to invoke external -shell commands, with propagation of interrupts (requires Poly/ML 5.2). -Do not use OS.Process.system etc. from the basis library! +shell commands, with propagation of interrupts (requires Poly/ML +5.2.1). Do not use OS.Process.system etc. from the basis library! *** System *** diff -r 5eff800a695f -r c3d1f87a3cb0 doc-src/IsarImplementation/Thy/ML.thy --- a/doc-src/IsarImplementation/Thy/ML.thy Wed Dec 24 13:29:49 2008 -0800 +++ b/doc-src/IsarImplementation/Thy/ML.thy Wed Dec 24 13:39:20 2008 -0800 @@ -107,18 +107,23 @@ section {* Thread-safe programming *} text {* - Recent versions of Poly/ML (5.2 or later) support multithreaded - execution based on native operating system threads of the underlying - platform. Thus threads will actually be executed in parallel on - multi-core systems. A speedup-factor of approximately 2--4 can be - expected for large well-structured Isabelle sessions, where theories - are organized as a graph with sufficiently many independent nodes. + Recent versions of Poly/ML (5.2.1 or later) support robust + multithreaded execution, based on native operating system threads of + the underlying platform. Thus threads will actually be executed in + parallel on multi-core systems. A speedup-factor of approximately + 1.5--3 can be expected on a regular 4-core machine.\footnote{There + is some inherent limitation of the speedup factor due to garbage + collection, which is still sequential. It helps to provide initial + heap space generously, using the \texttt{-H} option of Poly/ML.} + Threads also help to organize advanced operations of the system, + with explicit communication between sub-components, real-time + conditions, time-outs etc. - Threads lack the memory protection of separate processes, but + Threads lack the memory protection of separate processes, and operate concurrently on shared heap memory. This has the advantage that results of independent computations are immediately available - to other threads, without requiring explicit communication, - reloading, or even recoding of data. + to other threads, without requiring untyped character streams, + awkward serialization etc. On the other hand, some programming guidelines need to be observed in order to make unprotected parallelism work out smoothly. While @@ -143,27 +148,29 @@ \end{itemize} - Note that ML bindings within the toplevel environment (@{verbatim - "type"}, @{verbatim val}, @{verbatim "structure"} etc.) due to - run-time invocation of the compiler are non-critical, because - Isabelle/Isar incorporates such bindings within the theory or proof - context. - The majority of tools implemented within the Isabelle/Isar framework will not require any of these critical elements: nothing special needs to be observed when staying in the purely functional fragment of ML. Note that output via the official Isabelle channels does not - even count as direct I/O in the above sense, so the operations @{ML - "writeln"}, @{ML "warning"}, @{ML "tracing"} etc.\ are safe. + count as direct I/O, so the operations @{ML "writeln"}, @{ML + "warning"}, @{ML "tracing"} etc.\ are safe. + + Moreover, ML bindings within the toplevel environment (@{verbatim + "type"}, @{verbatim val}, @{verbatim "structure"} etc.) due to + run-time invocation of the compiler are also safe, because + Isabelle/Isar manages this as part of the theory or proof context. - \paragraph{Multithreading in Isabelle/Isar.} Our parallel execution - model is centered around the theory loader. Whenever a given - subgraph of theories needs to be updated, the system schedules a - number of threads to process the sources as required, while - observing their dependencies. Thus concurrency is limited to - independent nodes according to the theory import relation. + \paragraph{Multithreading in Isabelle/Isar.} The theory loader + automatically exploits the overall parallelism of independent nodes + in the development graph, as well as the inherent irrelevance of + proofs for goals being fully specified in advance. This means, + checking of individual Isar proofs is parallelized by default. + Beyond that, very sophisticated proof tools may use local + parallelism internally, via the general programming model of + ``future values'' (see also @{"file" + "~~/src/Pure/Concurrent/future.ML"}). - Any user-code that works relatively to the present background theory + Any ML code that works relatively to the present background theory is already safe. Contextual data may be easily stored within the theory or proof context, thanks to the generic data concept of Isabelle/Isar (see \secref{sec:context-data}). This greatly @@ -179,9 +186,13 @@ quickly, otherwise parallel execution performance may degrade significantly. - Despite this potential bottle-neck, we refrain from fine-grained - locking mechanism within user-code: the restriction to a single lock - prevents deadlocks without demanding special precautions. + Despite this potential bottle-neck, centralized locking is + convenient, because it prevents deadlocks without demanding special + precautions. Explicit communication demands other means, though. + The high-level abstraction of synchronized variables @{"file" + "~~/src/Pure/Concurrent/synchronized.ML"} enables parallel + components to communicate via shared state; see also @{"file" + "~~/src/Pure/Concurrent/mailbox.ML"} as canonical example. \paragraph{Good conduct of impure programs.} The following guidelines enable non-functional programs to participate in diff -r 5eff800a695f -r c3d1f87a3cb0 doc-src/IsarImplementation/Thy/document/ML.tex --- a/doc-src/IsarImplementation/Thy/document/ML.tex Wed Dec 24 13:29:49 2008 -0800 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Wed Dec 24 13:39:20 2008 -0800 @@ -128,18 +128,23 @@ \isamarkuptrue% % \begin{isamarkuptext}% -Recent versions of Poly/ML (5.2 or later) support multithreaded - execution based on native operating system threads of the underlying - platform. Thus threads will actually be executed in parallel on - multi-core systems. A speedup-factor of approximately 2--4 can be - expected for large well-structured Isabelle sessions, where theories - are organized as a graph with sufficiently many independent nodes. +Recent versions of Poly/ML (5.2.1 or later) support robust + multithreaded execution, based on native operating system threads of + the underlying platform. Thus threads will actually be executed in + parallel on multi-core systems. A speedup-factor of approximately + 1.5--3 can be expected on a regular 4-core machine.\footnote{There + is some inherent limitation of the speedup factor due to garbage + collection, which is still sequential. It helps to provide initial + heap space generously, using the \texttt{-H} option of Poly/ML.} + Threads also help to organize advanced operations of the system, + with explicit communication between sub-components, real-time + conditions, time-outs etc. - Threads lack the memory protection of separate processes, but + Threads lack the memory protection of separate processes, and operate concurrently on shared heap memory. This has the advantage that results of independent computations are immediately available - to other threads, without requiring explicit communication, - reloading, or even recoding of data. + to other threads, without requiring untyped character streams, + awkward serialization etc. On the other hand, some programming guidelines need to be observed in order to make unprotected parallelism work out smoothly. While @@ -163,25 +168,26 @@ \end{itemize} - Note that ML bindings within the toplevel environment (\verb|type|, \verb|val|, \verb|structure| etc.) due to - run-time invocation of the compiler are non-critical, because - Isabelle/Isar incorporates such bindings within the theory or proof - context. - The majority of tools implemented within the Isabelle/Isar framework will not require any of these critical elements: nothing special needs to be observed when staying in the purely functional fragment of ML. Note that output via the official Isabelle channels does not - even count as direct I/O in the above sense, so the operations \verb|writeln|, \verb|warning|, \verb|tracing| etc.\ are safe. + count as direct I/O, so the operations \verb|writeln|, \verb|warning|, \verb|tracing| etc.\ are safe. + + Moreover, ML bindings within the toplevel environment (\verb|type|, \verb|val|, \verb|structure| etc.) due to + run-time invocation of the compiler are also safe, because + Isabelle/Isar manages this as part of the theory or proof context. - \paragraph{Multithreading in Isabelle/Isar.} Our parallel execution - model is centered around the theory loader. Whenever a given - subgraph of theories needs to be updated, the system schedules a - number of threads to process the sources as required, while - observing their dependencies. Thus concurrency is limited to - independent nodes according to the theory import relation. + \paragraph{Multithreading in Isabelle/Isar.} The theory loader + automatically exploits the overall parallelism of independent nodes + in the development graph, as well as the inherent irrelevance of + proofs for goals being fully specified in advance. This means, + checking of individual Isar proofs is parallelized by default. + Beyond that, very sophisticated proof tools may use local + parallelism internally, via the general programming model of + ``future values'' (see also \hyperlink{file.~~/src/Pure/Concurrent/future.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}future{\isachardot}ML}}}}). - Any user-code that works relatively to the present background theory + Any ML code that works relatively to the present background theory is already safe. Contextual data may be easily stored within the theory or proof context, thanks to the generic data concept of Isabelle/Isar (see \secref{sec:context-data}). This greatly @@ -197,9 +203,11 @@ quickly, otherwise parallel execution performance may degrade significantly. - Despite this potential bottle-neck, we refrain from fine-grained - locking mechanism within user-code: the restriction to a single lock - prevents deadlocks without demanding special precautions. + Despite this potential bottle-neck, centralized locking is + convenient, because it prevents deadlocks without demanding special + precautions. Explicit communication demands other means, though. + The high-level abstraction of synchronized variables \hyperlink{file.~~/src/Pure/Concurrent/synchronized.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}synchronized{\isachardot}ML}}}} enables parallel + components to communicate via shared state; see also \hyperlink{file.~~/src/Pure/Concurrent/mailbox.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}mailbox{\isachardot}ML}}}} as canonical example. \paragraph{Good conduct of impure programs.} The following guidelines enable non-functional programs to participate in diff -r 5eff800a695f -r c3d1f87a3cb0 doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Wed Dec 24 13:29:49 2008 -0800 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Wed Dec 24 13:39:20 2008 -0800 @@ -683,17 +683,23 @@ @{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\ @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\ @{syntax_def (inner) num} & = & @{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat} \\ + @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\ @{syntax_def (inner) xnum} & = & @{verbatim "#"}@{syntax_ref nat}@{text " | "}@{verbatim "#-"}@{syntax_ref nat} \\ @{syntax_def (inner) xstr} & = & @{verbatim "''"} @{text "\"} @{verbatim "''"} \\ \end{supertabular} \end{center} - The token categories @{syntax_ref (inner) num}, @{syntax_ref (inner) - xnum}, and @{syntax_ref (inner) xstr} are not used in Pure. - Object-logics may implement numerals and string constants by adding - appropriate syntax declarations, together with some translation - functions (e.g.\ see Isabelle/HOL). + The token categories @{syntax (inner) num}, @{syntax (inner) + float_token}, @{syntax (inner) xnum}, and @{syntax (inner) xstr} are + not used in Pure. Object-logics may implement numerals and string + constants by adding appropriate syntax declarations, together with + some translation functions (e.g.\ see Isabelle/HOL). + + The derived categories @{syntax_def (inner) num_const} and + @{syntax_def (inner) float_const} provide robust access to @{syntax + (inner) num}, and @{syntax (inner) float_token}, respectively: the + syntax tree holds a syntactic constant instead of a free variable. *} diff -r 5eff800a695f -r c3d1f87a3cb0 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Dec 24 13:29:49 2008 -0800 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Dec 24 13:39:20 2008 -0800 @@ -702,16 +702,21 @@ \indexdef{inner}{syntax}{tid}\hypertarget{syntax.inner.tid}{\hyperlink{syntax.inner.tid}{\mbox{\isa{tid}}}} & = & \indexref{}{syntax}{typefree}\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}} \\ \indexdef{inner}{syntax}{tvar}\hypertarget{syntax.inner.tvar}{\hyperlink{syntax.inner.tvar}{\mbox{\isa{tvar}}}} & = & \indexref{}{syntax}{typevar}\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}} \\ \indexdef{inner}{syntax}{num}\hypertarget{syntax.inner.num}{\hyperlink{syntax.inner.num}{\mbox{\isa{num}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\ + \indexdef{inner}{syntax}{float\_token}\hypertarget{syntax.inner.float-token}{\hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isacharunderscore}token}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\ \indexdef{inner}{syntax}{xnum}\hypertarget{syntax.inner.xnum}{\hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}} & = & \verb|#|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|#-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\ \indexdef{inner}{syntax}{xstr}\hypertarget{syntax.inner.xstr}{\hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}}} & = & \verb|''| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|''| \\ \end{supertabular} \end{center} - The token categories \indexref{inner}{syntax}{num}\hyperlink{syntax.inner.num}{\mbox{\isa{num}}}, \indexref{inner}{syntax}{xnum}\hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}, and \indexref{inner}{syntax}{xstr}\hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}} are not used in Pure. - Object-logics may implement numerals and string constants by adding - appropriate syntax declarations, together with some translation - functions (e.g.\ see Isabelle/HOL).% + The token categories \hyperlink{syntax.inner.num}{\mbox{\isa{num}}}, \hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isacharunderscore}token}}}, \hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}, and \hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}} are + not used in Pure. Object-logics may implement numerals and string + constants by adding appropriate syntax declarations, together with + some translation functions (e.g.\ see Isabelle/HOL). + + The derived categories \indexdef{inner}{syntax}{num\_const}\hypertarget{syntax.inner.num-const}{\hyperlink{syntax.inner.num-const}{\mbox{\isa{num{\isacharunderscore}const}}}} and + \indexdef{inner}{syntax}{float\_const}\hypertarget{syntax.inner.float-const}{\hyperlink{syntax.inner.float-const}{\mbox{\isa{float{\isacharunderscore}const}}}} provide robust access to \hyperlink{syntax.inner.num}{\mbox{\isa{num}}}, and \hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isacharunderscore}token}}}, respectively: the + syntax tree holds a syntactic constant instead of a free variable.% \end{isamarkuptext}% \isamarkuptrue% % diff -r 5eff800a695f -r c3d1f87a3cb0 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Wed Dec 24 13:29:49 2008 -0800 +++ b/src/Pure/Syntax/lexicon.ML Wed Dec 24 13:39:20 2008 -0800 @@ -145,8 +145,18 @@ val tidT = Type ("tid", []); val tvarT = Type ("tvar", []); -val terminals = - ["id", "longid", "var", "tid", "tvar", "num", "float", "xnum", "xstr"]; +val terminal_kinds = + [("id", IdentSy), + ("longid", LongIdentSy), + ("var", VarSy), + ("tid", TFreeSy), + ("tvar", TVarSy), + ("num", NumSy), + ("float_token", FloatSy), + ("xnum", XNumSy), + ("xstr", StrSy)]; + +val terminals = map #1 terminal_kinds; val is_terminal = member (op =) terminals; @@ -186,16 +196,10 @@ (* predef_term *) -fun predef_term "id" = SOME (Token (IdentSy, "id", Position.no_range)) - | predef_term "longid" = SOME (Token (LongIdentSy, "longid", Position.no_range)) - | predef_term "var" = SOME (Token (VarSy, "var", Position.no_range)) - | predef_term "tid" = SOME (Token (TFreeSy, "tid", Position.no_range)) - | predef_term "tvar" = SOME (Token (TVarSy, "tvar", Position.no_range)) - | predef_term "num" = SOME (Token (NumSy, "num", Position.no_range)) - | predef_term "float" = SOME (Token (FloatSy, "float", Position.no_range)) - | predef_term "xnum" = SOME (Token (XNumSy, "xnum", Position.no_range)) - | predef_term "xstr" = SOME (Token (StrSy, "xstr", Position.no_range)) - | predef_term _ = NONE; +fun predef_term s = + (case AList.lookup (op =) terminal_kinds s of + SOME sy => SOME (Token (sy, s, Position.no_range)) + | NONE => NONE); (* xstr tokens *) @@ -382,21 +386,27 @@ | "0" :: "b" :: cs => (1, 2, cs) | "-" :: cs => (~1, 10, cs) | cs => (1, 10, cs)); - val value = sign * #1 (Library.read_radix_int radix digs); - in {radix = radix, leading_zeros = leading_zeros digs, value = value} end; + in + {radix = radix, + leading_zeros = leading_zeros digs, + value = sign * #1 (Library.read_radix_int radix digs)} + end; end; fun read_float str = let val (sign, cs) = - (case Symbol.explode str of "-" :: cs => (~1, cs) | cs => (1, cs)); - val (intpart,fracpart) = + (case Symbol.explode str of + "-" :: cs => (~1, cs) + | cs => (1, cs)); + val (intpart, fracpart) = (case take_prefix Symbol.is_digit cs of - (intpart, "." :: fracpart) => (intpart,fracpart) - | _ => sys_error "read_float") - in {mant = sign * #1 (Library.read_int (intpart@fracpart)), - exp = length fracpart} + (intpart, "." :: fracpart) => (intpart, fracpart) + | _ => raise Fail "read_float"); + in + {mant = sign * #1 (Library.read_int (intpart @ fracpart)), + exp = length fracpart} end end; diff -r 5eff800a695f -r c3d1f87a3cb0 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Wed Dec 24 13:29:49 2008 -0800 +++ b/src/Pure/pure_thy.ML Wed Dec 24 13:39:20 2008 -0800 @@ -322,7 +322,7 @@ ("", typ "var => logic", Delimfix "_"), ("_DDDOT", typ "logic", Delimfix "..."), ("_constify", typ "num => num_const", Delimfix "_"), - ("_constify", typ "float => float_const", Delimfix "_"), + ("_constify", typ "float_token => float_const", Delimfix "_"), ("_indexnum", typ "num_const => index", Delimfix "\\<^sub>_"), ("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"), ("_indexdefault", typ "index", Delimfix ""),