# HG changeset patch # User desharna # Date 1638048027 -3600 # Node ID a8927420a48bc93edd9303bc247cdc4078deef5f # Parent b5031a8f77180dc99232b40438db84c1de7df984# Parent 25e9e7088561ba5a9b1f0e7063229c6afba2f675 merged diff -r b5031a8f7718 -r a8927420a48b Admin/Release/CHECKLIST --- 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: diff -r b5031a8f7718 -r a8927420a48b src/Pure/Admin/build_release.scala --- 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 @@ " %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, - "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) } } diff -r b5031a8f7718 -r a8927420a48b src/Pure/Admin/build_status.scala --- 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)) }), diff -r b5031a8f7718 -r a8927420a48b src/Pure/Admin/isabelle_cronjob.scala --- 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" + diff -r b5031a8f7718 -r a8927420a48b src/Pure/Admin/isabelle_devel.scala --- 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)) }) diff -r b5031a8f7718 -r a8927420a48b src/Pure/ML/ml_statistics.scala --- 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)))