--- a/Admin/Windows/Cygwin/isabelle/postinstall Thu Oct 13 14:30:53 2022 +0200
+++ b/Admin/Windows/Cygwin/isabelle/postinstall Thu Oct 13 16:45:49 2022 +0200
@@ -4,8 +4,7 @@
bash /etc/postinstall/base-files-mketc.sh.done
-mkpasswd -l >/etc/passwd
-mkgroup -l >/etc/group
+mkpasswd -l -u "$USERNAME" -p "$(cygpath -u "$HOMEDRIVE$HOMEPATH\\..")" >/etc/passwd
find -type d -exec setfacl -m default:user::rwx,default:group::r-x,default:other:r-x '{}' +
find -type d -exec chmod 755 '{}' +
--- a/Admin/components/main Thu Oct 13 14:30:53 2022 +0200
+++ b/Admin/components/main Thu Oct 13 16:45:49 2022 +0200
@@ -20,7 +20,7 @@
nunchaku-0.5
opam-2.0.7
pdfjs-2.14.305
-polyml-test-15c840d48c9a
+polyml-test-bafe319bc3a6-1
postgresql-42.5.0
scala-3.2.0
smbc-0.4.1
--- a/Admin/polyml/README Thu Oct 13 14:30:53 2022 +0200
+++ b/Admin/polyml/README Thu Oct 13 16:45:49 2022 +0200
@@ -3,8 +3,8 @@
This compilation of Poly/ML (https://www.polyml.org) is based on the
source distribution from
-https://github.com/polyml/polyml/commit/39d96a2def90 (official release
-5.9 with minimal additions fixes-5.9).
+https://github.com/polyml/polyml/commit/bafe319bc3a6 (after official
+version 5.9).
The Isabelle repository provides an administrative tool "isabelle
build_polyml", which can be used in the polyml component directory as
@@ -55,4 +55,4 @@
Makarius
- 26-Nov-2021
+ 09-Oct-2022
--- a/Admin/polyml/settings Thu Oct 13 14:30:53 2022 +0200
+++ b/Admin/polyml/settings Thu Oct 13 16:45:49 2022 +0200
@@ -2,7 +2,17 @@
POLYML_HOME="$COMPONENT"
-ML_PLATFORM="${ISABELLE_APPLE_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_PLATFORM64}}}"
+if [ -n "$ISABELLE_APPLE_PLATFORM64" ]
+then
+ if grep "ML_system_apple.*=.*false" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
+ then
+ ML_PLATFORM="$ISABELLE_PLATFORM64"
+ else
+ ML_PLATFORM="$ISABELLE_APPLE_PLATFORM64"
+ fi
+else
+ ML_PLATFORM="${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}"
+fi
if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
then
--- a/NEWS Thu Oct 13 14:30:53 2022 +0200
+++ b/NEWS Thu Oct 13 16:45:49 2022 +0200
@@ -238,6 +238,10 @@
total_on_trancl
totalp_on_tranclp
+* Theory "HOL-Library.Signed_Division": class signed_division carries
+assumptions; use syntactic type classes signed_division and
+signed_modulo as alternatives.
+
* New theory "HOL-Library.NList" of fixed length lists.
* New Theory "HOL-Library.Code_Abstract_Char" implements characters by
@@ -448,6 +452,11 @@
together. Potential INCOMPATIBILITY for existing
$ISABELLE_HOME_USER/etc/settings.
+* The system option "ML_system_apple" controls the use of native
+Apple/ARM64 for Poly/ML: default "true". Like "ML_system_64" this only
+works when saved in "$ISABELLE_HOME_USER/etc/preferences" (e.g. after
+shutdown of Isabelle/jEdit).
+
New in Isabelle2021-1 (December 2021)
--- a/etc/options Thu Oct 13 14:30:53 2022 +0200
+++ b/etc/options Thu Oct 13 16:45:49 2022 +0200
@@ -161,7 +161,10 @@
-- "ML debugger instrumentation for newly compiled code"
public option ML_system_64 : bool = false
- -- "ML system for 64bit platform is used if possible (change requires restart)"
+ -- "prefer native 64bit platform (change requires restart)"
+
+public option ML_system_apple : bool = true
+ -- "prefer native Apple/ARM64 platform (change requires restart)"
public option ML_process_policy : string = ""
-- "ML process command prefix (process policy)"
--- a/src/Pure/Admin/build_release.scala Thu Oct 13 14:30:53 2022 +0200
+++ b/src/Pure/Admin/build_release.scala Thu Oct 13 16:45:49 2022 +0200
@@ -249,7 +249,8 @@
"cd " + File.bash_path(remote_dir),
"tar -xf tmp.tar",
build_command,
- """perl -pi -e "s/ISABELLE_APPLE_PLATFORM64/ISABELLE_WINDOWS_PLATFORM64/g;" "$(bin/isabelle getenv -b POLYML_HOME)/etc/settings" """,
+ """mkdir -p "$(bin/isabelle getenv -b ISABELLE_HOME_USER)/etc" """,
+ """{ echo "ML_system_apple = false" > "$(bin/isabelle getenv -b ISABELLE_HOME_USER)/etc/preferences"; }""",
build_command,
"tar -cf tmp.tar heaps")
ssh.execute(build_script.mkString(" && "), settings = false).check
--- a/src/Pure/General/bytes.ML Thu Oct 13 14:30:53 2022 +0200
+++ b/src/Pure/General/bytes.ML Thu Oct 13 16:45:49 2022 +0200
@@ -48,7 +48,7 @@
(* primitive operations *)
-val chunk_size = 1024 * 1024 - 8;
+val chunk_size = 65000;
abstype T = Bytes of
{buffer: string list, chunks: string list, m: int (*buffer size*), n: int (*chunks size*)}
--- a/src/Pure/General/http.scala Thu Oct 13 14:30:53 2022 +0200
+++ b/src/Pure/General/http.scala Thu Oct 13 16:45:49 2022 +0200
@@ -276,10 +276,11 @@
}
def server(
+ port: Int = 0,
name: String = UUID.random().toString,
services: List[Service] = isabelle_services
): Server = {
- val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, 0), 0)
+ val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, port), 0)
http_server.setExecutor(null)
val server = new Server(name, http_server)
--- a/src/Pure/Thy/sessions.scala Thu Oct 13 14:30:53 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Thu Oct 13 16:45:49 2022 +0200
@@ -99,7 +99,7 @@
sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) {
override def toString: String = "Sessions.Deps(" + sessions_structure + ")"
- def is_empty: Boolean = session_bases.isEmpty
+ def is_empty: Boolean = session_bases.keysIterator.forall(_.isEmpty)
def apply(name: String): Base = session_bases(name)
def get(name: String): Option[Base] = session_bases.get(name)
--- a/src/Pure/Tools/server_commands.scala Thu Oct 13 14:30:53 2022 +0200
+++ b/src/Pure/Tools/server_commands.scala Thu Oct 13 16:45:49 2022 +0200
@@ -316,8 +316,8 @@
override val command_body: Server.Command_Body =
{ case (context, Purge_Theories(args)) =>
- val session = context.server.the_session(args.session_id)
- command(args, session)._1
+ val session = context.server.the_session(args.session_id)
+ command(args, session)._1
}
}
}