diff --git a/etc/build.props b/etc/build.props --- a/etc/build.props +++ b/etc/build.props @@ -1,350 +1,350 @@ 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_go.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/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.ML_Statistics$Handler \ 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/etc/settings b/etc/settings --- a/etc/settings +++ b/etc/settings @@ -1,196 +1,203 @@ # -*- 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_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0" ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m" ISABELLE_JAVAC_OPTIONS="-encoding UTF-8 -Xlint:-options -deprecation -source 17 -target 17" ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -feature -java-output-version 17 -source 3.3 -old-syntax -no-indent -color never -pagewidth 78 -J-Xms512m -J-Xmx4g -J-Xss16m" ISABELLE_SCALA_JAR="$ISABELLE_HOME/lib/classes/isabelle.jar" #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) ### case "$ISABELLE_PLATFORM_FAMILY" in windows*) ISABELLE_PDFLATEX="pdflatex -interaction=nonstopmode -c-style-errors" ;; *) ISABELLE_PDFLATEX="pdflatex -interaction=nonstopmode -file-line-error" ;; esac ISABELLE_LUALATEX="lualatex --interaction=nonstopmode --file-line-error" ISABELLE_BIBTEX="bibtex" ISABELLE_MAKEINDEX="makeindex -c -q" ISABELLE_EPSTOPDF="epstopdf" ### ### Misc path settings ### isabelle_directory '~' isabelle_directory '$ISABELLE_HOME_USER' isabelle_directory '~~' isabelle_directory '$ISABELLE_COMPONENTS_BASE' ISABELLE_COMPONENT_REPOSITORY="https://isabelle.sketis.net/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). case "$ISABELLE_PLATFORM_FAMILY" in windows*) ISABELLE_TMP_PREFIX="$TMPDIR/isabelle" ;; *) ISABELLE_TMP_PREFIX="/tmp/isabelle-${USER:-$LOGNAME}" ;; esac # 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 and external files ### # 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/Examples/Seq.thy:~~/src/HOL/Examples/Drinker.thy:~~/src/HOL/Examples/ML.thy:~~/src/HOL/Unix/Unix.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" ISABELLE_EXTERNAL_FILES="bmp:eps:gif:jpeg:jpg:pdf:png:xmp" ### ### Registry ### isabelle_registry "$ISABELLE_HOME/etc/registry.toml?" isabelle_registry "$ISABELLE_HOME_USER/etc/registry.toml?" ### ### Symbol rendering ### ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols?" ### ### OCaml ### ISABELLE_OPAM_ROOT="$USER_HOME/.opam" ISABELLE_OCAML_VERSION="ocaml-base-compiler.4.12.0" ### ### Haskell ### ISABELLE_STACK_ROOT="$USER_HOME/.stack" ISABELLE_STACK_RESOLVER="lts-22.13" ISABELLE_GHC_VERSION="ghc-9.6.4" ### ### .Net / Fsharp ### ISABELLE_DOTNET_VERSION="8.0.203" ### +### Go +### + +ISABELLE_GO_VERSION="1.22.1" + + +### ### Misc settings ### ISABELLE_GNUPLOT="gnuplot" ISABELLE_FONTFORGE="fontforge" #ISABELLE_SMLNJ="/usr/bin/sml" #ISABELLE_SWIPL="/usr/bin/swipl" diff --git a/lib/Tools/go b/lib/Tools/go new file mode 100755 --- /dev/null +++ b/lib/Tools/go @@ -0,0 +1,13 @@ +#!/usr/bin/env bash +# +# Author: Makarius +# +# DESCRIPTION: invoke go within the Isabelle environment + +if [ -z "$ISABELLE_GOEXE" ]; then + echo "Missing Go installation: need to run \"isabelle go_setup\" first" >&2 + exit 2 +else + export GOROOT="$ISABELLE_GOROOT" + exec "$ISABELLE_GOEXE/go" "$@" +fi diff --git a/lib/Tools/gofmt b/lib/Tools/gofmt new file mode 100755 --- /dev/null +++ b/lib/Tools/gofmt @@ -0,0 +1,13 @@ +#!/usr/bin/env bash +# +# Author: Makarius +# +# DESCRIPTION: invoke gofmt within the Isabelle environment + +if [ -z "$ISABELLE_GOEXE" ]; then + echo "Missing Go installation: need to run \"isabelle go_setup\" first" >&2 + exit 2 +else + export GOROOT="$ISABELLE_GOROOT" + exec "$ISABELLE_GOEXE/gofmt" "$@" +fi diff --git a/src/Pure/System/components.scala b/src/Pure/System/components.scala --- a/src/Pure/System/components.scala +++ b/src/Pure/System/components.scala @@ -1,489 +1,491 @@ /* Title: Pure/System/components.scala Author: Makarius Isabelle system components. */ package isabelle import java.io.{File => JFile} import scala.jdk.CollectionConverters._ 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)) } /* platforms */ sealed case class Platforms(family_platforms: Map[String, List[Path]]) { def + (entry: (String, List[Path])): Platforms = Platforms(family_platforms + entry) def defined(family: String): Boolean = family_platforms.isDefinedAt(family) def apply(family: String): List[Path] = family_platforms.getOrElse(family, Nil) def path_iterator: Iterator[Path] = family_platforms.valuesIterator.flatten } val default_platforms: Platforms = { def paths(args: String*): List[Path] = args.toList.map(Path.explode) Platforms( Map( Platform.Family.linux_arm.toString -> paths("arm64-linux", "arm64_32-linux"), Platform.Family.linux.toString -> paths("x86_64-linux", "x86_64_32-linux"), Platform.Family.macos.toString -> paths("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"), Platform.Family.windows.toString -> paths("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows"), "obsolete" -> paths("x86-linux", "x86-cygwin") )) } /* component collections */ def static_component_repository: String = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE") val dynamic_components_base: String = "${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}" val classic_components_base: Path = Path.explode("$USER_HOME/.isabelle/contrib") val default_catalogs: List[String] = List("main") val optional_catalogs: List[String] = List("main", "optional") def admin(dir: Path): Path = dir + Path.explode("Admin/components") def contrib(dir: Path = Path.current, name: String = ""): Path = dir + Path.explode("contrib") + Path.explode(name) def unpack( dir: Path, archive: Path, ssh: SSH.System = SSH.Local, progress: Progress = new Progress ): String = { val name = Archive.get_name(archive.file_name) progress.echo("Unpacking " + archive.base) ssh.execute( "tar -C " + ssh.bash_path(dir) + " -x -z -f " + ssh.bash_path(archive), progress_stdout = progress.echo(_), progress_stderr = progress.echo(_)).check name } def clean_base( base_dir: Path, platforms: List[Platform.Family] = Platform.Family.list, ssh: SSH.System = SSH.Local, progress: Progress = new Progress ): Unit = { for { name <- ssh.read_dir(base_dir) dir = base_dir + Path.basic(name) if is_component_dir(dir) } Directory(dir, ssh = ssh).clean(preserve = platforms, progress = progress) } def resolve( base_dir: Path, name: String, target_dir: Option[Path] = None, copy_dir: Option[Path] = None, clean_platforms: Option[List[Platform.Family]] = None, clean_archives: Boolean = false, component_repository: String = Components.static_component_repository, ssh: SSH.System = SSH.Local, progress: Progress = new Progress ): Unit = { ssh.make_directory(base_dir) val archive_name = Archive(name) val archive = base_dir + Path.basic(archive_name) if (!ssh.is_file(archive)) { val remote = Url.append_path(component_repository, archive_name) ssh.download_file(remote, archive, progress = progress) } for (dir <- copy_dir) { ssh.make_directory(dir) ssh.copy_file(archive, dir) } val unpack_dir = target_dir getOrElse base_dir unpack(unpack_dir, archive, ssh = ssh, progress = progress) if (clean_platforms.isDefined) { Directory(unpack_dir + Path.basic(name), ssh = ssh). clean(preserve = clean_platforms.get, progress = progress) } if (clean_archives) { progress.echo("Removing " + quote(archive_name)) ssh.delete(archive) } } def provide(local_dir: Path, base_dir: Path = classic_components_base, ssh: SSH.System = SSH.Local, progress: Progress = new Progress ): Directory = { val base_name = local_dir.expand.base val local_directory = Directory(local_dir).check val remote_directory = Directory(base_dir + base_name, ssh = ssh) if (!remote_directory.ok) { progress.echo("Providing " + base_name + ssh.print) Isabelle_System.with_tmp_file("tmp", ext = "tar") { local_tmp_tar => ssh.with_tmp_dir { remote_tmp_dir => val remote_tmp_tar = remote_tmp_dir + Path.basic("tmp.tar") val remote_dir = ssh.make_directory(remote_directory.path) Isabelle_System.gnutar( "-cf " + File.bash_path(local_tmp_tar) + " .", dir = local_dir).check ssh.write_file(remote_tmp_tar, local_tmp_tar) ssh.execute( "tar -C " + ssh.bash_path(remote_dir) + " -xf " + ssh.bash_path(remote_tmp_tar)).check } } } remote_directory.check } /* component directories */ def directories(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_COMPONENTS")) def is_component_dir(dir: Path, ssh: SSH.System = SSH.Local): Boolean = ssh.is_file(dir + Path.explode("etc/settings")) || ssh.is_file(dir + Path.explode("etc/components")) /* component directory content */ object Directory { def apply(path: Path, ssh: SSH.System = SSH.Local): Directory = new Directory(ssh.absolute_path(path), ssh) } class Directory private(val path: Path, val ssh: SSH.System = SSH.Local) { override def toString: String = path.toString + ssh.print def etc: Path = path + Path.basic("etc") def src: Path = path + Path.basic("src") def bin: Path = path + Path.basic("bin") def lib: Path = path + Path.basic("lib") def settings: Path = etc + Path.basic("settings") def components: Path = etc + Path.basic("components") def build_props: Path = etc + Path.basic("build.props") def platform_props: Path = etc + Path.basic("platform.props") def README: Path = path + Path.basic("README") def LICENSE: Path = path + Path.basic("LICENSE") - def create(progress: Progress = new Progress): Directory = { - progress.echo("Creating component directory " + toString) - ssh.new_directory(path) + def create(progress: Progress = new Progress, permissive: Boolean = false): Directory = { + if (!permissive || !ssh.is_dir(path)) { + progress.echo("Creating component directory " + toString) + ssh.new_directory(path) + } ssh.make_directory(etc) this } def get_platforms(): Platforms = { val props_path = platform_props.expand val props = if (props_path.is_file) { try { for (case (a, b) <- File.read_props(props_path).asScala.toList) yield { if (!default_platforms.defined(a)) error("Bad platform family " + quote(a)) val ps = List.from(b.split("\\s+").iterator.filter(_.nonEmpty)).map(Path.explode) for (p <- ps if !p.all_basic) error("Bad path outside component " + p) a -> ps } } catch { case ERROR(msg) => error(msg + Position.here(Position.File(props_path.implode))) } } else Nil props.foldLeft(default_platforms)(_ + _) } def clean( preserve: List[Platform.Family] = Platform.Family.list, progress: Progress = new Progress ): Unit = { val platforms = get_platforms() val preserve_path = Set.from(for (a <- preserve; p <- platforms(a.toString)) yield p) for (dir <- platforms.path_iterator if !preserve_path(dir) && ssh.is_dir(path + dir)) { progress.echo("Removing " + (path.base + dir)) ssh.rm_tree(path + dir) } } def ok: Boolean = ssh.is_file(settings) || ssh.is_file(components) || Sessions.is_session_dir(path, ssh = ssh) def check: Directory = if (!ssh.is_dir(path)) error("Bad component directory: " + toString) else if (!ok) { error("Malformed component directory: " + toString + "\n (missing \"etc/settings\" or \"etc/components\" or \"ROOT\" or \"ROOTS\")") } else this def read_components(): List[String] = split_lines(ssh.read(components)).filter(_.nonEmpty) def write_components(lines: List[String]): Unit = ssh.write(components, terminate_lines(lines)) def write_settings(text: String): Unit = ssh.write(settings, "# -*- shell-script -*- :mode=shellscript:\n" + text) } /* component repository content */ val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1") sealed case class SHA1_Entry(digest: SHA1.Digest, name: String) { override def toString: String = SHA1.shasum(digest, name).toString } def read_components_sha1(lines: List[String] = Nil): List[SHA1_Entry] = (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_Entry(SHA1.fake_digest(sha1), name)) case _ => error("Bad components.sha1 entry: " + quote(line)) }) def write_components_sha1(entries: List[SHA1_Entry]): Unit = File.write(components_sha1, entries.sortBy(_.name).mkString) /** manage user components **/ val components_path: Path = Path.explode("$ISABELLE_HOME_USER/etc/components") def read_components(): List[String] = if (components_path.is_file) Library.trim_split_lines(File.read(components_path)) else Nil def write_components(lines: List[String]): Unit = { Isabelle_System.make_directory(components_path.dir) File.write(components_path, terminate_lines(lines)) } def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = { val path = path0.expand.absolute if (add) Directory(path).check val lines1 = read_components() val lines2 = lines1.filter(line => line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path)) val lines3 = if (add) lines2 ::: List(path.implode) else lines2 if (lines1 != lines3) write_components(lines3) val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed" progress.echo(prefix + " component " + path) } /* main entry point */ def main(args: Array[String]): Unit = { Command_Line.tool { for (arg <- args) { val add = if (arg.startsWith("+")) true else if (arg.startsWith("-")) false else error("Bad argument: " + quote(arg)) val path = Path.explode(arg.substring(1)) update_components(add, path, progress = new Console_Progress) } } } /** build and publish components **/ def components_build( options: Options, components: List[Path], progress: Progress = new Progress, publish: Boolean = false, force: Boolean = false, update_components_sha1: Boolean = false ): Unit = { val archives: List[Path] = for (path <- components) yield { path.file_name match { case Archive(_) => path case name => Directory(path).check val component_path = path.expand val archive_dir = component_path.dir val archive_name = Archive(name) val archive = archive_dir + Path.explode(archive_name) if (archive.is_file && !force) { error("Component archive already exists: " + archive) } progress.echo("Packaging " + archive_name) Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name), dir = archive_dir).check archive } } if ((publish && archives.nonEmpty) || update_components_sha1) { val server = options.string("isabelle_components_server") if (server.isEmpty) error("Undefined option isabelle_components_server") using(SSH.open_session(options, server)) { ssh => val components_dir = Path.explode(options.string("isabelle_components_dir")) val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { error("Bad remote directory: " + dir) } if (publish) { for (archive <- archives) { val archive_name = archive.file_name val name = Archive.get_name(archive_name) val remote_component = components_dir + archive.base val remote_contrib = contrib_dir + Path.explode(name) // component archive if (ssh.is_file(remote_component) && !force) { error("Remote component archive already exists: " + remote_component) } progress.echo("Uploading " + archive_name) ssh.write_file(remote_component, archive) // contrib directory val is_standard_component = Isabelle_System.with_tmp_dir("component") { tmp_dir => Isabelle_System.extract(archive, tmp_dir) Directory(tmp_dir + Path.explode(name)).ok } if (is_standard_component) { if (ssh.is_dir(remote_contrib)) { if (force) ssh.rm_tree(remote_contrib) else error("Remote component directory already exists: " + remote_contrib) } progress.echo("Unpacking remote " + archive_name) ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + ssh.bash_path(remote_component)).check } else { progress.echo_warning("No unpacking of non-standard component: " + archive_name) } } } // remote SHA1 digests if (update_components_sha1) { val lines = for { entry <- ssh.read_dir(components_dir) if ssh.is_file(components_dir + Path.basic(entry)) && entry.endsWith(Archive.suffix) } yield { progress.echo("Digesting remote " + entry) ssh.execute("cd " + ssh.bash_path(components_dir) + "; sha1sum " + Bash.string(entry)).check.out } write_components_sha1(read_components_sha1(lines)) } } } // local SHA1 digests { val new_entries = for (archive <- archives) yield { val name = archive.file_name progress.echo("Digesting local " + name) SHA1_Entry(SHA1.digest(archive), name) } val new_names = new_entries.map(_.name).toSet write_components_sha1( new_entries ::: read_components_sha1().filterNot(entry => new_names.contains(entry.name))) } } /* Isabelle tool wrapper */ private val relevant_options = List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir") val isabelle_tool = Isabelle_Tool("components_build", "build and publish Isabelle components", Scala_Project.here, { args => var publish = false var update_components_sha1 = false var force = false var options = Options.init() def show_options: String = cat_lines(relevant_options.flatMap(options.get).map(_.print)) val getopts = Getopts(""" Usage: isabelle components_build [OPTIONS] ARCHIVES... DIRS... Options are: -P publish on SSH server (see options below) -f force: overwrite existing component archives and directories -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -u update all SHA1 keys in Isabelle repository Admin/components Build and publish Isabelle components as .tar.gz archives on SSH server, depending on system options: """ + Library.indent_lines(2, show_options) + "\n", "P" -> (_ => publish = true), "f" -> (_ => force = true), "o:" -> (arg => options = options + arg), "u" -> (_ => update_components_sha1 = true)) val more_args = getopts(args) if (more_args.isEmpty && !update_components_sha1) getopts.usage() val progress = new Console_Progress components_build(options, more_args.map(Path.explode), progress = progress, publish = publish, force = force, update_components_sha1 = update_components_sha1) }) } diff --git a/src/Pure/System/isabelle_tool.scala b/src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala +++ b/src/Pure/System/isabelle_tool.scala @@ -1,206 +1,206 @@ /* Title: Pure/System/isabelle_tool.scala Author: Makarius Isabelle system tools: external executables or internal Scala functions. */ package isabelle object Isabelle_Tool { /* external tools */ private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS")) private def is_external(dir: Path, name: String): Boolean = { val file = (dir + Path.explode(name)).file try { file.isFile && file.canRead && file.canExecute && !File.is_backup(name) } catch { case _: SecurityException => false } } private def find_external(name: String): Option[List[String] => Unit] = dirs().collectFirst( { case dir if is_external(dir, name) => { (args: List[String]) => val tool = dir + Path.explode(name) val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args)) sys.exit(result.print_stdout.rc) } }) /* internal tools */ private lazy val internal_tools: List[Isabelle_Tool] = Isabelle_System.make_services(classOf[Isabelle_Scala_Tools]).flatMap(_.tools) private def find_internal(name: String): Option[List[String] => Unit] = internal_tools.collectFirst({ case tool if tool.name == name => args => Command_Line.tool { tool.body(args) } }) /* list tools */ abstract class Entry { def name: String def position: Properties.T def description: String def print: String = description match { case "" => name case descr => name + " - " + descr } } sealed case class External(name: String, path: Path) extends Entry { def position: Properties.T = Position.File(path.absolute.implode) def description: String = { val Pattern = """.*\bDESCRIPTION: *(.*)""".r split_lines(File.read(path)).collectFirst({ case Pattern(s) => s }) getOrElse "" } } def external_tools(): List[External] = { for { dir <- dirs() if dir.is_dir name <- File.read_dir(dir) if is_external(dir, name) } yield External(name, dir + Path.explode(name)) } def isabelle_tools(): List[Entry] = (external_tools() ::: internal_tools).sortBy(_.name) object Isabelle_Tools extends Scala.Fun_String("isabelle_tools") { val here = Scala_Project.here def apply(arg: String): String = if (arg.nonEmpty) error("Bad argument: " + quote(arg)) else { val result = isabelle_tools().map(entry => (entry.name, entry.position)) val body = { import XML.Encode._; list(pair(string, properties))(result) } YXML.string_of_body(body) } } /* command line entry point */ def exe(isabelle_home: Path): Path = isabelle_home + Path.explode("bin/isabelle") def main(args: Array[String]): Unit = { Command_Line.tool { args.toList match { case Nil | List("-?") => val tool_descriptions = isabelle_tools().map(_.print) Getopts(""" Usage: isabelle TOOL [ARGS ...] Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help. Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage() case tool_name :: tool_args => find_external(tool_name) orElse find_internal(tool_name) match { case Some(tool) => tool(tool_args) case None => error("Unknown Isabelle tool: " + quote(tool_name)) } } } } } sealed case class Isabelle_Tool( name: String, description: String, here: Scala_Project.Here, body: List[String] => Unit ) extends Isabelle_Tool.Entry { def position: Position.T = here.position } class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) extends Isabelle_System.Service class Tools extends Isabelle_Scala_Tools( Build.isabelle_tool1, Build.isabelle_tool2, Build.isabelle_tool3, Build.isabelle_tool4, Build_Benchmark.isabelle_tool, Build_Schedule.isabelle_tool, CI_Build.isabelle_tool, Doc.isabelle_tool, Docker_Build.isabelle_tool, Document_Build.isabelle_tool, Dotnet_Setup.isabelle_tool, Dump.isabelle_tool, Export.isabelle_tool, + Go_Setup.isabelle_tool, Logo.isabelle_tool, ML_Process.isabelle_tool, Mercurial.isabelle_tool1, Mercurial.isabelle_tool2, Mkroot.isabelle_tool, Options.isabelle_tool, Phabricator.isabelle_tool1, Phabricator.isabelle_tool2, Phabricator.isabelle_tool3, Phabricator.isabelle_tool4, Profiling.isabelle_tool, Profiling_Report.isabelle_tool, Scala_Project.isabelle_tool, Server.isabelle_tool, Sessions.isabelle_tool, Sync.isabelle_tool, Update.isabelle_tool, Update_Cartouches.isabelle_tool, Update_Comments.isabelle_tool, Update_Header.isabelle_tool, Update_Then.isabelle_tool, Update_Theorems.isabelle_tool, isabelle.mirabelle.Mirabelle.isabelle_tool, isabelle.vscode.Language_Server.isabelle_tool, isabelle.vscode.VSCode_Main.isabelle_tool) class Admin_Tools extends Isabelle_Scala_Tools( Build_Doc.isabelle_tool, Build_Log.isabelle_tool, Build_Status.isabelle_tool, Check_Sources.isabelle_tool, Component_Bash_Process.isabelle_tool, Component_CSDP.isabelle_tool, Component_CVC5.isabelle_tool, Component_Cygwin.isabelle_tool, Component_E.isabelle_tool, Component_EPTCS.isabelle_tool, Component_Easychair.isabelle_tool, Component_Foiltex.isabelle_tool, Component_Fonts.isabelle_tool, - Component_Go.isabelle_tool, Component_Hugo.isabelle_tool, Component_Javamail.isabelle_tool, Component_JDK.isabelle_tool, Component_JEdit.isabelle_tool, Component_Jsoup.isabelle_tool, Component_LIPIcs.isabelle_tool, Component_LLNCS.isabelle_tool, Component_Minisat.isabelle_tool, Component_MLton.isabelle_tool, Component_PDFjs.isabelle_tool, Component_PolyML.isabelle_tool1, Component_PolyML.isabelle_tool2, Component_PostgreSQL.isabelle_tool, Component_Prismjs.isabelle_tool, Component_Rsync.isabelle_tool, Component_SPASS.isabelle_tool, Component_SQLite.isabelle_tool, Component_Scala.isabelle_tool, Component_Stack.isabelle_tool, Component_Vampire.isabelle_tool, Component_VeriT.isabelle_tool, Component_Windows_App.isabelle_tool, Component_Zipperposition.isabelle_tool, Component_Zstd.isabelle_tool, Components.isabelle_tool, isabelle.vscode.Component_VSCode.isabelle_tool, isabelle.vscode.Component_VSCodium.isabelle_tool1, isabelle.vscode.Component_VSCodium.isabelle_tool2) diff --git a/src/Pure/Admin/component_go.scala b/src/Pure/Tools/go_setup.scala rename from src/Pure/Admin/component_go.scala rename to src/Pure/Tools/go_setup.scala --- a/src/Pure/Admin/component_go.scala +++ b/src/Pure/Tools/go_setup.scala @@ -1,152 +1,172 @@ -/* Title: Pure/Admin/component_go.scala +/* Title: Pure/Tools/go_setup.scala Author: Makarius -Build Isabelle component for Go: https://go.dev +Dynamic setup of Go component. */ package isabelle -object Component_Go { +object Go_Setup { /* platform information */ sealed case class Platform_Info(platform: String, go_platform: String) extends Platform.Info { def paths: List[String] = List(platform, "pkg/tool/" + go_platform) def download(base_url: String, version: String): String = { val ext = if (is_windows) ".zip" else ".tar.gz" Url.append_path(base_url, "go" + version + "." + go_platform.replace("_", "-") + ext) } } val all_platforms: List[Platform_Info] = List( Platform_Info("arm64-darwin", "darwin_arm64"), Platform_Info("arm64-linux", "linux_arm64"), Platform_Info("x86_64-darwin", "darwin_amd64"), Platform_Info("x86_64-linux", "linux_amd64"), Platform_Info("x86_64-windows", "windows_amd64")) - - /* build go */ - - val default_url = "https://go.dev/dl" - val default_version = "1.22.1" - - def build_go( - base_url: String = default_url, - version: String = default_version, - target_dir: Path = Path.current, - progress: Progress = new Progress - ): Unit = { - val component_dir = - Components.Directory(target_dir + Path.basic("go-" + version)).create(progress = progress) + def check_platform_spec(spec: String): String = + Platform.check_spec(all_platforms, spec) - /* download */ + /* Go download and setup */ + + def default_platform: String = + Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true, apple = true) + def default_target_dir: Path = Components.default_components_base + val default_url = "https://go.dev/dl" + def default_version: String = Isabelle_System.getenv_strict("ISABELLE_GO_VERSION") + + def go_setup( + platforms: List[String] = List(default_platform), + base_url: String = default_url, + version: String = default_version, + target_dir: Path = default_target_dir, + progress: Progress = new Progress, + force: Boolean = false + ): Unit = { + platforms.foreach(check_platform_spec) + + + /* component directory */ + + val component_dir = + Components.Directory(target_dir + Path.basic("go-" + version)).create(permissive = true) + + progress.echo("Component directory " + component_dir) + + component_dir.write_settings(""" +ISABELLE_GOROOT="$COMPONENT" + +if [ -n "$ISABELLE_WINDOWS_PLATFORM64" -a -d "$ISABELLE_GOROOT/$ISABELLE_WINDOWS_PLATFORM64" ]; then + ISABELLE_GOEXE="$ISABELLE_GOROOT/$ISABELLE_WINDOWS_PLATFORM64" +elif [ -n "$ISABELLE_APPLE_PLATFORM64" -a -d "$ISABELLE_GOROOT/$ISABELLE_APPLE_PLATFORM64" ]; then + ISABELLE_GOEXE="$ISABELLE_GOROOT/$ISABELLE_APPLE_PLATFORM64" +elif [ -d "$ISABELLE_GOROOT/$ISABELLE_PLATFORM64" ]; then + ISABELLE_GOEXE="$ISABELLE_GOROOT/$ISABELLE_PLATFORM64" +fi +""") + + File.write(component_dir.platform_props, + (for ((a, b) <- all_platforms.groupBy(_.family_name).iterator) + yield a + " = " + b.flatMap(_.paths).mkString(" ") + ).mkString("", "\n", "\n")) + + for (old <- proper_string(Isabelle_System.getenv("ISABELLE_GOROOT"))) { + Components.update_components(false, Path.explode(old)) + } + + Components.update_components(true, component_dir.path) + + + /* download and setup */ Isabelle_System.with_tmp_dir("download") { download_dir => - for (platform <- all_platforms.reverse) { - val download = platform.download(base_url, version) + for (platform <- all_platforms if platforms.exists(platform.is)) { + val platform_dir = component_dir.path + platform.path + if (platform_dir.is_dir && !force) { + progress.echo_warning("Platform " + platform + " already installed") + } + else { + progress.echo("Platform " + platform + " ...") + progress.expose_interrupt() - val archive_name = - Url.get_base_name(download) getOrElse - error("Malformed download URL " + quote(download)) - val archive_path = download_dir + Path.basic(archive_name) + if (force) { + for (name <- platform.paths) { + val dir = component_dir.path + Path.explode(name) + if (dir.is_dir) Isabelle_System.rm_tree(dir) + } + } - Isabelle_System.download_file(download, archive_path, progress = progress) - Isabelle_System.extract(archive_path, component_dir.path, strip = true) + val download = platform.download(base_url, version) - val platform_dir = component_dir.path + platform.path - Isabelle_System.move_file(component_dir.bin, platform_dir) + val archive_name = + Url.get_base_name(download) getOrElse + error("Malformed download URL " + quote(download)) + val archive_path = download_dir + Path.basic(archive_name) + + Isabelle_System.download_file(download, archive_path) + Isabelle_System.extract(archive_path, component_dir.path, strip = true) + Isabelle_System.move_file(component_dir.bin, platform_dir) + } } } File.find_files(component_dir.path.file, pred = file => File.is_exe(file.getName)). foreach(file => File.set_executable(File.path(file))) - /* isabelle tool */ - - val isabelle_tool_dir = component_dir.path + Path.explode("isabelle_tool") - Isabelle_System.make_directory(isabelle_tool_dir) - - for (tool <- List("go", "gofmt")) { - val isabelle_tool = isabelle_tool_dir + Path.basic(tool) - File.write(isabelle_tool, -"""#!/usr/bin/env bash -# -# Author: Makarius -# -# DESCRIPTION: invoke """ + tool + """ within the Isabelle environment - -export GOROOT="$ISABELLE_GOROOT" -exec "$ISABELLE_GOEXE/""" + tool + """" "$@" -""") - File.set_executable(isabelle_tool) - } - - - /* settings */ - - component_dir.write_settings(""" -ISABELLE_GOROOT="$COMPONENT" -ISABELLE_GOEXE="$ISABELLE_GOROOT/${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}" - -ISABELLE_TOOLS="$ISABELLE_TOOLS:$ISABELLE_GOROOT/isabelle_tool" -""") - - - /* platform.props */ - - File.write(component_dir.platform_props, - (for ((a, b) <- all_platforms.groupBy(_.family_name).iterator) - yield a + " = " + b.flatMap(_.paths).mkString(" ") - ).mkString("", "\n", "\n")) - - /* README */ File.write(component_dir.README, - """This distribution of Go has been assembled from official downloads from -""" + base_url + """ + """This installation of Go has been produced via "isabelle go_setup". Makarius """ + Date.Format.date(Date.now()) + "\n") } /* Isabelle tool wrapper */ val isabelle_tool = - Isabelle_Tool("component_go", "build component for Go", Scala_Project.here, + Isabelle_Tool("go_setup", "dynamic setup of Go component", Scala_Project.here, { args => - var target_dir = Path.current + var target_dir = default_target_dir var base_url = default_url var version = default_version + var force = false + var platforms = List(default_platform) val getopts = Getopts(""" -Usage: isabelle component_go [OPTIONS] +Usage: isabelle go_setup [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_url + """") -V VERSION version (default: """" + default_version + """") + -f force fresh installation of specified platforms + -p PLATFORMS comma-separated list of platform specifications, + as family or formal name (default: """ + quote(default_platform) + """) - Build component for Go development environment. + Download the Go development environment and configure it as Isabelle + component. See also https://go.dev """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => base_url = arg), - "V:" -> (arg => version = arg)) + "V:" -> (arg => version = arg), + "f" -> (_ => force = true), + "p:" -> (arg => platforms = space_explode(',', arg).map(check_platform_spec))) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() - build_go(base_url = base_url, version = version, target_dir = target_dir, - progress = progress) + go_setup(platforms = platforms, base_url = base_url, version = version, + target_dir = target_dir, progress = progress, force = force) }) }