Re: [isabelle] Isabelle2021-1-RC3 sledgehammer works fine on ARM64



On 13/11/2021 22:05, Frédéric Boulanger wrote:
> 
> I provide my students with a Docker image containing all the software they
> need for the year, and some of them have MacBooks with M1 chips so they need
> the arm64-linux version of the image.
> 
> I did not make extensive tests and only checked that what I need for my
> courses works. I also managed to build the Why3 <http://why3.lri.fr/> Isabelle
> session in which many proofs "by smt" failed with RC1, so I guess it is all
> the interface with smt solvers that benefits from the work on Poly/ML.

Poly/ML on arm64 is one thing, and external provers are another thing. I have
successfully built most tools for arm64-linux, with the following exceptions:

    . cvc4
    . z3
    . nunchaku
    . smbc

The default for the "smt" proof method is z3, but veriT is getting more and
more significant, which is already on arm64-linux.

After spending many hours with z3-4.4.0 and z3-4.4.1, which are both quite old
but close to our current component z3-4.4.0pre-3, I've come to the conclusion
that supporting z3 on arm64-linux requires a proper update to a current
version https://github.com/Z3Prover/z3/tags

We cannot warp the underlying z3 several years from distant past into the
present, without significant work on the Isabelle side.

So for Isabelle2021-1-RC1 nothing is going to happen --- unless you come up
with a patch for z3-4.4.0 or z3-4.4.1 (based on the included one for 4.4.1).


	Makarius
diff -ru src-orig/util/debug.cpp src/util/debug.cpp
--- src-orig/util/debug.cpp	2015-10-05 14:07:19.000000000 +0200
+++ src/util/debug.cpp	2021-11-15 16:37:30.034668913 +0100
@@ -76,7 +76,7 @@
     for (;;) {
         std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB\n";
         char result;
-        bool ok = (std::cin >> result);
+        bool ok = bool(std::cin >> result);
         if (!ok) exit(ERR_INTERNAL_FATAL); // happens if std::cin is eof or unattached.
         switch(result) {
         case 'C':
diff -ru src-orig/util/hwf.cpp src/util/hwf.cpp
--- src-orig/util/hwf.cpp	2015-10-05 14:07:19.000000000 +0200
+++ src/util/hwf.cpp	2021-11-15 16:38:05.506073093 +0100
@@ -45,7 +45,7 @@
 // clear to the compiler what instructions should be used. E.g., for sqrt(), the Windows compiler selects
 // the x87 FPU, even when /arch:SSE2 is on. 
 // Luckily, these are kind of standardized, at least for Windows/Linux/OSX.
-#ifdef __clang__
+#if defined(__clang__) || (defined(__GNUC__) && !defined(__SSE2__))
 #undef USE_INTRINSICS
 #else
 #include <emmintrin.h>
diff -ru src-orig/util/mpz.cpp src/util/mpz.cpp
--- src-orig/util/mpz.cpp	2015-10-05 14:07:19.000000000 +0200
+++ src/util/mpz.cpp	2021-11-15 16:52:36.355432500 +0100
@@ -134,7 +134,7 @@
 #endif
     
     mpz one(1);
-    set(m_two64, UINT64_MAX);
+    set(m_two64, static_cast<int64>UINT64_MAX);
     add(m_two64, one, m_two64);
 }
 
diff -ru src-orig/util/util.h src/util/util.h
--- src-orig/util/util.h	2015-10-05 14:07:19.000000000 +0200
+++ src/util/util.h	2021-11-15 16:38:47.281371291 +0100
@@ -48,7 +48,7 @@
 #define INT64_MAX static_cast<int64>(0x7fffffffffffffffull)
 #endif                              
 #ifndef UINT64_MAX
-#define UINT64_MAX 0xffffffffffffffffull
+#define UINT64_MAX static_cast<uint64>(0xffffffffffffffffull)
 #endif
 
 #ifdef _WINDOWS


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.