diff --git a/bin/isabelle_java b/bin/isabelle_java
--- a/bin/isabelle_java
+++ b/bin/isabelle_java
@@ -1,72 +1,72 @@
#!/usr/bin/env bash
#
# Author: Makarius
#
# Isabelle/Java cold start -- without settings environment
unset CDPATH
if [ -L "$0" ]; then
TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
fi
export ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
(
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $ISABELLE_TOOL_JAVA_OPTIONS)"
- isabelle_setup_classpath
+ classpath "$ISABELLE_SETUP_CLASSPATH"
[ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
echo "$ISABELLE_ROOT"
echo "$CYGWIN_ROOT"
echo "$JAVA_HOME"
echo "$(platform_path "$ISABELLE_CLASSPATH")"
for ARG in "${JAVA_ARGS[@]}"; do echo "$ARG"; done
) | {
LINE_COUNT=0
export ISABELLE_ROOT=""
export CYGWIN_ROOT=""
unset JAVA_HOME
unset ISABELLE_CLASSPATH
unset JAVA_ARGS; declare -a JAVA_ARGS
while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
do
case "$LINE_COUNT" in
0)
LINE_COUNT=1
ISABELLE_ROOT="$REPLY"
;;
1)
LINE_COUNT=2
CYGWIN_ROOT="$REPLY"
;;
2)
LINE_COUNT=3
JAVA_HOME="$REPLY"
;;
3)
LINE_COUNT=4
ISABELLE_CLASSPATH="$REPLY"
;;
*)
JAVA_ARGS["${#JAVA_ARGS[@]}"]="$REPLY"
;;
esac
done
if [ -z "$JAVA_HOME" ]; then
echo "Unknown JAVA_HOME -- Java unavailable" >&2
exit 127
else
unset ISABELLE_HOME
unset CLASSPATH
exec "$JAVA_HOME/bin/java" "${JAVA_ARGS[@]}" \
-classpath "$ISABELLE_CLASSPATH" "$@"
fi
}
diff --git a/lib/Tools/java b/lib/Tools/java
--- a/lib/Tools/java
+++ b/lib/Tools/java
@@ -1,15 +1,16 @@
#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: invoke Java within the Isabelle environment
eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
-isabelle_setup_classpath
+classpath "$ISABELLE_SETUP_CLASSPATH"
+unset ISABELLE_SETUP_CLASSPATH
[ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
unset CLASSPATH
isabelle_java java "${JAVA_ARGS[@]}" \
-classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
diff --git a/lib/Tools/scala b/lib/Tools/scala
--- a/lib/Tools/scala
+++ b/lib/Tools/scala
@@ -1,21 +1,24 @@
#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: invoke Scala within the Isabelle environment
isabelle_admin_build jars || exit $?
eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
declare -a SCALA_ARGS=()
for ARG in "${JAVA_ARGS[@]}"
do
SCALA_ARGS["${#SCALA_ARGS[@]}"]="-J$ARG"
done
+classpath "$ISABELLE_SETUP_CLASSPATH"
+unset ISABELLE_SETUP_CLASSPATH
+
[ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
unset CLASSPATH
isabelle_scala scala "${SCALA_ARGS[@]}" \
-classpath "$(platform_path "$ISABELLE_CLASSPATH")" \
-Disabelle.scala.classpath="$(platform_path "$ISABELLE_CLASSPATH")" "$@"
diff --git a/lib/Tools/scalac b/lib/Tools/scalac
--- a/lib/Tools/scalac
+++ b/lib/Tools/scalac
@@ -1,10 +1,16 @@
#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: invoke Scala compiler within the Isabelle environment
isabelle_admin_build jars || exit $?
+classpath "$ISABELLE_SETUP_CLASSPATH"
+unset ISABELLE_SETUP_CLASSPATH
+
+[ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
+unset CLASSPATH
+
isabelle_scala scalac -Dfile.encoding=UTF-8 \
-classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
diff --git a/lib/scripts/getfunctions b/lib/scripts/getfunctions
--- a/lib/scripts/getfunctions
+++ b/lib/scripts/getfunctions
@@ -1,318 +1,309 @@
# -*- shell-script -*- :mode=shellscript:
#
# Author: Makarius
#
# Isabelle shell functions, with on-demand re-initialization for
# non-interactive bash processess. NB: bash shell functions are not portable
# and may be dropped by aggressively POSIX-conformant versions of /bin/sh.
unset CDPATH
if type splitarray >/dev/null 2>/dev/null
then
:
else
if [ "$OSTYPE" = cygwin ]; then
function platform_path() { cygpath -i -C UTF8 -w -p "$@"; }
function standard_path() { cygpath -i -u -p "$@" | tr -d '\r'; }
else
function platform_path() { echo "$@"; }
function standard_path() { echo "$@"; }
fi
export -f platform_path standard_path
#GNU tar (notably on macOS)
function tar() {
if [ -f "$ISABELLE_TAR" ]; then
"$ISABELLE_TAR" "$@"
else
"$(type -P tar)" "$@"
fi
}
export -f tar
#OCaml management via OPAM
function isabelle_opam ()
{
if [ -z "$ISABELLE_OPAM" ]; then
echo "Unknown ISABELLE_OPAM -- OCaml management tools unavailable" >&2
return 127
else
env OPAMROOT="$ISABELLE_OPAM_ROOT" OPAMCOLOR="never" "$ISABELLE_OPAM" "$@"
fi
}
export -f isabelle_opam
#GHC management via Stack
function isabelle_stack ()
{
if [ -z "$ISABELLE_STACK" ]; then
echo "Unknown ISABELLE_STACK -- GHC management tools unavailable" >&2
return 127
else
env STACK_ROOT="$(platform_path "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" --resolver "$ISABELLE_STACK_RESOLVER" --compiler "$ISABELLE_GHC_VERSION" "$@"
fi
}
export -f isabelle_stack
#robust invocation via ISABELLE_JDK_HOME
function isabelle_jdk ()
{
if [ -z "$ISABELLE_JDK_HOME" ]; then
echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2
return 127
else
local PRG="$1"; shift
"$ISABELLE_JDK_HOME/bin/$PRG" "$@"
fi
}
export -f isabelle_jdk
#robust invocation via JAVA_HOME
function isabelle_java ()
{
if [ -z "$JAVA_HOME" ]; then
echo "Unknown JAVA_HOME -- Java unavailable" >&2
return 127
else
local PRG="$1"; shift
"$JAVA_HOME/bin/$PRG" "$@"
fi
}
export -f isabelle_java
#robust invocation via SCALA_HOME
function isabelle_scala ()
{
if [ -z "$JAVA_HOME" ]; then
echo "Unknown JAVA_HOME -- Java unavailable" >&2
return 127
elif [ -z "$SCALA_HOME" ]; then
echo "Unknown SCALA_HOME -- Scala unavailable" >&2
return 127
else
local PRG="$1"; shift
"$SCALA_HOME/bin/$PRG" "$@"
fi
}
export -f isabelle_scala
#classpath
function classpath ()
{
local X=""
for X in "$@"
do
if [ -z "$ISABELLE_CLASSPATH" ]; then
ISABELLE_CLASSPATH="$X"
else
ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
fi
done
export ISABELLE_CLASSPATH
}
export -f classpath
#java_library
function java_library ()
{
local X=""
for X in "$@"
do
case "$ISABELLE_PLATFORM_FAMILY" in
linux)
if [ -z "$LD_LIBRARY_PATH" ]; then
export LD_LIBRARY_PATH="$X"
else
export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:$X"
fi
;;
macos)
if [ -z "$JAVA_LIBRARY_PATH" ]; then
export JAVA_LIBRARY_PATH="$X"
else
export JAVA_LIBRARY_PATH="$JAVA_LIBRARY_PATH:$X"
fi
;;
windows)
if [ -z "$PATH" ]; then
export PATH="$X"
else
export PATH="$PATH:$X"
fi
;;
esac
done
export ISABELLE_CLASSPATH
}
export -f java_library
#Isabelle fonts
function isabelle_fonts ()
{
local X=""
for X in "$@"
do
if [ -z "$ISABELLE_FONTS" ]; then
ISABELLE_FONTS="$X"
else
ISABELLE_FONTS="$ISABELLE_FONTS:$X"
fi
done
export ISABELLE_FONTS
}
export -f isabelle_fonts
function isabelle_fonts_hidden ()
{
local X=""
for X in "$@"
do
if [ -z "$ISABELLE_FONTS_HIDDEN" ]; then
ISABELLE_FONTS_HIDDEN="$X"
else
ISABELLE_FONTS_HIDDEN="$ISABELLE_FONTS_HIDDEN:$X"
fi
done
export ISABELLE_FONTS_HIDDEN
}
export -f isabelle_fonts_hidden
#Isabelle/Scala services
function isabelle_scala_service ()
{
local X=""
for X in "$@"
do
if [ -z "$ISABELLE_SCALA_SERVICES" ]; then
ISABELLE_SCALA_SERVICES="$X"
else
ISABELLE_SCALA_SERVICES="$ISABELLE_SCALA_SERVICES:$X"
fi
done
export ISABELLE_SCALA_SERVICES
}
export -f isabelle_scala_service
#Special directories
function isabelle_directory ()
{
local X=""
for X in "$@"
do
if [ -z "$ISABELLE_DIRECTORIES" ]; then
ISABELLE_DIRECTORIES="$X"
else
ISABELLE_DIRECTORIES="$ISABELLE_DIRECTORIES:$X"
fi
done
export ISABELLE_DIRECTORIES
}
export -f isabelle_directory
-#setup classpath
-function isabelle_setup_classpath
-{
- classpath "$(isabelle_java java -classpath "$(platform_path "$ISABELLE_SETUP_JAR")" isabelle.setup.Setup classpath)"
-}
-export -f isabelle_setup_classpath
-
#administrative build
function isabelle_admin_build ()
{
- {
- if [ -e "$ISABELLE_HOME/Admin/build" ]; then
- "$ISABELLE_HOME/Admin/build" "$@"
- fi
- } && isabelle_setup_classpath
+ if [ -e "$ISABELLE_HOME/Admin/build" ]; then
+ "$ISABELLE_HOME/Admin/build" "$@"
+ fi
}
export -f isabelle_admin_build
#arrays
function splitarray ()
{
SPLITARRAY=()
local IFS="$1"; shift
local X=""
for X in $*
do
SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
done
}
export -f splitarray
#init component tree
function init_component ()
{
local COMPONENT="$1"
case "$COMPONENT" in
/*) ;;
*)
echo >&2 "Absolute component path required: \"$COMPONENT\""
exit 2
;;
esac
if [ -d "$COMPONENT" ]; then
if [ -z "$ISABELLE_COMPONENTS" ]; then
ISABELLE_COMPONENTS="$COMPONENT"
else
ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
fi
else
echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
ISABELLE_COMPONENTS_MISSING="$COMPONENT"
else
ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
fi
fi
if [ -f "$COMPONENT/etc/settings" ]; then
source "$COMPONENT/etc/settings"
local RC="$?"
if [ "$RC" -ne 0 ]; then
echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
exit 2
fi
fi
if [ -f "$COMPONENT/etc/components" ]; then
init_components "$COMPONENT" "$COMPONENT/etc/components"
fi
}
export -f init_component
#init component forest
function init_components ()
{
local REPLY=""
local BASE="$1"
local CATALOG="$2"
local COMPONENT=""
local -a COMPONENTS=()
if [ ! -f "$CATALOG" ]; then
echo >&2 "Bad component catalog file: \"$CATALOG\""
exit 2
fi
{
while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
do
case "$REPLY" in
\#* | "") ;;
/*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;;
*) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;;
esac
done
} < "$CATALOG"
for COMPONENT in "${COMPONENTS[@]}"
do
init_component "$COMPONENT"
done
}
export -f init_components
fi
diff --git a/lib/scripts/getsettings b/lib/scripts/getsettings
--- a/lib/scripts/getsettings
+++ b/lib/scripts/getsettings
@@ -1,134 +1,136 @@
# -*- shell-script -*- :mode=shellscript:
#
# Author: Makarius
#
# Static Isabelle environment for root of process tree.
export ISABELLE_HOME
export BASH_ENV="$ISABELLE_HOME/lib/scripts/getfunctions"
source "$BASH_ENV"
if [ -z "$ISABELLE_SETTINGS_PRESENT" ]
then
export ISABELLE_SETTINGS_PRESENT=true
set -o allexport
#sane environment defaults (notably on macOS)
if [ "$ISABELLE_APP" = true -a -x /usr/libexec/path_helper ]; then
eval $(/usr/libexec/path_helper -s)
fi
#Cygwin vs. POSIX
if [ "$OSTYPE" = cygwin ]
then
unset INI_DIR
if [ -n "$TEMP_WINDOWS" ]; then
TMPDIR="$(cygpath -u "$TEMP_WINDOWS")"
TMP="$TMPDIR"
TEMP="$TMPDIR"
fi
if [ -z "$USER_HOME" ]; then
USER_HOME="$(cygpath -u "$USERPROFILE")"
fi
CYGWIN_ROOT="$(platform_path "/")"
ISABELLE_ROOT="$(platform_path "$ISABELLE_HOME")"
ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
unset CLASSPATH
else
if [ -z "$USER_HOME" ]; then
USER_HOME="$HOME"
fi
ISABELLE_ROOT="$ISABELLE_HOME"
ISABELLE_CLASSPATH="$CLASSPATH"
unset CLASSPATH
fi
#init cumulative settings
ISABELLE_FONTS=""
ISABELLE_FONTS_HIDDEN=""
ISABELLE_SCALA_SERVICES=""
ISABELLE_DIRECTORIES=""
#main executables
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
ISABELLE_SCALA_SCRIPT="$ISABELLE_HOME/bin/isabelle_scala_script"
PATH="$ISABELLE_HOME/bin:$PATH"
#platform
source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
if [ -z "$ISABELLE_PLATFORM_FAMILY" ]; then
echo 1>&2 "Failed to determine hardware and operating system type!"
exit 2
fi
if [ -z "$ISABELLE_IDENTIFIER" -a -f "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER" ]
then
ISABELLE_IDENTIFIER="$(cat "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER")"
fi
ISABELLE_NAME="${ISABELLE_IDENTIFIER:-Isabelle}"
# components
ISABELLE_COMPONENTS=""
ISABELLE_COMPONENTS_MISSING=""
#main components
init_component "$ISABELLE_HOME"
[ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
if [ -d "$ISABELLE_HOME_USER" ]; then
init_component "$ISABELLE_HOME_USER"
else
mkdir -p "$ISABELLE_HOME_USER"
chmod $(umask -S) "$ISABELLE_HOME_USER"
fi
#POLYML_EXE
if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then
POLYML_EXE="$ML_HOME/poly.exe"
else
POLYML_EXE="$ML_HOME/poly"
fi
#ML system identifier
if [ -z "$ML_PLATFORM" ]; then
ML_IDENTIFIER="$ML_SYSTEM"
else
ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
fi
#enforce ISABELLE_OCAMLFIND
if [ -d "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin" ]; then
ISABELLE_OCAMLFIND="$ISABELLE_HOME/lib/scripts/ocamlfind"
fi
#enforce ISABELLE_GHC
if [ -f "$ISABELLE_STACK_ROOT/ISABELLE_GHC_EXE-$ISABELLE_PLATFORM_FAMILY" ]; then
if [ -f "$(cat "$ISABELLE_STACK_ROOT/ISABELLE_GHC_EXE-$ISABELLE_PLATFORM_FAMILY")" ]; then
ISABELLE_GHC="$ISABELLE_HOME/lib/scripts/ghc"
ISABELLE_GHC_STACK=true
fi
fi
#enforce JAVA_HOME
if [ -d "$ISABELLE_JDK_HOME/jre" ]
then
export JAVA_HOME="$ISABELLE_JDK_HOME/jre"
else
export JAVA_HOME="$ISABELLE_JDK_HOME"
fi
+ISABELLE_SETUP_CLASSPATH="$(isabelle_java java -classpath "$(platform_path "$ISABELLE_SETUP_JAR")" isabelle.setup.Setup classpath)"
+
set +o allexport
fi
diff --git a/src/Pure/Admin/build_release.scala b/src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala
+++ b/src/Pure/Admin/build_release.scala
@@ -1,935 +1,937 @@
/* Title: Pure/Admin/build_release.scala
Author: Makarius
Build full Isabelle distribution from repository.
*/
package isabelle
object Build_Release
{
/** release context **/
private def execute(dir: Path, script: String): Unit =
Isabelle_System.bash(script, cwd = dir.file).check
private def execute_tar(dir: Path, args: String, strip: Int = 0): Unit =
Isabelle_System.gnutar(args, dir = dir, strip = strip).check
object Release_Context
{
def apply(
target_dir: Path,
release_name: String = "",
components_base: Path = Components.default_components_base,
progress: Progress = new Progress): Release_Context =
{
val date = Date.now()
val dist_name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date))
val dist_dir = (target_dir + Path.explode("dist-" + dist_name)).absolute
new Release_Context(release_name, dist_name, dist_dir, components_base, progress)
}
}
class Release_Context private[Build_Release](
val release_name: String,
val dist_name: String,
val dist_dir: Path,
val components_base: Path,
val progress: Progress)
{
override def toString: String = dist_name
val isabelle: Path = Path.explode(dist_name)
val isabelle_dir: Path = dist_dir + isabelle
val isabelle_archive: Path = dist_dir + isabelle.tar.gz
val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
def other_isabelle(dir: Path): Other_Isabelle =
Other_Isabelle(dir + isabelle,
isabelle_identifier = dist_name + "-build",
progress = progress)
def make_announce(id: String): Unit =
{
if (release_name.isEmpty) {
File.write(isabelle_dir + Path.explode("ANNOUNCE"),
"""
IMPORTANT NOTE
==============
This is a snapshot of Isabelle/""" + id + """ from the repository.
""")
}
}
def make_contrib(): Unit =
{
Isabelle_System.make_directory(Components.contrib(isabelle_dir))
File.write(Components.contrib(isabelle_dir, name = "README"),
"""This directory contains add-on components that contribute to the main
Isabelle distribution. Separate licensing conditions apply, see each
directory individually.
""")
}
def bundle_info(platform: Platform.Family.Value): Bundle_Info =
platform match {
case Platform.Family.linux_arm =>
Bundle_Info(platform, "Linux (ARM)", dist_name + "_linux_arm.tar.gz")
case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz")
case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
}
}
sealed case class Bundle_Info(
platform: Platform.Family.Value,
platform_description: String,
name: String)
{
def path: Path = Path.explode(name)
}
/** release archive **/
val ISABELLE: Path = Path.basic("Isabelle")
val ISABELLE_ID: Path = Path.explode("etc/ISABELLE_ID")
val ISABELLE_TAGS: Path = Path.explode("etc/ISABELLE_TAGS")
val ISABELLE_IDENTIFIER: Path = Path.explode("etc/ISABELLE_IDENTIFIER")
object Release_Archive
{
def make(bytes: Bytes, rename: String = ""): Release_Archive =
{
Isabelle_System.with_tmp_dir("tmp")(dir =>
Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path =>
{
val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE)
Bytes.write(archive_path, bytes)
execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = 1)
val id = File.read(isabelle_dir + ISABELLE_ID)
val tags = File.read(isabelle_dir + ISABELLE_TAGS)
val identifier = File.read(isabelle_dir + ISABELLE_IDENTIFIER)
val (bytes1, identifier1) =
if (rename.isEmpty || rename == identifier) (bytes, identifier)
else {
File.write(isabelle_dir + ISABELLE_IDENTIFIER, rename)
Isabelle_System.move_file(isabelle_dir, dir + Path.basic(rename))
execute_tar(dir, "-czf " + File.bash_path(archive_path) + " " + Bash.string(rename))
(Bytes.read(archive_path), rename)
}
new Release_Archive(bytes1, id, tags, identifier1)
})
)
}
def read(path: Path, rename: String = ""): Release_Archive =
make(Bytes.read(path), rename = rename)
def get(url: String, rename: String = "", progress: Progress = new Progress): Release_Archive =
{
val bytes =
if (Path.is_wellformed(url)) Bytes.read(Path.explode(url))
else Isabelle_System.download(url, progress = progress).bytes
make(bytes, rename = rename)
}
}
case class Release_Archive private[Build_Release](
bytes: Bytes, id: String, tags: String, identifier: String)
{
override def toString: String = identifier
}
/** generated content **/
/* bundled components */
class Bundled(platform: Option[Platform.Family.Value] = None)
{
def detect(s: String): Boolean =
s.startsWith("#bundled") && !s.startsWith("#bundled ")
def apply(name: String): String =
"#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name
private val Pattern1 = ("""^#bundled:(.*)$""").r
private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r
def unapply(s: String): Option[String] =
s match {
case Pattern1(name) => Some(name)
case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name)
case _ => None
}
}
def record_bundled_components(dir: Path): Unit =
{
val catalogs =
List("main", "bundled").map((_, new Bundled())) :::
Platform.Family.list.flatMap(platform =>
List(platform.toString, "bundled-" + platform.toString).
map((_, new Bundled(platform = Some(platform)))))
File.append(Components.components(dir),
terminate_lines("#bundled components" ::
(for {
(catalog, bundled) <- catalogs.iterator
path = Components.admin(dir) + Path.basic(catalog)
if path.is_file
line <- split_lines(File.read(path))
if line.nonEmpty && !line.startsWith("#")
} yield bundled(line)).toList))
}
def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) =
{
val Bundled = new Bundled(platform = Some(platform))
val components =
for { Bundled(name) <- Components.read_components(dir) } yield name
val jdk_component =
components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component")
(components, jdk_component)
}
def activate_components(
dir: Path, platform: Platform.Family.Value, more_names: List[String]): Unit =
{
def contrib_name(name: String): String =
Components.contrib(name = name).implode
val Bundled = new Bundled(platform = Some(platform))
Components.write_components(dir,
Components.read_components(dir).flatMap(line =>
line match {
case Bundled(name) =>
if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name))
else None
case _ => if (Bundled.detect(line)) None else Some(line)
}) ::: more_names.map(contrib_name))
}
/** build release **/
/* build heaps */
private def build_heaps(
options: Options,
platform: Platform.Family.Value,
build_sessions: List[String],
local_dir: Path): Unit =
{
val server_option = "build_host_" + platform.toString
val ssh =
options.string(server_option) match {
case "" =>
if (Platform.family == platform) SSH.Local
else error("Undefined option " + server_option + ": cannot build heaps")
case SSH.Target(user, host) =>
SSH.open_session(options, host = host, user = user)
case s => error("Malformed option " + server_option + ": " + quote(s))
}
try {
Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar =>
{
execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
ssh.with_tmp_dir(remote_dir =>
{
val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
ssh.write_file(remote_tmp_tar, local_tmp_tar)
val remote_commands =
List(
"cd " + File.bash_path(remote_dir),
"tar -xf tmp.tar",
"bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
"tar -cf tmp.tar heaps")
ssh.execute(remote_commands.mkString(" && "), settings = false).check
ssh.read_file(remote_tmp_tar, local_tmp_tar)
})
execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
})
}
finally { ssh.close() }
}
/* Isabelle application */
def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n"): Unit =
{
val title = "# Java runtime options"
File.write(path, (title :: options).map(_ + line_ending).mkString)
}
def make_isabelle_app(
platform: Platform.Family.Value,
isabelle_target: Path,
isabelle_name: String,
jdk_component: String,
classpath: List[Path],
dock_icon: Boolean = false): Unit =
{
val script = """#!/usr/bin/env bash
#
# Author: Makarius
#
# Main Isabelle application script.
# minimal Isabelle environment
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/../.."; pwd)"
source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
#paranoia settings -- avoid intrusion of alien options
unset "_JAVA_OPTIONS"
unset "JAVA_TOOL_OPTIONS"
#paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc.
unset XMODIFIERS
COMPONENT="$ISABELLE_HOME/contrib/""" + jdk_component + """"
source "$COMPONENT/etc/settings"
# main
declare -a JAVA_OPTIONS=($(grep -v '^#' "$ISABELLE_HOME/Isabelle.options"))
"$ISABELLE_HOME/bin/isabelle" env "$ISABELLE_HOME/lib/scripts/java-gui-setup"
exec "$ISABELLE_JDK_HOME/bin/java" \
"-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \
-classpath """" + classpath.map(p => "$ISABELLE_HOME/" + p.implode).mkString(":") + """" \
"-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
""" + (if (dock_icon) """"-Xdock:icon=$ISABELLE_HOME/lib/logo/isabelle_transparent-128.png" \
""" else "") + """isabelle.jedit.Main "$@"
"""
val script_path = isabelle_target + Path.explode("lib/scripts/Isabelle_app")
File.write(script_path, script)
File.set_executable(script_path, true)
val component_dir = isabelle_target + Path.explode("contrib/Isabelle_app")
Isabelle_System.move_file(
component_dir + Path.explode(Platform.Family.standard(platform)) + Path.explode("Isabelle"),
isabelle_target + Path.explode(isabelle_name))
Isabelle_System.rm_tree(component_dir)
}
def make_isabelle_plist(path: Path, isabelle_name: String, isabelle_rev: String): Unit =
{
File.write(path, """
CFBundleDevelopmentRegion
English
CFBundleIconFile
isabelle.icns
CFBundleIdentifier
de.tum.in.isabelle
CFBundleDisplayName
""" + isabelle_name + """
CFBundleInfoDictionaryVersion
6.0
CFBundleName
""" + isabelle_name + """
CFBundlePackageType
APPL
CFBundleShortVersionString
""" + isabelle_name + """
CFBundleSignature
????
CFBundleVersion
""" + isabelle_rev + """
NSHumanReadableCopyright
LSMinimumSystemVersion
10.11
LSApplicationCategoryType
public.app-category.developer-tools
NSHighResolutionCapable
true
NSSupportsAutomaticGraphicsSwitching
true
CFBundleDocumentTypes
CFBundleTypeExtensions
thy
CFBundleTypeIconFile
theory.icns
CFBundleTypeName
Isabelle theory file
CFBundleTypeRole
Editor
LSTypeIsPackage
""")
}
/* main */
def use_release_archive(
context: Release_Context,
archive: Release_Archive,
id: String = ""): Unit =
{
if (id.nonEmpty && id != archive.id) {
error("Mismatch of release identification " + id + " vs. archive " + archive.id)
}
if (!context.isabelle_archive.is_file || Bytes.read(context.isabelle_archive) != archive.bytes) {
Bytes.write(context.isabelle_archive, archive.bytes)
}
}
def build_release_archive(
context: Release_Context,
version: String,
parallel_jobs: Int = 1): Unit =
{
val progress = context.progress
val hg = Mercurial.repository(Path.ISABELLE_HOME)
val id =
try { hg.id(version) }
catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
if (context.isabelle_archive.is_file) {
progress.echo_warning("Found existing release archive: " + context.isabelle_archive)
use_release_archive(context, Release_Archive.read(context.isabelle_archive), id = id)
}
else {
progress.echo_warning("Preparing release " + context.dist_name + " ...")
Isabelle_System.new_directory(context.dist_dir)
hg.archive(context.isabelle_dir.expand.implode, rev = id, options = "--type files")
for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
(context.isabelle_dir + Path.explode(name)).file.delete
}
File.write(context.isabelle_dir + ISABELLE_ID, id)
File.write(context.isabelle_dir + ISABELLE_TAGS, hg.tags(rev = id))
File.write(context.isabelle_dir + ISABELLE_IDENTIFIER, context.dist_name)
context.make_announce(id)
context.make_contrib()
execute(context.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
record_bundled_components(context.isabelle_dir)
/* build tools and documentation */
val other_isabelle = context.other_isabelle(context.dist_dir)
other_isabelle.init_settings(
other_isabelle.init_components(
components_base = context.components_base, catalogs = List("main")))
other_isabelle.resolve_components(echo = true)
try {
val export_classpath =
"export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
other_isabelle.bash(export_classpath + "Admin/build all", echo = true).check
other_isabelle.bash(export_classpath + "bin/isabelle jedit -b", echo = true).check
}
catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) }
try {
other_isabelle.bash(
"bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
}
catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) }
other_isabelle.make_news()
for (name <- List("Admin", "browser_info", "heaps")) {
Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
}
other_isabelle.cleanup()
progress.echo_warning("Creating release archive " + context.isabelle_archive + " ...")
execute(context.dist_dir, """chmod -R a+r . && chmod -R u+w . && chmod -R g=o .""")
execute(context.dist_dir,
"""find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""")
execute_tar(context.dist_dir, "-czf " +
File.bash_path(context.isabelle_archive) + " " + Bash.string(context.dist_name))
}
}
def default_platform_families: List[Platform.Family.Value] = Platform.Family.list0
def build_release(
options: Options,
context: Release_Context,
afp_rev: String = "",
platform_families: List[Platform.Family.Value] = default_platform_families,
more_components: List[Path] = Nil,
website: Option[Path] = None,
build_sessions: List[String] = Nil,
build_library: Boolean = false,
parallel_jobs: Int = 1): Unit =
{
val progress = context.progress
/* release directory */
val archive = Release_Archive.read(context.isabelle_archive)
for (path <- List(context.isabelle, ISABELLE)) {
Isabelle_System.rm_tree(context.dist_dir + path)
}
Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path =>
{
Bytes.write(archive_path, archive.bytes)
val extract =
List("README", "NEWS", "ANNOUNCE", "COPYRIGHT", "CONTRIBUTORS", "doc").
map(name => context.dist_name + "/" + name)
execute_tar(context.dist_dir,
"-xzf " + File.bash_path(archive_path) + " " + Bash.strings(extract))
})
Isabelle_System.symlink(Path.explode(context.dist_name), context.dist_dir + ISABELLE)
/* make application bundles */
val bundle_infos = platform_families.map(context.bundle_info)
for (bundle_info <- bundle_infos) {
val isabelle_name = context.dist_name
val platform = bundle_info.platform
progress.echo("\nApplication bundle for " + platform)
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
// release archive
execute_tar(tmp_dir, "-xzf " + File.bash_path(context.isabelle_archive))
val other_isabelle = context.other_isabelle(tmp_dir)
val isabelle_target = other_isabelle.isabelle_home
// bundled components
progress.echo("Bundled components:")
val contrib_dir = Components.contrib(isabelle_target)
val (bundled_components, jdk_component) =
get_bundled_components(isabelle_target, platform)
Components.resolve(context.components_base, bundled_components,
target_dir = Some(contrib_dir),
copy_dir = Some(context.dist_dir + Path.explode("contrib")),
progress = progress)
val more_components_names =
more_components.map(Components.unpack(contrib_dir, _, progress = progress))
Components.purge(contrib_dir, platform)
activate_components(isabelle_target, platform, more_components_names)
// Java parameters
val java_options: List[String] =
(for {
variable <-
List(
"ISABELLE_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_OPTIONS")
opt <- Word.explode(other_isabelle.getenv(variable))
}
yield {
val s = "-Dapple.awt.application.name="
if (opt.startsWith(s)) s + isabelle_name else opt
}) ::: List("-Disabelle.jedit_server=" + isabelle_name)
val classpath: List[Path] =
{
val base = isabelle_target.absolute
- Path.split(other_isabelle.setup_classpath()).map(path =>
+ val classpath1 = Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH"))
+ val classpath2 = Path.split(other_isabelle.getenv("ISABELLE_SETUP_CLASSPATH"))
+ (classpath1 ::: classpath2).map(path =>
{
val abs_path = path.absolute
File.relative_path(base, abs_path) match {
case Some(rel_path) => rel_path
- case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
+ case None => error("Bad classpath element: " + abs_path)
}
})
}
val jedit_options = Path.explode("src/Tools/jEdit/etc/options")
val jedit_props =
Path.explode(other_isabelle.getenv("JEDIT_HOME") + "/properties/jEdit.props")
// build heaps
if (build_sessions.nonEmpty) {
progress.echo("Building heaps " + commas_quote(build_sessions) + " ...")
build_heaps(options, platform, build_sessions, isabelle_target)
}
// application bundling
platform match {
case Platform.Family.linux_arm | Platform.Family.linux =>
File.change(isabelle_target + jedit_options,
_.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24"))
File.change(isabelle_target + jedit_props,
_.replaceAll("console.fontsize=.*", "console.fontsize=18")
.replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18")
.replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18")
.replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18")
.replaceAll("view.fontsize=.*", "view.fontsize=24")
.replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16"))
make_isabelle_options(
isabelle_target + Path.explode("Isabelle.options"), java_options)
make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, classpath)
progress.echo("Packaging " + bundle_info.name + " ...")
execute_tar(tmp_dir,
"-czf " + File.bash_path(context.dist_dir + bundle_info.path) + " " +
Bash.string(isabelle_name))
case Platform.Family.macos =>
File.change(isabelle_target + jedit_props,
_.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
.replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d"))
// macOS application bundle
val app_contents = isabelle_target + Path.explode("Contents")
for (icon <- List("lib/logo/isabelle.icns", "lib/logo/theory.icns")) {
Isabelle_System.copy_file(isabelle_target + Path.explode(icon),
Isabelle_System.make_directory(app_contents + Path.explode("Resources")))
}
make_isabelle_plist(
app_contents + Path.explode("Info.plist"), isabelle_name, archive.id)
make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component,
classpath, dock_icon = true)
val isabelle_options = Path.explode("Isabelle.options")
make_isabelle_options(
isabelle_target + isabelle_options,
java_options ::: List("-Disabelle.app=true"))
// application archive
progress.echo("Packaging " + bundle_info.name + " ...")
val isabelle_app = Path.explode(isabelle_name + ".app")
Isabelle_System.move_file(tmp_dir + Path.explode(isabelle_name),
tmp_dir + isabelle_app)
execute_tar(tmp_dir,
"-czf " + File.bash_path(context.dist_dir + bundle_info.path) + " " +
File.bash_path(isabelle_app))
case Platform.Family.windows =>
File.change(isabelle_target + jedit_props,
_.replaceAll("foldPainter=.*", "foldPainter=Square"))
// application launcher
Isabelle_System.move_file(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
val app_template = Path.explode("~~/Admin/Windows/launch4j")
make_isabelle_options(
isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
java_options, line_ending = "\r\n")
val isabelle_xml = Path.explode("isabelle.xml")
val isabelle_exe = bundle_info.path
File.write(tmp_dir + isabelle_xml,
File.read(app_template + isabelle_xml)
.replace("{ISABELLE_NAME}", isabelle_name)
.replace("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe))
.replace("{ICON}",
File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
.replace("{SPLASH}",
File.platform_path(app_template + Path.explode("isabelle.bmp")))
.replace("{CLASSPATH}",
cat_lines(classpath.map(cp =>
" %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "")))
.replace("\\jdk\\", "\\" + jdk_component + "\\"))
execute(tmp_dir,
"\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
Isabelle_System.copy_file(app_template + Path.explode("manifest.xml"),
isabelle_target + isabelle_exe.ext("manifest"))
// Cygwin setup
val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
Isabelle_System.copy_file(cygwin_template + Path.explode("Cygwin-Terminal.bat"),
isabelle_target)
val cygwin_mirror =
File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
val cygwin_bat = Path.explode("Cygwin-Setup.bat")
File.write(isabelle_target + cygwin_bat,
File.read(cygwin_template + cygwin_bat).replace("{MIRROR}", cygwin_mirror))
File.set_executable(isabelle_target + cygwin_bat, true)
for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
val path = Path.explode(name)
Isabelle_System.copy_file(cygwin_template + path,
isabelle_target + Path.explode("contrib/cygwin") + path)
}
execute(isabelle_target,
"""find . -type f -not -name "*.exe" -not -name "*.dll" """ +
(if (Platform.is_macos) "-perm +100" else "-executable") +
" -print0 > contrib/cygwin/isabelle/executables")
execute(isabelle_target,
"""find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
"""> contrib/cygwin/isabelle/symlinks""")
execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
// executable archive (self-extracting 7z)
val archive_name = isabelle_name + ".7z"
val exe_archive = tmp_dir + Path.explode(archive_name)
exe_archive.file.delete
progress.echo("Packaging " + archive_name + " ...")
execute(tmp_dir,
"7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
val sfx_txt =
File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt"))
.replace("{ISABELLE_NAME}", isabelle_name)
Bytes.write(context.dist_dir + isabelle_exe,
Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
File.set_executable(context.dist_dir + isabelle_exe, true)
}
})
progress.echo("DONE")
}
/* minimal website */
for (dir <- website) {
val website_platform_bundles =
for {
bundle_info <- bundle_infos
if (context.dist_dir + bundle_info.path).is_file
} yield (bundle_info.name, bundle_info)
val isabelle_link =
HTML.link(Isabelle_System.isabelle_repository.changeset(archive.id),
HTML.text("Isabelle/" + archive.id))
val afp_link =
HTML.link(Isabelle_System.afp_repository.changeset(afp_rev),
HTML.text("AFP/" + afp_rev))
HTML.write_document(dir, "index.html",
List(HTML.title(context.dist_name)),
List(
HTML.section(context.dist_name),
HTML.subsection("Downloads"),
HTML.itemize(
List(HTML.link(context.dist_name + ".tar.gz", HTML.text("Source archive"))) ::
website_platform_bundles.map({ case (bundle, bundle_info) =>
List(HTML.link(bundle, HTML.text(bundle_info.platform_description + " bundle"))) })),
HTML.subsection("Repositories"),
HTML.itemize(
List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link))))))
Isabelle_System.copy_file(context.isabelle_archive, dir)
for ((bundle, _) <- website_platform_bundles) {
Isabelle_System.copy_file(context.dist_dir + Path.explode(bundle), dir)
}
}
/* HTML library */
if (build_library) {
if (context.isabelle_library_archive.is_file) {
progress.echo_warning("Library archive already exists: " + context.isabelle_library_archive)
}
else {
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
val bundle =
context.dist_dir + Path.explode(context.dist_name + "_" + Platform.family + ".tar.gz")
execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
val other_isabelle = context.other_isabelle(tmp_dir)
Isabelle_System.make_directory(other_isabelle.etc)
File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
" -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
" -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
other_isabelle.isabelle_home_user.file.delete
execute(tmp_dir, "chmod -R a+r " + Bash.string(context.dist_name))
execute(tmp_dir, "chmod -R g=o " + Bash.string(context.dist_name))
execute_tar(tmp_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
" " + Bash.string(context.dist_name + "/browser_info"))
})
}
}
}
/** command line entry point **/
def main(args: Array[String]): Unit =
{
Command_Line.tool {
var afp_rev = ""
var components_base: Path = Components.default_components_base
var target_dir = Path.current
var release_name = ""
var source_archive = ""
var website: Option[Path] = None
var build_sessions: List[String] = Nil
var more_components: List[Path] = Nil
var parallel_jobs = 1
var build_library = false
var options = Options.init()
var platform_families = default_platform_families
var rev = ""
val getopts = Getopts("""
Usage: Admin/build_release [OPTIONS]
Options are:
-A REV corresponding AFP changeset id
-C DIR base directory for Isabelle components (default: """ +
Components.default_components_base + """)
-D DIR target directory (default ".")
-R RELEASE explicit release name
-S ARCHIVE use existing source archive (file or URL)
-W WEBSITE produce minimal website in given directory
-b SESSIONS build platform-specific session images (separated by commas)
-c ARCHIVE clean bundling with additional component .tar.gz archive
-j INT maximum number of parallel jobs (default 1)
-l build library
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-p NAMES platform families (default: """ + default_platform_families.mkString(",") + """)
-r REV Mercurial changeset id (default: ARCHIVE or RELEASE or tip)
Build Isabelle release in base directory, using the local repository clone.
""",
"A:" -> (arg => afp_rev = arg),
"C:" -> (arg => components_base = Path.explode(arg)),
"D:" -> (arg => target_dir = Path.explode(arg)),
"R:" -> (arg => release_name = arg),
"S:" -> (arg => source_archive = arg),
"W:" -> (arg => website = Some(Path.explode(arg))),
"b:" -> (arg => build_sessions = space_explode(',', arg)),
"c:" -> (arg =>
{
val path = Path.explode(arg)
Components.Archive.get_name(path.file_name)
more_components = more_components ::: List(path)
}),
"j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
"l" -> (_ => build_library = true),
"o:" -> (arg => options = options + arg),
"p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)),
"r:" -> (arg => rev = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
error("Building for windows requires 7z")
val progress = new Console_Progress()
def make_context(name: String): Release_Context =
Release_Context(target_dir,
release_name = name,
components_base = components_base,
progress = progress)
val context =
if (source_archive.isEmpty) {
val context = make_context(release_name)
val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip"
build_release_archive(context, version, parallel_jobs = parallel_jobs)
context
}
else {
val archive =
Release_Archive.get(source_archive, rename = release_name, progress = progress)
val context = make_context(archive.identifier)
Isabelle_System.make_directory(context.dist_dir)
use_release_archive(context, archive, id = rev)
context
}
build_release(options, context, afp_rev = afp_rev, platform_families = platform_families,
more_components = more_components, build_sessions = build_sessions,
build_library = build_library, parallel_jobs = parallel_jobs, website = website)
}
}
}
diff --git a/src/Pure/Admin/other_isabelle.scala b/src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala
+++ b/src/Pure/Admin/other_isabelle.scala
@@ -1,138 +1,134 @@
/* Title: Pure/Admin/other_isabelle.scala
Author: Makarius
Manage other Isabelle distributions.
*/
package isabelle
object Other_Isabelle
{
def apply(isabelle_home: Path,
isabelle_identifier: String = "",
user_home: Path = Path.USER_HOME,
progress: Progress = new Progress): Other_Isabelle =
new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress)
}
class Other_Isabelle(
val isabelle_home: Path,
val isabelle_identifier: String,
user_home: Path,
progress: Progress)
{
other_isabelle =>
override def toString: String = isabelle_home.toString
if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined)
error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
/* static system */
def bash(
script: String,
redirect: Boolean = false,
echo: Boolean = false,
strict: Boolean = true): Process_Result =
progress.bash(
"export USER_HOME=" + File.bash_path(user_home) + "\n" +
Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
def apply(
cmdline: String,
redirect: Boolean = false,
echo: Boolean = false,
strict: Boolean = true): Process_Result =
bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict)
def resolve_components(echo: Boolean): Unit =
other_isabelle(
"env ISABELLE_TOOLS=" + Bash.string(Isabelle_System.getenv("ISABELLE_TOOLS")) +
" isabelle components -a", redirect = true, echo = echo).check
def getenv(name: String): String =
other_isabelle("getenv -b " + Bash.string(name)).check.out
- def setup_classpath(): String =
- other_isabelle("env bash -c " +
- Bash.string("isabelle_setup_classpath && isabelle getenv -b ISABELLE_CLASSPATH")).check.out
-
val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER"))
val etc: Path = isabelle_home_user + Path.explode("etc")
val etc_settings: Path = etc + Path.explode("settings")
val etc_preferences: Path = etc + Path.explode("preferences")
/* NEWS */
def make_news(): Unit =
{
val doc_dir = isabelle_home + Path.explode("doc")
val fonts_dir = Isabelle_System.make_directory(doc_dir + Path.explode("fonts"))
Isabelle_Fonts.make_entries(getenv = getenv, hidden = true).
foreach(entry => Isabelle_System.copy_file(entry.path, fonts_dir))
HTML.write_document(doc_dir, "NEWS.html",
List(HTML.title("NEWS")),
List(
HTML.chapter("NEWS"),
HTML.source(Symbol.decode(File.read(isabelle_home + Path.explode("NEWS"))))))
}
/* components */
def init_components(
component_repository: String = Components.default_component_repository,
components_base: Path = Components.default_components_base,
catalogs: List[String] = Nil,
components: List[String] = Nil): List[String] =
{
val dir = Components.admin(isabelle_home)
("ISABELLE_COMPONENT_REPOSITORY=" + Bash.string(component_repository)) ::
catalogs.map(name =>
"init_components " + File.bash_path(components_base) + " " +
File.bash_path(dir + Path.basic(name))) :::
components.map(name =>
"init_component " + File.bash_path(components_base + Path.basic(name)))
}
/* settings */
def clean_settings(): Boolean =
if (!etc_settings.is_file) true
else if (File.read(etc_settings).startsWith("# generated by Isabelle")) {
etc_settings.file.delete; true
}
else false
def init_settings(settings: List[String]): Unit =
{
if (!clean_settings())
error("Cannot proceed with existing user settings file: " + etc_settings)
Isabelle_System.make_directory(etc_settings.dir)
File.write(etc_settings,
"# generated by Isabelle " + Date.now() + "\n" +
"#-*- shell-script -*- :mode=shellscript:\n" +
settings.mkString("\n", "\n", "\n"))
}
/* cleanup */
def cleanup(): Unit =
{
clean_settings()
etc.file.delete
isabelle_home_user.file.delete
}
}
diff --git a/src/Pure/System/scala.scala b/src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala
+++ b/src/Pure/System/scala.scala
@@ -1,285 +1,284 @@
/* Title: Pure/System/scala.scala
Author: Makarius
Support for Scala at runtime.
*/
package isabelle
import java.io.{File => JFile, StringWriter, PrintWriter}
import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter}
import scala.tools.nsc.interpreter.{IMain, Results}
import scala.tools.nsc.interpreter.shell.ReplReporterImpl
object Scala
{
/** registered functions **/
abstract class Fun(val name: String, val thread: Boolean = false)
{
override def toString: String = name
def multi: Boolean = true
def position: Properties.T = here.position
def here: Scala_Project.Here
def invoke(args: List[Bytes]): List[Bytes]
}
abstract class Fun_Strings(name: String, thread: Boolean = false)
extends Fun(name, thread = thread)
{
override def invoke(args: List[Bytes]): List[Bytes] =
apply(args.map(_.text)).map(Bytes.apply)
def apply(args: List[String]): List[String]
}
abstract class Fun_String(name: String, thread: Boolean = false)
extends Fun_Strings(name, thread = thread)
{
override def multi: Boolean = false
override def apply(args: List[String]): List[String] =
List(apply(Library.the_single(args)))
def apply(arg: String): String
}
class Functions(val functions: Fun*) extends Isabelle_System.Service
lazy val functions: List[Fun] =
Isabelle_System.make_services(classOf[Functions]).flatMap(_.functions)
/** demo functions **/
object Echo extends Fun_String("echo")
{
val here = Scala_Project.here
def apply(arg: String): String = arg
}
object Sleep extends Fun_String("sleep")
{
val here = Scala_Project.here
def apply(seconds: String): String =
{
val t =
seconds match {
case Value.Double(s) => Time.seconds(s)
case _ => error("Malformed argument: " + quote(seconds))
}
val t0 = Time.now()
t.sleep()
val t1 = Time.now()
(t1 - t0).toString
}
}
/** compiler **/
def class_path(): List[String] =
- Library.distinct(
- for {
- prop <- List("isabelle.scala.classpath", "java.class.path")
- elems = System.getProperty(prop, "") if elems.nonEmpty
- elem <- space_explode(JFile.pathSeparatorChar, elems) if elem.nonEmpty
- } yield elem)
+ for {
+ prop <- List("isabelle.scala.classpath", "java.class.path")
+ elems = System.getProperty(prop, "") if elems.nonEmpty
+ elem <- space_explode(JFile.pathSeparatorChar, elems) if elem.nonEmpty
+ } yield elem
object Compiler
{
def context(
error: String => Unit = Exn.error,
jar_dirs: List[JFile] = Nil): Context =
{
def find_jars(dir: JFile): List[String] =
File.find_files(dir, file => file.getName.endsWith(".jar")).
map(File.absolute_name)
val settings = new GenericRunnerSettings(error)
settings.classpath.value =
(class_path() ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
new Context(settings)
}
def default_print_writer: PrintWriter =
new NewLinePrintWriter(new ConsoleWriter, true)
class Context private [Compiler](val settings: GenericRunnerSettings)
{
override def toString: String = settings.toString
def interpreter(
print_writer: PrintWriter = default_print_writer,
class_loader: ClassLoader = null): IMain =
{
new IMain(settings, new ReplReporterImpl(settings, print_writer))
{
override def parentClassLoader: ClassLoader =
if (class_loader == null) super.parentClassLoader
else class_loader
}
}
def toplevel(interpret: Boolean, source: String): List[String] =
{
val out = new StringWriter
val interp = interpreter(new PrintWriter(out))
val marker = '\u000b'
val ok =
interp.withLabel(marker.toString) {
if (interpret) interp.interpret(source) == Results.Success
else (new interp.ReadEvalPrint).compile(source)
}
out.close()
val Error = """(?s)^\S* error: (.*)$""".r
val errors =
space_explode(marker, Library.strip_ansi_color(out.toString)).
collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
if (!ok && errors.isEmpty) List("Error") else errors
}
}
}
object Toplevel extends Fun_String("scala_toplevel")
{
val here = Scala_Project.here
def apply(arg: String): String =
{
val (interpret, source) =
YXML.parse_body(arg) match {
case Nil => (false, "")
case List(XML.Text(source)) => (false, source)
case body => import XML.Decode._; pair(bool, string)(body)
}
val errors =
try { Compiler.context().toplevel(interpret, source) }
catch { case ERROR(msg) => List(msg) }
locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
}
}
/** invoke Scala functions from ML **/
/* invoke function */
object Tag extends Enumeration
{
val NULL, OK, ERROR, FAIL, INTERRUPT = Value
}
def function_thread(name: String): Boolean =
functions.find(fun => fun.name == name) match {
case Some(fun) => fun.thread
case None => false
}
def function_body(name: String, args: List[Bytes]): (Tag.Value, List[Bytes]) =
functions.find(fun => fun.name == name) match {
case Some(fun) =>
Exn.capture { fun.invoke(args) } match {
case Exn.Res(null) => (Tag.NULL, Nil)
case Exn.Res(res) => (Tag.OK, res)
case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, Nil)
case Exn.Exn(e) => (Tag.ERROR, List(Bytes(Exn.message(e))))
}
case None => (Tag.FAIL, List(Bytes("Unknown Isabelle/Scala function: " + quote(name))))
}
/* protocol handler */
class Handler extends Session.Protocol_Handler
{
private var session: Session = null
private var futures = Map.empty[String, Future[Unit]]
override def init(session: Session): Unit =
synchronized { this.session = session }
override def exit(): Unit = synchronized
{
for ((id, future) <- futures) cancel(id, future)
futures = Map.empty
}
private def result(id: String, tag: Scala.Tag.Value, res: List[Bytes]): Unit =
synchronized
{
if (futures.isDefinedAt(id)) {
session.protocol_command_raw("Scala.result", Bytes(id) :: Bytes(tag.id.toString) :: res)
futures -= id
}
}
private def cancel(id: String, future: Future[Unit]): Unit =
{
future.cancel()
result(id, Scala.Tag.INTERRUPT, Nil)
}
private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
{
msg.properties match {
case Markup.Invoke_Scala(name, id) =>
def body: Unit =
{
val (tag, res) = Scala.function_body(name, msg.chunks)
result(id, tag, res)
}
val future =
if (Scala.function_thread(name)) {
Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body)
}
else Future.fork(body)
futures += (id -> future)
true
case _ => false
}
}
private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized
{
msg.properties match {
case Markup.Cancel_Scala(id) =>
futures.get(id) match {
case Some(future) => cancel(id, future)
case None =>
}
true
case _ => false
}
}
override val functions =
List(
Markup.Invoke_Scala.name -> invoke_scala,
Markup.Cancel_Scala.name -> cancel_scala)
}
}
class Scala_Functions extends Scala.Functions(
Scala.Echo,
Scala.Sleep,
Scala.Toplevel,
Bytes.Decode_Base64,
Bytes.Encode_Base64,
Doc.Doc_Names,
Bash.Process,
Bibtex.Check_Database,
Isabelle_System.Make_Directory,
Isabelle_System.Copy_Dir,
Isabelle_System.Copy_File,
Isabelle_System.Copy_File_Base,
Isabelle_System.Rm_Tree,
Isabelle_System.Download,
Isabelle_System.Isabelle_Id,
Isabelle_Tool.Isabelle_Tools,
isabelle.atp.SystemOnTPTP.List_Systems,
isabelle.atp.SystemOnTPTP.Run_System)