--- a/Admin/Release/CHECKLIST Sat Nov 27 14:45:00 2021 +0100
+++ b/Admin/Release/CHECKLIST Sat Nov 27 22:20:27 2021 +0100
@@ -73,7 +73,7 @@
- fully-automated packaging (e.g. on lxcisa0):
- hg up -r DISTNAME && Admin/build_release -J .../java11 -D /p/home/isabelle/dist -b HOL -l -R DISTNAME
+ hg up -r DISTNAME && Admin/build_release -D /p/home/isabelle/dist -b HOL -l -R DISTNAME
- Docker image:
--- a/src/Pure/Admin/build_release.scala Sat Nov 27 14:45:00 2021 +0100
+++ b/src/Pure/Admin/build_release.scala Sat Nov 27 22:20:27 2021 +0100
@@ -17,6 +17,9 @@
private def execute_tar(dir: Path, args: String, strip: Int = 0): Unit =
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(
@@ -490,7 +493,6 @@
context: Release_Context,
afp_rev: String = "",
platform_families: List[Platform.Family.Value] = default_platform_families,
- java_home: Path = default_java_home,
more_components: List[Path] = Nil,
website: Option[Path] = None,
build_sessions: List[String] = Nil,
@@ -703,9 +705,21 @@
" <cp>%EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "</cp>")))
.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,
- "env JAVA_HOME=" + File.bash_platform_path(java_home) +
- " \"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
+ 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"))
@@ -823,6 +837,9 @@
val other_isabelle = context.other_isabelle(tmp_dir)
+ 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
@@ -841,15 +858,12 @@
/** command line entry point **/
- def default_java_home: Path = Path.explode("$JAVA_HOME").expand
-
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 java_home = default_java_home
var release_name = ""
var source_archive = ""
var website: Option[Path] = None
@@ -869,7 +883,6 @@
-C DIR base directory for Isabelle components (default: """ +
Components.default_components_base + """)
-D DIR target directory (default ".")
- -J JAVA_HOME Java version for running launch4j (e.g. version 11)
-R RELEASE explicit release name
-S ARCHIVE use existing source archive (file or URL)
-W WEBSITE produce minimal website in given directory
@@ -886,7 +899,6 @@
"A:" -> (arg => afp_rev = arg),
"C:" -> (arg => components_base = Path.explode(arg)),
"D:" -> (arg => target_dir = Path.explode(arg)),
- "J:" -> (arg => java_home = Path.explode(arg)),
"R:" -> (arg => release_name = arg),
"S:" -> (arg => source_archive = arg),
"W:" -> (arg => website = Some(Path.explode(arg))),
@@ -933,7 +945,7 @@
}
build_release(options, context, afp_rev = afp_rev, platform_families = platform_families,
- java_home = java_home, more_components = more_components, build_sessions = build_sessions,
+ more_components = more_components, build_sessions = build_sessions,
build_library = build_library, parallel_jobs = parallel_jobs, website = website)
}
}
--- a/src/Pure/Admin/build_status.scala Sat Nov 27 14:45:00 2021 +0100
+++ b/src/Pure/Admin/build_status.scala Sat Nov 27 22:20:27 2021 +0100
@@ -204,7 +204,7 @@
profiles: List[Profile] = default_profiles,
only_sessions: Set[String] = Set.empty,
ml_statistics: Boolean = false,
- ml_statistics_domain: String => Boolean = (key: String) => true,
+ ml_statistics_domain: String => Boolean = _ => true,
verbose: Boolean = false): Data =
{
val date = Date.now()
@@ -377,7 +377,7 @@
List(HTML.description(
List(HTML.text("status date:") -> HTML.text(data.date.toString))))),
HTML.par(
- List(HTML.itemize(data.entries.map({ case data_entry =>
+ List(HTML.itemize(data.entries.map(data_entry =>
List(
HTML.link(clean_name(data_entry.name) + "/index.html",
HTML.text(data_entry.name))) :::
@@ -388,7 +388,7 @@
List(HTML.span(HTML.error_message, HTML.text("Failed sessions:"))) :::
List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
})
- }))))))
+ ))))))
for (data_entry <- data.entries) {
val data_name = data_entry.name
@@ -423,10 +423,10 @@
entry.ml_timing.elapsed.minutes.toString,
entry.ml_timing.resources.minutes.toString,
entry.maximum_code.toString,
- entry.maximum_code.toString,
+ entry.average_code.toString,
+ entry.maximum_stack.toString,
entry.average_stack.toString,
- entry.maximum_stack.toString,
- entry.average_heap.toString,
+ entry.maximum_heap.toString,
entry.average_heap.toString,
entry.stored_heap.toString).mkString(" "))))
@@ -608,7 +608,7 @@
"l:" -> (arg => options = options + ("build_log_history=" + arg)),
"o:" -> (arg => options = options + arg),
"s:" -> (arg =>
- space_explode('x', arg).map(Value.Int.parse(_)) match {
+ space_explode('x', arg).map(Value.Int.parse) match {
case List(w, h) if w > 0 && h > 0 => image_size = (w, h)
case _ => error("Error bad PNG image size: " + quote(arg))
}),
--- a/src/Pure/Admin/isabelle_cronjob.scala Sat Nov 27 14:45:00 2021 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sat Nov 27 22:20:27 2021 +0100
@@ -314,7 +314,7 @@
{
List(
List(Remote_Build("Linux A", "augsburg1",
- options = "-m32 -B -M1x2,2,4" +
+ options = "-m32 -B -M4" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_MLTON=mlton" +
--- a/src/Pure/Admin/isabelle_devel.scala Sat Nov 27 14:45:00 2021 +0100
+++ b/src/Pure/Admin/isabelle_devel.scala Sat Nov 27 22:20:27 2021 +0100
@@ -44,7 +44,6 @@
val context = Build_Release.Release_Context(target_dir)
Build_Release.build_release_archive(context, rev)
Build_Release.build_release(options, context, afp_rev = afp_rev,
- java_home = Path.explode("$BUILD_JAVA_HOME"),
build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")),
website = Some(website_dir))
})
--- a/src/Pure/ML/ml_statistics.scala Sat Nov 27 14:45:00 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala Sat Nov 27 22:20:27 2021 +0100
@@ -194,7 +194,7 @@
val empty: ML_Statistics = apply(Nil)
def apply(ml_statistics0: List[Properties.T], heading: String = "",
- domain: String => Boolean = (key: String) => true): ML_Statistics =
+ domain: String => Boolean = _ => true): ML_Statistics =
{
require(ml_statistics0.forall(props => Now.unapply(props).isDefined), "missing \"now\" field")
@@ -260,6 +260,11 @@
val time_start: Double,
val duration: Double)
{
+ override def toString: String =
+ if (content.isEmpty) "ML_Statistics.empty"
+ else "ML_Statistics(length = " + content.length + ", fields = " + fields.size + ")"
+
+
/* content */
def maximum(field: String): Double =
@@ -286,7 +291,7 @@
def update_data(data: XYSeriesCollection, selected_fields: List[String]): Unit =
{
- data.removeAllSeries
+ data.removeAllSeries()
for (field <- selected_fields) {
val series = new XYSeries(field)
content.foreach(entry => series.add(entry.time, entry.get(field)))