Quelle Scala.thy

Sprache: Isabelle

(*:maxLineLen=78:*)

theory Scala
imports Base
begin

chapter ‹Isabelle/Scala systems programming \label{sec:scala}›

text ‹
Isabelle/ML and Isabelle/Scala are the two main implementation languages of
the Isabelle environment:

▪ Isabelle/ML is for ∗‹mathematics›, to develop tools within the context
of symbolic logic, e.g.\ for constructing proofs or defining
domain-specific formal languages. See the ∗‹Isabelle/Isar implementation
manual› cite‹"isabelle-implementation"› for more details.

▪ Isabelle/Scala is for ∗‹physics›, 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:

▪ Isabelle command-line tools (\secref{sec:scala-tools}) run in a separate
Java process.

▪ 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.

▪ The ▩‹Console/Scala› 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
🚫‹$ISABELLE_HOME/lib/classes/isabelle.jar›. 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 🚫‹etc/settings› (GNU bash script). The
shell function 🚫‹classpath› helps to write
🚫‹etc/settings› in a portable manner: it refers to library ▩‹jar›
files in standard POSIX path notation. On Windows, this is converted to
native platform format, before invoking Java (\secref{sec:scala-tools}).

┉
There is also an implicit build process for Isabelle/Scala/Java modules,
based on 🚫‹etc/build.props› within the component directory (see also
\secref{sec:scala-build}). See 🚫‹$ISABELLE_HOME/src/Tools/Demo/README.md›
for an example components with command-line tools in Isabelle/Scala.
›

section ‹Command-line tools \label{sec:scala-tools}›

subsection ‹Java Runtime Environment \label{sec:tool-java}›

text ‹
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 ▩‹-help› in
particular.

The ▩‹java› executable is taken from @{setting ISABELLE_JDK_HOME}, according
to the standard directory layout for regular distributions of OpenJDK.

The shell function 🚫‹isabelle_jdk› allows shell scripts to
invoke other Java tools robustly (e.g.\ ▩‹isabelle_jdk jar›), without
depending on accidental operating system installations.
›

subsection ‹Scala toplevel \label{sec:tool-scala}›

text ‹
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 ▩‹-help› in particular. This allows
to interact with Isabelle/Scala interactively.
›

subsubsection ‹Example›

text ‹
Explore the Isabelle system environment in Scala:
@{verbatim [display, indent = 2] ‹$ isabelle scala›}
@{scala [display, indent = 2]
‹import isabelle._

isabelle_home = Isabelle_System.getenv("ISABELLE_HOME")

options = Options.init()
.bool("browser_info")
.string("document")›}
›

subsection ‹Scala compiler \label{sec:tool-scalac}›

text ‹
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 ▩‹class›
or ▩‹jar› files can be added to the Java classpath using the shell function
🚫‹classpath›.

A more convenient high-level approach works via 🚫‹etc/build.props›
(see \secref{sec:scala-build}).
›

section ‹Isabelle/Scala/Java modules \label{sec:scala-build}›

subsection ‹Component configuration via 🚫‹etc/build.props››

text ‹
Isabelle components may augment the Isabelle/Scala/Java environment
declaratively via properties given in 🚫‹etc/build.props› (within the
component directory). This specifies an output ▩‹jar› ∗‹module›, based on
Scala or Java ∗‹sources›, and arbitrary ∗‹resources›. Moreover, a module can
specify ∗‹services› that are subclasses of
🚫‹isabelle.Isabelle_System.Service›; 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.

┉
The syntax of 🚫‹etc/build.props› follows a regular Java properties
file🚫‹🌐‹https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/Properties.html#load(java.io.Reader)››,
but the encoding is ▩‹UTF-8›, instead of historic ▩‹ISO 8859-1› 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. ▩‹$ISABELLE_HOME›).

▪ ▩‹title› (required) is a human-readable description of the module, used
in printed messages.

▪ ▩‹module› specifies a ▩‹jar› file name for the output module, as result
of the specified sources (and resources). If this is absent (or
▩‹no_build› is set, as described below), there is no implicit build
process. The contributing sources might be given nonetheless, notably for
@{tool scala_project} (\secref{sec:tool-scala-project}), which includes
Scala/Java sources of components, while suppressing ▩‹jar› modules (to
avoid duplication of program content).

▪ ▩‹no_build› is a Boolean property, with default ▩‹false›. If set to
▩‹true›, the implicit build process for the given ▩‹module› is ∗‹omitted›
--- it is assumed to be provided by other means.

▪ ▩‹scalac_options› and ▩‹javac_options› 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 ▩‹scalac› and ▩‹javac›, respectively.

▪ ▩‹main› specifies the main entry point for the ▩‹jar› module. This is
only relevant for direct invocation like ``▩‹java -jar test.jar›''.

