diff --git a/etc/settings b/etc/settings
--- a/etc/settings
+++ b/etc/settings
@@ -1,169 +1,170 @@
# -*- shell-script -*- :mode=shellscript:
#
# Isabelle system settings.
#
# Important notes:
# * See the "system" manual for explanations on Isabelle settings
# * User settings go into $ISABELLE_HOME_USER/etc/settings
# * DO NOT EDIT the repository copy of this file!
# * DO NOT COPY this file into the $ISABELLE_HOME_USER directory!
###
### Isabelle/Scala
###
ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.8 -Xmax-classfile-name 130 -J-Xms128m -J-Xmx1024m -J-Xss2m"
ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0 -Djdk.gtk.version=2.2 --illegal-access=warn"
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss16m"
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
isabelle_scala_tools 'isabelle.Regular_Tools'
[ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_tools 'isabelle.Admin_Tools'
isabelle_file_format 'isabelle.Bibtex$File_Format'
#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
###
### Interactive sessions (cf. isabelle console)
###
ISABELLE_LINE_EDITOR="rlwrap"
###
### Batch sessions (cf. isabelle build)
###
ISABELLE_BUILD_OPTIONS=""
###
### Document preparation (cf. isabelle latex/document)
###
ISABELLE_LATEX="latex -file-line-error"
ISABELLE_PDFLATEX="pdflatex -file-line-error"
ISABELLE_BIBTEX="bibtex"
ISABELLE_MAKEINDEX="makeindex"
ISABELLE_EPSTOPDF="epstopdf"
if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then
ISABELLE_LATEX="latex -c-style-errors"
ISABELLE_PDFLATEX="pdflatex -c-style-errors"
fi
###
### Misc path settings
###
ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components"
+ISABELLE_COMPONENTS_BASE="$USER_HOME/.isabelle/contrib"
# The place for user configuration, heap files, etc.
if [ -z "$ISABELLE_IDENTIFIER" ]; then
ISABELLE_HOME_USER="$USER_HOME/.isabelle"
else
ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER"
fi
# Where to look for isabelle tools (multiple dirs separated by ':').
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
# Location for temporary files (should be on a local file system).
ISABELLE_TMP_PREFIX="${TMPDIR:-/tmp}/isabelle-$USER"
# Heap locations.
ISABELLE_HEAPS="$ISABELLE_HOME_USER/heaps"
ISABELLE_HEAPS_SYSTEM="$ISABELLE_HOME/heaps"
# HTML browser info.
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
ISABELLE_BROWSER_INFO_SYSTEM="$ISABELLE_HOME/browser_info"
# Site settings check -- just to make it a little bit harder to copy this file verbatim!
[ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
{ echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; }
ISABELLE_SITE_SETTINGS_PRESENT=true
###
### Default logic
###
ISABELLE_LOGIC=HOL
###
### Docs
###
# Where to look for docs (multiple dirs separated by ':').
ISABELLE_DOCS="$ISABELLE_HOME/doc"
ISABELLE_DOCS_RELEASE_NOTES="~~/ANNOUNCE:~~/README:~~/NEWS:~~/COPYRIGHT:~~/CONTRIBUTORS:~~/contrib/README:~~/src/Tools/jEdit/README:~~/README_REPOSITORY"
ISABELLE_DOCS_EXAMPLES="~~/src/HOL/ex/Seq.thy:~~/src/HOL/ex/ML.thy:~~/src/HOL/Unix/Unix.thy:~~/src/HOL/Isar_Examples/Drinker.thy:~~/src/Tools/SML/Examples.thy:~~/src/Pure/ROOT.ML"
# "open" within desktop environment (potentially asynchronous)
case "$ISABELLE_PLATFORM_FAMILY" in
linux)
ISABELLE_OPEN="xdg-open"
;;
macos)
ISABELLE_OPEN="open"
;;
windows)
ISABELLE_OPEN="cygstart"
;;
esac
PDF_VIEWER="$ISABELLE_OPEN"
DVI_VIEWER="$ISABELLE_OPEN"
###
### Symbol rendering
###
ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
###
### OCaml
###
ISABELLE_OPAM_ROOT="$ISABELLE_HOME_USER/opam"
ISABELLE_OCAML_VERSION="4.05.0"
###
### Haskell
###
ISABELLE_STACK_ROOT="$ISABELLE_HOME_USER/stack"
ISABELLE_STACK_RESOLVER="lts-12.13"
ISABELLE_GHC_VERSION="ghc-8.4.3"
###
### Misc settings
###
ISABELLE_GNUPLOT="gnuplot"
ISABELLE_FONTFORGE="fontforge"
#ISABELLE_MLTON="/usr/bin/mlton"
#ISABELLE_SMLNJ="/usr/bin/sml"
#ISABELLE_SWIPL="/usr/bin/swipl"
diff --git a/lib/Tools/components b/lib/Tools/components
--- a/lib/Tools/components
+++ b/lib/Tools/components
@@ -1,146 +1,146 @@
#!/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
echo " Resolve Isabelle components via download and installation."
echo " COMPONENTS are identified via base name."
echo
echo " ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\""
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=""
while getopts "IR:al" OPT
do
case "$OPT" in
I)
INIT_SETTINGS="true"
;;
R)
COMPONENT_REPOSITORY="$OPTARG"
;;
a)
ALL_MISSING="true"
;;
l)
LIST_ONLY="true"
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
# args
[ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && 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 "$USER_HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"'
+ SETTINGS_CONTENT='init_components "$ISABELLE_COMPONENTS_BASE" "$ISABELLE_HOME/Admin/components/main"'
if [ -e "$SETTINGS" ]; then
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
else
echo "Initializing \"$SETTINGS\""
mkdir -p "$(dirname "$SETTINGS")"
echo "$SETTINGS_CONTENT" > "$SETTINGS"
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
else
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 --fail --silent "$REMOTE" > "${FULL_NAME}.tar.gz.part" || \
fail "Failed to download \"$REMOTE\""
if perl -e "exit((stat('${FULL_NAME}.tar.gz.part'))[7] == 0 ? 0 : 1);"
then
rm -f "${FULL_NAME}.tar.gz.part"
else
mv "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz"
fi
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
fi
fi
done
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,592 +1,594 @@
/* Title: Pure/Admin/build_history.scala
Author: Makarius
Build other history versions.
*/
package isabelle
import java.io.{File => JFile}
import java.time.format.DateTimeFormatter
import java.util.Locale
object Build_History
{
/* log files */
val engine = "build_history"
val log_prefix = engine + "_"
val META_INFO_MARKER = "\fmeta_info = "
/* 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 windows_32 = "x86-windows"
val windows_64 = "x86_64-windows"
val platform_32 = other_isabelle.getenv("ISABELLE_PLATFORM32")
val platform_64 = other_isabelle.getenv("ISABELLE_PLATFORM64")
val platform_family = other_isabelle.getenv("ISABELLE_PLATFORM_FAMILY")
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_32)) windows_32
else platform_32 // x86-cygwin
}
else {
val (platform, platform_name) =
if (arch_64) (platform_64, "x86_64-" + platform_family)
else (platform_32, "x86-" + platform_family)
if (check_dir(platform)) platform else err(platform_name)
}
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
}
/** build_history **/
private val default_user_home = Path.explode("$USER_HOME")
private val default_rev = "tip"
private val default_multicore = (1, 1)
private val default_heap = 1500
private val default_isabelle_identifier = "build_history"
def build_history(
options: Options,
root: Path,
user_home: Path = default_user_home,
progress: Progress = No_Progress,
rev: String = default_rev,
afp_rev: Option[String] = None,
afp_partition: Int = 0,
isabelle_identifier: String = default_isabelle_identifier,
ml_statistics_step: Int = 1,
- components_base: Option[Path] = None,
+ 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,
verbose: Boolean = false,
build_tags: List[String] = Nil,
build_args: List[String] = Nil): List[(Process_Result, Path)] =
{
/* sanity checks */
if (File.eq(Path.explode("~~"), root))
error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").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 build_history within existing Isabelle settings environment")
}
/* checkout Isabelle + AFP repository */
def checkout(dir: Path, version: String): String =
{
val hg = Mercurial.repository(dir)
hg.update(rev = version, clean = true)
progress.echo_if(verbose, hg.log(version, options = "-l1"))
hg.id(rev = version)
}
val isabelle_version = checkout(root, rev)
val afp_repos = root + Path.explode("AFP")
val afp_version = afp_rev.map(checkout(afp_repos, _))
val (afp_build_args, afp_sessions) =
if (afp_rev.isEmpty) (Nil, Nil)
else {
val afp = AFP.init(options, afp_repos)
(List("-d", "~~/AFP/thys"), afp.partition(afp_partition))
}
/* 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(base = components_base, catalogs = List("main", "optional"))
+ other_isabelle.init_components(
+ components_base = components_base, catalogs = List("main", "optional"))
other_isabelle.init_settings(component_settings ::: init_settings)
other_isabelle.resolve_components(verbose)
val ml_platform =
augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
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(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\" " +
"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(tool, echo = verbose)
Isabelle_System.rm_tree(isabelle_base_log)
}
Isabelle_System.rm_tree(isabelle_output)
Isabelle_System.mkdirs(isabelle_output)
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.mkdirs(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_result =
Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
user_home = user_home, progress = build_out_progress)(
"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_version) :::
afp_version.map(Build_Log.Prop.afp_version.name -> _).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 =>
Build_Log.Log_File.print_props(Build_Log.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.ext("xz") + " ...")
File.write_xz(log_path.ext("xz"),
terminate_lines(
Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: build_result.out_lines :::
session_build_info :::
ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
session_errors.map(Build_Log.Log_File.print_props(Build_Log.ERROR_MESSAGE_MARKER, _)) :::
heap_sizes), XZ.options(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.ext("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])
{
Command_Line.tool0 {
var afp_rev: Option[String] = None
var multicore_base = false
- var components_base: Option[Path] = None
+ 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 more_settings: List[String] = Nil
var fresh = false
var hostname = ""
var init_settings: List[String] = Nil
var arch_64 = false
var output_file = ""
var rev = default_rev
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_history [OPTIONS] REPOSITORY [ARGS ...]
Options are:
-A REV include $ISABELLE_HOME/AFP repository at given revision
-B first multicore build serves as base for scheduling information
- -C DIR base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
+ -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)
-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)
-o FILE output file for log names (default: stdout)
-r REV update to revision (default: """ + default_rev + """)
-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:" -> (arg => afp_rev = Some(arg)),
"B" -> (_ => multicore_base = true),
- "C:" -> (arg => components_base = Some(Path.explode(arg))),
+ "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)),
"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),
"r:" -> (arg => rev = 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 =
build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev,
afp_rev = afp_rev, afp_partition = afp_partition,
isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
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,
verbose = verbose, build_tags = build_tags, build_args = build_args)
if (output_file == "") {
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 = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
if (rc != 0 && exit_code) sys.exit(rc)
}
}
/** remote build_history -- via command-line **/
def remote_build_history(
ssh: SSH.Session,
isabelle_repos_self: Path,
isabelle_repos_other: Path,
isabelle_repos_source: String = Isabelle_Cronjob.isabelle_repos_source,
afp_repos_source: String = AFP.repos_source,
isabelle_identifier: String = "remote_build_history",
self_update: Boolean = false,
progress: Progress = No_Progress,
rev: String = "",
afp_rev: Option[String] = None,
options: String = "",
args: String = ""): List[(String, Bytes)] =
{
/* Isabelle self repository */
val self_hg =
Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = ssh)
def execute(cmd: String, args: String, echo: Boolean = false, strict: Boolean = true): Unit =
ssh.execute(
Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
ssh.bash_path(isabelle_repos_self + Path.explode(cmd)) + " " + args,
progress_stdout = progress.echo_if(echo, _),
progress_stderr = progress.echo_if(echo, _),
strict = strict).check
if (self_update) {
val hg = Mercurial.repository(Path.explode("~~"))
hg.push(self_hg.root_url, force = true)
self_hg.update(rev = hg.parent(), clean = true)
execute("bin/isabelle", "components -I")
execute("bin/isabelle", "components -a", echo = true)
execute("Admin/build", "jars_fresh")
}
val rev_id = self_hg.id(rev)
/* Isabelle other + AFP repository */
if (Mercurial.is_repository(isabelle_repos_other, ssh = ssh)) {
ssh.rm_tree(isabelle_repos_other)
}
val other_hg =
Mercurial.clone_repository(
ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev_id, ssh = ssh)
val afp_options =
if (afp_rev.isEmpty) ""
else {
val afp_repos = isabelle_repos_other + Path.explode("AFP")
val afp_hg = Mercurial.setup_repository(afp_repos_source, afp_repos, ssh = ssh)
" -A " + Bash.string(afp_rev.get)
}
/* Admin/build_history */
ssh.with_tmp_dir(tmp_dir =>
{
val output_file = tmp_dir + Path.explode("output")
execute("Admin/build_history",
"-o " + ssh.bash_path(output_file) +
(if (rev == "") "" else " -r " + Bash.string(rev_id)) + " " +
options + afp_options + " " + ssh.bash_path(isabelle_repos_other) + " " + args,
echo = true, strict = false)
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,776 +1,777 @@
/* Title: Pure/Admin/build_release.scala
Author: Makarius
Build full Isabelle distribution from repository.
*/
package isabelle
object Build_Release
{
/** release info **/
sealed case class Bundle_Info(
platform: Platform.Family.Value,
platform_description: String,
name: String)
{
def path: Path = Path.explode(name)
}
class Release private[Build_Release](
progress: Progress,
val date: Date,
val dist_name: String,
val dist_dir: Path,
val dist_version: String,
val ident: String)
{
val isabelle_dir: Path = dist_dir + Path.explode(dist_name)
val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".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 + Path.explode(dist_name),
isabelle_identifier = dist_name + "-build",
progress = progress)
def bundle_info(platform: Platform.Family.Value): Bundle_Info =
platform match {
case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
case Platform.Family.macos => Bundle_Info(platform, "Mac OS X", dist_name + "_macos.tar.gz")
case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
}
}
/** generated content **/
/* patch release */
private def change_file(dir: Path, name: String, f: String => String)
{
val file = dir + Path.explode(name)
File.write(file, f(File.read(file)))
}
private val getsettings_file: String = "lib/scripts/getsettings"
private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r
def patch_release(release: Release, is_official: Boolean)
{
val dir = release.isabelle_dir
for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala"))
{
change_file(dir, name,
s =>
s.replaceAllLiterally("val is_identified = false", "val is_identified = true")
.replaceAllLiterally("val is_official = false", "val is_official = " + is_official))
}
change_file(dir, getsettings_file,
s =>
s.replaceAllLiterally("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident))
.replaceAllLiterally("ISABELLE_IDENTIFIER=\"\"",
"ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
change_file(dir, "lib/html/library_index_header.template",
s => s.replaceAllLiterally("{ISABELLE}", release.dist_name))
for {
name <-
List(
"src/Pure/System/distribution.ML",
"src/Pure/System/distribution.scala",
"lib/Tools/version") }
{
change_file(dir, name,
s => s.replaceAllLiterally("repository version", release.dist_version))
}
change_file(dir, "README",
s => s.replaceAllLiterally("some repository version of Isabelle", release.dist_version))
}
/* ANNOUNCE */
def make_announce(release: Release)
{
File.write(release.isabelle_dir + Path.explode("ANNOUNCE"),
"""
IMPORTANT NOTE
==============
This is a snapshot of Isabelle/""" + release.ident + """ from the repository.
""")
}
/* NEWS */
def make_news(other_isabelle: Other_Isabelle, dist_version: String)
{
val target = other_isabelle.isabelle_home + Path.explode("doc")
val target_fonts = target + Path.explode("fonts")
Isabelle_System.mkdirs(target_fonts)
other_isabelle.copy_fonts(target_fonts)
HTML.write_document(target, "NEWS.html",
List(HTML.title("NEWS (" + dist_version + ")")),
List(
HTML.chapter("NEWS"),
HTML.source(
Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS"))))))
}
/* 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)
{
val catalogs =
List("main", "bundled").map((_, new Bundled())) :::
default_platform_families.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
val path = Components.admin(dir) + Path.basic(catalog)
if path.is_file
line <- split_lines(File.read(path))
if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build")
} 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)
if !name.startsWith("jedit_build")
} 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])
{
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(_)))
}
def make_contrib(dir: Path)
{
Isabelle_System.mkdirs(Components.contrib(dir))
File.write(Components.contrib(dir, "README"),
"""This directory contains add-on components that contribute to the main
Isabelle distribution. Separate licensing conditions apply, see each
directory individually.
""")
}
/** build_release **/
private def execute(dir: Path, script: String): Unit =
Isabelle_System.bash(script, cwd = dir.file).check
private def execute_tar(dir: Path, args: String): Unit =
Isabelle_System.gnutar(args, dir = dir).check
private val default_platform_families: List[Platform.Family.Value] =
List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos)
def build_release(base_dir: Path,
options: Options,
- components_base: Option[Path] = None,
+ components_base: Path = Components.default_components_base,
progress: Progress = No_Progress,
rev: String = "",
afp_rev: String = "",
official_release: Boolean = false,
proper_release_name: Option[String] = None,
platform_families: List[Platform.Family.Value] = default_platform_families,
more_components: List[Path] = Nil,
website: Option[Path] = None,
build_library: Boolean = false,
parallel_jobs: Int = 1): Release =
{
val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME"))
val release =
{
val date = Date.now()
val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date))
val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute
val version = proper_string(rev) orElse proper_release_name getOrElse "tip"
val ident =
try { hg.id(version) }
catch { case ERROR(_) => error("Bad repository version: " + version) }
val dist_version =
proper_release_name match {
case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date)
case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date)
}
new Release(progress, date, dist_name, dist_dir, dist_version, ident)
}
/* make distribution */
if (release.isabelle_archive.is_file) {
progress.echo_warning("Release archive already exists: " + release.isabelle_archive)
val archive_ident =
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
val getsettings = Path.explode(release.dist_name + "/" + getsettings_file)
execute_tar(tmp_dir, "-xzf " +
File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings))
split_lines(File.read(tmp_dir + getsettings))
.collectFirst({ case ISABELLE_ID(ident) => ident })
.getOrElse(error("Failed to read ISABELLE_ID from " + release.isabelle_archive))
})
if (release.ident != archive_ident) {
error("Mismatch of release identification " + release.ident +
" vs. archive " + archive_ident)
}
}
else {
progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...")
Isabelle_System.mkdirs(release.dist_dir)
if (release.isabelle_dir.is_dir)
error("Directory " + release.isabelle_dir + " already exists")
progress.echo_warning("Retrieving Mercurial repository version " + release.ident)
hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files")
for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
(release.isabelle_dir + Path.explode(name)).file.delete
}
progress.echo_warning("Preparing distribution " + quote(release.dist_name))
patch_release(release, proper_release_name.isDefined && official_release)
if (proper_release_name.isEmpty) make_announce(release)
make_contrib(release.isabelle_dir)
execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
record_bundled_components(release.isabelle_dir)
/* build tools and documentation */
val other_isabelle = release.other_isabelle(release.dist_dir)
other_isabelle.init_settings(
- other_isabelle.init_components(base = components_base, catalogs = List("main")))
+ other_isabelle.init_components(components_base = 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(_) => error("Failed to build tools") }
try {
other_isabelle.bash(
"./bin/isabelle build_doc -a -s -j " + parallel_jobs, echo = true).check
}
catch { case ERROR(_) => error("Failed to build documentation") }
make_news(other_isabelle, release.dist_version)
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 distribution archive " + release.isabelle_archive)
def execute_dist_name(script: String): Unit =
Isabelle_System.bash(script, cwd = release.dist_dir.file,
env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check
execute_dist_name("""
set -e
chmod -R a+r "$DIST_NAME"
chmod -R u+w "$DIST_NAME"
chmod -R g=o "$DIST_NAME"
find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w
""")
execute_tar(release.dist_dir, "-czf " +
File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name))
execute_dist_name("""
set -e
mv "$DIST_NAME" "${DIST_NAME}-old"
mkdir "$DIST_NAME"
mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \
"${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME"
mkdir "$DIST_NAME/doc"
mv "${DIST_NAME}-old/doc/"*.pdf \
"${DIST_NAME}-old/doc/"*.html \
"${DIST_NAME}-old/doc/"*.css \
"${DIST_NAME}-old/doc/fonts" \
"${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc"
rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle
rm -rf "${DIST_NAME}-old"
""")
}
/* make application bundles */
val bundle_infos = platform_families.map(release.bundle_info)
for (bundle_info <- bundle_infos) {
val bundle_archive = release.dist_dir + bundle_info.path
if (bundle_archive.is_file && more_components.isEmpty)
progress.echo_warning("Application bundle already exists: " + bundle_archive)
else {
val isabelle_name = release.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(release.isabelle_archive))
val other_isabelle = release.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(other_isabelle.components_base(components_base),
- bundled_components, target_dir = Some(contrib_dir), progress = progress)
+ Components.resolve(components_base, bundled_components,
+ target_dir = Some(contrib_dir), 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_title = "# Java runtime options"
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 opt) ::: List("-Disabelle.jedit_server=" + isabelle_name)
val classpath: List[Path] =
{
val base = isabelle_target.absolute
Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).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)
}
}) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
}
val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
// application bundling
platform match {
case Platform.Family.linux =>
File.write(isabelle_target + Path.explode(isabelle_name + ".options"),
terminate_lines(java_options_title :: java_options))
val isabelle_run = isabelle_target + Path.explode(isabelle_name + ".run")
File.write(isabelle_run,
File.read(Path.explode("~~/Admin/Linux/Isabelle.run"))
.replaceAllLiterally("{CLASSPATH}",
classpath.map("$ISABELLE_HOME/" + _).mkString(":"))
.replaceAllLiterally("/jdk/", "/" + jdk_component + "/"))
File.executable(isabelle_run)
val linux_app = isabelle_target + Path.explode("contrib/linux_app")
File.move(linux_app + Path.explode("Isabelle"),
isabelle_target + Path.explode(isabelle_name))
Isabelle_System.rm_tree(linux_app)
val archive_name = isabelle_name + "_linux.tar.gz"
progress.echo("Packaging " + archive_name + " ...")
execute_tar(tmp_dir,
"-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
Bash.string(isabelle_name))
case Platform.Family.macos =>
File.write(isabelle_target + jedit_props,
File.read(isabelle_target + jedit_props)
.replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
.replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
.replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar="))
// MacOS application bundle
File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
val isabelle_app = Path.explode(isabelle_name + ".app")
val app_dir = tmp_dir + isabelle_app
File.move(tmp_dir + Path.explode("macos_app/Isabelle.app"), app_dir)
val app_contents = app_dir + Path.explode("Contents")
val app_resources = app_contents + Path.explode("Resources")
File.move(tmp_dir + Path.explode(isabelle_name), app_resources)
File.write(app_contents + Path.explode("Info.plist"),
File.read(Path.explode("~~/Admin/MacOS/Info.plist"))
.replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
.replaceAllLiterally("{JAVA_OPTIONS}",
terminate_lines(java_options.map(opt => "" + opt + ""))))
for (cp <- classpath) {
File.link(
Path.explode("../Resources/" + isabelle_name + "/") + cp,
app_contents + Path.explode("Java"),
force = true)
}
File.link(
Path.explode("../Resources/" + isabelle_name + "/contrib/" +
jdk_component + "/x86_64-darwin"),
app_contents + Path.explode("PlugIns/bundled.jdk"),
force = true)
File.link(
Path.explode("../../Info.plist"),
app_resources + Path.explode(isabelle_name + "/" + isabelle_name + ".plist"),
force = true)
File.link(
Path.explode("Contents/Resources/" + isabelle_name),
app_dir + Path.explode("Isabelle"),
force = true)
// application archive
val archive_name = isabelle_name + "_macos.tar.gz"
progress.echo("Packaging " + archive_name + " ...")
execute_tar(tmp_dir,
"-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
File.bash_path(isabelle_app))
case Platform.Family.windows =>
File.write(isabelle_target + jedit_props,
File.read(isabelle_target + jedit_props)
.replaceAll("lookAndFeel=.*",
"lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
.replaceAll("foldPainter=.*", "foldPainter=Square"))
// application launcher
File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
val app_template = Path.explode("~~/Admin/Windows/launch4j")
File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
(java_options_title :: java_options).map(_ + "\r\n").mkString)
val isabelle_xml = Path.explode("isabelle.xml")
val isabelle_exe = Path.explode(isabelle_name + ".exe")
File.write(tmp_dir + isabelle_xml,
File.read(app_template + isabelle_xml)
.replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
.replaceAllLiterally("{OUTFILE}",
File.platform_path(isabelle_target + isabelle_exe))
.replaceAllLiterally("{ICON}",
File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
.replaceAllLiterally("{SPLASH}",
File.platform_path(app_template + Path.explode("isabelle.bmp")))
.replaceAllLiterally("{CLASSPATH}",
cat_lines(classpath.map(cp =>
" %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "")))
.replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\"))
execute(tmp_dir,
"\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
File.copy(app_template + Path.explode("manifest.xml"),
isabelle_target + isabelle_exe.ext("manifest"))
// Cygwin setup
val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
File.copy(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)
.replaceAllLiterally("{MIRROR}", cygwin_mirror))
File.executable(isabelle_target + cygwin_bat)
for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
val path = Path.explode(name)
File.copy(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 exe_archive = tmp_dir + Path.explode(isabelle_name + ".7z")
exe_archive.file.delete
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")).
replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
Bytes.write(release.dist_dir + isabelle_exe,
Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
File.executable(release.dist_dir + isabelle_exe)
}
})
progress.echo("DONE")
}
}
/* minimal website */
for (dir <- website) {
val website_platform_bundles =
for {
bundle_info <- bundle_infos
if (release.dist_dir + bundle_info.path).is_file
} yield (bundle_info.name, bundle_info)
val afp_link =
HTML.link(AFP.repos_source + "/commits/" + afp_rev, HTML.text("AFP/" + afp_rev))
HTML.write_document(dir, "index.html",
List(HTML.title(release.dist_name)),
List(
HTML.chapter(release.dist_name + " (" + release.ident + ")"),
HTML.itemize(
website_platform_bundles.map({ case (bundle, bundle_info) =>
List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) :::
(if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link)))))
for ((bundle, _) <- website_platform_bundles)
File.copy(release.dist_dir + Path.explode(bundle), dir)
}
/* HTML library */
if (build_library) {
if (release.isabelle_library_archive.is_file) {
progress.echo_warning("Library archive already exists: " + release.isabelle_library_archive)
}
else {
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
val bundle =
release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz")
execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
val other_isabelle = release.other_isabelle(tmp_dir)
Isabelle_System.mkdirs(other_isabelle.etc)
File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
other_isabelle.bash("bin/isabelle build -j " + parallel_jobs +
" -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
" -s -c -a -d '~~/src/Benchmarks'", echo = true).check
other_isabelle.isabelle_home_user.file.delete
execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name))
execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name))
execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) +
" " + Bash.string(release.dist_name + "/browser_info"))
})
}
}
release
}
/** command line entry point **/
def main(args: Array[String])
{
Command_Line.tool0 {
var afp_rev = ""
- var components_base: Option[Path] = None
+ var components_base: Path = Components.default_components_base
var official_release = false
var proper_release_name: Option[String] = None
var website: Option[Path] = None
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] BASE_DIR
Options are:
-A REV corresponding AFP changeset id
- -C DIR base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
+ -C DIR base directory for Isabelle components (default: """ +
+ Components.default_components_base + """)
-O official release (not release-candidate)
-R RELEASE proper release with name
-W WEBSITE produce minimal website in given directory
-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: RELEASE or tip)
Build Isabelle release in base directory, using the local repository clone.
""",
"A:" -> (arg => afp_rev = arg),
- "C:" -> (arg => components_base = Some(Path.explode(arg))),
+ "C:" -> (arg => components_base = Path.explode(arg)),
"O" -> (_ => official_release = true),
"R:" -> (arg => proper_release_name = Some(arg)),
"W:" -> (arg => website = Some(Path.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)
val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() }
val progress = new Console_Progress()
if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
error("Building for windows requires 7z")
build_release(Path.explode(base_dir), options, components_base = components_base,
progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release,
proper_release_name = proper_release_name, website = website,
platform_families =
if (platform_families.isEmpty) default_platform_families
else platform_families,
more_components = more_components, build_library = build_library,
parallel_jobs = parallel_jobs)
}
}
}
diff --git a/src/Pure/Admin/components.scala b/src/Pure/Admin/components.scala
--- a/src/Pure/Admin/components.scala
+++ b/src/Pure/Admin/components.scala
@@ -1,293 +1,295 @@
/* Title: Pure/Admin/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 */
+ val default_components_base = Path.explode("$ISABELLE_COMPONENTS_BASE")
+
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 = No_Progress): String =
{
val name = Archive.get_name(archive.file_name)
progress.echo("Unpacking " + name)
Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check
name
}
def resolve(base_dir: Path, names: List[String],
target_dir: Option[Path] = None,
progress: Progress = No_Progress)
{
Isabelle_System.mkdirs(base_dir)
for (name <- names) {
val archive_name = Archive(name)
val archive = base_dir + Path.explode(archive_name)
if (!archive.is_file) {
val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive_name
progress.echo("Getting " + remote)
Bytes.write(archive, Url.read_bytes(Url(remote)))
}
unpack(target_dir getOrElse base_dir, archive, progress = progress)
}
}
def purge(dir: Path, platform: Platform.Family.Value)
{
def purge_platforms(platforms: String*): Set[String] =
platforms.flatMap(name => List("x86-" + name, "x86_64-" + name)).toSet + "ppc-darwin"
val purge_set =
platform match {
case Platform.Family.linux => purge_platforms("darwin", "cygwin", "windows")
case Platform.Family.macos => purge_platforms("linux", "cygwin", "windows")
case Platform.Family.windows => purge_platforms("linux", "darwin")
}
File.find_files(dir.file,
(file: JFile) => file.isDirectory && purge_set(file.getName),
include_dirs = true).foreach(Isabelle_System.rm_tree)
}
/* component directory content */
def settings(dir: Path = Path.current): Path = dir + Path.explode("etc/settings")
def components(dir: Path = Path.current): Path = dir + Path.explode("etc/components")
def check_dir(dir: Path): Boolean =
settings(dir).is_file || components(dir).is_file
def read_components(dir: Path): List[String] =
split_lines(File.read(components(dir))).filter(_.nonEmpty)
def write_components(dir: Path, lines: List[String]): Unit =
File.write(components(dir), terminate_lines(lines))
/* component repository content */
val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1")
sealed case class SHA1_Digest(sha1: String, file_name: String)
{
override def toString: String = sha1 + " " + file_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, name))
case _ => error("Bad components.sha1 entry: " + quote(line))
})
def write_components_sha1(entries: List[SHA1_Digest]) =
File.write(components_sha1, entries.sortBy(_.file_name).mkString("", "\n", "\n"))
/** build and publish components **/
def build_components(
options: Options,
components: List[Path],
progress: Progress = No_Progress,
publish: Boolean = false,
force: Boolean = false,
update_components_sha1: Boolean = false)
{
val archives: List[Path] =
for (path <- components) yield {
path.file_name match {
case Archive(_) => path
case name =>
if (!path.is_dir) error("Bad component directory: " + path)
else if (!check_dir(path)) {
error("Malformed component directory: " + path +
"\n (requires " + settings() + " or " + Components.components() + ")")
}
else {
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) {
options.string("isabelle_components_server") match {
case SSH.Target(user, host) =>
using(SSH.open_session(options, host = host, user = user))(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.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
check_dir(tmp_dir + Path.explode(name))
})
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 entry.is_file && entry.name.endsWith(Archive.suffix)
}
yield {
progress.echo("Digesting remote " + entry.name)
Library.trim_line(
ssh.execute("cd " + ssh.bash_path(components_dir) +
"; sha1sum " + Bash.string(entry.name)).check.out)
}
write_components_sha1(read_components_sha1(lines))
}
})
case s => error("Bad isabelle_components_server: " + quote(s))
}
}
// local SHA1 digests
{
val new_entries =
for (archive <- archives)
yield {
val file_name = archive.file_name
progress.echo("Digesting local " + file_name)
val sha1 = SHA1.digest(archive).rep
SHA1_Digest(sha1, file_name)
}
val new_names = new_entries.map(_.file_name).toSet
write_components_sha1(
new_entries :::
read_components_sha1().filterNot(entry => new_names.contains(entry.file_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", args =>
{
var publish = false
var update_components_sha1 = false
var force = false
var options = Options.init()
def show_options: String =
cat_lines(relevant_options.map(name => options.options(name).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.prefix_lines(" ", 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/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,118 +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.explode("$USER_HOME"),
progress: Progress = No_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("components -a", redirect = true, echo = echo).check
def getenv(name: String): String =
other_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")
def copy_fonts(target_dir: Path): Unit =
Isabelle_Fonts.make_entries(getenv = getenv(_), hidden = true).
foreach(entry => File.copy(entry.path, target_dir))
/* components */
- def components_base(base: Option[Path]): Path =
- base getOrElse Components.contrib(isabelle_home_user.dir)
-
def init_components(
- base: Option[Path] = None,
+ components_base: Path = Components.default_components_base,
catalogs: List[String] = Nil,
components: List[String] = Nil): List[String] =
{
- val base_dir = components_base(base)
val dir = Components.admin(isabelle_home)
catalogs.map(name =>
- "init_components " + File.bash_path(base_dir) + " " + File.bash_path(dir + Path.basic(name))) :::
+ "init_components " + File.bash_path(components_base) + " " +
+ File.bash_path(dir + Path.basic(name))) :::
components.map(name =>
- "init_component " + File.bash_path(base_dir + Path.basic(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])
{
if (!clean_settings())
error("Cannot proceed with existing user settings file: " + etc_settings)
Isabelle_System.mkdirs(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()
{
clean_settings()
etc.file.delete
isabelle_home_user.file.delete
}
}