diff --git a/Admin/Windows/Cygwin/setup_server b/Admin/Windows/Cygwin/setup_server
--- a/Admin/Windows/Cygwin/setup_server
+++ b/Admin/Windows/Cygwin/setup_server
@@ -1,23 +1,23 @@
#!/usr/bin/env bash
CYGWIN_MAIN="https://cygwin.com"
CYGWIN_MIRROR="https://ftp.eq.uc.pt/software/pc/prog/cygwin"
function fail()
{
echo "$1" >&2
exit 2
}
function download()
{
local URL="$1"
local DIR="${2:-.}"
mkdir -p "$DIR" || fail "Cannot create directory: \"$DIR\""
echo "Downloading $URL ..."
- curl --fail --silent "$URL" > "$DIR"/"$(basename "$URL")" || fail "FAILED"
+ curl --fail --silent --location "$URL" > "$DIR"/"$(basename "$URL")" || fail "FAILED"
}
download "$CYGWIN_MAIN/setup-x86_64.exe"
download "$CYGWIN_MIRROR/x86_64/setup.xz" "x86_64"
download "$CYGWIN_MIRROR/x86_64/setup.xz.sig" "x86_64"
diff --git a/lib/Tools/components b/lib/Tools/components
--- a/lib/Tools/components
+++ b/lib/Tools/components
@@ -1,175 +1,157 @@
#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: resolve Isabelle components
## diagnostics
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS] [COMPONENTS ...]"
echo
echo " Options are:"
echo " -I init user settings"
echo " -R URL component repository (default \$ISABELLE_COMPONENT_REPOSITORY)"
echo " -a resolve all missing components"
echo " -l list status"
echo " -u DIR update \$ISABELLE_HOME_USER/etc/components: add directory"
echo " -x DIR update \$ISABELLE_HOME_USER/etc/components: remove directory"
echo
echo " Resolve Isabelle components via download and installation: given COMPONENTS"
echo " are identified via base name. Further operations manage etc/settings and"
echo " etc/components in \$ISABELLE_HOME_USER."
echo
echo " ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\""
echo " ISABELLE_HOME_USER=\"$ISABELLE_HOME_USER\""
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## process command line
#options
INIT_SETTINGS=""
COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY"
ALL_MISSING=""
LIST_ONLY=""
declare -a UPDATE_COMPONENTS=()
while getopts "IR:alu:x:" OPT
do
case "$OPT" in
I)
INIT_SETTINGS="true"
;;
R)
COMPONENT_REPOSITORY="$OPTARG"
;;
a)
ALL_MISSING="true"
;;
l)
LIST_ONLY="true"
;;
u)
UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="+$OPTARG"
;;
x)
UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="-$OPTARG"
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
# args
[ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" -a "${#UPDATE_COMPONENTS[@]}" -eq 0 ] && usage
if [ -z "$ALL_MISSING" ]; then
splitarray ":" "$@"
else
splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@"
fi
declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}")
## main
splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}")
splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}")
if [ -n "$INIT_SETTINGS" ]; then
SETTINGS="$ISABELLE_HOME_USER/etc/settings"
SETTINGS_CONTENT='init_components "${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}" "$ISABELLE_HOME/Admin/components/main"'
if [ ! -e "$SETTINGS" ]; then
echo "Initializing \"$SETTINGS\""
mkdir -p "$(dirname "$SETTINGS")"
{
echo "#-*- shell-script -*- :mode=shellscript:"
echo
echo "$SETTINGS_CONTENT"
} > "$SETTINGS"
elif grep "init_components.*components/main" "$SETTINGS" >/dev/null 2>/dev/null
then
:
else
echo "User settings file already exists!"
echo
echo "Edit \"$SETTINGS\" manually"
echo "and add the following line near its start:"
echo
echo " $SETTINGS_CONTENT"
echo
fi
elif [ -n "$LIST_ONLY" ]; then
echo
echo "Available components:"
for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo " $NAME"; done
echo
echo "Missing components:"
for NAME in "${MISSING_COMPONENTS[@]}"; do echo " $NAME"; done
elif [ "${#UPDATE_COMPONENTS[@]}" -ne 0 ]; then
isabelle scala_build || exit $?
exec isabelle java isabelle.Components "${UPDATE_COMPONENTS[@]}"
else
+ source "$ISABELLE_HOME/lib/scripts/download_file"
for NAME in "${SELECTED_COMPONENTS[@]}"
do
BASE_NAME="$(basename "$NAME")"
FULL_NAME=""
for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}"
do
[ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X"
done
if [ -z "$FULL_NAME" ]; then
echo "Ignoring irrelevant component \"$NAME\""
elif [ -d "$FULL_NAME" ]; then
echo "Skipping existing component \"$FULL_NAME\""
else
if [ ! -e "${FULL_NAME}.tar.gz" ]; then
- REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
- type -p curl > /dev/null || fail "Cannot download files: missing curl"
- echo "Getting \"$REMOTE\""
- mkdir -p "$(dirname "$FULL_NAME")"
-
- CURL_OPTIONS="--fail --silent --location"
- if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ]; then
- case $(sw_vers -productVersion) in
- 10.*)
- CURL_OPTIONS="$CURL_OPTIONS --insecure"
- ;;
- esac
- fi
- if curl $CURL_OPTIONS "$REMOTE" > "${FULL_NAME}.tar.gz.part"
- then
- mv -f "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz"
- else
- rm -f "${FULL_NAME}.tar.gz.part"
- fail "Failed to download \"$REMOTE\""
- fi
+ download_file "$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz" "${FULL_NAME}.tar.gz" || exit $?
fi
if [ -e "${FULL_NAME}.tar.gz" ]; then
echo "Unpacking \"${FULL_NAME}.tar.gz\""
- tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz" || exit 2
+ tar -C "$(dirname "$FULL_NAME")" -x -z -f "${FULL_NAME}.tar.gz" || exit 2
fi
fi
done
fi
diff --git a/lib/scripts/download_file b/lib/scripts/download_file
new file mode 100644
--- /dev/null
+++ b/lib/scripts/download_file
@@ -0,0 +1,40 @@
+# -*- shell-script -*- :mode=shellscript:
+#
+# Bash function to download file via "curl".
+
+function download_file ()
+{
+ [ "$#" -ne 2 ] && {
+ echo "Bad arguments for download_file" >&2
+ return 2
+ }
+ local REMOTE="$1"
+ local LOCAL="$2"
+
+ type -p curl > /dev/null || {
+ echo "Require \"curl\" to download files" >&2
+ return 2
+ }
+
+ local CURL_OPTIONS="--fail --silent --location"
+ if [ "$(uname -s)" = "Darwin" ]
+ then
+ case $(sw_vers -productVersion) in
+ 10.*)
+ CURL_OPTIONS="$CURL_OPTIONS --insecure"
+ ;;
+ esac
+ fi
+
+ echo "Getting \"$REMOTE\""
+ mkdir -p "$(dirname "$LOCAL")"
+
+ if curl $CURL_OPTIONS "$REMOTE" > "${LOCAL}.part"
+ then
+ mv -f "${LOCAL}.part" "$LOCAL"
+ else
+ rm -f "${LOCAL}.part"
+ echo "Failed to download \"$REMOTE\"" >&2
+ return 2
+ fi
+}
diff --git a/src/Pure/Admin/build_history.scala b/src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala
+++ b/src/Pure/Admin/build_history.scala
@@ -1,605 +1,605 @@
/* Title: Pure/Admin/build_history.scala
Author: Makarius
Build other history versions.
*/
package isabelle
object Build_History {
/* log files */
val engine = "build_history"
val log_prefix = engine + "_"
/* augment settings */
def augment_settings(
other_isabelle: Other_Isabelle,
threads: Int,
arch_64: Boolean,
heap: Int,
max_heap: Option[Int],
more_settings: List[String]
): String = {
val (ml_platform, ml_settings) = {
val cygwin_32 = "x86-cygwin"
val windows_32 = "x86-windows"
val windows_64 = "x86_64-windows"
val windows_64_32 = "x86_64_32-windows"
val platform_32 = other_isabelle.getenv("ISABELLE_PLATFORM32")
val platform_64 = other_isabelle.getenv("ISABELLE_PLATFORM64")
val platform_64_32 = platform_64.replace("x86_64-", "x86_64_32-")
val polyml_home =
try { Path.explode(other_isabelle.getenv("ML_HOME")).dir }
catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
def err(platform: String): Nothing =
error("Platform " + platform + " unavailable on this machine")
def check_dir(platform: String): Boolean =
platform != "" && ml_home(platform).is_dir
val ml_platform =
if (Platform.is_windows && arch_64) {
if (check_dir(windows_64)) windows_64 else err(windows_64)
}
else if (Platform.is_windows && !arch_64) {
if (check_dir(windows_64_32)) windows_64_32
else if (check_dir(cygwin_32)) cygwin_32
else if (check_dir(windows_32)) windows_32
else err(windows_32)
}
else if (arch_64) {
if (check_dir(platform_64)) platform_64 else err(platform_64)
}
else if (check_dir(platform_64_32)) platform_64_32
else platform_32
val ml_options =
"--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
" --gcthreads " + threads +
(if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
(ml_platform,
List(
"ML_HOME=" + File.bash_path(ml_home(ml_platform)),
"ML_PLATFORM=" + quote(ml_platform),
"ML_OPTIONS=" + quote(ml_options)))
}
val thread_settings =
List(
"ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
"ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
val settings =
List(ml_settings, thread_settings) :::
(if (more_settings.isEmpty) Nil else List(more_settings))
File.append(other_isabelle.etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_))))
ml_platform
}
/** local build **/
private val default_user_home = Path.USER_HOME
private val default_multicore = (1, 1)
private val default_heap = 1500
private val default_isabelle_identifier = "build_history"
def local_build(
options: Options,
root: Path,
user_home: Path = default_user_home,
progress: Progress = new Progress,
afp: Boolean = false,
afp_partition: Int = 0,
isabelle_identifier: String = default_isabelle_identifier,
ml_statistics_step: Int = 1,
component_repository: String = Components.default_component_repository,
components_base: Path = Components.default_components_base,
fresh: Boolean = false,
hostname: String = "",
multicore_base: Boolean = false,
multicore_list: List[(Int, Int)] = List(default_multicore),
arch_64: Boolean = false,
heap: Int = default_heap,
max_heap: Option[Int] = None,
init_settings: List[String] = Nil,
more_settings: List[String] = Nil,
more_preferences: List[String] = Nil,
verbose: Boolean = false,
build_tags: List[String] = Nil,
build_args: List[String] = Nil
): List[(Process_Result, Path)] = {
/* sanity checks */
if (File.eq(Path.ISABELLE_HOME, root)) {
error("Repository coincides with ISABELLE_HOME=" + Path.ISABELLE_HOME.expand)
}
for ((threads, _) <- multicore_list if threads < 1) {
error("Bad threads value < 1: " + threads)
}
for ((_, processes) <- multicore_list if processes < 1) {
error("Bad processes value < 1: " + processes)
}
if (heap < 100) error("Bad heap value < 100: " + heap)
if (max_heap.isDefined && max_heap.get < heap) {
error("Bad max_heap value < heap: " + max_heap.get)
}
System.getenv("ISABELLE_SETTINGS_PRESENT") match {
case null | "" =>
case _ => error("Cannot run Admin/build_other within existing Isabelle settings environment")
}
/* Isabelle + AFP directory */
def directory(dir: Path): Mercurial.Hg_Sync.Directory = {
val directory = Mercurial.Hg_Sync.directory(dir)
if (verbose) progress.echo(directory.log)
directory
}
val isabelle_directory = directory(root)
val afp_directory = if (afp) Some(directory(root + Path.explode("AFP"))) else None
val (afp_build_args, afp_sessions) =
if (afp_directory.isEmpty) (Nil, Nil)
else {
val (opt, sessions) = {
if (afp_partition == 0) ("-d", Nil)
else {
try {
val afp_info = AFP.init(options, base_dir = afp_directory.get.root)
("-d", afp_info.partition(afp_partition))
} catch { case ERROR(_) => ("-D", Nil) }
}
}
(List(opt, "~~/AFP/thys"), sessions)
}
/* main */
val other_isabelle =
Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
user_home = user_home, progress = progress)
val build_host = proper_string(hostname) getOrElse Isabelle_System.hostname()
val build_history_date = Date.now()
val build_group_id = build_host + ":" + build_history_date.time.ms
var first_build = true
for ((threads, processes) <- multicore_list) yield {
/* init settings */
val component_settings =
other_isabelle.init_components(
component_repository = component_repository,
components_base = components_base,
- catalogs = List("main", "optional"))
+ catalogs = Components.optional_catalogs)
other_isabelle.init_settings(component_settings ::: init_settings)
other_isabelle.resolve_components(echo = verbose)
val ml_platform =
augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
File.write(other_isabelle.etc_preferences, cat_lines(more_preferences))
val isabelle_output =
other_isabelle.isabelle_home_user + Path.explode("heaps") +
Path.explode(other_isabelle.getenv("ML_IDENTIFIER"))
val isabelle_output_log = isabelle_output + Path.explode("log")
val isabelle_base_log = isabelle_output + Path.explode("../base_log")
if (first_build) {
other_isabelle.resolve_components(echo = verbose)
if (fresh) {
Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes"))
}
other_isabelle.bash(
- "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
+ "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty")) + ":$PATH\" " +
"bin/isabelle jedit -b", redirect = true, echo = verbose).check
for {
tool <- List("ghc_setup", "ocaml_setup")
if other_isabelle.getenv("ISABELLE_" + Word.uppercase(tool)) == "true" &&
(other_isabelle.isabelle_home + Path.explode("lib/Tools/" + tool)).is_file
} other_isabelle.bash("bin/isabelle " + tool, echo = verbose)
Isabelle_System.rm_tree(isabelle_base_log)
}
Isabelle_System.rm_tree(isabelle_output)
Isabelle_System.make_directory(isabelle_output)
(other_isabelle.isabelle_home_user + Path.explode("mash_state")).file.delete
val log_path =
other_isabelle.isabelle_home_user +
Build_Log.log_subdir(build_history_date) +
Build_Log.log_filename(Build_History.engine, build_history_date,
List(build_host, ml_platform, "M" + threads) ::: build_tags)
Isabelle_System.make_directory(log_path.dir)
val build_out = other_isabelle.isabelle_home_user + Path.explode("log/build.out")
val build_out_progress = new File_Progress(build_out)
build_out.file.delete
/* build */
if (multicore_base && !first_build && isabelle_base_log.is_dir) {
Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
}
val build_start = Date.now()
val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args
val build_isabelle =
Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
user_home = user_home, progress = build_out_progress)
val build_result =
build_isabelle.bash("bin/isabelle build " + Bash.strings(build_args1 ::: afp_sessions),
redirect = true, echo = true, strict = false)
val build_end = Date.now()
val build_info: Build_Log.Build_Info =
Build_Log.Log_File(log_path.file_name, build_result.out_lines).
parse_build_info(ml_statistics = true)
/* output log */
val store = Sessions.store(options + "build_database_server=false")
val meta_info =
Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) :::
Properties.lines_nonempty(Build_Log.Prop.build_args.name, build_args1) :::
List(
Build_Log.Prop.build_group_id.name -> build_group_id,
Build_Log.Prop.build_id.name -> (build_host + ":" + build_start.time.ms),
Build_Log.Prop.build_engine.name -> Build_History.engine,
Build_Log.Prop.build_host.name -> build_host,
Build_Log.Prop.build_start.name -> Build_Log.print_date(build_start),
Build_Log.Prop.build_end.name -> Build_Log.print_date(build_end),
Build_Log.Prop.isabelle_version.name -> isabelle_directory.id) :::
afp_directory.map(dir => Build_Log.Prop.afp_version.name -> dir.id).toList
build_out_progress.echo("Reading session build info ...")
val session_build_info =
build_info.finished_sessions.flatMap { session_name =>
val database = isabelle_output + store.database(session_name)
if (database.is_file) {
using(SQLite.open_database(database)) { db =>
val theory_timings =
try {
store.read_theory_timings(db, session_name).map(ps =>
Protocol.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps))
}
catch { case ERROR(_) => Nil }
val session_sources =
store.read_build(db, session_name).map(_.sources) match {
case Some(sources) if sources.length == SHA1.digest_length =>
List("Sources " + session_name + " " + sources)
case _ => Nil
}
theory_timings ::: session_sources
}
}
else Nil
}
build_out_progress.echo("Reading ML statistics ...")
val ml_statistics =
build_info.finished_sessions.flatMap { session_name =>
val database = isabelle_output + store.database(session_name)
val log_gz = isabelle_output + store.log_gz(session_name)
val properties =
if (database.is_file) {
using(SQLite.open_database(database))(db =>
store.read_ml_statistics(db, session_name))
}
else if (log_gz.is_file) {
Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
}
else Nil
val trimmed_properties =
if (ml_statistics_step <= 0) Nil
else if (ml_statistics_step == 1) properties
else {
(for { (ps, i) <- properties.iterator.zipWithIndex if i % ml_statistics_step == 0 }
yield ps).toList
}
trimmed_properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps)
}
build_out_progress.echo("Reading error messages ...")
val session_errors =
build_info.failed_sessions.flatMap { session_name =>
val database = isabelle_output + store.database(session_name)
val errors =
if (database.is_file) {
try {
using(SQLite.open_database(database))(db => store.read_errors(db, session_name))
} // column "errors" could be missing
catch { case _: java.sql.SQLException => Nil }
}
else Nil
errors.map(msg => List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> msg))
}
build_out_progress.echo("Reading heap sizes ...")
val heap_sizes =
build_info.finished_sessions.flatMap { session_name =>
val heap = isabelle_output + Path.explode(session_name)
if (heap.is_file) {
Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
}
else None
}
build_out_progress.echo("Writing log file " + log_path.xz + " ...")
File.write_xz(log_path.xz,
terminate_lines(
Protocol.Meta_Info_Marker(meta_info) :: build_result.out_lines :::
session_build_info :::
ml_statistics.map(Protocol.ML_Statistics_Marker.apply) :::
session_errors.map(Protocol.Error_Message_Marker.apply) :::
heap_sizes), Compress.Options_XZ(6))
/* next build */
if (multicore_base && first_build && isabelle_output_log.is_dir) {
Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log)
}
Isabelle_System.rm_tree(isabelle_output)
first_build = false
(build_result, log_path.xz)
}
}
/* command line entry point */
private object Multicore {
private val Pat1 = """^(\d+)$""".r
private val Pat2 = """^(\d+)x(\d+)$""".r
def parse(s: String): (Int, Int) =
s match {
case Pat1(Value.Int(x)) => (x, 1)
case Pat2(Value.Int(x), Value.Int(y)) => (x, y)
case _ => error("Bad multicore configuration: " + quote(s))
}
}
def main(args: Array[String]): Unit = {
Command_Line.tool {
var afp = false
var multicore_base = false
var components_base: Path = Components.default_components_base
var heap: Option[Int] = None
var max_heap: Option[Int] = None
var multicore_list = List(default_multicore)
var isabelle_identifier = default_isabelle_identifier
var afp_partition = 0
var component_repository = Components.default_component_repository
var more_settings: List[String] = Nil
var more_preferences: List[String] = Nil
var fresh = false
var hostname = ""
var init_settings: List[String] = Nil
var arch_64 = false
var output_file = ""
var ml_statistics_step = 1
var build_tags = List.empty[String]
var user_home = default_user_home
var verbose = false
var exit_code = false
val getopts = Getopts("""
Usage: Admin/build_other [OPTIONS] ISABELLE_HOME [ARGS ...]
Options are:
-A include $ISABELLE_HOME/AFP directory
-B first multicore build serves as base for scheduling information
-C DIR base directory for Isabelle components (default: """ +
Components.default_components_base + """)
-H SIZE minimal ML heap in MB (default: """ + default_heap + """ for x86, """ +
default_heap * 2 + """ for x86_64)
-M MULTICORE multicore configurations (see below)
-N NAME alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
-P NUMBER AFP partition number (0, 1, 2, default: 0=unrestricted)
-R URL remote repository for Isabelle components (default: """ +
Components.default_component_repository + """)
-U SIZE maximal ML heap in MB (default: unbounded)
-e TEXT additional text for generated etc/settings
-f fresh build of Isabelle/Scala components (recommended)
-h NAME override local hostname
-i TEXT initial text for generated etc/settings
-m ARCH processor architecture (32=x86, 64=x86_64, default: x86)
-n no build: sync only
-o FILE output file for log names (default: stdout)
-p TEXT additional text for generated etc/preferences
-s NUMBER step size for ML statistics (0=none, 1=all, n=step, default: 1)
-t TAG free-form build tag (multiple occurrences possible)
-u DIR alternative USER_HOME directory
-v verbose
-x return overall exit code from build processes
Build Isabelle sessions from the history of another REPOSITORY clone,
passing ARGS directly to its isabelle build tool.
Each MULTICORE configuration consists of one or two numbers (default 1):
THREADS or THREADSxPROCESSES, e.g. -M 1,2,4 or -M 1x4,2x2,4.
""",
"A" -> (_ => afp = true),
"B" -> (_ => multicore_base = true),
"C:" -> (arg => components_base = Path.explode(arg)),
"H:" -> (arg => heap = Some(Value.Int.parse(arg))),
"M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)),
"N:" -> (arg => isabelle_identifier = arg),
"P:" -> (arg => afp_partition = Value.Int.parse(arg)),
"R:" -> (arg => component_repository = arg),
"U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
"e:" -> (arg => more_settings = more_settings ::: List(arg)),
"f" -> (_ => fresh = true),
"h:" -> (arg => hostname = arg),
"i:" -> (arg => init_settings = init_settings ::: List(arg)),
"m:" ->
{
case "32" | "x86" => arch_64 = false
case "64" | "x86_64" => arch_64 = true
case bad => error("Bad processor architecture: " + quote(bad))
},
"o:" -> (arg => output_file = arg),
"p:" -> (arg => more_preferences = more_preferences ::: List(arg)),
"s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)),
"t:" -> (arg => build_tags = build_tags ::: List(arg)),
"u:" -> (arg => user_home = Path.explode(arg)),
"v" -> (_ => verbose = true),
"x" -> (_ => exit_code = true))
val more_args = getopts(args)
val (root, build_args) =
more_args match {
case root :: build_args => (Path.explode(root), build_args)
case _ => getopts.usage()
}
val progress = new Console_Progress(stderr = true)
val results =
local_build(Options.init(), root, user_home = user_home, progress = progress,
afp = afp, afp_partition = afp_partition,
isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
component_repository = component_repository, components_base = components_base,
fresh = fresh, hostname = hostname, multicore_base = multicore_base,
multicore_list = multicore_list, arch_64 = arch_64,
heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
max_heap = max_heap, init_settings = init_settings, more_settings = more_settings,
more_preferences = more_preferences, verbose = verbose, build_tags = build_tags,
build_args = build_args)
if (output_file.isEmpty) {
for ((_, log_path) <- results) Output.writeln(log_path.implode, stdout = true)
}
else {
File.write(Path.explode(output_file),
cat_lines(for ((_, log_path) <- results) yield log_path.implode))
}
val rc = results.foldLeft(Process_Result.RC.ok) { case (rc, (res, _)) => rc max res.rc }
if (rc != Process_Result.RC.ok && exit_code) sys.exit(rc)
}
}
/** remote build -- via rsync and ssh **/
def remote_build(
ssh: SSH.Session,
isabelle_self: Path,
isabelle_other: Path,
isabelle_identifier: String = "remote_build_history",
progress: Progress = new Progress,
protect_args: Boolean = false,
rev: String = "",
afp_repos: Option[Path] = None,
afp_rev: String = "",
options: String = "",
args: String = "",
no_build: Boolean = false
): List[(String, Bytes)] = {
/* synchronize Isabelle + AFP repositories */
def sync(target: Path, accurate: Boolean = false,
rev: String = "", afp_rev: String = "", afp: Boolean = false
): Unit = {
val context =
Rsync.Context(progress, ssh_port = ssh.port, ssh_control_path = ssh.control_path,
protect_args = protect_args)
Sync.sync(ssh.options, context, ssh.rsync_path(target),
thorough = accurate, preserve_jars = !accurate,
rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None)
}
def execute(command: String, args: String,
echo: Boolean = false,
strict: Boolean = true
): Unit =
ssh.execute(
Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
ssh.bash_path(isabelle_self + Path.explode(command)) + " " + args,
progress_stdout = progress.echo_if(echo, _),
progress_stderr = progress.echo_if(echo, _),
strict = strict).check
sync(isabelle_self)
execute("bin/isabelle", "components -I")
execute("bin/isabelle", "components -a", echo = true)
execute("bin/isabelle", "jedit -bf")
sync(isabelle_other, accurate = true,
rev = proper_string(rev) getOrElse "tip",
afp_rev = proper_string(afp_rev) getOrElse "tip",
afp = true)
/* build */
if (no_build) Nil
else {
ssh.with_tmp_dir { tmp_dir =>
val output_file = tmp_dir + Path.explode("output")
val build_options = (if (afp_repos.isEmpty) "" else " -A") + " " + options
try {
execute("Admin/build_other",
"-o " + ssh.bash_path(output_file) + build_options + " " +
ssh.bash_path(isabelle_other) + " " + args,
echo = true, strict = false)
}
catch {
case ERROR(msg) =>
cat_error(msg, "The error(s) above occurred for Admin/build_other " + build_options)
}
for (line <- split_lines(ssh.read(output_file)))
yield {
val log = Path.explode(line)
val bytes = ssh.read_bytes(log)
ssh.rm(log)
(log.file_name, bytes)
}
}
}
}
}
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,968 +1,967 @@
/* 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: Boolean = false): Process_Result =
Isabelle_System.gnutar(args, dir = dir, strip = strip).check
private def bash_java_opens(args: String*): String =
Bash.strings(args.toList.flatMap(arg => List("--add-opens", arg + "=ALL-UNNAMED")))
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, suffix: String = "-build"): Other_Isabelle =
Other_Isabelle(dir + isabelle,
isabelle_identifier = dist_name + suffix,
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("build_release")(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 = true)
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.Directory(dir).components,
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.Directory(dir).read_components() } 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))
val component_dir = Components.Directory(dir)
component_dir.write_components(
component_dir.read_components().flatMap(line =>
line match {
case Bundled(name) =>
if (Components.Directory(Components.contrib(dir, name)).ok) 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,
progress: Progress = new Progress,
): Unit = {
val server_option = "build_host_" + platform.toString
val server = options.string(server_option)
progress.echo("Building heaps for " + commas_quote(build_sessions) +
" (" + server_option + " = " + quote(server) + ") ...")
val ssh =
if (server.nonEmpty) SSH.open_session(options, server)
else if (Platform.family == platform) SSH.Local
else error("Undefined option " + server_option + ": cannot build heaps")
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 build_command =
"bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions)
def system_apple(b: Boolean): String =
"""{ echo "ML_system_apple = """ + b + """" > "$(bin/isabelle getenv -b ISABELLE_HOME_USER)/etc/preferences"; }"""
val build_script =
List(
"cd " + File.bash_path(remote_dir),
"tar -xf tmp.tar",
"""mkdir -p "$(bin/isabelle getenv -b ISABELLE_HOME_USER)/etc" """,
system_apple(false),
build_command,
system_apple(true),
build_command,
"tar -cf tmp.tar heaps")
ssh.execute(build_script.mkString(" && "), settings = false).check
ssh.read_file(remote_tmp_tar, local_tmp_tar)
}
execute_tar(local_dir, "-xvf " + File.bash_path(local_tmp_tar))
.out_lines.sorted.foreach(progress.echo)
}
}
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.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
""")
}
/* NEWS */
private def make_news(other_isabelle: Other_Isabelle): Unit = {
val news_file = other_isabelle.isabelle_home + Path.explode("NEWS")
val doc_dir = other_isabelle.isabelle_home + Path.explode("doc")
val fonts_dir = Isabelle_System.make_directory(doc_dir + Path.explode("fonts"))
Isabelle_Fonts.make_entries(getenv = other_isabelle.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(news_file)))))
}
/* 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.self_repository()
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(File.standard_path(context.isabelle_dir), rev = id)
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.init_components(components_base = context.components_base))
other_isabelle.resolve_components(echo = true)
try {
other_isabelle.bash(
"export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n" +
"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) }
make_news(other_isabelle)
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))
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
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 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) {
build_heaps(options, platform, build_sessions, isabelle_target, progress = progress)
}
// application bundling
Components.purge(contrib_dir, platform)
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 + "\\"))
val java_opts =
bash_java_opens(
"java.base/java.io",
"java.base/java.lang",
"java.base/java.lang.reflect",
"java.base/java.text",
"java.base/java.util",
"java.desktop/java.awt.font")
val launch4j_jar =
Path.explode("windows_app/launch4j-" + Platform.family + "/launch4j.jar")
execute(tmp_dir,
cat_lines(List(
"export LAUNCH4J=" + File.bash_platform_path(launch4j_jar),
"isabelle java " + java_opts + " -jar \"$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)
}
other_isabelle.cleanup()
}
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, suffix = "")
Isabelle_System.make_directory(other_isabelle.etc)
File.write(other_isabelle.etc_settings, "ML_OPTIONS=\"--minheap 1000 --maxheap 4000\"\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: """ + quote(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,112 +1,115 @@
/* 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 =
+ 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)
+ }
}
final class Other_Isabelle private(
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 resolve_components(echo: Boolean): Unit = {
other_isabelle.bash(
"bin/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.bash("bin/isabelle getenv -b " + Bash.string(name)).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")
/* components */
def init_components(
component_repository: String = Components.default_component_repository,
components_base: Path = Components.default_components_base,
- catalogs: List[String] = Nil,
+ catalogs: List[String] = Components.default_catalogs,
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/General/ssh.scala b/src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala
+++ b/src/Pure/General/ssh.scala
@@ -1,362 +1,387 @@
/* Title: Pure/General/ssh.scala
Author: Makarius
SSH client on OpenSSH command-line tools, preferably with connection
multiplexing, but this does not work on Windows.
*/
package isabelle
import java.util.{Map => JMap}
import java.io.{File => JFile}
object SSH {
/* client command */
def client_command(port: Int = 0, control_path: String = ""): String =
if (control_path.isEmpty || control_path == Bash.string(control_path)) {
"ssh" +
(if (port > 0) " -p " + port else "") +
(if (control_path.nonEmpty) " -o ControlPath=" + control_path else "")
}
else error ("Malformed SSH control socket: " + quote(control_path))
/* OpenSSH configuration and command-line */
// see https://linux.die.net/man/5/ssh_config
object Config {
def entry(x: String, y: String): String = x + "=" + y
def entry(x: String, y: Int): String = entry(x, y.toString)
def entry(x: String, y: Long): String = entry(x, y.toString)
def entry(x: String, y: Boolean): String = entry(x, if (y) "yes" else "no")
def make(options: Options,
port: Int = 0,
user: String = "",
control_master: Boolean = false,
control_path: String = ""
): List[String] = {
val ssh_batch_mode = options.bool("ssh_batch_mode")
val ssh_compression = options.bool("ssh_compression")
val ssh_alive_interval = options.real("ssh_alive_interval").round
val ssh_alive_count_max = options.int("ssh_alive_count_max")
List(
entry("BatchMode", ssh_batch_mode),
entry("Compression", ssh_compression)) :::
(if (ssh_alive_interval >= 0) List(entry("ServerAliveInterval", ssh_alive_interval)) else Nil) :::
(if (ssh_alive_count_max >= 0) List(entry("ServerAliveCountMax", ssh_alive_count_max)) else Nil) :::
(if (port > 0) List(entry("Port", port)) else Nil) :::
(if (user.nonEmpty) List(entry("User", user)) else Nil) :::
(if (control_master) List("ControlMaster=yes", "ControlPersist=yes") else Nil) :::
(if (control_path.nonEmpty) List("ControlPath=" + control_path) else Nil)
}
def option(entry: String): String = "-o " + Bash.string(entry)
def option(x: String, y: String): String = option(entry(x, y))
def option(x: String, y: Int): String = option(entry(x, y))
def option(x: String, y: Long): String = option(entry(x, y))
def option(x: String, y: Boolean): String = option(entry(x, y))
def command(command: String, config: List[String]): String =
Bash.string(command) + config.map(entry => " " + option(entry)).mkString
}
def sftp_string(str: String): String = {
val special = "[]?*\\{} \"'"
if (str.isEmpty) "\"\""
else if (str.exists(special.contains)) {
val res = new StringBuilder
for (c <- str) {
if (special.contains(c)) res += '\\'
res += c
}
res.toString()
}
else str
}
/* open session */
def open_session(
options: Options,
host: String,
port: Int = 0,
user: String = ""
): Session = {
val multiplex = options.bool("ssh_multiplexing") && !Platform.is_windows
val (control_master, control_path) =
if (multiplex) (true, Isabelle_System.tmp_file("ssh", initialized = false).getPath)
else (false, "")
new Session(options, host, port, user, control_master, control_path)
}
class Session private[SSH](
val options: Options,
val host: String,
val port: Int,
val user: String,
control_master: Boolean,
val control_path: String
) extends System {
ssh =>
def port_suffix: String = if (port > 0) ":" + port else ""
def user_prefix: String = if (user.nonEmpty) user + "@" else ""
override def toString: String = user_prefix + host + port_suffix
override def hg_url: String = "ssh://" + toString + "/"
override def rsync_prefix: String = user_prefix + host + ":"
/* local ssh commands */
def run_command(command: String,
master: Boolean = false,
opts: String = "",
args: String = "",
cwd: JFile = null,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
strict: Boolean = true
): Process_Result = {
val config =
Config.make(options, port = port, user = user,
control_master = master, control_path = control_path)
val cmd =
Config.command(command, config) +
(if (opts.nonEmpty) " " + opts else "") +
(if (args.nonEmpty) " -- " + args else "")
Isabelle_System.bash(cmd, cwd = cwd, progress_stdout = progress_stdout,
progress_stderr = progress_stderr, strict = strict)
}
def run_sftp(
script: String,
init: Path => Unit = _ => (),
exit: Path => Unit = _ => ()
): Process_Result = {
Isabelle_System.with_tmp_dir("ssh") { dir =>
init(dir)
File.write(dir + Path.explode("script"), script)
val result =
run_command("sftp", opts = "-b script", args = Bash.string(host), cwd = dir.file).check
exit(dir)
result
}
}
def run_ssh(master: Boolean = false, opts: String = "", args: String = ""): Process_Result = {
val args1 = Bash.string(host) + (if (args.nonEmpty) " " + args else "")
run_command("ssh", master = master, opts = opts, args = args1)
}
/* init and exit */
val user_home: String = {
run_ssh(master = control_master, args = "printenv HOME \";\" printenv SHELL").check.out_lines
match {
case List(user_home, shell) =>
if (shell.endsWith("/bash")) user_home
else {
error("Bad SHELL for " + quote(toString) + " -- expected GNU bash, but found " + shell)
}
case _ => error("Malformed remote environment for " + quote(toString))
}
}
val settings: JMap[String, String] = JMap.of("HOME", user_home, "USER_HOME", user_home)
override def close(): Unit = {
if (control_path.nonEmpty) run_ssh(opts = "-O exit").check
}
/* remote commands */
override def execute(cmd_line: String,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
settings: Boolean = true,
strict: Boolean = true
): Process_Result = {
val args1 = Bash.string(host) + " " + Bash.string("export USER_HOME=\"$HOME\"\n" + cmd_line)
run_command("ssh", args = args1, progress_stdout = progress_stdout,
progress_stderr = progress_stderr, strict = strict)
}
+ override def download_file(
+ url_name: String,
+ file: Path,
+ progress: Progress = new Progress
+ ): Unit = {
+ val cmd_line =
+ File.read(Path.explode("~~/lib/scripts/download_file")) + "\n" +
+ "download_file " + Bash.string(url_name) + " " + bash_path(file)
+ execute(cmd_line,
+ progress_stdout = progress.echo,
+ progress_stderr = progress.echo).check
+ }
+
override lazy val isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(ssh))
/* remote file-system */
override def expand_path(path: Path): Path = path.expand_env(settings)
def remote_path(path: Path): String = expand_path(path).implode
override def bash_path(path: Path): String = Bash.string(remote_path(path))
def sftp_path(path: Path): String = sftp_string(remote_path(path))
def rm(path: Path): Unit = run_sftp("rm " + sftp_path(path))
override def is_dir(path: Path): Boolean = run_ssh(args = "test -d " + bash_path(path)).ok
override def is_file(path: Path): Boolean = run_ssh(args = "test -f " + bash_path(path)).ok
override def make_directory(path: Path): Path = {
if (!execute("mkdir -p " + bash_path(path)).ok) {
error("Failed to create directory: " + quote(remote_path(path)))
}
path
}
+ override def copy_file(src: Path, dst: Path): Unit = {
+ val direct = if (is_dir(dst)) "/." else ""
+ if (!execute("cp -a " + bash_path(src) + " " + bash_path(dst) + direct).ok) {
+ error("Failed to copy file " + expand_path(src) + " to " +
+ expand_path(dst) + " (ssh " + toString + ")")
+ }
+ }
+
def read_dir(path: Path): List[String] =
run_sftp("@cd " + sftp_path(path) + "\n@ls -1 -a").out_lines.flatMap(s =>
if (s == "." || s == "..") None
else Some(Library.perhaps_unprefix("./", s)))
private def get_file[A](path: Path, f: Path => A): A = {
var result: Option[A] = None
run_sftp("get -p " + sftp_path(path) + " local",
exit = dir => result = Some(f(dir + Path.explode("local"))))
result.get
}
private def put_file(path: Path, f: Path => Unit): Unit =
run_sftp("put -p local " + sftp_path(path),
init = dir => f(dir + Path.explode("local")))
override def read_file(path: Path, local_path: Path): Unit =
get_file(path, Isabelle_System.copy_file(_, local_path))
override def read_bytes(path: Path): Bytes =
get_file(path, Bytes.read)
override def read(path: Path): String =
get_file(path, File.read)
override def write_file(path: Path, local_path: Path): Unit =
put_file(path, Isabelle_System.copy_file(local_path, _))
def write_bytes(path: Path, bytes: Bytes): Unit =
put_file(path, Bytes.write(_, bytes))
def write(path: Path, text: String): Unit =
put_file(path, File.write(_, text))
/* tmp dirs */
def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir))
def rm_tree(remote_dir: String): Unit =
execute("rm -r -f " + Bash.string(remote_dir)).check
def tmp_dir(): String =
execute("mktemp -d /tmp/ssh-XXXXXXXXXXXX").check.out
override def with_tmp_dir[A](body: Path => A): A = {
val remote_dir = tmp_dir()
try { body(Path.explode(remote_dir)) }
finally { rm_tree(remote_dir) }
}
/* port forwarding */
def port_forwarding(
remote_port: Int,
remote_host: String = "localhost",
local_port: Int = 0,
local_host: String = "localhost",
ssh_close: Boolean = false
): Port_Forwarding = {
val port = if (local_port > 0) local_port else Isabelle_System.local_port()
val forward = List(local_host, port, remote_host, remote_port).mkString(":")
val forward_option = "-L " + Bash.string(forward)
val cancel: () => Unit =
if (control_path.nonEmpty) {
run_ssh(opts = forward_option + " -O forward").check
() => run_ssh(opts = forward_option + " -O cancel") // permissive
}
else {
val result = Synchronized[Exn.Result[Boolean]](Exn.Res(false))
val thread = Isabelle_Thread.fork("port_forwarding") {
val opts =
forward_option +
" " + Config.option("SessionType", "none") +
" " + Config.option("PermitLocalCommand", true) +
" " + Config.option("LocalCommand", "pwd")
try {
run_command("ssh", opts = opts, args = Bash.string(host),
progress_stdout = _ => result.change(_ => Exn.Res(true))).check
}
catch { case exn: Throwable => result.change(_ => Exn.Exn(exn)) }
}
result.guarded_access {
case res@Exn.Res(ok) => if (ok) Some((), res) else None
case Exn.Exn(exn) => throw exn
}
() => thread.interrupt()
}
val shutdown_hook =
Isabelle_System.create_shutdown_hook { cancel() }
new Port_Forwarding(host, port, remote_host, remote_port) {
override def toString: String = forward
override def close(): Unit = {
cancel()
Isabelle_System.remove_shutdown_hook(shutdown_hook)
if (ssh_close) ssh.close()
}
}
}
}
abstract class Port_Forwarding private[SSH](
val host: String,
val port: Int,
val remote_host: String,
val remote_port: Int
) extends AutoCloseable
/* system operations */
trait System extends AutoCloseable {
def close(): Unit = ()
def hg_url: String = ""
def rsync_prefix: String = ""
def rsync_path(path: Path): String = rsync_prefix + expand_path(path).implode
def expand_path(path: Path): Path = path.expand
def bash_path(path: Path): String = File.bash_path(path)
def is_dir(path: Path): Boolean = path.is_dir
def is_file(path: Path): Boolean = path.is_file
def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
+ def copy_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1)
def read_bytes(path: Path): Bytes = Bytes.read(path)
def read(path: Path): String = File.read(path)
def execute(command: String,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
settings: Boolean = true,
strict: Boolean = true): Process_Result =
Isabelle_System.bash(command,
progress_stdout = progress_stdout,
progress_stderr = progress_stderr,
env = if (settings) Isabelle_System.settings() else null,
strict = strict)
+ def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
+ Isabelle_System.download_file(url_name, file, progress = progress)
+
def isabelle_platform: Isabelle_Platform = Isabelle_Platform()
}
object Local extends System
}
diff --git a/src/Pure/System/components.scala b/src/Pure/System/components.scala
--- a/src/Pure/System/components.scala
+++ b/src/Pure/System/components.scala
@@ -1,373 +1,388 @@
/* Title: Pure/System/components.scala
Author: Makarius
Isabelle system components.
*/
package isabelle
import java.io.{File => JFile}
object Components {
/* archive name */
object Archive {
val suffix: String = ".tar.gz"
def apply(name: String): String =
if (name == "") error("Bad component name: " + quote(name))
else name + suffix
def unapply(archive: String): Option[String] = {
for {
name0 <- Library.try_unsuffix(suffix, archive)
name <- proper_string(name0)
} yield name
}
def get_name(archive: String): String =
unapply(archive) getOrElse
error("Bad component archive name (expecting .tar.gz): " + quote(archive))
}
/* component collections */
def default_component_repository: String =
Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY")
val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
+ val default_catalogs: List[String] = List("main")
+ val optional_catalogs: List[String] = List("main", "optional")
+
def admin(dir: Path): Path = dir + Path.explode("Admin/components")
def contrib(dir: Path = Path.current, name: String = ""): Path =
dir + Path.explode("contrib") + Path.explode(name)
- def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = {
+ def unpack(
+ dir: Path,
+ archive: Path,
+ ssh: SSH.System = SSH.Local,
+ progress: Progress = new Progress
+ ): String = {
val name = Archive.get_name(archive.file_name)
progress.echo("Unpacking " + name)
- Isabelle_System.extract(archive, dir)
+ ssh.execute(
+ "tar -C " + File.bash_path(dir) + " -x -z -f " + File.bash_path(archive),
+ progress_stdout = progress.echo,
+ progress_stderr = progress.echo).check
name
}
- def resolve(base_dir: Path, names: List[String],
+ def resolve(
+ base_dir: Path,
+ names: List[String],
target_dir: Option[Path] = None,
copy_dir: Option[Path] = None,
+ component_repository: String = Components.default_component_repository,
+ ssh: SSH.System = SSH.Local,
progress: Progress = new Progress
): Unit = {
- Isabelle_System.make_directory(base_dir)
+ ssh.make_directory(base_dir)
for (name <- names) {
val archive_name = Archive(name)
val archive = base_dir + Path.explode(archive_name)
- if (!archive.is_file) {
- val remote = Components.default_component_repository + "/" + archive_name
- Isabelle_System.download_file(remote, archive, progress = progress)
+ if (!ssh.is_file(archive)) {
+ val remote = Url.append_path(component_repository, archive_name)
+ ssh.download_file(remote, archive, progress = progress)
}
for (dir <- copy_dir) {
- Isabelle_System.make_directory(dir)
- Isabelle_System.copy_file(archive, dir)
+ ssh.make_directory(dir)
+ ssh.copy_file(archive, dir)
}
- unpack(target_dir getOrElse base_dir, archive, progress = progress)
+ unpack(target_dir getOrElse base_dir, archive, ssh = ssh, progress = progress)
}
}
private val platforms_family: Map[Platform.Family.Value, Set[String]] =
Map(
Platform.Family.linux_arm -> Set("arm64-linux", "arm64_32-linux"),
Platform.Family.linux -> Set("x86_64-linux", "x86_64_32-linux"),
Platform.Family.macos ->
Set("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"),
Platform.Family.windows ->
Set("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows"))
private val platforms_all: Set[String] =
Set("x86-linux", "x86-cygwin") ++ platforms_family.iterator.flatMap(_._2)
def purge(dir: Path, platform: Platform.Family.Value): Unit = {
val purge_set = platforms_all -- platforms_family(platform)
File.find_files(dir.file,
(file: JFile) => file.isDirectory && purge_set(file.getName),
include_dirs = true).foreach(Isabelle_System.rm_tree)
}
/* component directories */
def directories(): List[Path] =
Path.split(Isabelle_System.getenv_strict("ISABELLE_COMPONENTS"))
/* component directory content */
object Directory {
def apply(path: Path): Directory = new Directory(path.absolute)
}
class Directory private(val path: Path) {
override def toString: String = path.toString
def etc: Path = path + Path.basic("etc")
def src: Path = path + Path.basic("src")
def lib: Path = path + Path.basic("lib")
def settings: Path = etc + Path.basic("settings")
def components: Path = etc + Path.basic("components")
def build_props: Path = etc + Path.basic("build.props")
def README: Path = path + Path.basic("README")
def LICENSE: Path = path + Path.basic("LICENSE")
def create(progress: Progress = new Progress): Directory = {
progress.echo("Creating component directory " + path)
Isabelle_System.new_directory(path)
Isabelle_System.make_directory(etc)
this
}
def ok: Boolean = settings.is_file || components.is_file || Sessions.is_session_dir(path)
def check: Directory =
if (!path.is_dir) error("Bad component directory: " + path)
else if (!ok) {
error("Malformed component directory: " + path +
"\n (missing \"etc/settings\" or \"etc/components\" or \"ROOT\" or \"ROOTS\")")
}
else this
def read_components(): List[String] =
split_lines(File.read(components)).filter(_.nonEmpty)
def write_components(lines: List[String]): Unit =
File.write(components, terminate_lines(lines))
def write_settings(text: String): Unit =
File.write(settings, "# -*- shell-script -*- :mode=shellscript:\n" + text)
}
/* component repository content */
val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1")
sealed case class SHA1_Digest(digest: SHA1.Digest, name: String) {
override def toString: String = digest.shasum(name)
}
def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] =
(proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line =>
Word.explode(line) match {
case Nil => None
case List(sha1, name) => Some(SHA1_Digest(SHA1.fake_digest(sha1), name))
case _ => error("Bad components.sha1 entry: " + quote(line))
})
def write_components_sha1(entries: List[SHA1_Digest]): Unit =
File.write(components_sha1, entries.sortBy(_.name).mkString("", "\n", "\n"))
/** manage user components **/
val components_path: Path = Path.explode("$ISABELLE_HOME_USER/etc/components")
def read_components(): List[String] =
if (components_path.is_file) Library.trim_split_lines(File.read(components_path))
else Nil
def write_components(lines: List[String]): Unit = {
Isabelle_System.make_directory(components_path.dir)
File.write(components_path, Library.terminate_lines(lines))
}
def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = {
val path = path0.expand.absolute
if (add) Directory(path).check
val lines1 = read_components()
val lines2 =
lines1.filter(line =>
line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path))
val lines3 = if (add) lines2 ::: List(path.implode) else lines2
if (lines1 != lines3) write_components(lines3)
val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed"
progress.echo(prefix + " component " + path)
}
/* main entry point */
def main(args: Array[String]): Unit = {
Command_Line.tool {
for (arg <- args) {
val add =
if (arg.startsWith("+")) true
else if (arg.startsWith("-")) false
else error("Bad argument: " + quote(arg))
val path = Path.explode(arg.substring(1))
update_components(add, path, progress = new Console_Progress)
}
}
}
/** build and publish components **/
def build_components(
options: Options,
components: List[Path],
progress: Progress = new Progress,
publish: Boolean = false,
force: Boolean = false,
update_components_sha1: Boolean = false
): Unit = {
val archives: List[Path] =
for (path <- components) yield {
path.file_name match {
case Archive(_) => path
case name =>
Directory(path).check
val component_path = path.expand
val archive_dir = component_path.dir
val archive_name = Archive(name)
val archive = archive_dir + Path.explode(archive_name)
if (archive.is_file && !force) {
error("Component archive already exists: " + archive)
}
progress.echo("Packaging " + archive_name)
Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name),
dir = archive_dir).check
archive
}
}
if ((publish && archives.nonEmpty) || update_components_sha1) {
val server = options.string("isabelle_components_server")
if (server.isEmpty) error("Undefined option isabelle_components_server")
using(SSH.open_session(options, server)) { ssh =>
val components_dir = Path.explode(options.string("isabelle_components_dir"))
val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir"))
for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) {
error("Bad remote directory: " + dir)
}
if (publish) {
for (archive <- archives) {
val archive_name = archive.file_name
val name = Archive.get_name(archive_name)
val remote_component = components_dir + archive.base
val remote_contrib = contrib_dir + Path.explode(name)
// component archive
if (ssh.is_file(remote_component) && !force) {
error("Remote component archive already exists: " + remote_component)
}
progress.echo("Uploading " + archive_name)
ssh.write_file(remote_component, archive)
// contrib directory
val is_standard_component =
Isabelle_System.with_tmp_dir("component") { tmp_dir =>
Isabelle_System.extract(archive, tmp_dir)
Directory(tmp_dir + Path.explode(name)).ok
}
if (is_standard_component) {
if (ssh.is_dir(remote_contrib)) {
if (force) ssh.rm_tree(remote_contrib)
else error("Remote component directory already exists: " + remote_contrib)
}
progress.echo("Unpacking remote " + archive_name)
ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " +
ssh.bash_path(remote_component)).check
}
else {
progress.echo_warning("No unpacking of non-standard component: " + archive_name)
}
}
}
// remote SHA1 digests
if (update_components_sha1) {
val lines =
for {
entry <- ssh.read_dir(components_dir)
if ssh.is_file(components_dir + Path.basic(entry)) &&
entry.endsWith(Archive.suffix)
}
yield {
progress.echo("Digesting remote " + entry)
ssh.execute("cd " + ssh.bash_path(components_dir) +
"; sha1sum " + Bash.string(entry)).check.out
}
write_components_sha1(read_components_sha1(lines))
}
}
}
// local SHA1 digests
{
val new_entries =
for (archive <- archives)
yield {
val name = archive.file_name
progress.echo("Digesting local " + name)
SHA1_Digest(SHA1.digest(archive), name)
}
val new_names = new_entries.map(_.name).toSet
write_components_sha1(
new_entries :::
read_components_sha1().filterNot(entry => new_names.contains(entry.name)))
}
}
/* Isabelle tool wrapper */
private val relevant_options =
List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir")
val isabelle_tool =
Isabelle_Tool("build_components", "build and publish Isabelle components",
Scala_Project.here,
{ args =>
var publish = false
var update_components_sha1 = false
var force = false
var options = Options.init()
def show_options: String =
cat_lines(relevant_options.flatMap(options.get).map(_.print))
val getopts = Getopts("""
Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS...
Options are:
-P publish on SSH server (see options below)
-f force: overwrite existing component archives and directories
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-u update all SHA1 keys in Isabelle repository Admin/components
Build and publish Isabelle components as .tar.gz archives on SSH server,
depending on system options:
""" + Library.indent_lines(2, show_options) + "\n",
"P" -> (_ => publish = true),
"f" -> (_ => force = true),
"o:" -> (arg => options = options + arg),
"u" -> (_ => update_components_sha1 = true))
val more_args = getopts(args)
if (more_args.isEmpty && !update_components_sha1) getopts.usage()
val progress = new Console_Progress
build_components(options, more_args.map(Path.explode), progress = progress,
publish = publish, force = force, update_components_sha1 = update_components_sha1)
})
}
diff --git a/src/Pure/Tools/build_docker.scala b/src/Pure/Tools/build_docker.scala
--- a/src/Pure/Tools/build_docker.scala
+++ b/src/Pure/Tools/build_docker.scala
@@ -1,177 +1,177 @@
/* Title: Pure/Tools/build_docker.scala
Author: Makarius
Build docker image from Isabelle application bundle for Linux.
*/
package isabelle
object Build_Docker {
private val default_base = "ubuntu:22.04"
private val default_work_dir = Path.current
private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_linux(?:_arm)?\.tar\.gz$""".r
val packages: List[String] =
List("curl", "less", "libfontconfig1", "libgomp1", "openssh-client", "pwgen", "rsync")
val package_collections: Map[String, List[String]] =
Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"),
"latex" ->
List(
"texlive-bibtex-extra",
"texlive-fonts-extra",
"texlive-font-utils",
"texlive-latex-extra",
"texlive-science"))
def all_packages: List[String] =
packages ::: package_collections.valuesIterator.flatten.toList
def build_docker(progress: Progress,
app_archive: String,
base: String = default_base,
work_dir: Path = default_work_dir,
logic: String = default_logic,
no_build: Boolean = false,
entrypoint: Boolean = false,
output: Option[Path] = None,
more_packages: List[String] = Nil,
tag: String = "",
verbose: Boolean = false
): Unit = {
val isabelle_name =
app_archive match {
case Isabelle_Name(name) => name
case _ => error("Cannot determine Isabelle distribution name from " + app_archive)
}
val is_remote = Url.is_wellformed(app_archive)
val dockerfile =
"""## Dockerfile for """ + isabelle_name + """
FROM """ + base + """
SHELL ["/bin/bash", "-c"]
# packages
ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get -y update && \
apt-get install -y """ + Bash.strings(packages ::: more_packages) + """ && \
apt-get clean
# user
RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd)
USER isabelle
# Isabelle
WORKDIR /home/isabelle
""" + (if (is_remote)
- "RUN curl --fail --silent " + Bash.string(app_archive) + " > Isabelle.tar.gz"
+ "RUN curl --fail --silent --location " + Bash.string(app_archive) + " > Isabelle.tar.gz"
else "COPY Isabelle.tar.gz .") + """
RUN tar xzf Isabelle.tar.gz && \
mv """ + isabelle_name + """ Isabelle && \
sed -i -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$USER_HOME/.isabelle",g;' Isabelle/etc/settings && \
sed -i -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \
Isabelle/bin/isabelle build -o system_heaps -b """ + logic + """ && \
rm Isabelle.tar.gz""" + (if (entrypoint) """
ENTRYPOINT ["Isabelle/bin/isabelle"]
""" else "")
for (path <- output) {
progress.echo("Dockerfile: " + path.absolute)
File.write(path, dockerfile)
}
if (!no_build) {
Isabelle_System.make_directory(work_dir)
progress.echo("Docker working directory: " + work_dir.absolute)
Isabelle_System.with_tmp_dir("docker_build", base_dir = work_dir.file) { tmp_dir =>
progress.echo("Docker temporary directory: " + tmp_dir.absolute)
File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile)
if (is_remote) {
if (!Url.is_readable(app_archive))
error("Cannot access remote archive " + app_archive)
}
else {
Isabelle_System.copy_file(Path.explode(app_archive),
tmp_dir + Path.explode("Isabelle.tar.gz"))
}
val quiet_option = if (verbose) "" else " -q"
val tag_option = if (tag == "") "" else " -t " + Bash.string(tag)
progress.bash("docker build" + quiet_option + tag_option + " " + File.bash_path(tmp_dir),
echo = true).check
}
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_docker", "build Isabelle docker image",
Scala_Project.here,
{ args =>
var base = default_base
var entrypoint = false
var work_dir = default_work_dir
var logic = default_logic
var no_build = false
var output: Option[Path] = None
var more_packages: List[String] = Nil
var verbose = false
var tag = ""
val getopts = Getopts("""
Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE
Options are:
-B NAME base image (default """ + quote(default_base) + """)
-E set Isabelle/bin/isabelle as entrypoint
-P NAME additional Ubuntu package collection (""" +
package_collections.keySet.toList.sorted.map(quote(_)).mkString(", ") + """)
-W DIR working directory that is accessible to docker,
potentially via snap (default: """ + default_work_dir + """)
-l NAME default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
-n no docker build
-o FILE output generated Dockerfile
-p NAME additional Ubuntu package
-t TAG docker build tag
-v verbose
Build Isabelle docker image with default logic image, using a standard
Isabelle application archive for Linux (local file or remote URL).
""",
"B:" -> (arg => base = arg),
"E" -> (_ => entrypoint = true),
"P:" -> (arg =>
package_collections.get(arg) match {
case Some(ps) => more_packages :::= ps
case None => error("Unknown package collection " + quote(arg))
}),
"W:" -> (arg => work_dir = Path.explode(arg)),
"l:" -> (arg => logic = arg),
"n" -> (_ => no_build = true),
"o:" -> (arg => output = Some(Path.explode(arg))),
"p:" -> (arg => more_packages ::= arg),
"t:" -> (arg => tag = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
val app_archive =
more_args match {
case List(arg) => arg
case _ => getopts.usage()
}
build_docker(new Console_Progress(), app_archive, base = base, work_dir = work_dir,
logic = logic, no_build = no_build, entrypoint = entrypoint, output = output,
more_packages = more_packages, tag = tag, verbose = verbose)
})
}