▪ ▩‹requirements› is a list of ▩‹jar› modules that are needed in the
compilation process, but not provided by the regular classpath (notably
@{setting ISABELLE_CLASSPATH}).

A ∗‹normal entry› refers to a single ▩‹jar› file name, possibly with
settings variables as usual. E.g. 🚫‹$ISABELLE_SCALA_JAR› for the main
🚫‹$ISABELLE_HOME/lib/classes/isabelle.jar› (especially relevant for
add-on modules).

A ∗‹special entry› is of the form ▩‹env:›‹variable› and refers to a
settings variable from the Isabelle environment: its value may consist of
multiple ▩‹jar› entries (separated by colons). Environment variables are
not expanded recursively.

▪ ▩‹resources› is a list of files that should be included in the resulting
▩‹jar› file. Each item consists of a pair separated by colon:
‹source›▩‹:›‹target› means to copy an existing source file (relative to
the component directory) to the given target file or directory (relative
to the ▩‹jar› name space). A ‹file› specification without colon
abbreviates ‹file›▩‹:›‹file›, i.e. the file is copied while retaining its
relative path name.

▪ ▩‹sources› is a list of ▩‹.scala› or ▩‹.java› 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.

▪ ▩‹services› is a list of class names to be registered as Isabelle
service providers (subclasses of
🚫‹isabelle.Isabelle_System.Service›). 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
🚫‹isabelle.Isabelle_Scala_Tools› collects Scala command-line
tools, and class 🚫‹isabelle.Scala.Functions› collects Scala
functions (\secref{sec:scala-functions}).
›

subsection ‹Explicit Isabelle/Scala/Java build \label{sec:tool-scala-build}›

text ‹
The @{tool_def scala_build} tool explicitly invokes the build process for
all registered components.
@{verbatim [display]
‹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).
›}

For each registered Isabelle component that provides
🚫‹etc/build.props›, the specified output ▩‹module› is checked against
the corresponding input ▩‹requirements›, ▩‹resources›, ▩‹sources›. If
required, there is an automatic build using ▩‹scalac› or ▩‹javac› (or both).
The identity of input files is recorded within the output ▩‹jar›, using SHA1
digests in ▩‹META-INF/isabelle/shasum›.

┉
Option ▩‹-f› forces a fresh build, regardless of the up-to-date status of
input files vs. the output module.

┉
Option ▩‹-q› suppresses all output on stdout/stderr produced by the Scala or
Java compiler.

┉ Explicit invocation of @{tool scala_build} mainly serves testing or
applications with special options: the Isabelle system normally does an
automatic the build on demand.
›

subsection ‹Project setup for common Scala IDEs \label{sec:tool-scala-project}›

text ‹
The @{tool_def scala_project} tool creates a project configuration for all
Isabelle/Java/Scala modules specified in components via
🚫‹etc/build.props›, together with additional source files given on
the command-line:

@{verbatim [display]
‹Usage: isabelle scala_project [OPTIONS] [MORE_SOURCES ...]

Options are:
-D DIR project directory (default: "$ISABELLE_HOME_USER/scala_project")
-G use Gradle as build tool
-L make symlinks to original source files
-M use Maven as build tool
-f force update of existing directory
-v verbose

Setup project for Isabelle/Scala/jEdit --- to support common IDEs such
as IntelliJ IDEA. Either option -G or -M is mandatory to specify the
build tool.›}

The generated configuration is for Gradle🚫‹🌐‹https://gradle.org›› or
Maven🚫‹🌐‹https://maven.apache.org››, but the main purpose is to import it
into common IDEs like IntelliJ IDEA🚫‹🌐‹https://www.jetbrains.com/idea››.
This allows to explore the sources with static analysis and other hints in
real-time.

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.

┉
Option ▩‹-G› selects Gradle and ▩‹-M› selects Maven as Java/Scala build
tool: either one needs to be specified explicitly. These tools have a
tendency to break down unexpectedly, so supporting both increases the
chances that the generated IDE project works properly.

┉
Option ▩‹-L› produces ∗‹symlinks› to the original files: this allows to
develop Isabelle/Scala/jEdit modules within an external IDE. The default is
to ∗‹copy› source files, so editing them within the IDE has no permanent
effect on the originals.

┉
Option ▩‹-D› specifies an explicit project directory, instead of the default
🚫‹$ISABELLE_HOME_USER/scala_project›. Option ▩‹-f› forces an existing
project directory to be ∗‹purged› --- after some sanity checks that it has
been generated by @{tool "scala_project"} before.

┉
Option ▩‹-v› enables verbose mode.
›

subsubsection ‹Examples›

text ‹
Create a project directory and for editing the original sources:

@{verbatim [display] ‹isabelle scala_project -f -L›}

