--- a/ANNOUNCE Tue Jul 11 20:21:58 2023 +0100
+++ b/ANNOUNCE Tue Jul 11 20:22:08 2023 +0100
@@ -1,37 +1,33 @@
-Subject: Announcing Isabelle2022
+Subject: Announcing Isabelle2023
To: isabelle-users@cl.cam.ac.uk
-Isabelle2022 is now available.
+Isabelle2023 is now available.
-This version introduces notable changes over Isabelle2021-1: see the
+This version introduces notable changes over Isabelle2022: see the
NEWS file for further details. Here are various details:
-* HTML presentation is more robust and covers more files and links.
+* Documents: interactive document preparation via Isabelle/jEdit panel.
-* Display of instantiation for schematic goals.
+* Documents: demos for well-known LaTeX classes.
-* PIDE: improved Isabelle/VSCode based on bundled VSCodium engine.
+* Documents: more formal LaTeX citations.
-* HOL: various improvements of theory libraries.
+* HOL: various improvements of theory libraries, notably in HOL-Analysis.
* HOL: updates and improvements of Sledgehammer.
-* HOL: improved simproc support for record types.
+* ML: heap usage and stored heap size has been significantly reduced.
-* ML: scalable type Bytes.T with support for XZ compression.
-
-* System: bundled Node.js/Chromium/Electron platform (via VSCodium).
+* ML: improved implementations of functor Table() and corresponding Set().
-* System: Isabelle/Scala is based on Scala 3 (dotty compiler).
-
-* System: tools to sync hg repositories, notably Isabelle + AFP.
+* Scala and ML: support for Zstd compression.
-* System: improved "isabelle log" tool with regex filtering.
+* System: more robust "isabelle sync" tool via bundled "rsync" executables.
-* System: more robust SSH support in Isabelle/Scala.
+* Support for the Dotnet platform (.NET) and Fsharp (F#).
-You may get Isabelle2022 from the following mirror sites:
+You may get Isabelle2023 from the following mirror sites:
Cambridge (UK) https://www.cl.cam.ac.uk/research/hvg/Isabelle
Munich (Germany) https://isabelle.in.tum.de
--- a/Admin/Windows/Cygwin/README Tue Jul 11 20:21:58 2023 +0100
+++ b/Admin/Windows/Cygwin/README Tue Jul 11 20:22:08 2023 +0100
@@ -21,6 +21,7 @@
- https://isabelle.sketis.net/cygwin_2021 (Isabelle2021)
- https://isabelle.sketis.net/cygwin_2021-1 (Isabelle2021-1)
- https://isabelle.sketis.net/cygwin_2022 (Isabelle2022)
+ - https://isabelle.sketis.net/cygwin_2023 (Isabelle2023)
* Apache2 redirects for virtual host isabelle.conf:
```
@@ -52,6 +53,10 @@
Redirect /cygwin_2021-1/noarch/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/noarch/release
Redirect /cygwin_2022/x86_64/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/x86_64/release
Redirect /cygwin_2022/noarch/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/noarch/release
+ Redirect /cygwin_2022/x86_64/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/x86_64/release
+ Redirect /cygwin_2022/noarch/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/noarch/release
+ Redirect /cygwin_2023/x86_64/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/x86_64/release
+ Redirect /cygwin_2023/noarch/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/noarch/release
```
* Quasi-component: "isabelle component_cygwin" (as Administrator)
--- a/Admin/Windows/Cygwin/setup_server Tue Jul 11 20:21:58 2023 +0100
+++ b/Admin/Windows/Cygwin/setup_server Tue Jul 11 20:22:08 2023 +0100
@@ -21,3 +21,5 @@
download "$CYGWIN_MAIN/setup-x86_64.exe"
download "$CYGWIN_MIRROR/x86_64/setup.xz" "x86_64"
download "$CYGWIN_MIRROR/x86_64/setup.xz.sig" "x86_64"
+download "$CYGWIN_MIRROR/x86_64/setup.zst" "x86_64"
+download "$CYGWIN_MIRROR/x86_64/setup.zst.sig" "x86_64"
--- a/Admin/components/PLATFORMS Tue Jul 11 20:21:58 2023 +0100
+++ b/Admin/components/PLATFORMS Tue Jul 11 20:22:08 2023 +0100
@@ -47,7 +47,7 @@
macOS 13 Ventura (mini3 Mac14,12 -- MacMini M2)
x86_64-windows Windows 10
- x86_64-cygwin Cygwin 3.3.x https://isabelle.sketis.net/cygwin_2022 (x86_64/release)
+ x86_64-cygwin Cygwin 3.4.x https://isabelle.sketis.net/cygwin_2023 (x86_64/release)
Experimental platforms:
--- a/Admin/components/bundled Tue Jul 11 20:21:58 2023 +0100
+++ b/Admin/components/bundled Tue Jul 11 20:22:08 2023 +0100
@@ -1,2 +1,2 @@
#additional components to be bundled for release
-#naproche-20221024
+naproche-20230711
--- a/Admin/components/bundled-windows Tue Jul 11 20:21:58 2023 +0100
+++ b/Admin/components/bundled-windows Tue Jul 11 20:22:08 2023 +0100
@@ -1,3 +1,3 @@
#additional components to be bundled for release
-cygwin-20221002
+cygwin-20230711
windows_app-20181006
--- a/Admin/components/components.sha1 Tue Jul 11 20:21:58 2023 +0100
+++ b/Admin/components/components.sha1 Tue Jul 11 20:22:08 2023 +0100
@@ -76,6 +76,7 @@
fffaae24da4d274d34b8dc79a76b478b87ec31dd cygwin-20211007.tar.gz
66e16dccd7b177c086ab53013c1b74d09c1893ad cygwin-20220831.tar.gz
6cd34e30e2e650f239d19725c3d15c206fb3a7cf cygwin-20221002.tar.gz
+bc634cae08dea80238a830955894919af995cf06 cygwin-20230711.tar.gz
0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz
e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz
@@ -107,6 +108,7 @@
9534b721b7b78344f3225067ee4df28a5440b87e flatlaf-1.6.4.tar.gz
212a0f1f867511722024cc60156fd71872a16f92 flatlaf-1.6.tar.gz
6d4dbb6f2bde5804298d9008e3edceb0b9ee20ae flatlaf-2.4.tar.gz
+31d6abd58a4c2f7522f14283dfe04e2801a6e828 flatlaf-2.6.tar.gz
b1c40ce6c087da7e70e221ddd3fcadfa569acb2f foiltex-2.1.4b.tar.gz
f339234ec18369679be0095264e0c0af7762f351 gnu-utils-20210414.tar.gz
71259aa46134e6cf2c6473b4fc408051b3336490 gnu-utils-20211030.tar.gz
@@ -289,6 +291,7 @@
759848095e2ad506083d92b5646947e3c32f27a0 linux_app-20191223.tar.gz
1a449ce69ac874e21804595d16aaaf5a0d0d0c10 linux_app-20200110.tar.gz
5557b396f5a9aa22388d3e2171f9bc58e4bd6cd7 lipics-3.1.2.tar.gz
+881741f6e7192fd03835b542b1db820daf0ae79c lipics-3.1.3.tar.gz
71b6a272d10c53bb54cba23102e15334ec39bfce llncs-2.22.tar.gz
0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz
ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz
@@ -309,6 +312,7 @@
0b5a3161a18045540ab618249ba85a464c1fce66 naproche-20221002.tar.gz
48e9d4cbf95626c8e3013bee86ff82e67df6cefd naproche-20221018.tar.gz
c66f5ce13d429ea9c8dcc0d33d34b7abf178da5d naproche-20221024.tar.gz
+8e6cb32312336abcfe488b718bdc621461a7f132 naproche-20230711.tar.gz
d098dd0873b1720a77dc4e060267f9a6c93f341a naproche-2d99afe5c349.tar.gz
4a4e56fd03b7ba4edd38046f853873a90cf55d1a naproche-4ad61140062f.tar.gz
77252e0b40f89825b9b5935f9f0c4cd5d4e7012a naproche-6d0d76ce2f2a.tar.gz
@@ -467,6 +471,8 @@
8a2ca4d02cfedbfe4dad4490f1ed3ddba33a009a sqlite-jdbc-3.36.0.3.tar.gz
d2c707638b08ad56469b92dc2941d403efbb3394 sqlite-jdbc-3.39.4.1.tar.gz
12cb90b265bc2308858c63f00d5ecbfb80603dbd sqlite-jdbc-3.41.0.0.tar.gz
+68b1b61cffb1e6d4f5821cd6c3bebf2a74af6a97 sqlite-jdbc-3.42.0.0-1.tar.gz
+3535a04b8612cb1d98f0f7e41a0668e41667ec8b sqlite-jdbc-3.42.0.0.tar.gz
8d20968603f45a2c640081df1ace6a8b0527452a sqlite-jdbc-3.8.11.2.tar.gz
2369f06e8d095f9ba26df938b1a96000e535afff ssh-java-20161009.tar.gz
a2335d28b5b95d8d26500a53f1a9303fc5beaf36 ssh-java-20190323.tar.gz
@@ -475,6 +481,7 @@
f969443705aa8619e93af5b34ea98d15cd7efaf1 stack-2.1.3.tar.gz
ebd0221d038966aa8bde075f1b0189ff867b02ca stack-2.5.1.tar.gz
fa2d882ec45cbc8c7d2f3838b705a8316696dc66 stack-2.7.3.tar.gz
+18437bc9abd5b95be31a96f7c15a85a3ebf466cf stack-2.9.3.tar.gz
1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd sumatra_pdf-2.1.1.tar.gz
601e08d048d8e50b0729429c8928b667d9b6bde9 sumatra_pdf-2.3.2.tar.gz
14d46c2eb1a34821703da59d543433f581e91df3 sumatra_pdf-2.4.tar.gz
--- a/Admin/components/main Tue Jul 11 20:21:58 2023 +0100
+++ b/Admin/components/main Tue Jul 11 20:22:08 2023 +0100
@@ -7,7 +7,7 @@
e-2.6-1
easychair-3.5
eptcs-1.7.0
-flatlaf-2.4
+flatlaf-2.6
foiltex-2.1.4b
idea-icons-20210508
isabelle_fonts-20211004
@@ -18,7 +18,7 @@
jortho-1.0-2
jsoup-1.15.4
kodkodi-1.5.7
-lipics-3.1.2
+lipics-3.1.3
llncs-2.22
minisat-2.2.1-1
mlton-20210117-1
@@ -32,8 +32,8 @@
scala-3.3.0
smbc-0.4.1
spass-3.8ds-2
-sqlite-jdbc-3.41.0.0
-stack-2.7.3
+sqlite-jdbc-3.42.0.0-1
+stack-2.9.3
vampire-4.6
verit-2021.06.2-rmx
vscode_extension-20230206
--- a/COPYRIGHT Tue Jul 11 20:21:58 2023 +0100
+++ b/COPYRIGHT Tue Jul 11 20:22:08 2023 +0100
@@ -1,6 +1,6 @@
ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
-Copyright (c) 1986-2022,
+Copyright (c) 1986-2023,
University of Cambridge,
Technische Universitaet Muenchen,
and contributors.
--- a/NEWS Tue Jul 11 20:21:58 2023 +0100
+++ b/NEWS Tue Jul 11 20:22:08 2023 +0100
@@ -26,7 +26,8 @@
class.order.of_class.intro ~> order.intro_of_class
* The Eisbach 'method' command now takes an optional description for
-display with print_methods, similar to the 'method_setup' command.
+display with 'print_methods', similar to the 'method_setup' command.
+
*** Document preparation ***
@@ -80,7 +81,7 @@
- Add proof method "order".
* 'primcorec': Made the internal tactic more robust in the face of
- nested corecursion.
+nested corecursion.
* Theory "HOL.Map":
- Map.empty has been demoted to an input abbreviation.
@@ -455,6 +456,11 @@
via Compress.Options and Compress.Cache. Bytes.uncompress automatically
detects the compression scheme.
+* File.set_executable in Isabelle/Scala has changed its mandatory "flag"
+to optional "reset", which opposite polarity. INCOMPATIBILITY.
+
+* Update to GHC stack 2.9.3 with support for arm64-linux.
+
New in Isabelle2022 (October 2022)
--- a/etc/build.props Tue Jul 11 20:21:58 2023 +0100
+++ b/etc/build.props Tue Jul 11 20:22:08 2023 +0100
@@ -40,6 +40,7 @@
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_vampire.scala \
src/Pure/Admin/component_verit.scala \
src/Pure/Admin/component_zipperposition.scala \
--- a/src/Pure/Admin/component_cvc5.scala Tue Jul 11 20:21:58 2023 +0100
+++ b/src/Pure/Admin/component_cvc5.scala Tue Jul 11 20:22:08 2023 +0100
@@ -13,16 +13,16 @@
object Component_CVC5 {
/* platform information */
- sealed case class CVC5_Platform(platform_name: String, download_name: String) {
+ sealed case class Download_Platform(platform_name: String, download_name: String) {
def is_windows: Boolean = platform_name.endsWith("-windows")
}
- val platforms: List[CVC5_Platform] =
+ val platforms: List[Download_Platform] =
List(
- CVC5_Platform("arm64-darwin", "cvc5-macOS-arm64"),
- CVC5_Platform("x86_64-darwin", "cvc5-macOS"),
- CVC5_Platform("x86_64-linux", "cvc5-Linux"),
- CVC5_Platform("x86_64-windows", "cvc5-Win64.exe"))
+ Download_Platform("arm64-darwin", "cvc5-macOS-arm64"),
+ Download_Platform("x86_64-darwin", "cvc5-macOS"),
+ Download_Platform("x86_64-linux", "cvc5-Linux"),
+ Download_Platform("x86_64-windows", "cvc5-Win64.exe"))
/* build cvc5 */
--- a/src/Pure/Admin/component_cygwin.scala Tue Jul 11 20:21:58 2023 +0100
+++ b/src/Pure/Admin/component_cygwin.scala Tue Jul 11 20:22:08 2023 +0100
@@ -8,9 +8,9 @@
object Component_Cygwin {
- val default_mirror: String = "https://isabelle.sketis.net/cygwin_2022"
+ val default_mirror: String = "https://isabelle.sketis.net/cygwin_2023"
- val packages: List[String] = List("curl", "libgmp-devel", "nano", "openssh")
+ val packages: List[String] = List("curl", "libgmp-devel", "nano", "openssh", "perl", "rlwrap")
def build_cygwin(
target_dir: Path = Path.current,
--- a/src/Pure/Admin/component_jdk.scala Tue Jul 11 20:21:58 2023 +0100
+++ b/src/Pure/Admin/component_jdk.scala Tue Jul 11 20:22:08 2023 +0100
@@ -14,20 +14,20 @@
object Component_JDK {
/* platform information */
- sealed case class JDK_Platform(name: String, url_template: String) {
+ 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[JDK_Platform] =
+ val platforms: List[Download_Platform] =
List(
- JDK_Platform("arm64-darwin", "zulu{Z}-jdk{V}-macosx_aarch64.tar.gz"),
- JDK_Platform("arm64-linux", "zulu{Z}-jdk{V}-linux_aarch64.tar.gz"),
- JDK_Platform("x86_64-darwin", "zulu{Z}-jdk{V}-macosx_x64.tar.gz"),
- JDK_Platform("x86_64-linux", "zulu{Z}-jdk{V}-linux_x64.tar.gz"),
- JDK_Platform("x86_64-windows", "zulu{Z}-jdk{V}-win_x64.zip"))
+ 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 */
--- a/src/Pure/Admin/component_lipics.scala Tue Jul 11 20:21:58 2023 +0100
+++ b/src/Pure/Admin/component_lipics.scala Tue Jul 11 20:22:08 2023 +0100
@@ -23,7 +23,7 @@
/* build lipics component */
- val default_url = "https://github.com/dagstuhl-publishing/styles/archive/refs/tags/v2021.1.2.tar.gz"
+ val default_url = "https://github.com/dagstuhl-publishing/styles/archive/refs/tags/v2021.1.3.tar.gz"
def build_lipics(
download_url: String = default_url,
--- a/src/Pure/Admin/component_sqlite.scala Tue Jul 11 20:21:58 2023 +0100
+++ b/src/Pure/Admin/component_sqlite.scala Tue Jul 11 20:22:08 2023 +0100
@@ -11,7 +11,7 @@
/* build sqlite */
val default_download_url =
- "https://repo1.maven.org/maven2/org/xerial/sqlite-jdbc/3.41.0.0/sqlite-jdbc-3.41.0.0.jar"
+ "https://repo1.maven.org/maven2/org/xerial/sqlite-jdbc/3.42.0.0/sqlite-jdbc-3.42.0.0.jar"
def build_sqlite(
download_url: String = default_download_url,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/component_stack.scala Tue Jul 11 20:22:08 2023 +0100
@@ -0,0 +1,132 @@
+/* Title: Pure/Admin/component_stack.scala
+ Author: Makarius
+
+Build Isabelle component for GHC stack. See also:
+
+ - https://www.haskellstack.org
+ - https://github.com/commercialhaskell
+*/
+
+package isabelle
+
+
+object Component_Stack {
+ /* platform information */
+
+ sealed case class Download_Platform(platform_name: String, download_name: String) {
+ def is_windows: Boolean = platform_name.endsWith("-windows")
+ }
+
+ val platforms: List[Download_Platform] =
+ List(
+ Download_Platform("arm64-linux", "linux-aarch64"),
+ Download_Platform("x86_64-darwin", "osx-x86_64"),
+ Download_Platform("x86_64-linux", "linux-x86_64"),
+ Download_Platform("x86_64-windows", "windows-x86_64"))
+
+
+ /* build stack */
+
+ val default_url = "https://github.com/commercialhaskell/stack/releases/download"
+ val default_version = "2.9.3"
+
+ def build_stack(
+ base_url: String = default_url,
+ version: String = default_version,
+ target_dir: Path = Path.current,
+ progress: Progress = new Progress
+ ): Unit = {
+ /* component name */
+
+ val component = "stack-" + version
+ val component_dir =
+ Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
+
+
+ /* download executables */
+
+ for (platform <- platforms) {
+ val platform_dir =
+ Isabelle_System.make_directory(component_dir.path + Path.explode(platform.platform_name))
+
+ val url =
+ Url.append_path(base_url,
+ "v" + version + "/stack-" + version + "-" + platform.download_name + ".tar.gz")
+
+ val exe = Path.explode("stack").exe_if(platform.is_windows)
+
+ Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_file =>
+ Isabelle_System.with_tmp_dir("tmp") { tmp_dir =>
+ Isabelle_System.download_file(url, archive_file, progress = progress)
+ Isabelle_System.extract(archive_file, tmp_dir, strip = true)
+ Isabelle_System.move_file(tmp_dir + exe, platform_dir)
+ File.set_executable(platform_dir + exe)
+ }
+ }
+ }
+
+
+ /* settings */
+
+ component_dir.write_settings("""
+ISABELLE_STACK="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/stack"
+""")
+
+
+ /* README */
+
+ File.write(component_dir.README,
+ """This is stack """ + version + """ -- the Haskell Tool Stack.
+
+See also https://www.haskellstack.org and executables from
+""" + base_url + """
+
+The oldest supported version of macOS is 10.14 Mojave.
+
+The downloaded files were renamed and made executable.
+
+
+ Makarius
+ """ + Date.Format.date(Date.now()) + "\n")
+
+
+ /* AUTHORS and COPYING */
+
+ // download "latest" versions as reasonable approximation
+ Isabelle_System.download_file("https://raw.githubusercontent.com/commercialhaskell/stack/master/LICENSE",
+ component_dir.LICENSE)
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("component_stack", "build component for GHC stack", Scala_Project.here,
+ { args =>
+ var target_dir = Path.current
+ var base_url = default_url
+ var version = default_version
+
+ val getopts = Getopts("""
+Usage: isabelle component_stack [OPTIONS]
+
+ Options are:
+ -D DIR target directory (default ".")
+ -U URL download URL (default: """" + default_url + """")
+ -V VERSION version (default: """" + default_version + """")
+
+ Build component for GHC stack.
+""",
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "U:" -> (arg => base_url = arg),
+ "V:" -> (arg => version = arg))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ val progress = new Console_Progress()
+
+ build_stack(base_url = base_url, version = version, target_dir = target_dir,
+ progress = progress)
+ })
+}
--- a/src/Pure/Admin/component_zstd.scala Tue Jul 11 20:21:58 2023 +0100
+++ b/src/Pure/Admin/component_zstd.scala Tue Jul 11 20:22:08 2023 +0100
@@ -15,7 +15,7 @@
val source = jar_dir + Path.explode(template.replace("{V}", version))
val target = Isabelle_System.make_directory(component_dir + Path.basic(name))
Isabelle_System.copy_file(source, target)
- if (exe) File.set_executable(target + source.base, true)
+ if (exe) File.set_executable(target + source.base)
}
}
--- a/src/Pure/General/file.scala Tue Jul 11 20:21:58 2023 +0100
+++ b/src/Pure/General/file.scala Tue Jul 11 20:22:08 2023 +0100
@@ -388,10 +388,9 @@
else path.file.canExecute
}
- def set_executable(path: Path, flag: Boolean = false): Unit = {
- if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path)
- else if (Platform.is_windows) Isabelle_System.chmod("a-x", path)
- else path.file.setExecutable(flag, false)
+ def set_executable(path: Path, reset: Boolean = false): Unit = {
+ if (Platform.is_windows) Isabelle_System.chmod(if (reset) "a-x" else "a+x", path)
+ else path.file.setExecutable(!reset, false)
}
--- a/src/Pure/General/ssh.scala Tue Jul 11 20:21:58 2023 +0100
+++ b/src/Pure/General/ssh.scala Tue Jul 11 20:22:08 2023 +0100
@@ -246,8 +246,8 @@
error("Failed to change permissions of " + quote(remote_path(path)))
}
- override def set_executable(path: Path, flag: Boolean = false): Unit =
- if (!execute("chmod a" + (if (flag) "+" else "-") + "x " + bash_path(path)).ok) {
+ override def set_executable(path: Path, reset: Boolean = false): Unit =
+ if (!execute("chmod a" + (if (reset) "-" else "+") + "x " + bash_path(path)).ok) {
error("Failed to change executable status of " + quote(remote_path(path)))
}
@@ -408,8 +408,8 @@
def is_file(path: Path): Boolean = path.is_file
def delete(path: Path): Unit = path.file.delete
def restrict(path: Path): Unit = File.restrict(path)
- def set_executable(path: Path, flag: Boolean = false): Unit =
- File.set_executable(path, flag = flag)
+ def set_executable(path: Path, reset: Boolean = false): Unit =
+ File.set_executable(path, reset = reset)
def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
def rm_tree(dir: Path): Unit = Isabelle_System.rm_tree(dir)
def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
--- a/src/Pure/System/isabelle_tool.scala Tue Jul 11 20:21:58 2023 +0100
+++ b/src/Pure/System/isabelle_tool.scala Tue Jul 11 20:22:08 2023 +0100
@@ -183,6 +183,7 @@
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_Zipperposition.isabelle_tool,
--- a/src/Pure/Thy/export.scala Tue Jul 11 20:21:58 2023 +0100
+++ b/src/Pure/Thy/export.scala Tue Jul 11 20:22:08 2023 +0100
@@ -548,7 +548,7 @@
Isabelle_System.make_directory(path.dir)
val bytes = entry.bytes
if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes)
- File.set_executable(path, flag = entry.executable)
+ File.set_executable(path, reset = !entry.executable)
}
}
}
--- a/src/Pure/Tools/docker_build.scala Tue Jul 11 20:21:58 2023 +0100
+++ b/src/Pure/Tools/docker_build.scala Tue Jul 11 20:22:08 2023 +0100
@@ -15,7 +15,7 @@
private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_linux(?:_arm)?\.tar\.gz$""".r
val packages: List[String] =
- List("curl", "less", "libfontconfig1", "libgomp1", "openssh-client", "pwgen")
+ List("curl", "less", "libfontconfig1", "libgomp1", "openssh-client", "perl", "pwgen", "rlwrap")
val package_collections: Map[String, List[String]] =
Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"),
@@ -71,8 +71,8 @@
else "COPY Isabelle.tar.gz .") + """
RUN tar xzf Isabelle.tar.gz && \
mv """ + isabelle_name + """ Isabelle && \
- sed -i -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$USER_HOME/.isabelle",g;' Isabelle/etc/settings && \
- sed -i -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \
+ perl -pi -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$USER_HOME/.isabelle",g;' Isabelle/etc/settings && \
+ perl -pi -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \
Isabelle/bin/isabelle build -o system_heaps -b """ + logic + """ && \
rm Isabelle.tar.gz""" + (if (entrypoint) """
--- a/src/Pure/Tools/dotnet_setup.scala Tue Jul 11 20:21:58 2023 +0100
+++ b/src/Pure/Tools/dotnet_setup.scala Tue Jul 11 20:22:08 2023 +0100
@@ -52,7 +52,7 @@
def default_target_dir: Path = Components.default_components_base
def default_install_url: String = "https://dot.net/v1/dotnet-install"
- def default_version: String = "6.0.402"
+ def default_version: String = "6.0.411"
def dotnet_setup(
platform_spec: String = default_platform,
--- a/src/Tools/Haskell/Haskell.thy Tue Jul 11 20:21:58 2023 +0100
+++ b/src/Tools/Haskell/Haskell.thy Tue Jul 11 20:22:08 2023 +0100
@@ -1253,8 +1253,8 @@
{-# LANGUAGE OverloadedStrings #-}
module Isabelle.Position (
- T, line_of, column_of, offset_of, end_offset_of, file_of, id_of,
- start, none, put_file, file, file_only, put_id, id, id_only,
+ T, line_of, column_of, offset_of, end_offset_of, label_of, file_of, id_of,
+ start, none, label, put_file, file, file_only, put_id, id, id_only,
symbol, symbol_explode, symbol_explode_string, shift_offsets,
of_properties, properties_of, def_properties_of, entity_markup, make_entity_markup,
Report, Report_Text, is_reported, is_reported_range, here,