[isabelle-dev] Proven support for Linux ARM64

[Makarius]

On 19/03/2024 22:52, Haniel Barbosa wrote:
> 
> I'm happy to report that we got this working now (thanks to Daniel
> Larraz):
> 
>    https://github.com/cvc5/cvc5/releases/tag/latest

Many thanks.

I have tried it out briefly on all Isabelle platforms, see also 
https://isabelle-dev.sketis.net/rISABELLE67d28b35c5d8 --- cvc5-latest versions 
change quickly, so that precise version has disappeared already.


The arm64-linux version basically works on my 2 test machines: virtual Ubuntu 
22.04 and physical Raspberry PI with an old version of Debian.

I did see a few crashes, though, when several cvc5 processes are running 
concurrently. Maybe that is the same crash that Jasmin has observed on 
arm64-darwin: I am including a test example as changeset for AFP. That can be 
reproduced with the Isabelle component "cvc5-1.1.1" (e.g. edited into 
Admin/components/main followed by "Admin/init").


	Makarius


-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1710970338 -3600
#      Wed Mar 20 22:32:18 2024 +0100
# Node ID 6f574c87ab99f0fe09080536c4f36f0ba7eb81fa
# Parent  f51730d25fc3e688e4e3ec5ae0dd96f0f555d068
test

diff -r f51730d25fc3 -r 6f574c87ab99 thys/Given_Clause_Loops/DISCOUNT_Loop.thy
--- a/thys/Given_Clause_Loops/DISCOUNT_Loop.thy	Tue Mar 19 16:45:23 2024 +0100
+++ b/thys/Given_Clause_Loops/DISCOUNT_Loop.thy	Wed Mar 20 22:32:18 2024 +0100
@@ -314,7 +314,7 @@
   then have "(T, labeled_formulas_of (P, {}, A) \<union> {(C, YY)}) \<leadsto>LGC
     (T \<union> T', labeled_formulas_of (P, {}, A) \<union> {(C, Active)})"
     using lgc.step.schedule_infer by blast
-  then show ?thesis
+  then show ?thesis sledgehammer [cvc5, mepo, slices = 2]
     by (metis state.simps P0A_add_y_formula PYA_add_active_formula)
 qed