On Windows, this usually requires Administrator rights, in order to create
native symlinks.
›

section ‹Registered Isabelle/Scala functions \label{sec:scala-functions}›

subsection ‹Defining functions in Isabelle/Scala›

text ‹
The service class 🚫‹isabelle.Scala.Functions› collects Scala
functions of type 🚫‹isabelle.Scala.Fun›: by registering
instances via ▩‹services› in 🚫‹etc/build.props›
(\secref{sec:scala-build}), it becomes possible to invoke Isabelle/Scala
from Isabelle/ML (see below).

An example is the predefined collection of
🚫‹isabelle.Scala.Functions› in
🚫‹$ISABELLE_HOME/etc/build.props›. The overall list of registered functions
is accessible in Isabelle/Scala as
🚫‹isabelle.Scala.functions›.

The general class 🚫‹isabelle.Scala.Fun› expects a multi-argument
/ multi-result function
🚫‹List[isabelle.Bytes] => List[isabelle.Bytes]›; more common are
instances of 🚫‹isabelle.Scala.Fun_Strings› for type
🚫‹List[String] => List[String]›, or
🚫‹isabelle.Scala.Fun_String› for type
🚫‹String => String›.
›

subsection ‹Invoking functions in Isabelle/ML›

text ‹
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"} & : & ‹ML_antiquotation› \\
@{ML_antiquotation_def "scala"} & : & ‹ML_antiquotation› \\
\end{matharray}

🚫‹
(@{ML_antiquotation scala_function} |
@{ML_antiquotation scala}) @{syntax embedded}
›

🚫 ‹@{scala_function name}› inlines the checked function name as ML string
literal.

🚫 ‹@{scala name}› and ‹@{scala_thread name}› invoke the checked function via
the PIDE protocol. In Isabelle/ML this appears as a function of type
🚫‹string list -> string list› or 🚫‹string -> string›,
depending on the definition in Isabelle/Scala. Evaluation is subject to
interrupts within the ML runtime environment as usual. A 🚫‹null›
result in Scala raises an exception 🚫‹Scala.Null› in ML. The execution
of ‹@{scala}› works via a Scala future on a bounded thread farm, while
‹@{scala_thread}› always forks a separate Java/VM 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
🚫‹isabelle.Symbol.decode› and
🚫‹isabelle.Symbol.encode›.
›

subsubsection ‹Examples›

text ‹
Invoke the predefined Scala function 🚫‹echo›:
›

ML ‹
val s = "test";
val s' = 🚫‹echo› s;
🚫 (s = s')
›

text ‹
Let the Scala compiler process some toplevel declarations, producing a list
of errors:
›

ML ‹
val source = "class A(a: Int, b: Boolean)"
val errors =
🚫‹scala_toplevel› source
|> YXML.parse_body
|> let open XML.Decode in list string end;

🚫 (null errors)›

text ‹
The above is merely for demonstration. See 🚫‹Scala_Compiler.toplevel›
for a more convenient version with builtin decoding and treatment of errors.
›

section ‹Documenting Isabelle/Scala entities›

text ‹
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"} & : & ‹antiquotation› \\
@{antiquotation_def "scala_object"} & : & ‹antiquotation› \\
@{antiquotation_def "scala_type"} & : & ‹antiquotation› \\
@{antiquotation_def "scala_method"} & : & ‹antiquotation› \\
\end{matharray}

🚫‹
(@@{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}) + ',')) ')')?
›

🚫 ‹@{scala s}› is similar to ‹@{verbatim s}›, 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.

🚫 ‹@{scala_object x}› checks the given Scala object name (simple value or
ground module) and prints the result verbatim.

🚫 ‹@{scala_type T[A]}› checks the given Scala type name (with optional type
parameters) and prints the result verbatim.

🚫 ‹@{scala_method (in c[A]) m[B](n)}› checks the given Scala method ‹m› in
the context of class ‹c›. The method argument slots are either specified by
a number ‹n› or by a list of (optional) argument types; this may refer to
type variables specified for the class or method: ‹A› or ‹B› above.

Everything except for the method name ‹m› 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 ▩‹(›‹m›▩‹ _)›
in Scala (no overloading).
›

subsubsection ‹Examples›

text ‹
Miscellaneous Isabelle/Scala entities:

▪ object: 🚫‹isabelle.Isabelle_Process›
▪ type without parameter: @{scala_type isabelle.Console_Progress}
▪ type with parameter: @{scala_type List[A]}
▪ static method: 🚫‹isabelle.Isabelle_System.bash›
▪ class and method with type parameters:
@{scala_method (in List[A]) map[B]("A => B")}
▪ overloaded method with argument type: @{scala_method (in Int) "+" (Int)}
›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet am 2026-06-30) ¤

Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.