Email Gateway (Feb 06 2024 at 20:47): Email Gateway (Feb 06 2024 at 20:47):From: Makarius <makarius@sketis.net>
With Isabelle/37e57ac55559 we now have proven support for Linux ARM64, meaning
that there is a nightly "isabelle build -a" on a virtual server (from Netcup).
The Admin/build_release now works on Linux ARM64, and can produce logic images
for Linux ARM64. Thus regular repository snapshots (and release candidates)
support that platform by default, e.g. see
https://isatest.sketis.net/devel/release_snapshot
Still missing (to be investigated further) are the following external tools:
* z3: stuck at the rather old version 4.4.0, which lacks arm64-linux
binaries; the 4.4.1 arm64 package from ancient Debian is somewhat unstable on
current Ubuntu 20.04, see also failure of HOL-SMT_Examples recorded on
https://isatest.sketis.net/devel/build_status/index.html
* cvc4 (or rather cvc5)
* nunchaku
* smbc
* ocaml / opam
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Feb 13 2024 at 11:37):From: Makarius <makarius@sketis.net>
I've spent a lot of time experimenting with z3 4.4.0pre (0482e7fe727c), but
did not succeed so far (as of Isabelle/6e5f40cfa877): The session
HOL-SMT_Examples fails with timeout, due to non-terminating invocations of z3
on arm64-linux.
For verit there was a similar problem, but rebuilding it from source (with
"docker run -it ubuntu:18.04 bash") made it work; see also see
Isabelle/b14c4cb37d99.
For z3 the build instructions are as follows, using the attached z3.patch,
which is based on the Debian package and changes found in the z3 repository:
"""
docker run -it ubuntu:16.04 bash
apt-get update && apt-get upgrade -y && apt autoremove -y
apt install -y curl less libfontconfig1 libgomp1 openssh-client perl pwgen
rlwrap make g++ python
mkdir z3-4.4.0pre
cd z3-4.4.0pre
curl --location https://github.com/Z3Prover/z3/archive/0482e7fe727c.tar.gz |
tar --strip-components=1 -xz -f -
#inline z3.patch below
patch -p1 <<EOF
...
EOF
python scripts/mk_make.py
cd build && make
"""
That is minor progress, because the build works at all, by using ubuntu:16.04
instead of our official ubuntu:18.04 baseline.
For the planned release of Isabelle2024 (May 2024), I tend to disable z3 on
arm64-linux by default (via etc/settings of the component), and no longer
pretend that we have something working, see also
https://isabelle-dev.sketis.net/rISABELLE796ae338eb9d
Makarius
Email Gateway (Feb 14 2024 at 07:47):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Hi Makarius,
Thanks for investigating this. The binary components are always a special source of worry.
From what I understand, HOL-SMT_Examples will continue working thanks to the certificate caching mechanism that is used there. The mechanism isn't used in the AFP, though, which means arm64-linux users won't be able to load many AFP entries due to "smt" calls to Z3 in there. If this is too much of an issue, we could consider either of two solutions:
Replace the "smt" calls. Most of them could use the "(verit)" option instead, and for the others, we'd have to come up with alternative proofs. This possibly entails a lot of work, but it could be done by a "task force".
Use certificates for the AFP (and require their use in the future). Certificates take the form of low-level (SMT input, SMT output) pairs, so that when "smt" generates a given SMT input in the cache, the SMT output is used directly instead of running the SMT solver.
Best,
Jasmin
Email Gateway (Feb 14 2024 at 08:09):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Hi Makarius,
Still missing (to be investigated further) are the following external tools:
- z3: stuck at the rather old version 4.4.0, which lacks arm64-linux binaries; the 4.4.1 arm64 package from ancient Debian is somewhat unstable on current Ubuntu 20.04, see also failure of HOL-SMT_Examples recorded on https://isatest.sketis.net/devel/build_status/index.html
See my previous email.
- cvc4 (or rather cvc5)
CVC4 would be nice to have, but it's not critical in the same way as Z3.
cvc5 used to crash on Mac, but I'm told by Clark Barrett that with version 1.1.0 they've solved many Mac-specific bugs. I can experiment with it on my Mac and if it seems to work well, we could upgrade to that.
nunchaku
smbc
Nunchaku (and its backend SMBC) never left the experimental stage. Maybe we could move them out of "HOL" and mark them more clearly as experimental? I haven't given up all hopes of developing Nunchaku further and indeed just this week I was talking with a candidate about doing this, but it shouldn't block Isabelle releases.
- ocaml / opam
Thankfully somebody else's concern. :)
Jasmin
Email Gateway (Feb 14 2024 at 10:43):From: Lawrence Paulson <lp15@cam.ac.uk>
Somewhat to my surprise, there seem to be 1004 occurrences of “smt(z3" in the libraries and repository (I've never allowed it personally). It is outnumbered by verit more than 3 to 1, again a surprisingly low ratio.
Getting rid of them all would be a tedious business. One day we might consider automated tools to crawl over old the proofs and get rid of ugly things.
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Feb 14 2024 at 12:10):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Hi Larry,
"smt(z3" occurs seldom because z3 is the default for "smt", so often it's omitted. (I believe it used to be omitted and now it's explicit.)
Jasmin
Email Gateway (Feb 14 2024 at 12:23):From: Lawrence Paulson <lp15@cam.ac.uk>
That picks up a further 428 occurrences
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Feb 15 2024 at 09:04):From: Makarius <makarius@sketis.net>
I would say we just leave the status-quo for the Isabelle2024 release, i.e.
these tools are implicitly "experimental" and there is no arm64-linux support.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Feb 15 2024 at 13:51):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Hi Makarius,
Concerning cvc5: I tried downloading and running cvc5 1.1.1 for arm64 from
https://github.com/cvc5/cvc5/releases/
and I still get errors in Isabelle. For example, adding the line
sledgehammer[cvc5, mepo, slices=4]
before line 318 of the file "$AFP/thys/Given_Clause_Loops/DISCOUNT_Loop.thy" produces this output (nondeterministically):
Sledgehammering...
cvc5 found a proof...
cvc5 found a proof...
cvc5 found a proof...
cvc5 found a proof...
/tmp/isabelle-jasminblanchette/bash_script1894380443147744112: line 1: 30873 Abort trap: 6 /Users/jasminblanchette/.isabelle/contrib/cvc5-1.1.1/arm64-darwin/cvc5 --decision\=internal --simplification\=none --full-saturate-quant --proof-format-mode\=alethe --proof-granularity\=dsl-rewrite --no-stats --sat-random-seed\=1 --lang\=smt2 --tlimit 219 /tmp/isabelle-jasminblanchette/process10570530194278022654/cache-io-9904226 > /tmp/isabelle-jasminblanchette/process10570530194278022654/cache-io-9904228 2>&1
/tmp/isabelle-jasminblanchette/bash_script936180679870508119: line 1: 30876 Abort trap: 6 /Users/jasminblanchette/.isabelle/contrib/cvc5-1.1.1/arm64-darwin/cvc5 --trigger-sel\=max --full-saturate-quant --proof-format-mode\=alethe --proof-granularity\=dsl-rewrite --no-stats --sat-random-seed\=1 --lang\=smt2 --tlimit 222 /tmp/isabelle-jasminblanchette/process10570530194278022654/cache-io-9904284 > /tmp/isabelle-jasminblanchette/process10570530194278022654/cache-io-9904286 2>&1
/tmp/isabelle-jasminblanchette/bash_script2386389454125518978: line 1: 30882 Abort trap: 6 /Users/jasminblanchette/.isabelle/contrib/cvc5-1.1.1/arm64-darwin/cvc5 --full-saturate-quant --inst-when\=full-last-call --inst-no-entail --term-db-mode\=relevant --multi-trigger-linear --proof-format-mode\=alethe --proof-granularity\=dsl-rewrite --no-stats --sat-random-seed\=1 --lang\=smt2 --tlimit 221 /tmp/isabelle-jasminblanchette/process10570530194278022654/cache-io-9904420 > /tmp/isabelle-jasminblanchette/process10570530194278022654/cache-io-9904422 2>&1
cvc5: Try this: by (metis P0A_add_y_formula PYA_add_active_formula state.simps) (130 ms)
cvc5: Duplicate proof
cvc5: Duplicate proof
cvc5: Duplicate proof
Done
I don't know what the "Abort trap" warnings mean, because the prover seems to succeed nevertheless. I need to investigate. But I don't get these errors with CVC4.
Jasmin
Email Gateway (Feb 16 2024 at 14:10):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Hi all,
I've investigated further. The issue is hard to debug. It seems to arise only when minimizing proofs (where we call the solver repeatedly on often unprovable problems) and only when at least two solvers are run in parallel (i.e., when invoking Sledgehammer with "slices=2" or above).
I thought I might make some progress by replacing the "cvc5" binary with this script:
#!/bin/bash
cp ${!#} "$(mktemp /tmp/foo.XXXXXXXXX).smt"
/Users/jasminblanchette/.isabelle/contrib/cvc5-1.1.1/arm64-darwin/cvc5.bin $@
where "cvc5.bin" is the ARM64 Darwin cvc5 binary. But then the issue doesn't arise anymore!
As far as I can tell, the issue only arises with unprovable (sat) problems anyway, and it happens in such a way that it doesn't affect the workings of Sledgehammer. What's annoying is the yellow warning message in Isabelle/jEdit.
It looks like we can suppress the yellow message by writing a small wrapper script like the above (but using the proper idiom for retrieving the path of "cvc5.bin"). Is that what we should do? It would be great to leave CVC4 behind and to move to cvc5.
Jasmin
Email Gateway (Feb 16 2024 at 14:34):From: Makarius <makarius@sketis.net>
That could be some odd effect from switching between Intel and ARM on macOS,
maybe caused by our bash_process wrapper (which is for Intel in
Isabelle/0f01c575ff3e).
Apart from that, are you satisfied with cvc5-1.1.1? Does everything work with
the current Intel setup?
If so, I will see how to change our process wrappers such that everything
works again on all platforms.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Feb 17 2024 at 08:47):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
just my 5 cent: the certificates are helpful, but strictly relying on
them in distribution or AFP rules out people having no access to certain
provers to do work requiring potentially pervasive maintenance of proofs.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Feb 19 2024 at 11:51):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Hi Makarius,
I'm very satisfied with cvc5. I ran an evaluation on hundreds of goals from the AFP and the success rate went up from 52% for CVC4 to 64% for cvc5.
Jasmin
Email Gateway (Feb 29 2024 at 22:12):From: Makarius <makarius@sketis.net>
OK, so here is the cvc5-1.1.1 component for further testing:
https://isabelle-dev.sketis.net/rISABELLEf8fb4384180e
I only made some basic tests with sledgehammer in
src/HOL/Metis_Examples/Big_O.thy --- it looks fine so far on all platforms.
Note that arm64-linux is still missing from
https://github.com/cvc5/cvc5/releases/tag/cvc5-1.1.1
They claim that ARM64 is supported via cross compilation here:
https://github.com/cvc5/cvc5/blob/main/INSTALL.rst --- but they don't provide
binaries for download.
Maybe you can motivate the cvc5 guys to complete their set of downloads --- to
avoid "debianization" of this otherwise great tool --- meaning bad builds that
appear to work superficially.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Feb 29 2024 at 22:23):From: Makarius <makarius@sketis.net>
Now I've found the problem report, that I was looking for, but too late: The
cvc5 distribution of Isabelle/f8fb4384180e has the same problem (it uses the
"static" versions).
I've also updated all bash_process executables already in a861b0df74b4, now
with native arm64-darwin. This does not help here.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Mar 01 2024 at 17:22):From: Haniel Barbosa <hbarbosa@dcc.ufmg.br>
Hello,
FYI inspired by this thread we started to look into adding arm64 into
our CI pipeline so we can provide this binary for users. Unclear when
that'll materialize though.
Best,
Makarius <makarius@sketis.net> writes:
Email Gateway (Mar 01 2024 at 18:09):From: Makarius <makarius@sketis.net>
Haniel,
can you point to the place in the cvc5 repository (or elsewhere) where the
build happens? For now I could imitate that manually, e.g. on my own ARM64
Linux node together with docker.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Mar 01 2024 at 21:24):From: Haniel Barbosa <hbarbosa@dcc.ufmg.br>
Makarius <makarius@sketis.net> writes:
On 01/03/2024 18:21, Haniel Barbosa wrote:
FYI inspired by this thread we started to look into adding arm64
into
our CI pipeline so we can provide this binary for users. Unclear when
that'll materialize though.Haniel,
can you point to the place in the cvc5 repository (or elsewhere) where
the build happens? For now I could imitate that manually, e.g. on my
own ARM64 Linux node together with docker.
I'm not sure if I understand the question. The build system is based
on cmake and the code for it is here:
https://github.com/cvc5/cvc5/tree/main/cmake
There are a number of builds that happen during CI at GitHub that are
handled via the code here:
https://github.com/cvc5/cvc5/tree/main/.github/actions
There are also a number of builds that we run nightly but that is via
a private server (the binaries to download are generated from those,
and it's to that we will try to add arm64 builds).
If you have specific questions about it, the best is to use
https://github.com/cvc5/cvc5/discussions, where everybody in the team
will see it (I myself am no expert on the cvc5 build system hehe).
Best,
Makarius
Email Gateway (Mar 19 2024 at 21:53):From: Haniel Barbosa <hbarbosa@dcc.ufmg.br>
Hello,
I'm happy to report that we got this working now (thanks to Daniel
Larraz):
https://github.com/cvc5/cvc5/releases/tag/latest
Best,
Haniel Barbosa <hbarbosa@dcc.ufmg.br> writes:
Email Gateway (Mar 21 2024 at 09:47):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 27 2024 at 16:16 UTC