diff --git a/etc/settings b/etc/settings --- a/etc/settings +++ b/etc/settings @@ -1,185 +1,191 @@ # -*- 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) ### -if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then - ISABELLE_PDFLATEX="pdflatex -interaction=nonstopmode -c-style-errors" -else - ISABELLE_PDFLATEX="pdflatex -interaction=nonstopmode -file-line-error" -fi +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). -if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then - ISABELLE_TMP_PREFIX="$TMPDIR/isabelle" -else - ISABELLE_TMP_PREFIX="/tmp/isabelle-${USER:-$LOGNAME}" -fi +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) + linux*) ISABELLE_OPEN="xdg-open" ;; - macos) + macos*) ISABELLE_OPEN="open" ;; - windows) + 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-21.15" ISABELLE_GHC_VERSION="ghc-9.4.7" ### ### Misc settings ### ISABELLE_GNUPLOT="gnuplot" ISABELLE_FONTFORGE="fontforge" #ISABELLE_MLTON="/usr/bin/mlton" #ISABELLE_MLTON_OPTIONS="-pi-style npi" #ISABELLE_SMLNJ="/usr/bin/sml" #ISABELLE_SWIPL="/usr/bin/swipl" diff --git a/lib/Tools/scala b/lib/Tools/scala --- a/lib/Tools/scala +++ b/lib/Tools/scala @@ -1,19 +1,21 @@ #!/usr/bin/env bash # # Author: Makarius # # DESCRIPTION: invoke Scala within the Isabelle environment isabelle scala_build || exit $? classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH classpath "$CLASSPATH"; export CLASSPATH="" export jvm_cp_args="$(platform_path "$ISABELLE_CLASSPATH")" export JAVA_OPTS="$ISABELLE_JAVA_SYSTEM_OPTIONS -J-Dscala.usejavacp=true" -if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then - export TERM=dumb +case "$ISABELLE_PLATFORM_FAMILY" in + windows*) + export TERM=dumb + ;; fi isabelle_scala scala $ISABELLE_SCALAC_OPTIONS "$@" diff --git a/lib/scripts/getfunctions b/lib/scripts/getfunctions --- a/lib/scripts/getfunctions +++ b/lib/scripts/getfunctions @@ -1,316 +1,316 @@ # -*- shell-script -*- :mode=shellscript: # # Author: Makarius # # Isabelle shell functions, with on-demand re-initialization for # non-interactive bash processess. NB: bash shell functions are not portable # and may be dropped by aggressively POSIX-conformant versions of /bin/sh. unset CDPATH if type splitarray >/dev/null 2>/dev/null then : else if [ "$OSTYPE" = cygwin ]; then function platform_path() { cygpath -i -C UTF8 -w -p "$@"; } function standard_path() { cygpath -i -u -p "$@" | tr -d '\r'; } else function platform_path() { echo "$@"; } function standard_path() { echo "$@"; } fi export -f platform_path standard_path #GNU tar (notably on macOS) function tar() { if [ -f "$ISABELLE_TAR" ]; then "$ISABELLE_TAR" "$@" else "$(type -P tar)" "$@" fi } export -f tar #registry function isabelle_registry () { local X="" for X in "$@" do if [ -z "$ISABELLE_REGISTRY" ]; then ISABELLE_REGISTRY="$X" elif [ -n "$X" ]; then ISABELLE_REGISTRY="$ISABELLE_REGISTRY:$X" fi done export ISABELLE_REGISTRY } export -f isabelle_registry #OCaml management via OPAM function isabelle_opam () { if [ -z "$ISABELLE_OPAM" ]; then echo "Unknown ISABELLE_OPAM -- OCaml management tools unavailable" >&2 return 127 else env OPAMROOT="$ISABELLE_OPAM_ROOT" OPAMCOLOR="never" "$ISABELLE_OPAM" "$@" fi } export -f isabelle_opam #GHC management via Stack function isabelle_stack () { if [ -z "$ISABELLE_STACK" ]; then echo "Unknown ISABELLE_STACK -- GHC management tools unavailable" >&2 return 127 else env STACK_ROOT="$(platform_path "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" --resolver "$ISABELLE_STACK_RESOLVER" --compiler "$ISABELLE_GHC_VERSION" "$@" fi } export -f isabelle_stack #robust invocation via ISABELLE_JDK_HOME function isabelle_jdk () { if [ -z "$ISABELLE_JDK_HOME" ]; then echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2 return 127 else local PRG="$1"; shift "$ISABELLE_JDK_HOME/bin/$PRG" "$@" fi } export -f isabelle_jdk #robust invocation via JAVA_HOME function isabelle_java () { if [ -z "$JAVA_HOME" ]; then echo "Unknown JAVA_HOME -- Java unavailable" >&2 return 127 else local PRG="$1"; shift "$JAVA_HOME/bin/$PRG" "$@" fi } export -f isabelle_java #robust invocation via SCALA_HOME function isabelle_scala () { if [ -z "$JAVA_HOME" ]; then echo "Unknown JAVA_HOME -- Java unavailable" >&2 return 127 elif [ -z "$SCALA_HOME" ]; then echo "Unknown SCALA_HOME -- Scala unavailable" >&2 return 127 else local PRG="$1"; shift "$SCALA_HOME/bin/$PRG" "$@" fi } export -f isabelle_scala #classpath function classpath () { local X="" for X in "$@" do if [ -z "$ISABELLE_CLASSPATH" ]; then ISABELLE_CLASSPATH="$X" elif [ -n "$X" ]; then ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X" fi done export ISABELLE_CLASSPATH } export -f classpath #java_library function java_library () { local X="" for X in "$@" do case "$ISABELLE_PLATFORM_FAMILY" in - linux) + linux*) if [ -z "$LD_LIBRARY_PATH" ]; then export LD_LIBRARY_PATH="$X" else export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:$X" fi ;; - macos) + macos*) if [ -z "$JAVA_LIBRARY_PATH" ]; then export JAVA_LIBRARY_PATH="$X" else export JAVA_LIBRARY_PATH="$JAVA_LIBRARY_PATH:$X" fi ;; - windows) + windows*) if [ -z "$PATH" ]; then export PATH="$X" else export PATH="$PATH:$X" fi ;; esac done export ISABELLE_CLASSPATH } export -f java_library #Isabelle fonts function isabelle_fonts () { local X="" for X in "$@" do if [ -z "$ISABELLE_FONTS" ]; then ISABELLE_FONTS="$X" else ISABELLE_FONTS="$ISABELLE_FONTS:$X" fi done export ISABELLE_FONTS } export -f isabelle_fonts function isabelle_fonts_hidden () { local X="" for X in "$@" do if [ -z "$ISABELLE_FONTS_HIDDEN" ]; then ISABELLE_FONTS_HIDDEN="$X" else ISABELLE_FONTS_HIDDEN="$ISABELLE_FONTS_HIDDEN:$X" fi done export ISABELLE_FONTS_HIDDEN } export -f isabelle_fonts_hidden #Isabelle/Scala services function isabelle_scala_service () { local X="" for X in "$@" do if [ -z "$ISABELLE_SCALA_SERVICES" ]; then ISABELLE_SCALA_SERVICES="$X" else ISABELLE_SCALA_SERVICES="$ISABELLE_SCALA_SERVICES:$X" fi done export ISABELLE_SCALA_SERVICES } export -f isabelle_scala_service #Special directories function isabelle_directory () { local X="" for X in "$@" do if [ -z "$ISABELLE_DIRECTORIES" ]; then ISABELLE_DIRECTORIES="$X" else ISABELLE_DIRECTORIES="$ISABELLE_DIRECTORIES:$X" fi done export ISABELLE_DIRECTORIES } export -f isabelle_directory #arrays function splitarray () { SPLITARRAY=() local IFS="$1"; shift local X="" for X in $* do SPLITARRAY["${#SPLITARRAY[@]}"]="$X" done } export -f splitarray #init component tree function init_component () { local COMPONENT="$1" case "$COMPONENT" in /*) ;; *) echo >&2 "Absolute component path required: \"$COMPONENT\"" exit 2 ;; esac if [ -d "$COMPONENT" ]; then if [ -z "$ISABELLE_COMPONENTS" ]; then ISABELLE_COMPONENTS="$COMPONENT" else ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" fi else echo >&2 "### Missing Isabelle component: \"$COMPONENT\"" if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then ISABELLE_COMPONENTS_MISSING="$COMPONENT" else ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT" fi fi if [ -f "$COMPONENT/etc/settings" ]; then source "$COMPONENT/etc/settings" local RC="$?" if [ "$RC" -ne 0 ]; then echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\"" exit 2 fi fi if [ -f "$COMPONENT/etc/components" ]; then init_components "$COMPONENT" "$COMPONENT/etc/components" fi } export -f init_component #init component forest function init_components () { local REPLY="" local BASE="$1" local CATALOG="$2" local COMPONENT="" local -a COMPONENTS=() if [ ! -f "$CATALOG" ]; then echo >&2 "Bad component catalog file: \"$CATALOG\"" exit 2 fi { while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } do case "$REPLY" in \#* | "") ;; /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;; *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;; esac done } < "$CATALOG" for COMPONENT in "${COMPONENTS[@]}" do init_component "$COMPONENT" done } export -f init_components fi diff --git a/lib/scripts/getsettings b/lib/scripts/getsettings --- a/lib/scripts/getsettings +++ b/lib/scripts/getsettings @@ -1,137 +1,140 @@ # -*- shell-script -*- :mode=shellscript: # # Author: Makarius # # Static Isabelle environment for root of process tree. export ISABELLE_HOME export BASH_ENV="$ISABELLE_HOME/lib/scripts/getfunctions" source "$BASH_ENV" if [ -z "$ISABELLE_SETTINGS_PRESENT" ] then export ISABELLE_SETTINGS_PRESENT=true set -o allexport #sane environment defaults (notably on macOS) if [ "$ISABELLE_APP" = true -a -x /usr/libexec/path_helper ]; then eval $(/usr/libexec/path_helper -s) fi #Cygwin vs. POSIX if [ "$OSTYPE" = cygwin ] then unset INI_DIR TMPDIR="$(cygpath -u "$LOCALAPPDATA")/Temp" TMP="$TMPDIR" TEMP="$TMPDIR" if [ -z "$USER_HOME" ]; then USER_HOME="$(cygpath -u "$USERPROFILE")" fi CYGWIN_ROOT="$(platform_path "/")" ISABELLE_ROOT="$(platform_path "$ISABELLE_HOME")" ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")" export CLASSPATH="" else if [ -z "$USER_HOME" ]; then USER_HOME="$HOME" fi ISABELLE_ROOT="$ISABELLE_HOME" ISABELLE_CLASSPATH="$CLASSPATH" export CLASSPATH="" fi #init cumulative settings ISABELLE_FONTS="" ISABELLE_FONTS_HIDDEN="" ISABELLE_SCALA_SERVICES="" ISABELLE_DIRECTORIES="" #main executables ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" PATH="$ISABELLE_HOME/bin:$PATH" #platform source "$ISABELLE_HOME/lib/scripts/isabelle-platform" if [ -z "$ISABELLE_PLATFORM_FAMILY" ]; then echo 1>&2 "Failed to determine hardware and operating system type!" exit 2 fi if [ -z "$ISABELLE_IDENTIFIER" -a -f "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER" ] then ISABELLE_IDENTIFIER="$(cat "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER")" fi ISABELLE_NAME="${ISABELLE_IDENTIFIER:-Isabelle}" ISABELLE_HOSTNAME="$(hostname -s 2>/dev/null || uname -n)" # components ISABELLE_COMPONENTS="" ISABELLE_COMPONENTS_MISSING="" #main components init_component "$ISABELLE_HOME" [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin" if [ -d "$ISABELLE_HOME_USER" ]; then init_component "$ISABELLE_HOME_USER" else mkdir -p "$ISABELLE_HOME_USER" chmod $(umask -S) "$ISABELLE_HOME_USER" fi #POLYML_EXE -if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then - POLYML_EXE="$ML_HOME/poly.exe" -else - POLYML_EXE="$ML_HOME/poly" -fi +case "$ISABELLE_PLATFORM_FAMILY" in + windows*) + POLYML_EXE="$ML_HOME/poly.exe" + ;; + *) + POLYML_EXE="$ML_HOME/poly" + ;; +esac #ML system identifier if [ -z "$ML_PLATFORM" ]; then ML_IDENTIFIER="$ML_SYSTEM" else ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" fi #enforce ISABELLE_OCAMLFIND if [ -d "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin" ]; then ISABELLE_OCAMLFIND="$ISABELLE_HOME/lib/scripts/ocamlfind" fi #enforce ISABELLE_GHC if [ -f "$ISABELLE_STACK_ROOT/ISABELLE_GHC_EXE-$ISABELLE_PLATFORM_FAMILY" ]; then if [ -f "$(cat "$ISABELLE_STACK_ROOT/ISABELLE_GHC_EXE-$ISABELLE_PLATFORM_FAMILY")" ]; then ISABELLE_GHC="$ISABELLE_HOME/lib/scripts/ghc" ISABELLE_GHC_STACK=true fi fi #enforce JAVA_HOME if [ -d "$ISABELLE_JDK_HOME/jre" ] then export JAVA_HOME="$ISABELLE_JDK_HOME/jre" else export JAVA_HOME="$ISABELLE_JDK_HOME" fi if [ -e "$ISABELLE_SETUP_JAR" ]; then ISABELLE_SETUP_CLASSPATH="$(isabelle_jdk java -classpath "$(platform_path "$SCALA_INTERFACES:$ISABELLE_SETUP_JAR")" isabelle.setup.Setup classpath 2>/dev/null)" fi set +o allexport fi diff --git a/lib/scripts/java-gui-setup b/lib/scripts/java-gui-setup --- a/lib/scripts/java-gui-setup +++ b/lib/scripts/java-gui-setup @@ -1,11 +1,12 @@ #!/usr/bin/env bash # # java-gui-setup --- platform-specific setup for Java/Swing GUI applications -if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ] -then - JAVA_VERSION="$("$ISABELLE_JDK_HOME/bin/java" -version 2>&1 | head -n 1 | cut -d '"' -f2)" - JAVA_DOMAIN="com.azul.zulu.${JAVA_VERSION}.java" - defaults read "$JAVA_DOMAIN" AppleWindowTabbingMode >/dev/null 2>/dev/null || - defaults write "$JAVA_DOMAIN" AppleWindowTabbingMode manual >/dev/null 2>/dev/null -fi +case "$ISABELLE_PLATFORM_FAMILY" in + macos*) + JAVA_VERSION="$("$ISABELLE_JDK_HOME/bin/java" -version 2>&1 | head -n 1 | cut -d '"' -f2)" + JAVA_DOMAIN="com.azul.zulu.${JAVA_VERSION}.java" + defaults read "$JAVA_DOMAIN" AppleWindowTabbingMode >/dev/null 2>/dev/null || + defaults write "$JAVA_DOMAIN" AppleWindowTabbingMode manual >/dev/null 2>/dev/null + ;; +esac diff --git a/src/Pure/Admin/component_jdk.scala b/src/Pure/Admin/component_jdk.scala --- a/src/Pure/Admin/component_jdk.scala +++ b/src/Pure/Admin/component_jdk.scala @@ -1,165 +1,165 @@ /* Title: Pure/Admin/component_jdk.scala Author: Makarius Build Isabelle jdk component using downloads from Azul. */ package isabelle import java.nio.file.Files import java.nio.file.attribute.PosixFilePermission object Component_JDK { /* platform information */ sealed case class Download_Platform(name: String, url_template: String) { override def toString: String = name def url(base_url: String, jdk_version: String, zulu_version: String): String = base_url + "/" + url_template.replace("{V}", jdk_version).replace("{Z}", zulu_version) } val platforms: List[Download_Platform] = List( Download_Platform("arm64-darwin", "zulu{Z}-jdk{V}-macosx_aarch64.tar.gz"), Download_Platform("arm64-linux", "zulu{Z}-jdk{V}-linux_aarch64.tar.gz"), Download_Platform("x86_64-darwin", "zulu{Z}-jdk{V}-macosx_x64.tar.gz"), Download_Platform("x86_64-linux", "zulu{Z}-jdk{V}-linux_x64.tar.gz"), Download_Platform("x86_64-windows", "zulu{Z}-jdk{V}-win_x64.zip")) /* build jdk */ val default_base_url = "https://cdn.azul.com/zulu/bin" val default_jdk_version = "21.0.2" val default_zulu_version = "21.32.17-ca" def build_jdk( target_dir: Path = Path.current, base_url: String = default_base_url, jdk_version: String = default_jdk_version, zulu_version: String = default_zulu_version, progress: Progress = new Progress, ): Unit = { if (Platform.is_windows) error("Cannot build on Windows") /* component */ val component = "jdk-" + jdk_version val component_dir = Components.Directory(target_dir + Path.basic(component)).create(progress = progress) /* download */ for (platform <- platforms) { Isabelle_System.with_tmp_dir("download", component_dir.path.file) { dir => val url = platform.url(base_url, jdk_version, zulu_version) val name = Library.take_suffix(_ != '/', url.toList)._2.mkString val file = dir + Path.basic(name) Isabelle_System.download_file(url, file, progress = progress) val platform_dir = component_dir.path + Path.basic(platform.name) Isabelle_System.extract(file, platform_dir, strip = true) } } /* permissions */ for (file <- File.find_files(component_dir.path.file, include_dirs = true)) { val name = file.getName val path = file.toPath val perms = Files.getPosixFilePermissions(path) perms.add(PosixFilePermission.OWNER_READ) perms.add(PosixFilePermission.GROUP_READ) perms.add(PosixFilePermission.OTHERS_READ) perms.add(PosixFilePermission.OWNER_WRITE) if (File.is_dll(name) || File.is_exe(name) || file.isDirectory) { perms.add(PosixFilePermission.OWNER_EXECUTE) perms.add(PosixFilePermission.GROUP_EXECUTE) perms.add(PosixFilePermission.OTHERS_EXECUTE) } Files.setPosixFilePermissions(path, perms) } /* settings */ component_dir.write_settings(""" case "$ISABELLE_PLATFORM_FAMILY" in - linux) + linux*) ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64" ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; - windows) + windows*) ISABELLE_JAVA_PLATFORM="$ISABELLE_WINDOWS_PLATFORM64" ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; - macos) + macos*) if [ -n "$ISABELLE_APPLE_PLATFORM64" -a -d "$COMPONENT/$ISABELLE_APPLE_PLATFORM64" ] then ISABELLE_JAVA_PLATFORM="$ISABELLE_APPLE_PLATFORM64" else ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64" fi ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; esac """) /* README */ File.write(component_dir.README, """This is OpenJDK """ + jdk_version + """ based on downloads by Azul, see also https://www.azul.com/downloads/?package=jdk The main license is GPL2, but some modules are covered by other (more liberal) licenses, see legal/* for details. Linux, Windows, macOS all work uniformly, depending on platform-specific subdirectories. """) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("component_jdk", "build Isabelle jdk component using downloads from Azul", Scala_Project.here, { args => var target_dir = Path.current var base_url = default_base_url var jdk_version = default_jdk_version var zulu_version = default_zulu_version val getopts = Getopts(""" Usage: isabelle component_jdk [OPTIONS] Options are: -D DIR target directory (default ".") -U URL base URL (default: """" + default_base_url + """") -V NAME JDK version (default: """" + default_jdk_version + """") -Z NAME Zulu version (default: """" + default_zulu_version + """") Build Isabelle jdk component using downloads from Azul. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => base_url = arg), "V:" -> (arg => jdk_version = arg), "Z:" -> (arg => zulu_version = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_jdk(target_dir = target_dir, base_url = base_url, jdk_version = jdk_version, zulu_version = zulu_version, progress = progress) }) } diff --git a/src/Pure/System/isabelle_platform.scala b/src/Pure/System/isabelle_platform.scala --- a/src/Pure/System/isabelle_platform.scala +++ b/src/Pure/System/isabelle_platform.scala @@ -1,67 +1,65 @@ /* Title: Pure/System/isabelle_platform.scala Author: Makarius General hardware and operating system type for Isabelle system tools. */ package isabelle object Isabelle_Platform { val settings: List[String] = List( "ISABELLE_PLATFORM_FAMILY", "ISABELLE_PLATFORM64", "ISABELLE_WINDOWS_PLATFORM32", "ISABELLE_WINDOWS_PLATFORM64", "ISABELLE_APPLE_PLATFORM64") def apply(ssh: Option[SSH.Session] = None): Isabelle_Platform = { ssh match { case None => new Isabelle_Platform(settings.map(a => (a, Isabelle_System.getenv(a)))) case Some(ssh) => val script = File.read(Path.explode("~~/lib/scripts/isabelle-platform")) + "\n" + settings.map(a => "echo \"" + Bash.string(a) + "=$" + Bash.string(a) + "\"").mkString("\n") val result = ssh.execute("bash -c " + Bash.string(script)).check new Isabelle_Platform( result.out_lines.map(line => Properties.Eq.unapply(line) getOrElse error("Bad output: " + quote(result.out)))) } } lazy val self: Isabelle_Platform = apply() } class Isabelle_Platform private(val settings: List[(String, String)]) { private def get(name: String): String = settings.collectFirst({ case (a, b) if a == name => b }). getOrElse(error("Bad platform settings variable: " + quote(name))) val ISABELLE_PLATFORM64: String = get("ISABELLE_PLATFORM64") val ISABELLE_WINDOWS_PLATFORM64: String = get("ISABELLE_WINDOWS_PLATFORM64") val ISABELLE_APPLE_PLATFORM64: String = get("ISABELLE_APPLE_PLATFORM64") def is_arm: Boolean = ISABELLE_PLATFORM64.startsWith("arm64-") || ISABELLE_APPLE_PLATFORM64.startsWith("arm64-") val ISABELLE_PLATFORM_FAMILY: String = { val family0 = get("ISABELLE_PLATFORM_FAMILY") if (family0 == "linux" && is_arm) "linux_arm" else family0 } - def is_linux: Boolean = - ISABELLE_PLATFORM_FAMILY == "linux" || - ISABELLE_PLATFORM_FAMILY == "linux_arm" - def is_macos: Boolean = ISABELLE_PLATFORM_FAMILY == "macos" - def is_windows: Boolean = ISABELLE_PLATFORM_FAMILY == "windows" + def is_linux: Boolean = ISABELLE_PLATFORM_FAMILY.startsWith("linux") + def is_macos: Boolean = ISABELLE_PLATFORM_FAMILY.startsWith("macos") + def is_windows: Boolean = ISABELLE_PLATFORM_FAMILY.startsWith("windows") def arch_64: String = if (is_arm) "arm64" else "x86_64" def arch_64_32: String = if (is_arm) "arm64_32" else "x86_64_32" def os_name: String = if (is_macos) "darwin" else ISABELLE_PLATFORM_FAMILY override def toString: String = ISABELLE_PLATFORM_FAMILY } diff --git a/src/Tools/VSCode/src/component_vscodium.scala b/src/Tools/VSCode/src/component_vscodium.scala --- a/src/Tools/VSCode/src/component_vscodium.scala +++ b/src/Tools/VSCode/src/component_vscodium.scala @@ -1,462 +1,465 @@ /* Title: Tools/VSCode/src/component_vscodium.scala Author: Makarius Build the Isabelle system component for VSCodium: cross-compilation for all platforms. */ package isabelle.vscode import isabelle._ import java.security.MessageDigest import java.util.Base64 object Component_VSCodium { /* global parameters */ lazy val version: String = Isabelle_System.getenv_strict("ISABELLE_VSCODE_VERSION") val vscodium_repository = "https://github.com/VSCodium/vscodium.git" val vscodium_download = "https://github.com/VSCodium/vscodium/releases/download" private val resources = Path.explode("resources") /* Isabelle symbols (static subset only) */ lazy val symbols: Symbol.Symbols = Symbol.Symbols.make(File.read(Path.explode("~~/etc/symbols"))) def make_symbols(): File.Content = { val symbols_js = JSON.Format.pretty_print( for (entry <- symbols.entries) yield JSON.Object( "symbol" -> entry.symbol, "name" -> entry.name, "abbrevs" -> entry.abbrevs) ++ JSON.optional("code", entry.code)) File.content(Path.explode("symbols.json"), symbols_js) } def make_isabelle_encoding(header: String): File.Content = { val symbols_js = JSON.Format.pretty_print( for (entry <- symbols.entries; code <- entry.code) yield JSON.Object("symbol" -> entry.symbol, "code" -> code)) val path = Path.explode("isabelle_encoding.ts") val body = File.read(Path.explode("$ISABELLE_VSCODE_HOME/patches") + path) .replace("[/*symbols*/]", symbols_js) File.content(path, header + "\n" + body) } /* platform info */ sealed case class Platform_Info( platform: Platform.Family, download_template: String, build_name: String, env: List[String] ) { def primary: Boolean = platform == Platform.Family.linux def download_name: String = "VSCodium-" + download_template.replace("{VERSION}", version) def download_ext: String = if (download_template.endsWith(".zip")) "zip" else "tar.gz" def download(dir: Path, progress: Progress = new Progress): Unit = { Isabelle_System.with_tmp_file("download", ext = download_ext) { download_file => Isabelle_System.download_file(vscodium_download + "/" + version + "/" + download_name, download_file, progress = progress) progress.echo("Extract ...") Isabelle_System.extract(download_file, dir) } } def get_vscodium_repository(build_dir: Path, progress: Progress = new Progress): Unit = { progress.echo("Getting VSCodium repository ...") Isabelle_System.bash( List( "set -e", "git clone -n " + Bash.string(vscodium_repository) + " .", "git checkout -q " + Bash.string(version) ).mkString("\n"), cwd = build_dir.file).check progress.echo("Getting VSCode repository ...") Isabelle_System.bash(environment + "\n" + "./get_repo.sh", cwd = build_dir.file).check } def platform_dir(dir: Path): Path = { val platform_name = if (platform == Platform.Family.windows) Platform.Family.native(platform) else Platform.Family.standard(platform) dir + Path.explode(platform_name) } def build_dir(dir: Path): Path = dir + Path.explode(build_name) def environment: String = (("MS_TAG=" + Bash.string(version)) :: "SHOULD_BUILD=yes" :: "VSCODE_ARCH=x64" :: env) .map(s => "export " + s + "\n").mkString def patch_sources(base_dir: Path): String = { val dir = base_dir + Path.explode("vscode") Isabelle_System.with_copy_dir(dir, dir.orig) { // macos icns for (name <- Seq("build/lib/electron.js", "build/lib/electron.ts")) { File.change(dir + Path.explode(name), strict = true) { _.replace("""'resources/darwin/' + icon + '.icns'""", """'resources/darwin/' + icon.toLowerCase() + '.icns'""") } } // isabelle_encoding.ts { val common_dir = dir + Path.explode("src/vs/workbench/services/textfile/common") val header = split_lines(File.read(common_dir + Path.explode("encoding.ts"))) .takeWhile(_.trim.nonEmpty) make_isabelle_encoding(cat_lines(header)).write(common_dir) } // explicit patches { val patches_dir = Path.explode("$ISABELLE_VSCODE_HOME/patches") for (name <- Seq("cli", "isabelle_encoding", "no_ocaml_icons")) { val path = patches_dir + Path.explode(name).patch Isabelle_System.bash("patch -p1 < " + File.bash_path(path), cwd = dir.file).check } } Isabelle_System.make_patch(base_dir, dir.base.orig, dir.base) } } def patch_resources(base_dir: Path): String = { val dir = base_dir + resources val patch = Isabelle_System.with_copy_dir(dir, dir.orig) { val fonts_dir = dir + Path.explode("app/out/vs/base/browser/ui/fonts") HTML.init_fonts(fonts_dir.dir) make_symbols().write(fonts_dir) val workbench_css = dir + Path.explode("app/out/vs/workbench/workbench.desktop.main.css") val checksum1 = file_checksum(workbench_css) File.append(workbench_css, "\n\n" + HTML.fonts_css_dir(prefix = "../base/browser/ui")) val checksum2 = file_checksum(workbench_css) val file_name = workbench_css.file_name File.change_lines(dir + Path.explode("app/product.json")) { _.map(line => if (line.containsSlice(file_name) && line.contains(checksum1)) { line.replace(checksum1, checksum2) } else line) } Isabelle_System.make_patch(dir.dir, dir.orig.base, dir.base) } val app_dir = dir + Path.explode("app") val vscodium_app_dir = dir + Path.explode("vscodium") Isabelle_System.move_file(app_dir, vscodium_app_dir) Isabelle_System.make_directory(app_dir) if ((vscodium_app_dir + resources).is_dir) { Isabelle_System.copy_dir(vscodium_app_dir + resources, app_dir) } patch } def init_resources(base_dir: Path): Path = { val dir = base_dir + resources if (platform == Platform.Family.macos) { Isabelle_System.symlink(Path.explode("VSCodium.app/Contents/Resources"), dir) } dir } def setup_node(target_dir: Path, progress: Progress): Unit = { Isabelle_System.with_tmp_dir("download") { download_dir => download(download_dir, progress = progress) val dir1 = init_resources(download_dir) val dir2 = init_resources(target_dir) for (name <- Seq("app/node_modules.asar", "app/node_modules.asar.unpacked")) { val path = Path.explode(name) Isabelle_System.rm_tree(dir2 + path) Isabelle_System.copy_dir(dir1 + path, dir2 + path) } } } def setup_electron(dir: Path): Unit = { val electron = Path.explode("electron") platform match { case Platform.Family.linux | Platform.Family.linux_arm => Isabelle_System.move_file(dir + Path.explode("codium"), dir + electron) case Platform.Family.windows => Isabelle_System.move_file(dir + Path.explode("VSCodium.exe"), dir + electron.exe) Isabelle_System.move_file( dir + Path.explode("VSCodium.VisualElementsManifest.xml"), dir + Path.explode("electron.VisualElementsManifest.xml")) case Platform.Family.macos => } } def setup_executables(dir: Path): Unit = { Isabelle_System.rm_tree(dir + Path.explode("bin")) if (platform == Platform.Family.windows) { val files = File.find_files(dir.file, pred = { file => val name = file.getName File.is_dll(name) || File.is_exe(name) || File.is_node(name) }) files.foreach(file => File.set_executable(File.path(file))) Isabelle_System.bash("chmod -R o-w " + File.bash_path(dir)).check } } } // see https://github.com/microsoft/vscode/blob/main/build/gulpfile.vscode.js // function computeChecksum(filename) private def file_checksum(path: Path): String = { val digest = MessageDigest.getInstance("MD5") digest.update(Bytes.read(path).array) Bytes(Base64.getEncoder.encode(digest.digest())) .text.replaceAll("=", "") } private val platform_infos: Map[Platform.Family, Platform_Info] = Iterator( Platform_Info(Platform.Family.linux, "linux-x64-{VERSION}.tar.gz", "VSCode-linux-x64", List("OS_NAME=linux", "SKIP_LINUX_PACKAGES=True")), Platform_Info(Platform.Family.linux_arm, "linux-arm64-{VERSION}.tar.gz", "VSCode-linux-arm64", List("OS_NAME=linux", "SKIP_LINUX_PACKAGES=True", "VSCODE_ARCH=arm64")), Platform_Info(Platform.Family.macos, "darwin-x64-{VERSION}.zip", "VSCode-darwin-x64", List("OS_NAME=osx")), Platform_Info(Platform.Family.windows, "win32-x64-{VERSION}.zip", "VSCode-win32-x64", List("OS_NAME=windows", "SHOULD_BUILD_ZIP=no", "SHOULD_BUILD_EXE_SYS=no", "SHOULD_BUILD_EXE_USR=no", "SHOULD_BUILD_MSI=no", "SHOULD_BUILD_MSI_NOUP=no"))) .map(info => info.platform -> info).toMap def the_platform_info(platform: Platform.Family): Platform_Info = platform_infos.getOrElse(platform, error("No platform info for " + quote(platform.toString))) def linux_platform_info: Platform_Info = the_platform_info(Platform.Family.linux) /* check system */ def check_system(platforms: List[Platform.Family]): Unit = { if (Platform.family != Platform.Family.linux) error("Not a Linux/x86_64 system") Isabelle_System.require_command("git") Isabelle_System.require_command("node") Isabelle_System.require_command("yarn") Isabelle_System.require_command("jq") if (platforms.contains(Platform.Family.windows)) { Isabelle_System.require_command("wine") } } /* original repository clones and patches */ def vscodium_patch(progress: Progress = new Progress): String = { val platform_info = linux_platform_info check_system(List(platform_info.platform)) Isabelle_System.with_tmp_dir("build") { build_dir => platform_info.get_vscodium_repository(build_dir, progress = progress) val vscode_dir = build_dir + Path.explode("vscode") progress.echo("Prepare ...") Isabelle_System.with_copy_dir(vscode_dir, vscode_dir.orig) { progress.bash( List( "set -e", platform_info.environment, "./prepare_vscode.sh", // enforce binary diff of code.xpm "cp vscode/resources/linux/code.png vscode/resources/linux/rpm/code.xpm" ).mkString("\n"), cwd = build_dir.file, echo = progress.verbose).check Isabelle_System.make_patch(build_dir, vscode_dir.orig.base, vscode_dir.base, diff_options = "--exclude=.git --exclude=node_modules") } } } /* build vscodium */ def default_platforms: List[Platform.Family] = Platform.Family.list def component_vscodium( target_dir: Path = Path.current, platforms: List[Platform.Family] = default_platforms, progress: Progress = new Progress ): Unit = { check_system(platforms) /* component */ val component_name = "vscodium-" + version val component_dir = Components.Directory(target_dir + Path.explode(component_name)).create(progress = progress) /* patches */ progress.echo("\n* Building patches:") val patches_dir = Isabelle_System.new_directory(component_dir.path + Path.explode("patches")) def write_patch(name: String, patch: String): Unit = File.write(patches_dir + Path.explode(name).patch, patch) write_patch("01-vscodium", vscodium_patch(progress = progress)) /* build */ for (platform <- platforms) yield { val platform_info = the_platform_info(platform) Isabelle_System.with_tmp_dir("build") { build_dir => progress.echo("\n* Building " + platform + ":") platform_info.get_vscodium_repository(build_dir, progress = progress) val sources_patch = platform_info.patch_sources(build_dir) if (platform_info.primary) write_patch("02-isabelle_sources", sources_patch) progress.echo("Build ...") progress.bash(platform_info.environment + "\n" + "./build.sh", cwd = build_dir.file, echo = progress.verbose).check if (platform_info.primary) { Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path) } val platform_dir = platform_info.platform_dir(component_dir.path) Isabelle_System.copy_dir(platform_info.build_dir(build_dir), platform_dir) platform_info.setup_node(platform_dir, progress) platform_info.setup_electron(platform_dir) val resources_patch = platform_info.patch_resources(platform_dir) if (platform_info.primary) write_patch("03-isabelle_resources", resources_patch) Isabelle_System.copy_file( build_dir + Path.explode("vscode/node_modules/electron/dist/resources/default_app.asar"), platform_dir + resources) platform_info.setup_executables(platform_dir) } } Isabelle_System.bash("gzip *.patch", cwd = patches_dir.file).check /* settings */ component_dir.write_settings(""" ISABELLE_VSCODIUM_HOME="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}" -if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ]; then - ISABELLE_VSCODIUM_ELECTRON="$ISABELLE_VSCODIUM_HOME/VSCodium.app/Contents/MacOS/Electron" - ISABELLE_VSCODIUM_RESOURCES="$ISABELLE_VSCODIUM_HOME/VSCodium.app/Contents/Resources" -else - ISABELLE_VSCODIUM_ELECTRON="$ISABELLE_VSCODIUM_HOME/electron" - ISABELLE_VSCODIUM_RESOURCES="$ISABELLE_VSCODIUM_HOME/resources" -fi +case "$ISABELLE_PLATFORM_FAMILY" in + "macos"*) + ISABELLE_VSCODIUM_ELECTRON="$ISABELLE_VSCODIUM_HOME/VSCodium.app/Contents/MacOS/Electron" + ISABELLE_VSCODIUM_RESOURCES="$ISABELLE_VSCODIUM_HOME/VSCodium.app/Contents/Resources" + ;; + *) + ISABELLE_VSCODIUM_ELECTRON="$ISABELLE_VSCODIUM_HOME/electron" + ISABELLE_VSCODIUM_RESOURCES="$ISABELLE_VSCODIUM_HOME/resources" + ;; +esac """) /* README */ File.write(component_dir.README, "This is VSCodium " + version + " from " + vscodium_repository + """ It has been built from sources using "isabelle component_vscodium". This applies a few changes required for Isabelle/VSCode, see "patches" directory for a formal record. Makarius """ + Date.Format.date(Date.now()) + "\n") } /* Isabelle tool wrappers */ val isabelle_tool1 = Isabelle_Tool("component_vscodium", "build component for VSCodium", Scala_Project.here, { args => var target_dir = Path.current var platforms = default_platforms var verbose = false val getopts = Getopts(""" Usage: component_vscodium [OPTIONS] Options are: -D DIR target directory (default ".") -p NAMES platform families (default: """ + quote(platforms.mkString(",")) + """) -v verbose Build VSCodium from sources and turn it into an Isabelle component. The build platform needs to be Linux with nodejs/yarn, jq, and wine for targeting Windows. """, "D:" -> (arg => target_dir = Path.explode(arg)), "p:" -> (arg => platforms = space_explode(',', arg).map(Platform.Family.parse)), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress(verbose = verbose) component_vscodium(target_dir = target_dir, platforms = platforms, progress = progress) }) val isabelle_tool2 = Isabelle_Tool("vscode_patch", "patch VSCode source tree", Scala_Project.here, { args => var base_dir = Path.current val getopts = Getopts(""" Usage: vscode_patch [OPTIONS] Options are: -D DIR base directory (default ".") Patch original VSCode source tree for use with Isabelle/VSCode. """, "D:" -> (arg => base_dir = Path.explode(arg))) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val platform_info = the_platform_info(Platform.family) platform_info.patch_sources(base_dir) }) }