diff --git a/etc/build.props b/etc/build.props --- a/etc/build.props +++ b/etc/build.props @@ -1,350 +1,353 @@ title = Isabelle/Scala module = $ISABELLE_HOME/lib/classes/isabelle.jar main = isabelle.jedit.JEdit_Main resources = \ lib/services/java.nio.charset.spi.CharsetProvider:META-INF/services/ \ lib/logo/isabelle_transparent-32.gif:isabelle/ \ lib/logo/isabelle_transparent.gif:isabelle/ sources = \ src/HOL/SPARK/Tools/spark.scala \ src/HOL/Tools/ATP/system_on_tptp.scala \ src/HOL/Tools/Mirabelle/mirabelle.scala \ src/HOL/Tools/Nitpick/kodkod.scala \ src/Pure/Admin/afp.scala \ src/Pure/Admin/build_doc.scala \ src/Pure/Admin/build_history.scala \ src/Pure/Admin/build_log.scala \ src/Pure/Admin/build_release.scala \ src/Pure/Admin/build_status.scala \ src/Pure/Admin/check_sources.scala \ src/Pure/Admin/ci_build.scala \ src/Pure/Admin/component_bash_process.scala \ src/Pure/Admin/component_csdp.scala \ src/Pure/Admin/component_cvc5.scala \ src/Pure/Admin/component_cygwin.scala \ src/Pure/Admin/component_e.scala \ src/Pure/Admin/component_easychair.scala \ src/Pure/Admin/component_eptcs.scala \ src/Pure/Admin/component_foiltex.scala \ src/Pure/Admin/component_fonts.scala \ src/Pure/Admin/component_hugo.scala \ src/Pure/Admin/component_javamail.scala \ src/Pure/Admin/component_jdk.scala \ src/Pure/Admin/component_jedit.scala \ src/Pure/Admin/component_jsoup.scala \ src/Pure/Admin/component_lipics.scala \ src/Pure/Admin/component_llncs.scala \ src/Pure/Admin/component_minisat.scala \ src/Pure/Admin/component_mlton.scala \ src/Pure/Admin/component_pdfjs.scala \ src/Pure/Admin/component_polyml.scala \ src/Pure/Admin/component_postgresql.scala \ src/Pure/Admin/component_prismjs.scala \ src/Pure/Admin/component_rsync.scala \ src/Pure/Admin/component_scala.scala \ src/Pure/Admin/component_spass.scala \ src/Pure/Admin/component_sqlite.scala \ src/Pure/Admin/component_stack.scala \ src/Pure/Admin/component_windows_app.scala \ src/Pure/Admin/component_vampire.scala \ src/Pure/Admin/component_verit.scala \ src/Pure/Admin/component_zipperposition.scala \ src/Pure/Admin/component_zstd.scala \ src/Pure/Admin/isabelle_cronjob.scala \ src/Pure/Build/browser_info.scala \ src/Pure/Build/build.scala \ src/Pure/Build/build_benchmark.scala \ src/Pure/Build/build_cluster.scala \ src/Pure/Build/build_job.scala \ src/Pure/Build/build_process.scala \ src/Pure/Build/build_schedule.scala \ src/Pure/Build/database_progress.scala \ src/Pure/Build/export.scala \ src/Pure/Build/export_theory.scala \ src/Pure/Build/file_format.scala \ src/Pure/Build/resources.scala \ src/Pure/Build/sessions.scala \ src/Pure/Build/store.scala \ src/Pure/Concurrent/consumer_thread.scala \ src/Pure/Concurrent/counter.scala \ src/Pure/Concurrent/delay.scala \ src/Pure/Concurrent/event_timer.scala \ src/Pure/Concurrent/future.scala \ src/Pure/Concurrent/isabelle_thread.scala \ src/Pure/Concurrent/mailbox.scala \ src/Pure/Concurrent/multithreading.scala \ src/Pure/Concurrent/par_list.scala \ src/Pure/Concurrent/synchronized.scala \ src/Pure/GUI/color_value.scala \ src/Pure/GUI/desktop_app.scala \ src/Pure/GUI/gui.scala \ src/Pure/GUI/gui_thread.scala \ src/Pure/GUI/popup.scala \ src/Pure/GUI/wrap_panel.scala \ src/Pure/General/antiquote.scala \ src/Pure/General/base64.scala \ src/Pure/General/bibtex.scala \ src/Pure/General/bytes.scala \ src/Pure/General/cache.scala \ src/Pure/General/codepoint.scala \ src/Pure/General/comment.scala \ src/Pure/General/completion.scala \ src/Pure/General/compress.scala \ src/Pure/General/csv.scala \ src/Pure/General/date.scala \ src/Pure/General/exn.scala \ src/Pure/General/file.scala \ src/Pure/General/file_watcher.scala \ src/Pure/General/graph.scala \ src/Pure/General/graph_display.scala \ src/Pure/General/graphics_file.scala \ src/Pure/General/html.scala \ src/Pure/General/http.scala \ src/Pure/General/js.scala \ src/Pure/General/json.scala \ src/Pure/General/json_api.scala \ src/Pure/General/latex.scala \ src/Pure/General/linear_set.scala \ src/Pure/General/logger.scala \ src/Pure/General/long_name.scala \ src/Pure/General/mail.scala \ src/Pure/General/mailman.scala \ src/Pure/General/mercurial.scala \ src/Pure/General/multi_map.scala \ src/Pure/General/output.scala \ src/Pure/General/path.scala \ src/Pure/General/position.scala \ src/Pure/General/pretty.scala \ src/Pure/General/properties.scala \ src/Pure/General/rdf.scala \ src/Pure/General/rsync.scala \ src/Pure/General/scan.scala \ src/Pure/General/sha1.scala \ src/Pure/General/space.scala \ src/Pure/General/sql.scala \ src/Pure/General/ssh.scala \ src/Pure/General/symbol.scala \ src/Pure/General/time.scala \ src/Pure/General/timing.scala \ src/Pure/General/toml.scala \ src/Pure/General/untyped.scala \ src/Pure/General/url.scala \ src/Pure/General/utf8.scala \ src/Pure/General/uuid.scala \ src/Pure/General/value.scala \ src/Pure/General/word.scala \ src/Pure/General/zstd.scala \ src/Pure/Isar/document_structure.scala \ src/Pure/Isar/keyword.scala \ src/Pure/Isar/line_structure.scala \ src/Pure/Isar/outer_syntax.scala \ src/Pure/Isar/parse.scala \ src/Pure/Isar/token.scala \ src/Pure/ML/ml_console.scala \ src/Pure/ML/ml_heap.scala \ src/Pure/ML/ml_lex.scala \ src/Pure/ML/ml_process.scala \ src/Pure/ML/ml_profiling.scala \ src/Pure/ML/ml_statistics.scala \ src/Pure/ML/ml_syntax.scala \ src/Pure/PIDE/byte_message.scala \ src/Pure/PIDE/command.scala \ src/Pure/PIDE/command_span.scala \ src/Pure/PIDE/document.scala \ src/Pure/PIDE/document_editor.scala \ src/Pure/PIDE/document_id.scala \ src/Pure/PIDE/document_info.scala \ src/Pure/PIDE/document_status.scala \ src/Pure/PIDE/editor.scala \ src/Pure/PIDE/headless.scala \ src/Pure/PIDE/line.scala \ src/Pure/PIDE/markup.scala \ src/Pure/PIDE/markup_tree.scala \ src/Pure/PIDE/protocol.scala \ src/Pure/PIDE/protocol_handlers.scala \ src/Pure/PIDE/protocol_message.scala \ src/Pure/PIDE/prover.scala \ src/Pure/PIDE/query_operation.scala \ src/Pure/PIDE/rendering.scala \ src/Pure/PIDE/session.scala \ src/Pure/PIDE/text.scala \ src/Pure/PIDE/xml.scala \ src/Pure/PIDE/yxml.scala \ src/Pure/ROOT.scala \ src/Pure/System/bash.scala \ src/Pure/System/classpath.scala \ src/Pure/System/command_line.scala \ src/Pure/System/components.scala \ src/Pure/System/executable.scala \ src/Pure/System/getopts.scala \ src/Pure/System/host.scala \ src/Pure/System/isabelle_charset.scala \ src/Pure/System/isabelle_fonts.scala \ src/Pure/System/isabelle_platform.scala \ src/Pure/System/isabelle_process.scala \ src/Pure/System/isabelle_system.scala \ src/Pure/System/isabelle_tool.scala \ src/Pure/System/java_statistics.scala \ src/Pure/System/linux.scala \ src/Pure/System/mingw.scala \ src/Pure/System/nodejs.scala \ src/Pure/System/options.scala \ src/Pure/System/other_isabelle.scala \ src/Pure/System/platform.scala \ src/Pure/System/posix_interrupt.scala \ src/Pure/System/process_result.scala \ src/Pure/System/program_progress.scala \ src/Pure/System/progress.scala \ src/Pure/System/registry.scala \ src/Pure/System/scala.scala \ + src/Pure/System/setup_tool.scala \ src/Pure/System/system_channel.scala \ src/Pure/System/tty_loop.scala \ src/Pure/Thy/document_build.scala \ src/Pure/Thy/thy_element.scala \ src/Pure/Thy/thy_header.scala \ src/Pure/Thy/thy_syntax.scala \ src/Pure/Tools/check_keywords.scala \ src/Pure/Tools/debugger.scala \ src/Pure/Tools/doc.scala \ src/Pure/Tools/docker_build.scala \ src/Pure/Tools/dotnet_setup.scala \ src/Pure/Tools/dump.scala \ src/Pure/Tools/flarum.scala \ src/Pure/Tools/fontforge.scala \ src/Pure/Tools/go_setup.scala \ src/Pure/Tools/java_monitor.scala \ src/Pure/Tools/logo.scala \ src/Pure/Tools/mkroot.scala \ src/Pure/Tools/phabricator.scala \ src/Pure/Tools/print_operation.scala \ src/Pure/Tools/prismjs.scala \ src/Pure/Tools/profiling.scala \ src/Pure/Tools/profiling_report.scala \ src/Pure/Tools/scala_build.scala \ src/Pure/Tools/scala_project.scala \ src/Pure/Tools/server.scala \ src/Pure/Tools/server_commands.scala \ src/Pure/Tools/simplifier_trace.scala \ src/Pure/Tools/spell_checker.scala \ src/Pure/Tools/sync.scala \ src/Pure/Tools/task_statistics.scala \ src/Pure/Tools/update.scala \ src/Pure/Tools/update_cartouches.scala \ src/Pure/Tools/update_comments.scala \ src/Pure/Tools/update_header.scala \ src/Pure/Tools/update_then.scala \ src/Pure/Tools/update_theorems.scala \ src/Pure/library.scala \ src/Pure/pure_thy.scala \ src/Pure/term.scala \ src/Pure/term_xml.scala \ src/Pure/thm_name.scala \ src/Tools/Graphview/graph_file.scala \ src/Tools/Graphview/graph_panel.scala \ src/Tools/Graphview/graphview.scala \ src/Tools/Graphview/layout.scala \ src/Tools/Graphview/main_panel.scala \ src/Tools/Graphview/metrics.scala \ src/Tools/Graphview/model.scala \ src/Tools/Graphview/mutator.scala \ src/Tools/Graphview/mutator_dialog.scala \ src/Tools/Graphview/mutator_event.scala \ src/Tools/Graphview/popups.scala \ src/Tools/Graphview/shapes.scala \ src/Tools/Graphview/tree_panel.scala \ src/Tools/VSCode/src/channel.scala \ src/Tools/VSCode/src/component_vscode_extension.scala \ src/Tools/VSCode/src/component_vscodium.scala \ src/Tools/VSCode/src/dynamic_output.scala \ src/Tools/VSCode/src/language_server.scala \ src/Tools/VSCode/src/lsp.scala \ src/Tools/VSCode/src/preview_panel.scala \ src/Tools/VSCode/src/state_panel.scala \ src/Tools/VSCode/src/vscode_main.scala \ src/Tools/VSCode/src/vscode_model.scala \ src/Tools/VSCode/src/vscode_rendering.scala \ src/Tools/VSCode/src/vscode_resources.scala \ src/Tools/VSCode/src/vscode_spell_checker.scala \ src/Tools/jEdit/src/active.scala \ src/Tools/jEdit/src/base_plugin.scala \ src/Tools/jEdit/src/completion_popup.scala \ src/Tools/jEdit/src/context_menu.scala \ src/Tools/jEdit/src/debugger_dockable.scala \ src/Tools/jEdit/src/dockable.scala \ src/Tools/jEdit/src/document_dockable.scala \ src/Tools/jEdit/src/document_model.scala \ src/Tools/jEdit/src/document_view.scala \ src/Tools/jEdit/src/documentation_dockable.scala \ src/Tools/jEdit/src/fold_handling.scala \ src/Tools/jEdit/src/font_info.scala \ src/Tools/jEdit/src/graphview_dockable.scala \ src/Tools/jEdit/src/info_dockable.scala \ src/Tools/jEdit/src/isabelle.scala \ src/Tools/jEdit/src/isabelle_encoding.scala \ src/Tools/jEdit/src/isabelle_export.scala \ src/Tools/jEdit/src/isabelle_session.scala \ src/Tools/jEdit/src/isabelle_vfs.scala \ src/Tools/jEdit/src/jedit_bibtex.scala \ src/Tools/jEdit/src/jedit_editor.scala \ src/Tools/jEdit/src/jedit_jar.scala \ src/Tools/jEdit/src/jedit_lib.scala \ src/Tools/jEdit/src/jedit_main.scala \ src/Tools/jEdit/src/jedit_options.scala \ src/Tools/jEdit/src/jedit_plugins.scala \ src/Tools/jEdit/src/jedit_rendering.scala \ src/Tools/jEdit/src/jedit_resources.scala \ src/Tools/jEdit/src/jedit_sessions.scala \ src/Tools/jEdit/src/jedit_spell_checker.scala \ src/Tools/jEdit/src/keymap_merge.scala \ src/Tools/jEdit/src/main_plugin.scala \ src/Tools/jEdit/src/monitor_dockable.scala \ src/Tools/jEdit/src/output_dockable.scala \ src/Tools/jEdit/src/pide_docking_framework.scala \ src/Tools/jEdit/src/pretty_text_area.scala \ src/Tools/jEdit/src/pretty_tooltip.scala \ src/Tools/jEdit/src/process_indicator.scala \ src/Tools/jEdit/src/protocol_dockable.scala \ src/Tools/jEdit/src/query_dockable.scala \ src/Tools/jEdit/src/raw_output_dockable.scala \ src/Tools/jEdit/src/rich_text_area.scala \ src/Tools/jEdit/src/session_build.scala \ src/Tools/jEdit/src/simplifier_trace_dockable.scala \ src/Tools/jEdit/src/simplifier_trace_window.scala \ src/Tools/jEdit/src/sledgehammer_dockable.scala \ src/Tools/jEdit/src/state_dockable.scala \ src/Tools/jEdit/src/status_widget.scala \ src/Tools/jEdit/src/symbols_dockable.scala \ src/Tools/jEdit/src/syntax_style.scala \ src/Tools/jEdit/src/syslog_dockable.scala \ src/Tools/jEdit/src/text_overview.scala \ src/Tools/jEdit/src/text_structure.scala \ src/Tools/jEdit/src/theories_dockable.scala \ src/Tools/jEdit/src/theories_status.scala \ src/Tools/jEdit/src/timing_dockable.scala \ src/Tools/jEdit/src/token_markup.scala services = \ isabelle.Bash$Handler \ isabelle.Bibtex$File_Format \ isabelle.Build$Engine$Default \ isabelle.Build_Schedule$Build_Engine \ isabelle.Document_Build$Build_Engine \ isabelle.Document_Build$LIPIcs_LuaLaTeX_Engine \ isabelle.Document_Build$LIPIcs_PDFLaTeX_Engine \ isabelle.Document_Build$LuaLaTeX_Engine \ isabelle.Document_Build$PDFLaTeX_Engine \ isabelle.CI_Builds \ + isabelle.GHC_Setup \ isabelle.ML_Statistics$Handler \ + isabelle.OCaml_Setup \ isabelle.Print_Operation$Handler \ isabelle.Scala$Handler \ isabelle.Scala_Functions \ isabelle.Server_Commands \ isabelle.Sessions$ROOTS_File_Format \ isabelle.Simplifier_Trace$Handler \ isabelle.Tools \ isabelle.jedit.JEdit_Plugin0 \ isabelle.jedit.JEdit_Plugin1 \ isabelle.jedit.JEdit_JAR$Scala_Functions \ isabelle.nitpick.Kodkod$Handler \ isabelle.nitpick.Scala_Functions \ isabelle.spark.SPARK$Load_Command1 \ isabelle.spark.SPARK$Load_Command2 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,617 +1,611 @@ /* 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 make_64_32(platform: String): String = platform.replace("x86_64-", "x86_64_32-").replace("arm64-", "arm64_32-") def augment_settings( other_isabelle: Other_Isabelle, threads: Int, arch_64: Boolean, arch_apple: 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 = make_64_32(platform_64) val platform_apple_64 = other_isabelle.getenv("ISABELLE_APPLE_PLATFORM64") val platform_apple_64_32 = make_64_32(platform_apple_64) 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_apple && arch_64) { if (check_dir(platform_apple_64)) platform_apple_64 else err(platform_apple_64) } else if (arch_apple) { if (check_dir(platform_apple_64_32)) platform_apple_64_32 else err(platform_apple_64_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_multicore = (1, 1) private val default_heap = 1500 private val default_isabelle_identifier = "build_history" def local_build( options: Options, root: Path, progress: Progress = new Progress, afp: Boolean = false, isabelle_identifier: String = default_isabelle_identifier, ml_statistics_step: Int = 1, component_repository: String = Components.static_component_repository, components_base: String = Components.dynamic_components_base, clean_platforms: Option[List[Platform.Family]] = None, clean_archives: Boolean = false, fresh: Boolean = false, hostname: String = "", multicore_base: Boolean = false, multicore_list: List[(Int, Int)] = List(default_multicore), arch_64: Boolean = false, arch_apple: Boolean = false, heap: Int = default_heap, max_heap: Option[Int] = None, 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, afp_build_args) = if (afp) (Some(directory(root + Path.explode("AFP"))), List("-d", "~~/AFP/thys")) else (None, Nil) /* main */ val other_isabelle = Other_Isabelle(root, isabelle_identifier = isabelle_identifier, progress = progress) def resolve_components(): Unit = other_isabelle.resolve_components( echo = verbose, component_repository = component_repository, clean_platforms = clean_platforms, clean_archives = clean_archives) val build_host = proper_string(hostname) getOrElse Isabelle_System.hostname() val build_history_date = progress.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( components_base = components_base, catalogs = Components.optional_catalogs) other_isabelle.init_settings(component_settings) resolve_components() val ml_platform = augment_settings( other_isabelle, threads, arch_64, arch_apple, heap, max_heap, more_settings) File.write(other_isabelle.etc_preferences, cat_lines("build_log_verbose = true" :: more_preferences)) val isabelle_output = other_isabelle.expand_path( Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER")) val isabelle_output_log = isabelle_output + Path.explode("log") val isabelle_base_log = isabelle_output + Path.explode("../base_log") if (first_build) { resolve_components() other_isabelle.scala_build(fresh = fresh, echo = verbose) - - 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) - + Setup_Tool.init(other_isabelle, verbose = verbose) Isabelle_System.rm_tree(isabelle_base_log) } Isabelle_System.rm_tree(isabelle_output) Isabelle_System.make_directory(isabelle_output) other_isabelle.expand_path(Path.explode("$ISABELLE_HOME_USER/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.expand_path(Path.explode("$ISABELLE_HOME_USER/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 = progress.now() val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args val build_result = Other_Isabelle(root, isabelle_identifier = isabelle_identifier, progress = build_out_progress) .bash("bin/isabelle build " + Bash.strings(build_args1), redirect = true, echo = true, strict = false) val build_end = progress.now() val store = Store(options + "build_database_server=false") val build_info: Build_Log.Build_Info = Build_Log.Log_File(log_path.file_name, build_result.out_lines, cache = store.cache). parse_build_info(ml_statistics = true) /* output log */ 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.log_db(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.is_empty => List("Sources " + session_name + " " + sources.digest.toString) 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.log_db(session_name) val log_gz = isabelle_output + Store.log_gz(session_name) val properties = if (database.is_file) { using(SQLite.open_database(database))(store.read_ml_statistics(_, session_name)) } else if (log_gz.is_file) { Build_Log.Log_File.read(log_gz.file, cache = store.cache) .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.log_db(session_name) val errors = if (database.is_file) { try { using(SQLite.open_database(database))(store.read_errors(_, session_name)) } // column "errors" could be missing catch { case _: java.sql.SQLException => Nil } } else Nil for (msg <- errors) yield { val content = Library.encode_lines(Output.clean_yxml(msg)) List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> content) } } 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(File.size(heap)) + " 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 heap: Option[Int] = None var max_heap: Option[Int] = None var multicore_list = List(default_multicore) var isabelle_identifier = default_isabelle_identifier var clean_platforms: Option[List[Platform.Family]] = None var clean_archives = false var component_repository = Components.static_component_repository var components_base = Components.dynamic_components_base var arch_apple = false var more_settings: List[String] = Nil var more_preferences: List[String] = Nil var fresh = false var hostname = "" var arch_64 = false var output_file = "" var ml_statistics_step = 1 var build_tags = List.empty[String] 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 -H SIZE minimal ML heap in MB (default: """ + default_heap + """ for 32bit, """ + default_heap * 2 + """ for 64bit) -M MULTICORE multicore configurations (see below) -N NAME alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """) -O PLATFORMS clean resolved components, retaining only the given list platform families (separated by commas; default: do nothing) -Q clean archives of downloaded components -R URL remote repository for Isabelle components (default: """ + Components.static_component_repository + """) -S DIR base directory for Isabelle components (default: """ + quote(Components.dynamic_components_base) + """) -U SIZE maximal ML heap in MB (default: unbounded) -a processor architecture is Apple Silicon (ARM64) -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, 64, default: 32) -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) -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), "H:" -> (arg => heap = Some(Value.Int.parse(arg))), "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)), "N:" -> (arg => isabelle_identifier = arg), "O:" -> (arg => clean_platforms = Some(space_explode(',',arg).map(Platform.Family.parse))), "Q" -> (_ => clean_archives = true), "R:" -> (arg => component_repository = arg), "S:" -> (arg => components_base = arg), "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))), "a" -> (_ => arch_apple = true), "e:" -> (arg => more_settings = more_settings ::: List(arg)), "f" -> (_ => fresh = true), "h:" -> (arg => hostname = arg), "m:" -> { case "32" => arch_64 = false case "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)), "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, progress = progress, afp = afp, isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step, component_repository = component_repository, components_base = components_base, clean_platforms = clean_platforms, clean_archives = clean_archives, fresh = fresh, hostname = hostname, multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64, arch_apple = arch_apple, heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap), max_heap = max_heap, 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 = Process_Result.RC.merge(results.map(p => p._1.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", component_repository: String = Components.static_component_repository, components_base: String = Components.dynamic_components_base, clean_platform: Boolean = false, clean_archives: Boolean = false, shared_isabelle_self: Boolean = false, progress: Progress = new Progress, 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 = progress, ssh = ssh) Sync.sync(ssh.options, context, target, thorough = accurate, preserve_jars = !accurate, rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None) } if (!shared_isabelle_self) sync(isabelle_self) val self_isabelle = Other_Isabelle(isabelle_self, isabelle_identifier = isabelle_identifier, ssh = ssh, progress = progress) val clean_platforms = if (clean_platform) Some(List(ssh.isabelle_platform_family)) else None self_isabelle.init(fresh = !shared_isabelle_self, echo = true, component_repository = component_repository, other_settings = self_isabelle.init_components(components_base = components_base), clean_platforms = clean_platforms, clean_archives = clean_archives) 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_proper(afp_repos, " -A") + " " + options try { val script = ssh.bash_path(Path.explode("Admin/build_other")) + " -R " + Bash.string(component_repository) + " -S " + Bash.string(components_base) + (clean_platforms match { case Some(ps) => " -O " + Bash.string(ps.mkString(",")) case None => "" }) + (if (clean_archives) " -Q" else "") + " -o " + ssh.bash_path(output_file) + build_options + " " + ssh.bash_path(isabelle_other) + " " + args self_isabelle.bash(script, echo = true, strict = false).check } 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.delete(log) (log.file_name, bytes) } } } } } diff --git a/src/Pure/System/other_isabelle.scala b/src/Pure/System/other_isabelle.scala --- a/src/Pure/System/other_isabelle.scala +++ b/src/Pure/System/other_isabelle.scala @@ -1,186 +1,189 @@ /* Title: Pure/System/other_isabelle.scala Author: Makarius Manage other Isabelle distributions: support historic versions starting from tag "build_history_base". */ package isabelle object Other_Isabelle { def apply( root: Path, isabelle_identifier: String = "", ssh: SSH.System = SSH.Local, progress: Progress = new Progress ): Other_Isabelle = { val (isabelle_home, url_prefix) = ssh match { case session: SSH.Session => (ssh.absolute_path(root), session.rsync_prefix) case _ => if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) { error("Cannot manage other Isabelle distribution: global ISABELLE_SETTINGS_PRESENT") } (root.canonical, "") } val isabelle_home_url = url_prefix + isabelle_home.implode new Other_Isabelle(isabelle_home, isabelle_identifier, isabelle_home_url, ssh, progress) } } final class Other_Isabelle private( val isabelle_home: Path, val isabelle_identifier: String, isabelle_home_url: String, ssh: SSH.System, progress: Progress ) { + other_isabelle => + override def toString: String = isabelle_home_url /* static system */ def bash( script: String, redirect: Boolean = false, echo: Boolean = false, strict: Boolean = true ): Process_Result = { val env = Isabelle_System.export_env( user_home = ssh.user_home, isabelle_identifier = isabelle_identifier) ssh.execute(env + "cd " + ssh.bash_path(isabelle_home) + "\n" + script, progress_stdout = progress.echo_if(echo, _), progress_stderr = progress.echo_if(echo, _), redirect = redirect, settings = false, strict = strict) } def getenv(name: String): String = bash("bin/isabelle getenv -b " + Bash.string(name)).check.out val settings: Isabelle_System.Settings = (name: String) => getenv(name) def expand_path(path: Path): Path = path.expand_env(settings) def bash_path(path: Path): String = Bash.string(expand_path(path).implode) val isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER")) def etc: Path = isabelle_home_user + Path.explode("etc") def etc_settings: Path = etc + Path.explode("settings") def etc_preferences: Path = etc + Path.explode("preferences") /* components */ def init_components( components_base: String = Components.dynamic_components_base, catalogs: List[String] = Components.default_catalogs, components: List[String] = Nil ): List[String] = { val admin = Components.admin(Path.ISABELLE_HOME).implode catalogs.map(name => "init_components " + quote(components_base) + " " + quote(admin + "/" + name)) ::: components.map(name => "init_component " + quote(components_base) + "/" + name) } def resolve_components( echo: Boolean = false, clean_platforms: Option[List[Platform.Family]] = None, clean_archives: Boolean = false, component_repository: String = Components.static_component_repository ): Unit = { val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING")) for (path <- missing) { Components.resolve(path.dir, path.file_name, clean_platforms = clean_platforms, clean_archives = clean_archives, component_repository = component_repository, ssh = ssh, progress = if (echo) progress else new Progress) } } def scala_build(fresh: Boolean = false, echo: Boolean = false): Unit = { if (fresh) ssh.rm_tree(isabelle_home + Path.explode("lib/classes")) val dummy_stty = Path.explode("~~/lib/dummy_stty/stty") val dummy_stty_remote = expand_path(dummy_stty) if (!ssh.is_file(dummy_stty_remote)) { ssh.make_directory(dummy_stty_remote.dir) ssh.write_file(dummy_stty_remote, dummy_stty) ssh.set_executable(dummy_stty_remote) } try { bash( "export PATH=\"" + bash_path(dummy_stty_remote.dir) + ":$PATH\"\n" + "export CLASSPATH=" + Bash.string(getenv("ISABELLE_CLASSPATH")) + "\n" + "bin/isabelle jedit -b", echo = echo).check } catch { case ERROR(msg) => cat_error("Failed to build Isabelle/Scala/Java modules:", msg) } } /* settings */ def clean_settings(): Boolean = if (!ssh.is_file(etc_settings)) true else if (ssh.read(etc_settings).startsWith("# generated by Isabelle")) { ssh.delete(etc_settings) true } else false def init_settings(settings: List[String]): Unit = { if (clean_settings()) { ssh.make_directory(etc_settings.dir) ssh.write(etc_settings, "# generated by Isabelle " + Date.now() + "\n" + "#-*- shell-script -*- :mode=shellscript:\n" + settings.mkString("\n", "\n", "\n")) } else error("Cannot proceed with existing user settings file: " + etc_settings) } def debug_settings(): List[String] = { val debug = System.getProperty("isabelle.debug", "") == "true" if (debug) { List("ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.debug=true\"") } else Nil } /* init */ def init( other_settings: List[String] = init_components(), fresh: Boolean = false, echo: Boolean = false, clean_platforms: Option[List[Platform.Family]] = None, clean_archives: Boolean = false, component_repository: String = Components.static_component_repository ): Unit = { init_settings(other_settings) resolve_components( echo = echo, clean_platforms = clean_platforms, clean_archives = clean_archives, component_repository = component_repository) scala_build(fresh = fresh, echo = echo) + Setup_Tool.init(other_isabelle) } /* cleanup */ def cleanup(): Unit = { clean_settings() ssh.delete(etc) ssh.delete(isabelle_home_user) } } diff --git a/src/Pure/System/setup_tool.scala b/src/Pure/System/setup_tool.scala new file mode 100644 --- /dev/null +++ b/src/Pure/System/setup_tool.scala @@ -0,0 +1,37 @@ +/* Title: Pure/System/setup_tool.scala + Author: Makarius + +Additional setup tools for other Isabelle distribution. +*/ + +package isabelle + + +object Setup_Tool { + lazy val services: List[Setup_Tool] = + Isabelle_System.make_services(classOf[Setup_Tool]) + + def init(other_isabelle: Other_Isabelle, verbose: Boolean = false): Unit = + services.foreach(_.init(other_isabelle, verbose = verbose)) +} + +abstract class Setup_Tool(tool: String) +extends Isabelle_System.Service { + override def toString: String = tool + + val variable: String = "ISABELLE_" + Word.uppercase(tool) + val files: List[Path] = List(Path.explode("lib/Tools") + Path.basic(tool)) + + def test(other_isabelle: Other_Isabelle): Boolean = + other_isabelle.getenv(variable) == "true" && + files.exists(p => (other_isabelle.isabelle_home + p).is_file) + + def run(other_isabelle: Other_Isabelle, verbose: Boolean = false): Unit = + other_isabelle.bash("bin/isabelle " + Bash.string(tool), echo = verbose) + + def init(other_isabelle: Other_Isabelle, verbose: Boolean = false): Unit = + if (test(other_isabelle)) run(other_isabelle, verbose = verbose) +} + +class GHC_Setup extends Setup_Tool("ghc_setup") +class OCaml_Setup extends Setup_Tool("ocaml_setup")