# HG changeset patch # User wenzelm # Date 1607862544 -3600 # Node ID bd2269b6cd9957de048096d1e1d8bf9b9528bd0d # Parent fbdadf5760c263e90860ffeee3aa11531fd1dd96 updated "macOS" terminology: current Big Sur is already version 11; diff -r fbdadf5760c2 -r bd2269b6cd99 Admin/MacOS/README --- a/Admin/MacOS/README Sun Dec 13 13:16:07 2020 +0100 +++ b/Admin/MacOS/README Sun Dec 13 13:29:04 2020 +0100 @@ -1,5 +1,5 @@ -Isabelle/JVM application bundle for Mac OS X -============================================ +Isabelle/JVM application bundle for macOS +========================================= * http://java.net/projects/appbundler diff -r fbdadf5760c2 -r bd2269b6cd99 Admin/PLATFORMS --- a/Admin/PLATFORMS Sun Dec 13 13:16:07 2020 +0100 +++ b/Admin/PLATFORMS Sun Dec 13 13:29:04 2020 +0100 @@ -44,7 +44,7 @@ Old (partial support): - x86_64-darwin Mac OS X 10.11 El Capitan (macbroy2 MacPro4,1) + x86_64-darwin OS X 10.11 El Capitan (macbroy2 MacPro4,1) New (experimental): @@ -55,7 +55,7 @@ -------------------------------------- Isabelle requires 64 bit hardware running a 64 bit operating -system. Windows and Mac OS X allow x86 executables as well, but for +system. Windows and macOS allow x86 executables as well, but for Linux this requires separate installation of 32 bit shared libraries. The POSIX emulation on Windows via Cygwin64 works exclusively for x86_64. @@ -89,7 +89,7 @@ ISABELLE_WINDOWS_PLATFORM64 ISABELLE_WINDOWS_PLATFORM32 -These are always empty on Linux and Mac OS X, and non-empty on +These are always empty on Linux and macOS, and non-empty on Windows. They can be used like this to prefer native Windows and then Unix (first 64 bit second 32 bit): @@ -116,12 +116,12 @@ Known problems -------------- -* Mac OS X: If MacPorts is installed there is some danger that +* macOS: If MacPorts is installed there is some danger that accidental references to its shared libraries are created (e.g. libgmp). Use otool -L to check if compiled binaries also work without MacPorts. -* Mac OS X: If MacPorts is installed and its version of Perl takes +* macOS: If MacPorts is installed and its version of Perl takes precedence over /usr/bin/perl in the PATH, then the end-user needs to take care of installing extra modules, e.g. for HTTP support. Such add-ons are usually included in Apple's /usr/bin/perl by diff -r fbdadf5760c2 -r bd2269b6cd99 Admin/Release/CHECKLIST --- a/Admin/Release/CHECKLIST Sun Dec 13 13:16:07 2020 +0100 +++ b/Admin/Release/CHECKLIST Sun Dec 13 13:29:04 2020 +0100 @@ -45,9 +45,9 @@ - check doc/Contents, src/Tools/jEdit/dist/doc/Contents; -- test old HD display: Linux, Windows, Mac OS X; +- test old HD display: Linux, Windows, macOS; -- Mac OS X: check recent MacTeX; +- macOS: check recent MacTeX; - Windows: check recent MiKTeX; @@ -69,7 +69,7 @@ Packaging ========= -- Mac OS X: provide "gnutar" executable via shell PATH +- macOS: provide "gnutar" executable via shell PATH (e.g. copy of /usr/bin/gnutar from Mountain Lion) - fully-automated packaging (e.g. on lxcisa0): diff -r fbdadf5760c2 -r bd2269b6cd99 lib/scripts/getfunctions --- a/lib/scripts/getfunctions Sun Dec 13 13:16:07 2020 +0100 +++ b/lib/scripts/getfunctions Sun Dec 13 13:29:04 2020 +0100 @@ -20,7 +20,7 @@ fi export -f platform_path standard_path -#GNU tar (notably on Mac OS X) +#GNU tar (notably on macOS) if type -p gnutar >/dev/null then function tar() { gnutar "$@"; } diff -r fbdadf5760c2 -r bd2269b6cd99 lib/scripts/getsettings --- a/lib/scripts/getsettings Sun Dec 13 13:16:07 2020 +0100 +++ b/lib/scripts/getsettings Sun Dec 13 13:29:04 2020 +0100 @@ -17,7 +17,7 @@ set -o allexport -#sane environment defaults (notably on Mac OS X) +#sane environment defaults (notably on macOS) if [ "$ISABELLE_APP" = true -a -x /usr/libexec/path_helper ]; then eval $(/usr/libexec/path_helper -s) fi diff -r fbdadf5760c2 -r bd2269b6cd99 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Sun Dec 13 13:16:07 2020 +0100 +++ b/src/Doc/JEdit/JEdit.thy Sun Dec 13 13:29:04 2020 +0100 @@ -49,7 +49,7 @@ experts. Technically, Isabelle/jEdit consists of the original jEdit code base with minimal patches and a special plugin for Isabelle. This is integrated as a desktop application for the main operating system - families: Linux, Windows, Mac OS X. + families: Linux, Windows, macOS. End-users of Isabelle download and run a standalone application that exposes jEdit as a text editor on the surface. Thus there is occasionally a tendency @@ -98,7 +98,7 @@ underlines, hyperlinks, popup windows, icons, clickable output etc. Using the mouse together with the modifier key \<^verbatim>\CONTROL\ (Linux, Windows) - or \<^verbatim>\COMMAND\ (Mac OS X) exposes formal content via tooltips and/or + or \<^verbatim>\COMMAND\ (macOS) exposes formal content via tooltips and/or hyperlinks (see also \secref{sec:tooltips-hyperlinks}). Output (in popups etc.) may be explored recursively, using the same techniques as in the editor source buffer. @@ -219,7 +219,7 @@ text \ Isabelle/jEdit is normally invoked as a single-instance desktop application, - based on platform-specific executables for Linux, Windows, Mac OS X. + based on platform-specific executables for Linux, Windows, macOS. It is also possible to invoke the Prover IDE on the command-line, with some extra options and environment settings. The command-line usage of @{tool_def @@ -338,7 +338,7 @@ \<^descr>[Windows:] Regular \<^emph>\Windows\ is used by default. - \<^descr>[Mac OS X:] Regular \<^emph>\Mac OS X\ is used by default. + \<^descr>[macOS:] Regular \<^emph>\Mac OS X\ is used by default. The bundled \<^emph>\MacOSX\ plugin provides various functions that are expected from applications on that particular platform: quit from menu or dock, @@ -1241,7 +1241,7 @@ text \ Formally processed text (prover input or output) contains rich markup that can be explored by using the \<^verbatim>\CONTROL\ modifier key on Linux and Windows, - or \<^verbatim>\COMMAND\ on Mac OS X. Hovering with the mouse while the modifier is + or \<^verbatim>\COMMAND\ on macOS. Hovering with the mouse while the modifier is pressed reveals a \<^emph>\tooltip\ (grey box over the text with a yellow popup) and/or a \<^emph>\hyperlink\ (black rectangle over the text with change of mouse pointer); see also \figref{fig:tooltip}. @@ -2178,14 +2178,14 @@ \<^bold>\Workaround:\ Rebind keys via \<^emph>\Global Options~/ Shortcuts\. - \<^item> \<^bold>\Problem:\ The Mac OS X key sequence \<^verbatim>\COMMAND+COMMA\ for application + \<^item> \<^bold>\Problem:\ The macOS key sequence \<^verbatim>\COMMAND+COMMA\ for application \<^emph>\Preferences\ is in conflict with the jEdit default keyboard shortcut for \<^emph>\Incremental Search Bar\ (action @{action_ref "quick-search"}). \<^bold>\Workaround:\ Rebind key via \<^emph>\Global Options~/ Shortcuts\ according to the national keyboard layout, e.g.\ \<^verbatim>\COMMAND+SLASH\ on English ones. - \<^item> \<^bold>\Problem:\ On Mac OS X with native Apple look-and-feel, some exotic + \<^item> \<^bold>\Problem:\ On macOS with native Apple look-and-feel, some exotic national keyboards may cause a conflict of menu accelerator keys with regular jEdit key bindings. This leads to duplicate execution of the corresponding jEdit action. @@ -2193,12 +2193,12 @@ \<^bold>\Workaround:\ Disable the native Apple menu bar via Java runtime option \<^verbatim>\-Dapple.laf.useScreenMenuBar=false\. - \<^item> \<^bold>\Problem:\ Mac OS X system fonts sometimes lead to character drop-outs in + \<^item> \<^bold>\Problem:\ macOS system fonts sometimes lead to character drop-outs in the main text area. \<^bold>\Workaround:\ Use the default \<^verbatim>\Isabelle DejaVu\ fonts. - \<^item> \<^bold>\Problem:\ On Mac OS X the Java printer dialog sometimes does not work. + \<^item> \<^bold>\Problem:\ On macOS the Java printer dialog sometimes does not work. \<^bold>\Workaround:\ Use action @{action isabelle.draft} and print via the Web browser. @@ -2241,10 +2241,10 @@ \<^item> \<^bold>\Problem:\ Full-screen mode via jEdit action @{action_ref "toggle-full-screen"} (default keyboard shortcut \<^verbatim>\F11\) works on Windows, - but not on Mac OS X or various Linux/X11 window managers. + but not on macOS or various Linux/X11 window managers. \<^bold>\Workaround:\ Use native full-screen control of the window manager (notably - on Mac OS X). + on macOS). \<^item> \<^bold>\Problem:\ Heap space of the JVM may fill up and render the Prover IDE unresponsive, e.g.\ when editing big Isabelle sessions with many theories. diff -r fbdadf5760c2 -r bd2269b6cd99 src/Pure/Admin/build_jdk.scala --- a/src/Pure/Admin/build_jdk.scala Sun Dec 13 13:16:07 2020 +0100 +++ b/src/Pure/Admin/build_jdk.scala Sun Dec 13 13:29:04 2020 +0100 @@ -225,7 +225,7 @@ -D DIR target directory (default ".") Build jdk component from tar.gz archives, with original jdk archives - for Linux (arm64 and x86_64), Windows (x86_64), Mac OS X (x86_64). + for Linux (arm64 and x86_64), Windows (x86_64), macOS (x86_64). """, "D:" -> (arg => target_dir = Path.explode(arg))) diff -r fbdadf5760c2 -r bd2269b6cd99 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Sun Dec 13 13:16:07 2020 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Sun Dec 13 13:29:04 2020 +0100 @@ -237,7 +237,7 @@ " -e ISABELLE_SWIPL=swipl", args = "-N -a -d '~~/src/Benchmarks'", detect = Build_Log.Prop.build_tags + " = " + SQL.string("Benchmarks")), - Remote_Build("Mac OS X 10.14 Mojave (Old)", "lapnipkow3", + Remote_Build("macOS 10.14 Mojave (Old)", "lapnipkow3", options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true -p pide_session=false", self_update = true, args = "-a -d '~~/src/Benchmarks'"), Remote_Build("AFP old bulky", "lrzcloud1", self_update = true, @@ -264,19 +264,19 @@ detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), - Remote_Build("Poly/ML 5.7 Mac OS X", "macbroy2", + Remote_Build("Poly/ML 5.7 macOS", "macbroy2", history_base = "37074e22e8be", options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'", args = "-a", detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7")), - Remote_Build("Poly/ML 5.7.1 Mac OS X", "macbroy2", + Remote_Build("Poly/ML 5.7.1 macOS", "macbroy2", history_base = "a9d5b59c3e12", options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'", args = "-a", detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), - Remote_Build("Mac OS X", "macbroy2", + Remote_Build("macOS", "macbroy2", options = "-m32 -M8" + " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" + " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + @@ -286,11 +286,11 @@ args = "-a", detect = Build_Log.Prop.build_tags.undefined, history_base = "2c0f24e927dd"), - Remote_Build("Mac OS X, quick_and_dirty", "macbroy2", + Remote_Build("macOS, quick_and_dirty", "macbroy2", options = "-m32 -M8 -t quick_and_dirty -p pide_session=false", args = "-a -o quick_and_dirty", detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty"), history_base = "2c0f24e927dd"), - Remote_Build("Mac OS X, skip_proofs", "macbroy2", + Remote_Build("macOS, skip_proofs", "macbroy2", options = "-m32 -M8 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs", detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"), history_base = "2c0f24e927dd"), @@ -298,10 +298,10 @@ options = "-m32 -B -M1x2,2 -t polyml-test -i 'init_component /home/isabelle/contrib/polyml-5.7-20170217'", args = "-N -g timing", detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test")), - Remote_Build("Mac OS X 10.12 Sierra", "macbroy30", options = "-m32 -M2 -p pide_session=false", args = "-a", + Remote_Build("macOS 10.12 Sierra", "macbroy30", options = "-m32 -M2 -p pide_session=false", args = "-a", detect = Build_Log.Prop.build_start + " > date '2017-03-03'"), - Remote_Build("Mac OS X 10.10 Yosemite", "macbroy31", options = "-m32 -M2 -p pide_session=false", args = "-a"), - Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a", + Remote_Build("macOS 10.10 Yosemite", "macbroy31", options = "-m32 -M2 -p pide_session=false", args = "-a"), + Remote_Build("macOS 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a", detect = Build_Log.Prop.build_start + " < date '2017-03-03'")) ::: { for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) } @@ -323,11 +323,11 @@ List( List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90, options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")), - List(Remote_Build("Mac OS X 10.13 High Sierra", "lapbroy68", + List(Remote_Build("macOS 10.13 High Sierra", "lapbroy68", options = "-m32 -B -M1,2,4 -e ISABELLE_GHC_SETUP=true -p pide_session=false", self_update = true, args = "-a -d '~~/src/Benchmarks'")), List( - Remote_Build("Mac OS X 10.14 Mojave", "mini2", + Remote_Build("macOS 10.14 Mojave", "mini2", options = "-m32 -B -M1x2,2,4 -p pide_session=false" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_GHC_SETUP=true" + @@ -335,14 +335,14 @@ " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" + " -e ISABELLE_SWIPL=/usr/local/bin/swipl", self_update = true, args = "-a -d '~~/src/Benchmarks'"), - Remote_Build("Mac OS X, quick_and_dirty", "mini2", + Remote_Build("macOS, quick_and_dirty", "mini2", options = "-m32 -M4 -t quick_and_dirty -p pide_session=false", self_update = true, args = "-a -o quick_and_dirty", detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty")), - Remote_Build("Mac OS X, skip_proofs", "mini2", + Remote_Build("macOS, skip_proofs", "mini2", options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs", detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"))), - List(Remote_Build("Mac OS X 10.15 Catalina", "laramac01", user = "makarius", + List(Remote_Build("macOS 10.15 Catalina", "laramac01", user = "makarius", proxy_host = "laraserver", proxy_user = "makarius", self_update = true, options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",