--- a/Admin/components/components.sha1 Thu Dec 24 13:10:18 2020 +0000
+++ b/Admin/components/components.sha1 Thu Dec 24 15:40:57 2020 +0000
@@ -321,6 +321,7 @@
4d17611857fa3a93944c1f159c0fd2a161967aaf sqlite-jdbc-3.27.2.1.tar.gz
806be457eb79408fcc5a72aeca3f64b2d89a6b63 sqlite-jdbc-3.30.1.tar.gz
cba2b194114216b226d75d49a70d1bd12b141ac8 sqlite-jdbc-3.32.3.2.tar.gz
+29306acd6ce9f4c87032b2c271c6df035fe7d4d3 sqlite-jdbc-3.34.0.tar.gz
8d20968603f45a2c640081df1ace6a8b0527452a sqlite-jdbc-3.8.11.2.tar.gz
2369f06e8d095f9ba26df938b1a96000e535afff ssh-java-20161009.tar.gz
a2335d28b5b95d8d26500a53f1a9303fc5beaf36 ssh-java-20190323.tar.gz
--- a/Admin/components/main Thu Dec 24 13:10:18 2020 +0000
+++ b/Admin/components/main Thu Dec 24 15:40:57 2020 +0000
@@ -17,7 +17,7 @@
scala-2.12.12
smbc-0.4.1
spass-3.8ds-2
-sqlite-jdbc-3.32.3.2
+sqlite-jdbc-3.34.0
ssh-java-20190323
stack-2.5.1
vampire-4.2.2
--- a/lib/scripts/isabelle-platform Thu Dec 24 13:10:18 2020 +0000
+++ b/lib/scripts/isabelle-platform Thu Dec 24 15:40:57 2020 +0000
@@ -6,6 +6,7 @@
ISABELLE_PLATFORM_FAMILY=""
ISABELLE_PLATFORM32=""
ISABELLE_PLATFORM64=""
+ISABELLE_APPLE_PLATFORM64=""
ISABELLE_WINDOWS_PLATFORM32=""
ISABELLE_WINDOWS_PLATFORM64=""
@@ -34,6 +35,13 @@
;;
*)
ISABELLE_PLATFORM64=x86_64-darwin
+ case $(uname -m) in
+ arm64)
+ ISABELLE_APPLE_PLATFORM64=arm64-darwin
+ ;;
+ *)
+ ;;
+ esac
;;
esac
;;
--- a/src/HOL/Hoare/hoare_syntax.ML Thu Dec 24 13:10:18 2020 +0000
+++ b/src/HOL/Hoare/hoare_syntax.ML Thu Dec 24 15:40:57 2020 +0000
@@ -206,11 +206,14 @@
(** setup **)
+val _ =
+ Theory.setup
+ (Sign.parse_translation
+ [(\<^syntax_const>\<open>_hoare_vars\<close>, hoare_vars_tr),
+ (\<^syntax_const>\<open>_hoare_vars_tc\<close>, hoare_tc_vars_tr)]);
+
fun setup consts =
Data.put (SOME consts) #>
- Sign.parse_translation
- [(\<^syntax_const>\<open>_hoare_vars\<close>, hoare_vars_tr),
- (\<^syntax_const>\<open>_hoare_vars_tc\<close>, hoare_tc_vars_tr)] #>
Sign.print_translation
[(#Valid consts, spec_tr' \<^syntax_const>\<open>_hoare\<close>),
(#ValidTC consts, spec_tr' \<^syntax_const>\<open>_hoare_tc\<close>)];
--- a/src/Pure/Admin/build_sqlite.scala Thu Dec 24 13:10:18 2020 +0000
+++ b/src/Pure/Admin/build_sqlite.scala Thu Dec 24 15:40:57 2020 +0000
@@ -67,6 +67,7 @@
"META-INF/maven/org.xerial/sqlite-jdbc/LICENSE.zentus" -> ".",
"org/sqlite/native/Linux/aarch64/libsqlitejdbc.so" -> "arm64-linux",
"org/sqlite/native/Linux/x86_64/libsqlitejdbc.so" -> "x86_64-linux",
+ "org/sqlite/native/Mac/aarch64/libsqlitejdbc.jnilib" -> "arm64-darwin",
"org/sqlite/native/Mac/x86_64/libsqlitejdbc.jnilib" -> "x86_64-darwin",
"org/sqlite/native/Windows/x86_64/sqlitejdbc.dll" -> "x86_64-windows")
@@ -95,7 +96,8 @@
-D DIR target directory (default ".")
Build sqlite-jdbc component from the specified download URL (JAR), see also
- https://github.com/xerial/sqlite-jdbc/releases
+ https://github.com/xerial/sqlite-jdbc and
+ https://oss.sonatype.org/content/repositories/releases/org/xerial/sqlite-jdbc
""",
"D:" -> (arg => target_dir = Path.explode(arg)))
--- a/src/Pure/Admin/isabelle_cronjob.scala Thu Dec 24 13:10:18 2020 +0000
+++ b/src/Pure/Admin/isabelle_cronjob.scala Thu Dec 24 15:40:57 2020 +0000
@@ -350,6 +350,7 @@
List(
Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
options = "-m32 -M4" +
+ " -C /cygdrive/d/isatest/contrib" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
@@ -359,6 +360,7 @@
Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64_32-windows")),
Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
options = "-m64 -M4" +
+ " -C /cygdrive/d/isatest/contrib" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",