# HG changeset patch
# User paulson
# Date 1685527544 -3600
# Node ID acf27e8352d28f24312cc885dd51dded4e9473dc
# Parent  163e4835a8db3f0b1060c1c06a2b3c7cadce52cc# Parent  3d2db8057b9f3bc4bb91f29aeb014c674febcc8e
merged

diff -r 3d2db8057b9f -r acf27e8352d2 Admin/components/components.sha1
--- 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
diff -r 3d2db8057b9f -r acf27e8352d2 Admin/components/main
--- 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
diff -r 3d2db8057b9f -r acf27e8352d2 NEWS
--- 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"
diff -r 3d2db8057b9f -r acf27e8352d2 src/Pure/Admin/component_scala.scala
--- 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",
diff -r 3d2db8057b9f -r acf27e8352d2 src/Pure/ROOT.ML
--- 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";
-
diff -r 3d2db8057b9f -r acf27e8352d2 src/Pure/ROOT.scala
--- 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)
 }
-