(*:maxLineLen=78:*)
theory Scala
imports Base
begin
chapter \<open>Isabelle/Scala systems programming \label{sec:scala}\<close>
text \<open>
Isabelle/ML and Isabelle/Scala are the two main implementation languages of
the Isabelle environment:
\<^item> Isabelle/ML is for \<^emph>\<open>mathematics\<close>, to develop tools within the context
of symbolic logic, e.g.\ for constructing proofs or defining
domain-specific formal languages. See the \<^emph>\<open>Isabelle/Isar implementation
manual\<close> @{cite "isabelle-implementation"} for more details.
\<^item> Isabelle/Scala is for \<^emph>\<open>physics\<close>, to connect with the world of systems
and services, including editors and IDE frameworks.
There are various ways to access Isabelle/Scala modules and operations:
\<^item> Isabelle command-line tools (\secref{sec:scala-tools}) run in a separate
Java process.
\<^item> Isabelle/ML antiquotations access Isabelle/Scala functions
(\secref{sec:scala-functions}) via the PIDE protocol: execution happens
within the running Java process underlying Isabelle/Scala.
\<^item> The \<^verbatim>\<open>Console/Scala\<close> plugin of Isabelle/jEdit @{cite "isabelle-jedit"}
operates on the running Java application, using the Scala
read-eval-print-loop (REPL).
The main Isabelle/Scala/jEdit functionality is provided by
\<^file>\<open>$ISABELLE_HOME/lib/classes/isabelle.jar\<close>. Further underlying Scala and
Java libraries are bundled with Isabelle, e.g.\ to access SQLite or
PostgreSQL via JDBC.
Add-on Isabelle components may augment the system environment by providing
suitable configuration in \<^path>\<open>etc/settings\<close> (GNU bash script). The
shell function \<^bash_function>\<open>classpath\<close> helps to write
\<^path>\<open>etc/settings\<close> in a portable manner: it refers to library \<^verbatim>\<open>jar\<close>
files in standard POSIX path notation. On Windows, this is converted to
native platform format, before invoking Java (\secref{sec:scala-tools}).
\<^medskip>
There is also an implicit build process for Isabelle/Scala/Java modules,
based on \<^path>\<open>etc/build.props\<close> within the component directory (see also
\secref{sec:scala-build}).
\<close>
section \<open>Command-line tools \label{sec:scala-tools}\<close>
subsection \<open>Java Runtime Environment \label{sec:tool-java}\<close>
text \<open>
The @{tool_def java} tool is a direct wrapper for the Java Runtime
Environment, within the regular Isabelle settings environment
(\secref{sec:settings}) and Isabelle classpath. The command line arguments
are that of the bundled Java distribution: see option \<^verbatim>\<open>-help\<close> in
particular.
The \<^verbatim>\<open>java\<close> executable is taken from @{setting ISABELLE_JDK_HOME}, according
to the standard directory layout for regular distributions of OpenJDK.
The shell function \<^bash_function>\<open>isabelle_jdk\<close> allows shell scripts to
invoke other Java tools robustly (e.g.\ \<^verbatim>\<open>isabelle_jdk jar\<close>), without
depending on accidental operating system installations.
\<close>
subsection \<open>Scala toplevel \label{sec:tool-scala}\<close>
text \<open>
The @{tool_def scala} tool is a direct wrapper for the Scala toplevel,
similar to @{tool java} above. The command line arguments are that of the
bundled Scala distribution: see option \<^verbatim>\<open>-help\<close> in particular. This allows
to interact with Isabelle/Scala interactively.
\<close>
subsubsection \<open>Example\<close>
text \<open>
Explore the Isabelle system environment in Scala:
@{verbatim [display, indent = 2] \<open>$ isabelle scala\<close>}
@{scala [display, indent = 2]
\<open>import isabelle._
val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME")
val options = Options.init()
options.bool("browser_info")
options.string("document")\<close>}
\<close>
subsection \<open>Scala script wrapper\<close>
text \<open>
The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"}
allows to run Isabelle/Scala source files stand-alone programs, by using a
suitable ``hash-bang'' line and executable file permissions. For example:
@{verbatim [display, indent = 2] \<open>#!/usr/bin/env isabelle_scala_script\<close>}
@{scala [display, indent = 2]
\<open>val options = isabelle.Options.init()
Console.println("browser_info = " + options.bool("browser_info"))
Console.println("document = " + options.string("document"))\<close>}
This assumes that the executable may be found via the @{setting PATH} from
the process environment: this is the case when Isabelle settings are active,
e.g.\ in the context of the main Isabelle tool wrapper
\secref{sec:isabelle-tool}. Alternatively, the full
\<^file>\<open>$ISABELLE_HOME/bin/isabelle_scala_script\<close> may be specified in expanded
form.
\<close>
subsection \<open>Scala compiler \label{sec:tool-scalac}\<close>
text \<open>
The @{tool_def scalac} tool is a direct wrapper for the Scala compiler; see
also @{tool scala} above. The command line arguments are that of the
bundled Scala distribution.
This provides a low-level mechanism to compile further Scala modules,
depending on existing Isabelle/Scala functionality; the resulting \<^verbatim>\<open>class\<close>
or \<^verbatim>\<open>jar\<close> files can be added to the Java classpath using the shell function
\<^bash_function>\<open>classpath\<close>.
A more convenient high-level approach works via \<^path>\<open>etc/build.props\<close>
(see \secref{sec:scala-build}).
\<close>
section \<open>Isabelle/Scala/Java modules \label{sec:scala-build}\<close>
subsection \<open>Component configuration via \<^path>\<open>etc/build.props\<close>\<close>
text \<open>
Isabelle components may augment the Isabelle/Scala/Java environment
declaratively via properties given in \<^path>\<open>etc/build.props\<close> (within the
component directory). This specifies an output \<^verbatim>\<open>jar\<close> \<^emph>\<open>module\<close>, based on
Scala or Java \<^emph>\<open>sources\<close>, and arbitrary \<^emph>\<open>resources\<close>. Moreover, a module can
specify \<^emph>\<open>services\<close> that are subclasses of
\<^scala_type>\<open>isabelle.Isabelle_System.Service\<close>; these have a particular
meaning to Isabelle/Scala tools.
Before running a Scala or Java process, the Isabelle system implicitly
ensures that all provided modules are compiled and packaged (as jars). It is
also possible to invoke @{tool scala_build} explicitly, with extra options.
\<^medskip>
The syntax of in \<^path>\<open>etc/build.props\<close> follows a regular Java properties
file\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/15/docs/api/java.base/java/util/Properties.html#load(java.io.Reader)\<close>\<close>,
but the encoding is \<^verbatim>\<open>UTF-8\<close>, instead of historic \<^verbatim>\<open>ISO 8859-1\<close> from the API
documentation.
The subsequent properties are relevant for the Scala/Java build process.
Most properties are optional: the default is an empty string (or list). File
names are relative to the main component directory and may refer to Isabelle
settings variables (e.g. \<^verbatim>\<open>$ISABELLE_HOME\<close>).
\<^item> \<^verbatim>\<open>title\<close> (required) is a human-readable description of the module, used
in printed messages.
\<^item> \<^verbatim>\<open>module\<close> specifies a \<^verbatim>\<open>jar\<close> file name for the output module, as result
of compiling the specified sources (and resources). If this is absent,
there is no build process, but contributing sources may still be given,
possibly together with \<^verbatim>\<open>no_module\<close> as described below.
\<^item> \<^verbatim>\<open>no_module\<close> means that there is no build process, but the specified
\<^verbatim>\<open>jar\<close> is provided by other means. This is relevant for @{tool
scala_project} (\secref{sec:tool-scala-project}), which includes all
Scala/Java sources of components, but suppresses \<^verbatim>\<open>jar\<close> modules to avoid
duplication of content.
\<^item> \<^verbatim>\<open>scalac_options\<close> and \<^verbatim>\<open>javac_options\<close> augment the default settings
@{setting_ref ISABELLE_SCALAC_OPTIONS} and @{setting_ref
ISABELLE_JAVAC_OPTIONS} for this component; option syntax follows the
regular command-line tools \<^verbatim>\<open>scalac\<close> and \<^verbatim>\<open>javac\<close>, respectively.
\<^item> \<^verbatim>\<open>main\<close> specifies the main entry point for the \<^verbatim>\<open>jar\<close> module. This is
only relevant for direct invocation like ``\<^verbatim>\<open>java -jar test.jar\<close>''.
\<^item> \<^verbatim>\<open>requirements\<close> is a list of \<^verbatim>\<open>jar\<close> modules that are needed in the
compilation process, but not provided by the regular classpath (notably
@{setting ISABELLE_CLASSPATH}).
A \<^emph>\<open>normal entry\<close> refers to a single \<^verbatim>\<open>jar\<close> file name, possibly with
settings variables as usual. E.g. \<^file>\<open>$ISABELLE_SCALA_JAR\<close> for the main
\<^file>\<open>$ISABELLE_HOME/lib/classes/isabelle.jar\<close> (especially relevant for
add-on modules).
A \<^emph>\<open>special entry\<close> is of of the form \<^verbatim>\<open>env:\<close>\<open>variable\<close> and refers to a
settings variable from the Isabelle environment: its value may consist of
multiple \<^verbatim>\<open>jar\<close> entries (separated by colons). Environment variables are
not expanded recursively.
\<^item> \<^verbatim>\<open>resources\<close> is a list of files that should be included in the resulting
\<^verbatim>\<open>jar\<close> file. Each item consists of a pair separated by colon:
\<open>source\<close>\<^verbatim>\<open>:\<close>\<open>target\<close> means to copy an existing source file (relative to
the component directory) to the given target file or directory (relative
to the \<^verbatim>\<open>jar\<close> name space). A \<open>file\<close> specification without colon
abbreviates \<open>file\<close>\<^verbatim>\<open>:\<close>\<open>file\<close>, i.e. the file is copied while retaining its
relative path name.
\<^item> \<^verbatim>\<open>sources\<close> is a list of \<^verbatim>\<open>.scala\<close> or \<^verbatim>\<open>.java\<close> files that contribute to
the specified module. It is possible to use both languages simultaneously:
the Scala and Java compiler will be invoked consecutively to make this
work.
\<^item> \<^verbatim>\<open>services\<close> is a list of class names to be registered as Isabelle
service providers (subclasses of
\<^scala_type>\<open>isabelle.Isabelle_System.Service\<close>). Internal class names of
the underlying JVM need to be given: e.g. see method @{scala_method (in
java.lang.Object) getClass}.
Particular services require particular subclasses: instances are filtered
according to their dynamic type. For example, class
\<^scala_type>\<open>isabelle.Isabelle_Scala_Tools\<close> collects Scala command-line
tools, and class \<^scala_type>\<open>isabelle.Scala.Functions\<close> collects Scala
functions (\secref{sec:scala-functions}).
\<close>
subsection \<open>Explicit Isabelle/Scala/Java build \label{sec:tool-scala-build}\<close>
text \<open>
The @{tool_def scala_build} tool explicitly invokes the build process for
all registered components.
@{verbatim [display]
\<open>Usage: isabelle scala_build [OPTIONS]
Options are:
-f force fresh build
-q quiet mode: suppress stdout/stderr
Build Isabelle/Scala/Java modules of all registered components
(if required).
\<close>}
For each registered Isabelle component that provides
\<^path>\<open>etc/build.props\<close>, the specified output \<^verbatim>\<open>module\<close> is checked against
the corresponding input \<^verbatim>\<open>requirements\<close>, \<^verbatim>\<open>resources\<close>, \<^verbatim>\<open>sources\<close>. If
required, there is an automatic build using \<^verbatim>\<open>scalac\<close> or \<^verbatim>\<open>javac\<close> (or both).
The identity of input files is recorded within the output \<^verbatim>\<open>jar\<close>, using SHA1
digests in \<^verbatim>\<open>META-INF/isabelle/shasum\<close>.
\<^medskip>
Option \<^verbatim>\<open>-f\<close> forces a fresh build, regardless of the up-to-date status of
input files vs. the output module.
\<^medskip>
Option \<^verbatim>\<open>-q\<close> suppresses all output on stdout/stderr produced by the Scala or
Java compiler.
\<^medskip> Explicit invocation of \<^verbatim>\<open>isabelle scala_build\<close> mainly serves testing or
applications with special options: the Isabelle system normally does an
automatic the build on demand.
\<close>
subsection \<open>Project setup for common Scala IDEs \label{sec:tool-scala-project}\<close>
text \<open>
The @{tool_def scala_project} tool creates a project configuration for all
Isabelle/Scala/Java modules specified in components via \<^path>\<open>etc/build.props\<close>:
@{verbatim [display]
\<open>Usage: isabelle scala_project [OPTIONS] PROJECT_DIR
Options are:
-L make symlinks to original scala files
Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs
such as IntelliJ IDEA.\<close>}
The generated configuration is for Gradle\<^footnote>\<open>\<^url>\<open>https://gradle.org\<close>\<close>, but the
main purpose is to import it into common Scala IDEs, such as IntelliJ
IDEA\<^footnote>\<open>\<^url>\<open>https://www.jetbrains.com/idea\<close>\<close>. This allows to explore the
sources with static analysis and other hints in real-time.
The specified project directory needs to be fresh. The generated files refer
to physical file-system locations, using the path notation of the underlying
OS platform. Thus the project needs to be recreated whenever the Isabelle
installation is changed or moved.
\<^medskip>
By default, Scala sources are \<^emph>\<open>copied\<close> from the Isabelle distribution and
editing them within the IDE has no permanent effect.
Option \<^verbatim>\<open>-L\<close> produces \<^emph>\<open>symlinks\<close> to the original files: this allows to
develop Isabelle/Scala/jEdit within an external Scala IDE. Note that the
result cannot be built within the IDE: it requires implicit or explicit
\<^verbatim>\<open>isabelle scala_build\<close> (\secref{sec:tool-scala-build}).
\<close>
section \<open>Registered Isabelle/Scala functions \label{sec:scala-functions}\<close>
subsection \<open>Defining functions in Isabelle/Scala\<close>
text \<open>
A Scala functions of type \<^scala_type>\<open>String => String\<close> may be wrapped as
\<^scala_type>\<open>isabelle.Scala.Fun\<close> and collected via an instance of the
class \<^scala_type>\<open>isabelle.Scala.Functions\<close>. A system component can then
register that class via \<^verbatim>\<open>services\<close> in \<^path>\<open>etc/build.props\<close>
(\secref{sec:scala-build}). An example is the predefined collection of
\<^scala_type>\<open>isabelle.Scala.Functions\<close> in \<^file>\<open>$ISABELLE_HOME/etc/build.props\<close>.
The overall list of registered functions is accessible in Isabelle/Scala as
\<^scala_object>\<open>isabelle.Scala.functions\<close>.
\<close>
subsection \<open>Invoking functions in Isabelle/ML\<close>
text \<open>
Isabelle/PIDE provides a protocol to invoke registered Scala functions in
ML: this works both within the Prover IDE and in batch builds.
The subsequent ML antiquotations refer to Scala functions in a
formally-checked manner.
\begin{matharray}{rcl}
@{ML_antiquotation_def "scala_function"} & : & \<open>ML_antiquotation\<close> \\
@{ML_antiquotation_def "scala"} & : & \<open>ML_antiquotation\<close> \\
\end{matharray}
\<^rail>\<open>
(@{ML_antiquotation scala_function} |
@{ML_antiquotation scala}) @{syntax embedded}
\<close>
\<^descr> \<open>@{scala_function name}\<close> inlines the checked function name as ML string
literal.
\<^descr> \<open>@{scala name}\<close> and \<open>@{scala_thread name}\<close> invoke the checked function via
the PIDE protocol. In Isabelle/ML this appears as a function of type
\<^ML_type>\<open>string -> string\<close>, which is subject to interrupts within the ML
runtime environment as usual. A \<^scala>\<open>null\<close> result in Scala raises an
exception \<^ML>\<open>Scala.Null\<close> in ML. The execution of \<open>@{scala}\<close> works via a
Scala future on a bounded thread farm, while \<open>@{scala_thread}\<close> always forks
a separate Java thread.
The standard approach of representing datatypes via strings works via XML in
YXML transfer syntax. See Isabelle/ML operations and modules @{ML
YXML.string_of_body}, @{ML YXML.parse_body}, @{ML_structure XML.Encode},
@{ML_structure XML.Decode}; similarly for Isabelle/Scala. Isabelle symbols
may have to be recoded via Scala operations
\<^scala_method>\<open>isabelle.Symbol.decode\<close> and
\<^scala_method>\<open>isabelle.Symbol.encode\<close>.
\<close>
subsubsection \<open>Examples\<close>
text \<open>
Invoke the predefined Scala function \<^scala_function>\<open>echo\<close>:
\<close>
ML \<open>
val s = "test";
val s' = \<^scala>\<open>echo\<close> s;
\<^assert> (s = s')
\<close>
text \<open>
Let the Scala compiler process some toplevel declarations, producing a list
of errors:
\<close>
ML \<open>
val source = "class A(a: Int, b: Boolean)"
val errors =
\<^scala>\<open>scala_toplevel\<close> source
|> YXML.parse_body
|> let open XML.Decode in list string end;
\<^assert> (null errors)\<close>
text \<open>
The above is merely for demonstration. See \<^ML>\<open>Scala_Compiler.toplevel\<close>
for a more convenient version with builtin decoding and treatment of errors.
\<close>
section \<open>Documenting Isabelle/Scala entities\<close>
text \<open>
The subsequent document antiquotations help to document Isabelle/Scala
entities, with formal checking of names against the Isabelle classpath.
\begin{matharray}{rcl}
@{antiquotation_def "scala"} & : & \<open>antiquotation\<close> \\
@{antiquotation_def "scala_object"} & : & \<open>antiquotation\<close> \\
@{antiquotation_def "scala_type"} & : & \<open>antiquotation\<close> \\
@{antiquotation_def "scala_method"} & : & \<open>antiquotation\<close> \\
\end{matharray}
\<^rail>\<open>
(@@{antiquotation scala} | @@{antiquotation scala_object})
@{syntax embedded}
;
@@{antiquotation scala_type} @{syntax embedded} types
;
@@{antiquotation scala_method} class @{syntax embedded} types args
;
class: ('(' @'in' @{syntax name} types ')')?
;
types: ('[' (@{syntax name} ',' +) ']')?
;
args: ('(' (nat | (('_' | @{syntax name}) + ',')) ')')?
\<close>
\<^descr> \<open>@{scala s}\<close> is similar to \<open>@{verbatim s}\<close>, but the given source text is
checked by the Scala compiler as toplevel declaration (without evaluation).
This allows to write Isabelle/Scala examples that are statically checked.
\<^descr> \<open>@{scala_object x}\<close> checks the given Scala object name (simple value or
ground module) and prints the result verbatim.
\<^descr> \<open>@{scala_type T[A]}\<close> checks the given Scala type name (with optional type
parameters) and prints the result verbatim.
\<^descr> \<open>@{scala_method (in c[A]) m[B](n)}\<close> checks the given Scala method \<open>m\<close> in
the context of class \<open>c\<close>. The method argument slots are either specified by
a number \<open>n\<close> or by a list of (optional) argument types; this may refer to
type variables specified for the class or method: \<open>A\<close> or \<open>B\<close> above.
Everything except for the method name \<open>m\<close> is optional. The absence of the
class context means that this is a static method. The absence of arguments
with types means that the method can be determined uniquely as \<^verbatim>\<open>(\<close>\<open>m\<close>\<^verbatim>\<open> _)\<close>
in Scala (no overloading).
\<close>
subsubsection \<open>Examples\<close>
text \<open>
Miscellaneous Isabelle/Scala entities:
\<^item> object: \<^scala_object>\<open>isabelle.Isabelle_Process\<close>
\<^item> type without parameter: @{scala_type isabelle.Console_Progress}
\<^item> type with parameter: @{scala_type List[A]}
\<^item> static method: \<^scala_method>\<open>isabelle.Isabelle_System.bash\<close>
\<^item> class and method with type parameters:
@{scala_method (in List[A]) map[B]("A => B")}
\<^item> overloaded method with argument type: @{scala_method (in Int) "+" (Int)}
\<close>
end