--- a/Admin/components/components.sha1 Tue May 30 14:24:09 2023 +0100
+++ b/Admin/components/components.sha1 Wed May 31 11:05:44 2023 +0100
@@ -450,6 +450,7 @@
c58db22b9e1e90f5b7a3f5edd8bdb4ddab4947fd scala-3.2.0-2.tar.gz
7677b02fe06c992ca6cf82bf68adb16287294256 scala-3.2.0.tar.gz
bee1c9416a086e553057171e5cb571271ed02c60 scala-3.2.1.tar.gz
+989736bb2693fa2c484f45841364a0bcb642acc1 scala-3.3.0.tar.gz
abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz
cbd491c0feba1d21019d05564e76dd04f592ccb4 spass-3.8ds-1.tar.gz
edaa1268d82203067657aabcf0371ce7d4b579b9 spass-3.8ds-2.tar.gz
--- a/Admin/components/main Tue May 30 14:24:09 2023 +0100
+++ b/Admin/components/main Wed May 31 11:05:44 2023 +0100
@@ -29,7 +29,7 @@
postgresql-42.5.0
prismjs-1.29.0
rsync-3.2.7
-scala-3.2.0-2
+scala-3.3.0
smbc-0.4.1
spass-3.8ds-2
sqlite-jdbc-3.41.0.0
--- a/NEWS Tue May 30 14:24:09 2023 +0100
+++ b/NEWS Wed May 31 11:05:44 2023 +0100
@@ -10,12 +10,12 @@
*** General ***
* ML heap usage and stored heap size has been significantly reduced,
-especially for applications with a lot of definitions in a 'locale' or
-'class' context. The shrink factor is usually in the range 1.1 .. 2.0,
-but a factor 3 .. 10 has been seen in unusual situations. This often
-allows big applications to return to the "small" 64_32 memory model with
-its hard limit of 16 GiB, and thus reduce the heap size by another
-factor 1.8.
+especially for applications with a lot 'locale' or 'class' context
+switches, e.g. "definition (in loc)". The shrink factor is usually in
+the range 1.1 .. 2.0, but a factor 2 .. 10 has been seen as well. This
+often allows big applications to return to the "small" 64_32 memory
+model with its hard limit of 16 GiB, and thus reduce the heap size by
+another factor 1.8.
* The special "of_class" introduction rule for 'class' definitions has
been renamed from "class.NAME.of_class.intro" to "NAME.intro_of_class"
@@ -361,6 +361,25 @@
*** System ***
+* System options "context_theory_tracing" and "context_proof_tracing"
+store information about persistent context values (ML types theory,
+local_theory, Proof.context). This may reveal "memory leaks" in
+Isabelle/ML infrastructure or user tools, typically due to the lack of
+Thm.trim_context when thm values are stored as theory data.
+
+Below is a minimal example for Isabelle/ZF. The idea is to build a clean
+heap image with the above options enabled, and inspect the resulting ML
+heap later:
+
+ isabelle build -o context_theory_tracing -o context_proof_tracing -b -c ZF
+ isabelle process -l ZF -e "Session.print_context_tracing (K true)"
+
+An alternative to "isabelle process -l ZF" is "isabelle jedit -l ZF"
+with the subsequent ML snippets in an arbitrary theory context:
+
+ ML_command \<open>Session.print_context_tracing (K true)\<close>
+ ML \<open>Context.finish_tracing ()\<close>
+
* The "rsync" tool has been bundled as Isabelle component, with uniform
version and compilation options on all platforms. This allows to use
more recent options for extra robustness, notably "--secluded-args"
--- a/src/Pure/Admin/component_scala.scala Tue May 30 14:24:09 2023 +0100
+++ b/src/Pure/Admin/component_scala.scala Wed May 31 11:05:44 2023 +0100
@@ -34,14 +34,14 @@
}
val main_download: Download =
- Download("scala", "3.2.1", base_version = "",
+ Download("scala", "3.3.0", base_version = "",
url = "https://github.com/lampepfl/dotty/releases/download/{V}/scala3-{V}.tar.gz")
val lib_downloads: List[Download] = List(
Download("scala-parallel-collections", "1.0.4",
"https://mvnrepository.com/artifact/org.scala-lang.modules/scala-parallel-collections_{B}/{V}",
physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-parallel-collections_{B}/{V}/scala-parallel-collections_{B}-{V}.jar"),
- Download("scala-parser-combinators", "2.1.1",
+ Download("scala-parser-combinators", "2.3.0",
"https://mvnrepository.com/artifact/org.scala-lang.modules/scala-parser-combinators_{B}/{V}",
physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-parser-combinators_{B}/{V}/scala-parser-combinators_{B}-{V}.jar"),
Download("scala-swing", "3.0.0",
--- a/src/Pure/ROOT.ML Tue May 30 14:24:09 2023 +0100
+++ b/src/Pure/ROOT.ML Wed May 31 11:05:44 2023 +0100
@@ -370,4 +370,3 @@
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML";
-
--- a/src/Pure/ROOT.scala Tue May 30 14:24:09 2023 +0100
+++ b/src/Pure/ROOT.scala Wed May 31 11:05:44 2023 +0100
@@ -27,4 +27,3 @@
def if_proper[A](x: Iterable[A], body: => String): String = Library.if_proper(x, body)
def if_proper(b: Boolean, body: => String): String = Library.if_proper(b, body)
}
-