provide component cvc5-1.2.0, including arm64-linux;
workaround for ARM64 platform, avoid odd crash of "sledgehammer [cvc5, mepo, slices = 4]" before line 318 of "$AFP/thys/Given_Clause_Loops/DISCOUNT_Loop.thy";
--- a/Admin/components/components.sha1 Thu Jan 02 08:37:55 2025 +0100
+++ b/Admin/components/components.sha1 Thu Jan 02 12:13:18 2025 +0100
@@ -47,6 +47,7 @@
e99560d0b7cb9bafde2b0ec1a3a95af315918a25 cvc4-1.8.tar.gz
9e0d91f9f3bc0b69e60e50ca683cfcdcbfee6d62 cvc5-1.0.2.tar.gz
fb4dce7e622c5e3daf56e7db190e05c34985c9f6 cvc5-1.1.1.tar.gz
+9cd7fa5e32187383fbf461d3643cf982a318e39d cvc5-1.2.0.tar.gz
842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz
cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz
3b44cca04855016d5f8cfb5101b2e0579ab80197 cygwin-20130117.tar.gz
--- a/src/Pure/Admin/component_cvc5.scala Thu Jan 02 08:37:55 2025 +0100
+++ b/src/Pure/Admin/component_cvc5.scala Thu Jan 02 12:13:18 2025 +0100
@@ -14,6 +14,7 @@
/* platform information */
sealed case class Download_Platform(platform_name: String, download_name: String) {
+ def is_arm: Boolean = platform_name.startsWith("arm64-")
def is_windows: Boolean = platform_name.endsWith("-windows")
}
@@ -59,11 +60,21 @@
Isabelle_System.make_directory(platform_dir)
val exe_path = Path.explode("cvc5").exe_if(platform.is_windows)
+ val exe = platform_dir + exe_path
Isabelle_System.download_file(download, archive_path, progress = progress)
Isabelle_System.extract(archive_path, download_dir, strip = true)
Isabelle_System.copy_file(download_dir + Path.basic("bin") + exe_path, platform_dir)
- File.set_executable(platform_dir + exe_path)
+ File.set_executable(exe)
+
+ if (platform.is_arm) {
+ Isabelle_System.move_file(exe, exe.ext("bin"))
+ File.write(exe, """#!/usr/bin/env bash
+
+"$CVC5_HOME/cvc5.bin" "$@"
+""")
+ File.set_executable(exe)
+ }
}
}