diff --git a/etc/settings b/etc/settings --- a/etc/settings +++ b/etc/settings @@ -1,189 +1,196 @@ # -*- 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" + + +### ### Misc settings ### ISABELLE_GNUPLOT="gnuplot" ISABELLE_FONTFORGE="fontforge" #ISABELLE_SMLNJ="/usr/bin/sml" #ISABELLE_SWIPL="/usr/bin/swipl" diff --git a/src/Pure/Tools/dotnet_setup.scala b/src/Pure/Tools/dotnet_setup.scala --- a/src/Pure/Tools/dotnet_setup.scala +++ b/src/Pure/Tools/dotnet_setup.scala @@ -1,203 +1,204 @@ /* Title: Pure/Tools/dotnet_setup.scala Author: Makarius Dynamic setup of dotnet component. */ package isabelle object Dotnet_Setup { /* platforms */ sealed case class Platform_Info( name: String, os: String = "", arch: String = "x64", ext: String = "sh", exec: String = "bash", check: () => Unit = () => () ) { val family: Platform.Family = Platform.Family.from_platform(name) } private val all_platforms = List( Platform_Info("arm64-linux", os = "linux", arch = "arm64"), Platform_Info("x86_64-linux", os = "linux"), Platform_Info("arm64-darwin", os = "osx", arch = "arm64"), Platform_Info("x86_64-darwin", os = "osx"), Platform_Info("x86_64-windows", ext = "ps1", exec = "powershell -ExecutionPolicy ByPass", check = () => Isabelle_System.require_command("powershell", "-NoProfile -Command Out-Null"))) def check_platform_spec(spec: String): String = { val all_specs = Library.distinct(all_platforms.map(_.family.toString) ::: all_platforms.map(_.name)) if (all_specs.contains(spec)) spec else { error("Bad platform specification " + quote(spec) + "\n expected " + commas_quote(all_specs)) } } /* dotnet download and setup */ def default_platform: String = { val self = Isabelle_Platform.self proper_string(self.ISABELLE_WINDOWS_PLATFORM64).getOrElse( proper_string(self.ISABELLE_APPLE_PLATFORM64).getOrElse( self.ISABELLE_PLATFORM64)) } def default_target_dir: Path = Components.default_components_base def default_install_url: String = "https://dot.net/v1/dotnet-install" - def default_version: String = "8.0.203" + def default_version: String = Isabelle_System.getenv_strict("ISABELLE_DOTNET_VERSION") def dotnet_setup( platform_spec: String = default_platform, target_dir: Path = default_target_dir, install_url: String = default_install_url, version: String = default_version, force: Boolean = false, dry_run: Boolean = false, progress: Progress = new Progress ): Unit = { check_platform_spec(platform_spec) for { platform <- all_platforms if platform.family.toString == platform_spec || platform.name == platform_spec } { progress.expose_interrupt() /* component directory */ val component_dir = Components.Directory( target_dir + Path.explode(if (version.isEmpty) "dotnet-latest" else "dotnet-" + version)) if (!dry_run) { progress.echo("Component " + component_dir) Isabelle_System.make_directory(component_dir.etc) component_dir.write_settings(""" ISABELLE_DOTNET_ROOT="$COMPONENT" if [ -n "$ISABELLE_WINDOWS_PLATFORM64" -a -d "$ISABELLE_DOTNET_ROOT/$ISABELLE_WINDOWS_PLATFORM64" ]; then ISABELLE_DOTNET="$ISABELLE_DOTNET_ROOT/$ISABELLE_WINDOWS_PLATFORM64/dotnet.exe" elif [ -n "$ISABELLE_APPLE_PLATFORM64" -a -d "$ISABELLE_DOTNET_ROOT/$ISABELLE_APPLE_PLATFORM64" ]; then ISABELLE_DOTNET="$ISABELLE_DOTNET_ROOT/$ISABELLE_APPLE_PLATFORM64/dotnet" elif [ -d "$ISABELLE_DOTNET_ROOT/$ISABELLE_PLATFORM64" ]; then ISABELLE_DOTNET="$ISABELLE_DOTNET_ROOT/$ISABELLE_PLATFORM64/dotnet" fi DOTNET_CLI_TELEMETRY_OPTOUT="true" DOTNET_CLI_HOME="$(platform_path "$ISABELLE_HOME_USER/dotnet")" """) File.write(component_dir.README, """This installation of Dotnet has been produced via "isabelle dotnet_setup". Makarius """ + Date.Format.date(Date.now()) + "\n") for (old <- proper_string(Isabelle_System.getenv("ISABELLE_DOTNET_ROOT"))) { Components.update_components(false, Path.explode(old)) } Components.update_components(true, component_dir.path) } /* platform directory */ Isabelle_System.with_tmp_file("install", ext = platform.ext) { install => Isabelle_System.download_file(install_url + "." + platform.ext, install) val platform_dir = component_dir.path + Path.explode(platform.name) if (platform_dir.is_dir && !force) { progress.echo_warning("Platform " + platform.name + " already installed") } else { progress.echo("Platform " + platform.name + " ...") platform.check() if (platform_dir.is_dir && force) Isabelle_System.rm_tree(platform_dir) val script = platform.exec + " " + File.bash_platform_path(install) + if_proper(version, " -Version " + Bash.string(version)) + " -Architecture " + Bash.string(platform.arch) + if_proper(platform.os, " -OS " + Bash.string(platform.os)) + " -InstallDir " + Bash.string(platform.name) + (if (dry_run) " -DryRun" else "") + " -NoPath" progress.bash(script, echo = progress.verbose, cwd = if (dry_run) null else component_dir.path.file).check for (exe <- File.find_files(platform_dir.file, pred = _.getName.endsWith(".exe"))) { File.set_executable(File.path(exe)) } } } } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("dotnet_setup", "dynamic setup of dotnet component (for Fsharp)", Scala_Project.here, { args => var target_dir = default_target_dir var install_url = default_install_url var version = default_version var force = false var dry_run = false var platforms = List(default_platform) var verbose = false val getopts = Getopts(""" Usage: isabelle dotnet_setup [OPTIONS] Options are: -D DIR target directory (default: """ + default_target_dir.expand + """) -I URL URL for install script without extension (default: """ + quote(default_install_url) + """) - -V VERSION version (empty means "latest", default: """ + quote(default_version) + """) + -V VERSION version (empty means "latest", + default: ISABELLE_DOTNET_VERSION=""" + quote(default_version) + """) -f force fresh installation of specified platforms -n dry run: try download without installation -p PLATFORMS comma-separated list of platform specifications, as family or formal name (default: """ + quote(default_platform) + """) -v verbose Download the Dotnet / Fsharp platform and configure it as Isabelle component. See also: https://fsharp.org https://learn.microsoft.com/en-us/dotnet/core/tools/dotnet-install-script https://learn.microsoft.com/en-us/dotnet/core/tools/telemetry """, "D:" -> (arg => target_dir = Path.explode(arg)), "I:" -> (arg => install_url = arg), "V:" -> (arg => version = arg), "f" -> (_ => force = true), "n" -> (_ => dry_run = true), "p:" -> (arg => platforms = space_explode(',', arg).map(check_platform_spec)), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress(verbose = verbose) for (platform <- platforms) { dotnet_setup(platform_spec = platform, target_dir = target_dir, install_url = install_url, version = version, force = force, dry_run = dry_run, progress = progress) } }) }