--- a/Admin/components/components.sha1 Thu Mar 21 17:36:50 2024 +0100
+++ b/Admin/components/components.sha1 Thu Mar 21 21:04:49 2024 +0100
@@ -290,6 +290,7 @@
2155e0bdbd29cd3d2905454de2e7203b9661d239 jortho-1.0-2.tar.gz
ffe179867cf5ffaabbb6bb096db9bdc0d7110065 jortho-1.0.tar.gz
df8bb213d39a7eecae97e6af3b11752d6c704c90 jsoup-1.15.4.tar.gz
+b1c8e2a289e40cbc139a3c371348cef3b537b1c7 jsoup-1.17.2.tar.gz
6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz
afb04f4048a87bb888fe7b05b0139cb060c7925b kodkodi-1.5.2-1.tar.gz
5f95c96bb99927f3a026050f85bd056f37a9189e kodkodi-1.5.2.tar.gz
@@ -314,6 +315,8 @@
5fb1a2d21b220d0e588790c0203ac87c10ed0870 minisat-2.2.1-1.tar.gz
ae76bfaade3bf72ff6b2d3aafcd52fa45609fcd1 minisat-2.2.1.tar.gz
59aa13f48685326995714cc6028aebb789e445e3 mlton-20210117-1.tar.gz
+7624509ba58b9b8231626a66eda571fba69f7cd3 mlton-20210117-2.tar.gz
+2d8c08fc623e7643a10ee031c7e9e7cb7c01d53a mlton-20210117-3.tar.gz
5d48b7163a68c18b691bedc1511364b0b103baeb mlton-20210117.tar.gz
eda10c62da927a842c0a8881f726eac85e1cb4f7 naproche-20210122.tar.gz
edcb517b7578db4eec1b6573b624f291776e11f6 naproche-20210124.tar.gz
@@ -432,6 +435,7 @@
143d0d32a13d7d8e15b9bab866e14ad4308a6246 postgresql-42.5.0.tar.gz
36a6e17794a93070278ac590650870ab73e6a7fb postgresql-42.6.0.tar.gz
65bf0d99f4e80f5802c573106327c337fe608fe7 postgresql-42.7.1.tar.gz
+459c2b8da13910ba6c89ad91b9d26f4a63615117 postgresql-42.7.3.tar.gz
f132329ca1045858ef456cc08b197c9eeea6881b postgresql-9.4.1212.tar.gz
3fc5e7f759e7220b9e3fc5bac296e312e34a60ad prismjs-1.29.0.tar.gz
f042bba5fb82c7eb8aee99f92eb6ec38c8a067f7 python-3.10.4.tar.gz
@@ -479,6 +483,7 @@
cbd491c0feba1d21019d05564e76dd04f592ccb4 spass-3.8ds-1.tar.gz
edaa1268d82203067657aabcf0371ce7d4b579b9 spass-3.8ds-2.tar.gz
43b5afbcad575ab6817d2289756ca22fd2ef43a9 spass-3.8ds.tar.gz
+24a1397d06c79361d7507d59cbfe39962ce25148 sqlite-3.45.2.0.tar.gz
b016a785f1f78855c00d351ff598355c3b87450f sqlite-jdbc-3.18.0-1.tar.gz
b85b5bc071a59ef2a8326ceb1617d5a9a5be41cf sqlite-jdbc-3.18.0.tar.gz
e56117a67ab01fb24c7fc054ede3160cefdac5f8 sqlite-jdbc-3.20.0.tar.gz
@@ -515,6 +520,7 @@
8486387f61557147ec06b1f637117c017c8f0528 sumatra_pdf-3.1.2.tar.gz
e8648878f908e93d64a393231ab21fdac976a9c2 sumatra_pdf-3.3.3.tar.gz
25d2004325585fceb0a951181716f77fc4d9d0d4 sumatra_pdf-3.4.6.tar.gz
+20b43515c05ebd8d3ec090a119eff3acf2d912a5 sumatra_pdf-3.5.2.tar.gz
869ea6d8ea35c8ba68d7fcb028f16b2b7064c5fd vampire-1.0.tar.gz
399f687b56575b93e730f68c91c989cb48aa34d8 vampire-4.2.2.tar.gz
0402978ca952f08eea73e483b694928ac402a304 vampire-4.5.1-1.tar.gz
--- a/Admin/components/main Thu Mar 21 17:36:50 2024 +0100
+++ b/Admin/components/main Thu Mar 21 21:04:49 2024 +0100
@@ -17,23 +17,23 @@
jedit-20231120
jfreechart-1.5.3
jortho-1.0-2
-jsoup-1.15.4
+jsoup-1.17.2
kodkodi-1.5.7
lipics-3.1.3
llncs-2.23
minisat-2.2.1-1
-mlton-20210117-1
+mlton-20210117-3
nunchaku-0.5
opam-2.0.7
pdfjs-2.14.305
polyml-5.9.1
-postgresql-42.7.1
+postgresql-42.7.3
prismjs-1.29.0
rsync-3.2.7
scala-3.3.3
smbc-0.4.1
spass-3.8ds-2
-sqlite-jdbc-3.45.0.0
+sqlite-3.45.2.0
stack-2.15.1
vampire-4.8
verit-2021.06.2-rmx-1
--- a/Admin/components/windows Thu Mar 21 17:36:50 2024 +0100
+++ b/Admin/components/windows Thu Mar 21 21:04:49 2024 +0100
@@ -1,2 +1,2 @@
#additional components for Windows platform
-sumatra_pdf-3.4.6
+sumatra_pdf-3.5.2
--- a/NEWS Thu Mar 21 17:36:50 2024 +0100
+++ b/NEWS Thu Mar 21 21:04:49 2024 +0100
@@ -238,6 +238,11 @@
component javamail (previously javax.mail) from jakarta 2.1.2
using eclipse angus 2.0.2/2.0.1.
+* The Isabelle component for the MLton compiler now covers macOS and
+Linux (Intel), while Windows and Linux (ARM) are unsupported. The
+default for ISABELLE_MLTON_OPTIONS should work most of the time, but may
+have to be overridden (e.g. in $ISABELLE_HOME_USER/etc/settings).
+
* Update to GHC stack 2.15.1 with support for all platforms, including
ARM Linux and Apple Silicon.
--- a/etc/build.props Thu Mar 21 17:36:50 2024 +0100
+++ b/etc/build.props Thu Mar 21 21:04:49 2024 +0100
@@ -34,6 +34,7 @@
src/Pure/Admin/component_lipics.scala \
src/Pure/Admin/component_llncs.scala \
src/Pure/Admin/component_minisat.scala \
+ src/Pure/Admin/component_mlton.scala \
src/Pure/Admin/component_pdfjs.scala \
src/Pure/Admin/component_polyml.scala \
src/Pure/Admin/component_postgresql.scala \
--- a/etc/settings Thu Mar 21 17:36:50 2024 +0100
+++ b/etc/settings Thu Mar 21 21:04:49 2024 +0100
@@ -185,7 +185,5 @@
ISABELLE_GNUPLOT="gnuplot"
ISABELLE_FONTFORGE="fontforge"
-#ISABELLE_MLTON="/usr/bin/mlton"
-#ISABELLE_MLTON_OPTIONS="-pi-style npi"
#ISABELLE_SMLNJ="/usr/bin/sml"
#ISABELLE_SWIPL="/usr/bin/swipl"
--- a/src/HOL/Analysis/Set_Integral.thy Thu Mar 21 17:36:50 2024 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy Thu Mar 21 21:04:49 2024 +0100
@@ -1745,11 +1745,11 @@
subsection \<open>Averaging Theorem\<close>
text \<open>We aim to lift results from the real case to arbitrary Banach spaces.
- Our fundamental tool in this regard will be the averaging theorem. The proof of this theorem is due to Serge Lang (Real and Functional Analysis) \cite{Lang_1993}.
+ Our fundamental tool in this regard will be the averaging theorem. The proof of this theorem is due to Serge Lang (Real and Functional Analysis) \<^cite>\<open>"Lang_1993"\<close>.
The theorem allows us to make statements about a function's value almost everywhere, depending on the value its integral takes on various sets of the measure space.\<close>
text \<open>Before we introduce and prove the averaging theorem, we will first show the following lemma which is crucial for our proof.
- While not stated exactly in this manner, our proof makes use of the characterization of second-countable topological spaces given in the book General Topology by Ryszard Engelking (Theorem 4.1.15) \cite{engelking_1989}.
+ While not stated exactly in this manner, our proof makes use of the characterization of second-countable topological spaces given in the book General Topology by Ryszard Engelking (Theorem 4.1.15) \<^cite>\<open>"engelking_1989"\<close>.
(Engelking's book \emph{General Topology})\<close>
lemma balls_countable_basis:
--- a/src/HOL/Analysis/document/root.bib Thu Mar 21 17:36:50 2024 +0100
+++ b/src/HOL/Analysis/document/root.bib Thu Mar 21 21:04:49 2024 +0100
@@ -31,4 +31,23 @@
publisher={Springer Science \& Business Media}
}
+@book{Lang_1993,
+ place={New York},
+ title={Real and Functional Analysis},
+ publisher={Springer},
+ author={Lang, Serge},
+ year={1993},
+ isbn={978-1-4612-0897-6}
+}
+
+@book{engelking_1989,
+ title={General Topology},
+ author={Engelking, R.},
+ isbn={978-3-8853-8006-1},
+ series={Sigma series in pure mathematics},
+ url={https://books.google.com.tr/books?id=K3spAQAAMAAJ},
+ year={1989},
+ publisher={Heldermann}
+}
+
@misc{dummy}
--- a/src/HOL/Library/Centered_Division.thy Thu Mar 21 17:36:50 2024 +0100
+++ b/src/HOL/Library/Centered_Division.thy Thu Mar 21 21:04:49 2024 +0100
@@ -15,7 +15,7 @@
\noindent The following specification of division on integers centers
the modulus around zero. This is useful e.g.~to define division
on Gauss numbers.
- N.b.: This is not mentioned \cite{leijen01}.
+ N.b.: This is not mentioned \<^cite>\<open>"leijen01"\<close>.
\<close>
definition centered_divide :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close> (infixl \<open>cdiv\<close> 70)
--- a/src/HOL/Library/Signed_Division.thy Thu Mar 21 17:36:50 2024 +0100
+++ b/src/HOL/Library/Signed_Division.thy Thu Mar 21 21:04:49 2024 +0100
@@ -48,7 +48,7 @@
end
text \<open>
- \noindent The following specification of division is named ``T-division'' in \cite{leijen01}.
+ \noindent The following specification of division is named ``T-division'' in \<^cite>\<open>"leijen01"\<close>.
It is motivated by ISO C99, which in turn adopted the typical behavior of
hardware modern in the beginning of the 1990ies; but note ISO C99 describes
the instance on machine words, not mathematical integers.
--- a/src/HOL/Library/Word.thy Thu Mar 21 17:36:50 2024 +0100
+++ b/src/HOL/Library/Word.thy Thu Mar 21 21:04:49 2024 +0100
@@ -626,7 +626,7 @@
text \<open>
The following specification of word division just lifts the pre-existing
- division on integers named ``F-Division'' in \cite{leijen01}.
+ division on integers named ``F-Division'' in \<^cite>\<open>"leijen01"\<close>.
\<close>
instantiation word :: (len) semiring_modulo
--- a/src/Pure/Admin/component_jsoup.scala Thu Mar 21 17:36:50 2024 +0100
+++ b/src/Pure/Admin/component_jsoup.scala Thu Mar 21 21:04:49 2024 +0100
@@ -11,7 +11,7 @@
/* build jsoup */
val default_download_url =
- "https://repo1.maven.org/maven2/org/jsoup/jsoup/1.15.4/jsoup-1.15.4.jar"
+ "https://repo1.maven.org/maven2/org/jsoup/jsoup/1.17.2/jsoup-1.17.2.jar"
def build_jsoup(
download_url: String = default_download_url,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/component_mlton.scala Thu Mar 21 21:04:49 2024 +0100
@@ -0,0 +1,125 @@
+/* Title: Pure/Admin/component_mlton.scala
+ Author: Makarius
+
+Build Isabelle component for MLton. See also:
+
+ - http://mlton.org
+ - https://projects.laas.fr/tina/software.php
+*/
+
+package isabelle
+
+
+object Component_MLton {
+ /* platform information */
+
+ sealed case class Download_Platform(platform_name: String, download_name: String) {
+ def download(base_url: String, version: String): String =
+ Url.append_path(base_url, version + "." + download_name)
+ }
+
+ val platforms: List[Download_Platform] =
+ List(
+ Download_Platform("x86_64-darwin", "amd64-darwin-16.7-gmp-static.tgz"),
+ Download_Platform("x86_64-linux", "amd64-linux-glibc2.19-gmp-static.tgz"))
+
+
+ /* build mlton */
+
+ val default_url = "https://projects.laas.fr/tina/software"
+ val default_version = "mlton-20210117-1"
+
+ def build_mlton(
+ base_url: String = default_url,
+ version: String = default_version,
+ target_dir: Path = Path.current,
+ progress: Progress = new Progress
+ ): Unit = {
+ val component_dir =
+ Components.Directory(target_dir + Path.basic(version)).create(progress = progress)
+
+
+ /* download executables */
+
+ for (platform <- platforms) {
+ Isabelle_System.with_tmp_dir("download") { download_dir =>
+ val download = platform.download(base_url, version)
+
+ val archive_name =
+ Url.get_base_name(download) getOrElse
+ error("Malformed download URL " + quote(download))
+ val archive_path = download_dir + Path.basic(archive_name)
+
+ val platform_dir = component_dir.path + Path.explode(platform.platform_name)
+ Isabelle_System.make_directory(platform_dir)
+
+ Isabelle_System.download_file(download, archive_path, progress = progress)
+ Isabelle_System.extract(archive_path, platform_dir, strip = true)
+ Isabelle_System.copy_file(platform_dir + Path.basic("LICENSE"), platform_dir.expand.dir)
+ }
+ }
+
+
+ /* settings */
+
+ component_dir.write_settings("""
+if [ -d "$COMPONENT/$ISABELLE_PLATFORM64" ]; then
+ ISABELLE_MLTON="$COMPONENT/$ISABELLE_PLATFORM64/bin/mlton"
+ case "$ISABELLE_PLATFORM_FAMILY" in
+ linux*)
+ ISABELLE_MLTON_OPTIONS="-pi-style npi"
+ ;;
+ *)
+ ISABELLE_MLTON_OPTIONS=""
+ ;;
+ esac
+fi
+""")
+
+
+ /* README */
+
+ File.write(component_dir.README,
+ """This distribution of MLton has been taken from the TINA project
+https://projects.laas.fr/tina/software.php using following downloads:""" +
+ platforms.map(_.download(base_url, version)).mkString("\n\n ", "\n ", "\n\n") +
+"""Windows and Linux ARM are unsupported.
+
+
+ Makarius
+ """ + Date.Format.date(Date.now()) + "\n")
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("component_mlton", "build component for MLton", Scala_Project.here,
+ { args =>
+ var target_dir = Path.current
+ var base_url = default_url
+ var version = default_version
+
+ val getopts = Getopts("""
+Usage: isabelle component_mlton [OPTIONS]
+
+ Options are:
+ -D DIR target directory (default ".")
+ -U URL download URL (default: """" + default_url + """")
+ -V VERSION version (default: """" + default_version + """")
+
+ Build component for MLton compiler.
+""",
+ "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_mlton(base_url = base_url, version = version, target_dir = target_dir,
+ progress = progress)
+ })
+}
--- a/src/Pure/Admin/component_postgresql.scala Thu Mar 21 17:36:50 2024 +0100
+++ b/src/Pure/Admin/component_postgresql.scala Thu Mar 21 21:04:49 2024 +0100
@@ -13,7 +13,7 @@
val notable_urls =
List("https://jdbc.postgresql.org", "https://jdbc.postgresql.org/download")
- val default_download_url = "https://jdbc.postgresql.org/download/postgresql-42.7.1.jar"
+ val default_download_url = "https://jdbc.postgresql.org/download/postgresql-42.7.3.jar"
/* build postgresql */
@@ -82,13 +82,14 @@
/* settings */
component_dir.write_settings("""
-classpath "$COMPONENT/""" + download_name + """.jar"
+classpath "$COMPONENT/lib/""" + download_name + """.jar"
""")
/* jar */
- val jar = component_dir.path + Path.basic(download_name).jar
+ val jar = component_dir.lib + Path.basic(download_name).jar
+ Isabelle_System.make_directory(jar.dir)
Isabelle_System.download_file(download_url, jar, progress = progress)
}
--- a/src/Pure/Admin/component_sqlite.scala Thu Mar 21 17:36:50 2024 +0100
+++ b/src/Pure/Admin/component_sqlite.scala Thu Mar 21 21:04:49 2024 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Admin/component_sqlite.scala
Author: Makarius
-Build Isabelle sqlite-jdbc component from official download.
+Build Isabelle sqlite component from official download.
*/
package isabelle
@@ -11,7 +11,7 @@
/* build sqlite */
val default_main_url =
- "https://repo1.maven.org/maven2/org/xerial/sqlite-jdbc/3.45.0.0/sqlite-jdbc-3.45.0.0.jar"
+ "https://repo1.maven.org/maven2/org/xerial/sqlite-jdbc/3.45.2.0/sqlite-jdbc-3.45.2.0.jar"
val default_logger_url =
"https://repo1.maven.org/maven2/org/slf4j/slf4j-api/1.7.36/slf4j-api-1.7.36.jar"
@@ -35,8 +35,9 @@
/* component */
+ val component_name = main_name.replace("-jdbc", "")
val component_dir =
- Components.Directory(target_dir + Path.basic(main_name)).create(progress = progress)
+ Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
def download(url: String): Path = {
val path = component_dir.lib + Path.basic(Url.get_base_name(url).get)
@@ -101,7 +102,7 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("component_sqlite", "build Isabelle sqlite-jdbc component from official download",
+ Isabelle_Tool("component_sqlite", "build Isabelle sqlite component from official download",
Scala_Project.here,
{ args =>
var target_dir = Path.current
@@ -118,7 +119,7 @@
-V URL logger URL
(default: """" + default_logger_url + """")
- Build sqlite-jdbc component from the specified download URL (JAR), see also
+ Build sqlite component from the specified download URL (JAR), see also
https://github.com/xerial/sqlite-jdbc and
https://oss.sonatype.org/content/repositories/releases/org/xerial/sqlite-jdbc
""",
--- a/src/Pure/ROOT.ML Thu Mar 21 17:36:50 2024 +0100
+++ b/src/Pure/ROOT.ML Thu Mar 21 21:04:49 2024 +0100
@@ -372,3 +372,4 @@
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML";
+
--- a/src/Pure/System/isabelle_tool.scala Thu Mar 21 17:36:50 2024 +0100
+++ b/src/Pure/System/isabelle_tool.scala Thu Mar 21 21:04:49 2024 +0100
@@ -182,6 +182,7 @@
Component_LIPIcs.isabelle_tool,
Component_LLNCS.isabelle_tool,
Component_Minisat.isabelle_tool,
+ Component_MLton.isabelle_tool,
Component_PDFjs.isabelle_tool,
Component_PolyML.isabelle_tool1,
Component_PolyML.isabelle_tool2,
--- a/src/Pure/Tools/dotnet_setup.scala Thu Mar 21 17:36:50 2024 +0100
+++ b/src/Pure/Tools/dotnet_setup.scala Thu Mar 21 21:04:49 2024 +0100
@@ -19,7 +19,7 @@
exec: String = "bash",
check: () => Unit = () => ())
- val all_platforms =
+ private val all_platforms =
List(
Platform_Info(Platform.Family.linux_arm, "arm64-linux", os = "linux", arch = "arm64"),
Platform_Info(Platform.Family.linux, "x86_64-linux", os = "linux"),
@@ -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 = "8.0.201"
+ def default_version: String = "8.0.203"
def dotnet_setup(
platform_spec: String = default_platform,