--- a/.hgtags Thu Mar 13 14:47:56 2025 +0100
+++ b/.hgtags Thu Mar 13 15:49:15 2025 +0100
@@ -48,3 +48,4 @@
5888f0bec9718859a47c31da538bdef59c3f38b7 Isabelle2025-RC2
52290d6ab92d628c7d8a07638b21125e23733e1d Isabelle2025-RC3
ac7c09c6ff2f6886da114adfa7b1abd690c782ca Isabelle2025-RC4
+4b875a4c83b0696d326e598069b3b8dafcf511c8 Isabelle2025
--- a/Admin/Release/CHECKLIST Thu Mar 13 14:47:56 2025 +0100
+++ b/Admin/Release/CHECKLIST Thu Mar 13 15:49:15 2025 +0100
@@ -59,7 +59,7 @@
- Windows: check recent MiKTeX;
-- Phabricator:
+- Phorge:
. src/Doc/System/Phabricator.thy: check/update underlying Ubuntu version
. etc/options: check/update phabricator_version entries;
@@ -80,7 +80,7 @@
- regular packaging:
#on fast Linux machine, with access to build_host for each platform
- Admin/build_release -D ~/tmp/isadist -b HOL -R Isabelle2025 -j2 -l
+ Admin/build_release -D ~/tmp/isadist -b HOL -R Isabelle2025 -j2 -l -F -L
- Docker image:
--- a/Admin/components/bundled Thu Mar 13 14:47:56 2025 +0100
+++ b/Admin/components/bundled Thu Mar 13 15:49:15 2025 +0100
@@ -1,2 +1,1 @@
#additional components to be bundled for release
-naproche-20250228
--- a/Admin/components/components.sha1 Thu Mar 13 14:47:56 2025 +0100
+++ b/Admin/components/components.sha1 Thu Mar 13 15:49:15 2025 +0100
@@ -367,6 +367,7 @@
8212b431b495f2771c3c27bc3ae0418f55cefa88 naproche-20250125.tar.gz
da83a3350cf27ca1ab3c86de6b6b60178cfda0db naproche-20250201.tar.gz
434e2a6dc6fe681f7cb7b4e348fd26dbada17e61 naproche-20250228.tar.gz
+a7524802f0a12c3dc3cee594d8b22b91848eecb5 naproche-20250310.tar.gz
d098dd0873b1720a77dc4e060267f9a6c93f341a naproche-2d99afe5c349.tar.gz
4a4e56fd03b7ba4edd38046f853873a90cf55d1a naproche-4ad61140062f.tar.gz
77252e0b40f89825b9b5935f9f0c4cd5d4e7012a naproche-6d0d76ce2f2a.tar.gz
--- a/NEWS Thu Mar 13 14:47:56 2025 +0100
+++ b/NEWS Thu Mar 13 15:49:15 2025 +0100
@@ -221,8 +221,8 @@
* The Output dockable (and its variants used elsewhere) has been
improved as follows:
- - Its vertical scroll position is maintained more carefully, when
- messages are printed incrementally.
+ - Its scroll position is maintained more carefully, when messages are
+ printed incrementally.
- Performance of printing messages repeatedly has improved slightly,
with less load on the GUI thread.
@@ -426,6 +426,9 @@
Variable.variant_names or Variable.focus_params, instead of
Logic.goal_params etc.
+* Proper documentation for ML antiquotation \<^instantiate>: see
+"implementation" manual, section "2.6 Instantiation of formal entities".
+
* Antiquotation \<^instantiate>\<open>(no_beta) x = t in \<dots>\<close> is like
\<^instantiate>\<open>x = t in \<dots>\<close>, but without implicit beta-normalization.
This is occasionally useful for low-level applications.
--- a/src/Doc/Implementation/Logic.thy Thu Mar 13 14:47:56 2025 +0100
+++ b/src/Doc/Implementation/Logic.thy Thu Mar 13 15:49:15 2025 +0100
@@ -807,7 +807,9 @@
;
@@{ML_antiquotation thms} thms
;
- @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \<newline>
+ @@{ML_antiquotation lemma} @{syntax embedded_lemma}
+ ;
+ @{syntax_def embedded_lemma} ('(' @'open' ')')? ((prop +) + @'and') \<newline>
@{syntax for_fixes} @'by' method method?
;
@@{ML_antiquotation oracle_name} embedded
@@ -1359,4 +1361,128 @@
proof terms via XML/ML data representation.
\<close>
+section \<open>Instantiation of formal entities \label{sec:instantiation}\<close>
+
+text \<open>
+ The construction of formal entities (types, terms, theorems) in Isabelle/ML
+ can be tedious, error-prone, and costly at run-time. Repeated certification
+ of types/terms, or proof steps for theorems should be minimized, when
+ performance is relevant.
+
+ For example, consider a proof-producing decision procedure that refers to
+ certain term schemes and derived rules that need to be applied repeatedly. A
+ reasonably efficient approach is the subsequent separation of Isabelle/ML
+ \<^emph>\<open>compile-time\<close> vs. \<^emph>\<open>run-time\<close>. Lets say there is an ML module that is
+ loaded into the theory context to provide a tool as proof method, to be used
+ later in a different context.
+
+ \<^item> At compile-time, the ML module constructs templates for relevant formal
+ entities, e.g. as certified types/terms and proven theorems (with
+ parameters). This uses the source notation for types, terms, propositions,
+ inlined into Isabelle/ML. Formal parameters are taken from the template,
+ and turned into ML names (as in \<^verbatim>\<open>let\<close> expressions).
+
+ \<^item> At run-time, the ML tool takes concrete entities from the application
+ context, and instantiates the above templates accordingly. The formal
+ parameters of the compile-time template get assigned to concrete ML
+ values. ML names and types have already been properly checked by the ML
+ compiler, and the running program cannot go wrong in that respect. (It
+ \<^emph>\<open>can\<close> go wrong, concerning types of the implemented logic, though).
+
+ This approach is supported by ML antiquotations as follows.
+\<close>
+
+text %mlantiq \<open>
+ \begin{matharray}{rcl}
+ @{ML_antiquotation_def "instantiate"} & : & \<open>ML_antiquotation\<close> \\
+ \end{matharray}
+
+ \<^rail>\<open>
+ @@{ML_antiquotation instantiate} embedded
+ \<close>
+
+ \<^descr> \<open>@{instantiation source}\<close> refers to embedded source text to produce an
+ instantiation for a logical entity that is given literally in the text. The
+ content of the @{syntax embedded} argument follows the syntax category
+ @{syntax instantiation} defined below, using @{syntax embedded_ml} from
+ antiquotation @{ML_antiquotation Type} (\secref{sec:types}), and @{syntax
+ embedded_lemma} from antiquotation @{ML_antiquotation lemma}
+ (\secref{sec:thms}).
+
+ \<^rail>\<open>
+ @{syntax_def instantiation}: no_beta? (inst + @'and') @'in' @{syntax body}
+ ;
+ no_beta: '(' 'no_beta' ')'
+ ;
+ schematic: '(' 'schematic' ')'
+ ;
+ inst: ((type_ident | name) ((@'=' @{syntax embedded_ml}))?)
+ ;
+ body: body_type | body_term | body_prop | body_lemma
+ ;
+ body_type: ('typ' | 'ctyp') schematic? embedded
+ ;
+ body_term: ('term' | 'cterm') schematic? embedded
+ ;
+ body_prop: ('prop' | 'cprop') schematic? embedded
+ ;
+ body_lemma: 'lemma' schematic? @{syntax embedded_lemma}
+ \<close>
+
+ \<^item> An @{syntax inst} entry assigns a type/term variable to a suitable ML
+ value, given as ML expression in the current program context. The ML type
+ of the expression needs to fit to the situation: \<^verbatim>\<open>'a =\<close>~\<open>ty\<close> refers to
+ \<open>ty\<close>\<^verbatim>\<open>: typ\<close> or \<open>ty\<close>\<^verbatim>\<open>: ctyp\<close>, and \<^verbatim>\<open>a =\<close>~\<open>tm\<close> refers to \<open>tm\<close>\<^verbatim>\<open>: term\<close> or
+ \<open>tm\<close>\<^verbatim>\<open>: cterm\<close>. Only a body for uncertified \<^verbatim>\<open>typ\<close> / \<^verbatim>\<open>term\<close> / \<^verbatim>\<open>prop\<close>
+ admits uncertified \<^ML_type>\<open>typ\<close> or \<^ML_type>\<open>term\<close> parameters. The
+ other cases require certified \<^ML_type>\<open>ctyp\<close> or \<^ML_type>\<open>cterm\<close>
+ parameters.
+
+ If the RHS of the @{syntax inst} entry is omitted, it defaults to the LHS:
+ \<^verbatim>\<open>a\<close> becomes \<^verbatim>\<open>a = a\<close>. This only works for term variables that happen to
+ be legal ML identifiers, and not for type variables.
+
+ \<^item> The ``\<open>(schematic)\<close>'' option disables the usual check that all LHS names
+ in @{syntax inst} are exactly those present as free variables in the body
+ entity (type, term, prop, lemma statement). By default, omitted variables
+ cause an error, but with ``\<open>(schematic)\<close>'' they remain as schematic
+ variables. The latter needs to be used with care, because unexpected
+ variables may emerge, when the theory name space for constants changes
+ over time.
+
+ \<^item> The ``\<open>(no_beta)\<close>'' option disables the usual \<open>\<beta>\<close>-normalization for
+ \<open>body_term\<close> / \<open>body_prop\<close> / \<open>body_lemma\<close>, but has no effect on
+ \<open>body_type\<close>. This is occasionally useful for low-level applications, where
+ \<open>\<beta>\<close>-conversion is treated explicitly in primitive inferences.
+\<close>
+
+text %mlex \<open>
+ Below are some examples that demonstrate the antiquotation syntax.
+ Real-world applications may be found in the Isabelle sources, by searching
+ for the literal text ``\<^verbatim>\<open>\<^instantiate>\<close>''.
+\<close>
+
+ML \<open>
+ \<comment> \<open>uncertified type parameters\<close>
+ fun make_assoc_type (A: typ, B: typ) : typ =
+ \<^instantiate>\<open>'a = A and 'b = B in typ \<open>('a \<times> 'b) list\<close>\<close>;
+
+ \<comment> \<open>uncertified term parameters\<close>
+ val make_assoc_list : (term * term) list -> term list =
+ map (fn (x, y) =>
+ \<^instantiate>\<open>'a = \<open>fastype_of x\<close> and 'b = \<open>fastype_of y\<close> and
+ x and y in term \<open>(x, y)\<close> for x :: 'a and y :: 'b\<close>);
+
+ \<comment> \<open>theorem with certified term parameters\<close>
+ fun symmetry (x: cterm) (y: cterm) : thm =
+ \<^instantiate>\<open>'a = \<open>Thm.ctyp_of_cterm x\<close> and x and y in
+ lemma \<open>x = y \<Longrightarrow> y = x\<close> for x y :: 'a by simp\<close>
+
+ \<comment> \<open>theorem with certified type parameter, and schematic result\<close>
+ fun symmetry_schematic (A: ctyp) : thm =
+ \<^instantiate>\<open>'a = A in
+ lemma (schematic) \<open>x = y \<Longrightarrow> y = x\<close> for x y :: 'a by simp\<close>
+\<close>
+
+
end
--- a/src/Doc/JEdit/JEdit.thy Thu Mar 13 14:47:56 2025 +0100
+++ b/src/Doc/JEdit/JEdit.thy Thu Mar 13 15:49:15 2025 +0100
@@ -336,7 +336,7 @@
technical problems have accumulated in recent years (e.g.\ see
\secref{sec:problems}).
- In 2021, we are de-facto back to \<^emph>\<open>portable look-and-feels\<close>, which also
+ Since 2021, we are de-facto back to \<^emph>\<open>portable look-and-feels\<close>, which also
happen to be \emph{scalable} on high-resolution displays:
\<^item> \<^verbatim>\<open>FlatLaf Light\<close> is the default for Isabelle/jEdit on all platforms. It
@@ -1039,6 +1039,21 @@
\end{figure}
\<^medskip>
+ \<^emph>\<open>Explicit highlighting\<close> of output works via the \<^emph>\<open>Search\<close> field: it matches
+ the text against a given regular expression, in the notation of
+ Java.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close>
+ Results are also presented as a tree view, by sub-dividing the output panel
+ on demand.
+
+ \<^emph>\<open>Implicit highlighting\<close> of output is based on formal markup by the prover.
+ If the \<^emph>\<open>Auto hovering\<close> option is enabled (default), then mouse hovering
+ alone is sufficient to see highlighted ranges stemming from nested syntax
+ structure (see also \secref{sec:tooltips-hyperlinks}); together with the ALT
+ keyboard modifier this produces a selection that is ready for copy-paste.
+ Without \<^emph>\<open>Auto hovering\<close>, an additional keyboard modifier \<^verbatim>\<open>CONTROL\<close> (Linux,
+ Windows) or \<^verbatim>\<open>COMMAND\<close> (macOS) is required, as for input text.
+
+ \<^medskip>
Following the IDE principle, regular messages are attached to the original
source in the proper place and may be inspected on demand via popups. This
excludes messages that are somehow internal to the machinery of proof
@@ -1082,7 +1097,7 @@
proof state messages without further distraction, while all other messages
are displayed in \<^emph>\<open>Output\<close> (\secref{sec:output}).
\Figref{fig:output-and-state} shows a typical GUI layout where both panels
- are open.
+ are open, while the \<^emph>\<open>Proof state\<close> option is disabled within \<^emph>\<open>Output\<close>.
\begin{figure}[!htb]
\begin{center}
@@ -1151,10 +1166,8 @@
\<^item> The \<^emph>\<open>Apply\<close> button attaches a fresh query invocation to the current
context of the command where the cursor is pointing in the text.
- \<^item> The \<^emph>\<open>Search\<close> field allows to highlight query output according to some
- regular expression, in the notation that is commonly used on the Java
- platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close>
- This may serve as an additional visual filter of the result.
+ \<^item> The \<^emph>\<open>Search\<close> warks as in the \<^emph>\<open>Output\<close> panel (\secref{sec:output}), but
+ without an extra tree view.
\<^item> The \<^emph>\<open>Zoom\<close> box controls the font size of the output area.
@@ -1209,7 +1222,7 @@
\<close>
-section \<open>Tooltips and hyperlinks \label{sec:tooltips-hyperlinks}\<close>
+section \<open>Tooltips, hyperlinks, and syntax structure \label{sec:tooltips-hyperlinks}\<close>
text \<open>
Formally processed text (prover input or output) contains rich markup that
@@ -1255,6 +1268,29 @@
document processing of the editor session and thus prevents further
exploration: the chain of hyperlinks may end in some source file of the
underlying logic image, or within the ML bootstrap sources of Isabelle/Pure.
+
+ \<^medskip>
+ Hyperlinks refer to atomic entities of formal syntax, but it is also
+ possible to visualize nested syntax structure, according to formal markup by
+ the prover. This information is derived from by pretty-printing blocks
+ within mixfix annotations: it is automatic for \<^theory_text>\<open>infix\<close> and \<^theory_text>\<open>binder\<close>, but
+ needs to be specified explicitly for free-form mixfix syntax (by the authors
+ of the theory library). \Figref{fig:syntax-structure} illustrates the result
+ for nested \<^theory_text>\<open>infix\<close>-expressions in Isabelle/HOL.
+
+ \begin{figure}[!htb]
+ \begin{center}
+ \includegraphics[scale=0.333]{popup3} \\[1ex]
+ \includegraphics[scale=0.333]{popup4}
+ \end{center}
+ \caption{Visualized markup for nested infix expressions}
+ \label{fig:syntax-structure}
+ \end{figure}
+
+ Instead of exploring formal syntax via the mouse, it is also possible to use
+ the keyboard action @{action_def "isabelle.select-structure"} (\<^verbatim>\<open>C+7\<close>). It
+ extends the editor selection by adding the enclosing syntax structure.
+ Repeated invocation of this action extends the selection incrementally.
\<close>
Binary file src/Doc/JEdit/document/auto-tools.png has changed
Binary file src/Doc/JEdit/document/bibtex-mode.png has changed
Binary file src/Doc/JEdit/document/cite-completion.png has changed
Binary file src/Doc/JEdit/document/document-panel.png has changed
Binary file src/Doc/JEdit/document/isabelle-jedit.png has changed
Binary file src/Doc/JEdit/document/markdown-document.png has changed
Binary file src/Doc/JEdit/document/ml-debugger.png has changed
Binary file src/Doc/JEdit/document/output-and-state.png has changed
Binary file src/Doc/JEdit/document/output-including-state.png has changed
Binary file src/Doc/JEdit/document/output.png has changed
Binary file src/Doc/JEdit/document/popup1.png has changed
Binary file src/Doc/JEdit/document/popup2.png has changed
Binary file src/Doc/JEdit/document/popup3.png has changed
Binary file src/Doc/JEdit/document/popup4.png has changed
Binary file src/Doc/JEdit/document/query.png has changed
Binary file src/Doc/JEdit/document/scope1.png has changed
Binary file src/Doc/JEdit/document/scope2.png has changed
Binary file src/Doc/JEdit/document/sidekick-document.png has changed
Binary file src/Doc/JEdit/document/sidekick.png has changed
Binary file src/Doc/JEdit/document/sledgehammer.png has changed
Binary file src/Doc/JEdit/document/theories.png has changed
--- a/src/Doc/ROOT Thu Mar 13 14:47:56 2025 +0100
+++ b/src/Doc/ROOT Thu Mar 13 15:49:15 2025 +0100
@@ -226,6 +226,8 @@
"output.png"
"popup1.png"
"popup2.png"
+ "popup3.png"
+ "popup4.png"
"query.png"
"root.tex"
"scope1.png"