# HG changeset patch # User wenzelm # Date 1736343017 -3600 # Node ID 377887fbc9683fa4d4e5ef4d9cd8b73fcb4553d7 # Parent 2f70c60cdbb2c20f3bdca6099a0cfd4dc6ce2765 rebuild cvc5 component (still inactive); more robust workaround on all platforms, avoid crash of "sledgehammer [cvc5]" seen on x86_64-linux after line 75 of "$AFP/thys/Boolos_Curious_Inference_Automated/Boolos_Curious_Inference_Automated.thy"; diff -r 2f70c60cdbb2 -r 377887fbc968 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Wed Jan 08 05:38:13 2025 +0100 +++ b/Admin/components/components.sha1 Wed Jan 08 14:30:17 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 +061ab74da6f101b7cf9935d0dac0bf58c62b19b5 cvc5-1.2.0-1.tar.gz 9cd7fa5e32187383fbf461d3643cf982a318e39d cvc5-1.2.0.tar.gz 842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz diff -r 2f70c60cdbb2 -r 377887fbc968 src/Pure/Admin/component_cvc5.scala --- a/src/Pure/Admin/component_cvc5.scala Wed Jan 08 05:38:13 2025 +0100 +++ b/src/Pure/Admin/component_cvc5.scala Wed Jan 08 14:30:17 2025 +0100 @@ -60,21 +60,22 @@ Isabelle_System.make_directory(platform_dir) val exe_path = Path.explode("cvc5").exe_if(platform.is_windows) + val exe_bin_path = Path.explode("cvc5-bin").exe_if(platform.is_windows) + val exe = platform_dir + exe_path + val exe_bin = platform_dir + exe_bin_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(exe) + + Isabelle_System.copy_file(download_dir + Path.basic("bin") + exe_path, exe_bin) + File.set_executable(exe_bin) - if (platform.is_arm) { - Isabelle_System.move_file(exe, exe.ext("bin")) - File.write(exe, """#!/usr/bin/env bash + File.write(exe, """#!/usr/bin/env bash -"$CVC5_HOME/cvc5.bin" "$@" +"$CVC5_HOME/cvc5-bin" "$@" """) - File.set_executable(exe) - } + File.set_executable(exe) } }