merged.
--- 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"
+
--- 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"
--- 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
--- 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 ***
--- 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
--- 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
--- 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 "\<dots>"} @{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.
*}
--- 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%
%
--- 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;
--- 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 ""),