Email Gateway (Jan 31 2025 at 14:47): Email Gateway (Jan 31 2025 at 14:47):From: Makarius <makarius@sketis.net>
* HOL *
This refers to Isabelle/bbda3b4f3c99.
That is not just an update from version 4 to 5, but the change of spelling the
name indicates that it is a quite different system.
One guy at Lean Together 2025, when talking about Sledgehammer and
Magnushammer even put an exclamation mark at "Use cvc5!" (see minute 4:25 of
https://www.youtube.com/watch?v=T9fhMJmJRAw&list=PLlF-CfQhukNlzXdQvu1SVt9vcD4--fLlg&index=20).
The support for arm64-linux was not available before, which is extra
motivation to move on now. Thus we are almost complete in supporting that
platform.
Testing cvc5 beforehand, we did encounter a few oddities concerning signals
already, but lets hope that this workaround is now sufficient:
changeset: 81746:377887fbc968
user: wenzelm
date: Wed Jan 08 14:30:17 2025 +0100
files: Admin/components/components.sha1 src/Pure/Admin/component_cvc5.scala
description:
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";
It wraps everything into an outermost bash process, and refrains from using
"exec" to make a "POSIX tail call". Thus the resulting process hierarchy looks
more like a regular Terminal / shell process. (There are many fine points on
process hierarchies and signals that can be done wrong. While I don't
understand everything myself, I've seen enough bad approaches to be avoided.)
Makarius
Email Gateway (Jan 31 2025 at 22:45):From: Makarius <makarius@sketis.net>
On 31/01/2025 15:46, Makarius wrote:
The support for arm64-linux was not available before, which is extra
motivation to move on now. Thus we are almost complete in supporting that
platform.
I have tested it on my new arm64-linux desktop computer: 4 cores at 2.4 GHz, 8
GB RAM, 32 GB microSD storage --- for 110,- EUR total
https://www.reichelt.de/de/de/shop/produkt/das_reichelt_raspberry_pi_5_b_8_gb_all-in-bundle-370371
So far it looks good, but 8 GB is not much: I should have bought the 16 GB
version. The GPU performance is also a bit lacking (using UHD/4K resolution):
our jEdit Graphics2D painting is quite ambitious, but with Ubuntu 24.04 it
appears to be better than with the default Pi OS.
Makarius
Email Gateway (Jan 31 2025 at 23:12):From: Manuel Eberl <manuel@pruvisto.org>
In case you're not happy with the performance of the microSD storage, I
have this case for my Raspberry Pi 5 that has support for an NVMe SSD
and it works pretty well:
https://www.berrybase.at/argon-one-v3-m.2-case-fuer-raspberry-pi-5-nvme
Manuel
On 31/01/2025 23:44, Makarius wrote:
On 31/01/2025 15:46, Makarius wrote:
The support for arm64-linux was not available before, which is extra
motivation to move on now. Thus we are almost complete in supporting
that platform.I have tested it on my new arm64-linux desktop computer: 4 cores at
2.4 GHz, 8 GB RAM, 32 GB microSD storage --- for 110,- EUR total
https://www.reichelt.de/de/de/shop/produkt/das_reichelt_raspberry_pi_5_b_8_gb_all-in-bundle-370371So far it looks good, but 8 GB is not much: I should have bought the
16 GB version. The GPU performance is also a bit lacking (using UHD/4K
resolution): our jEdit Graphics2D painting is quite ambitious, but
with Ubuntu 24.04 it appears to be better than with the default Pi OS.Makarius
Email Gateway (Feb 01 2025 at 12:19):From: Makarius <makarius@sketis.net>
On 01/02/2025 00:12, Manuel Eberl wrote:
In case you're not happy with the performance of the microSD storage, I have
this case for my Raspberry Pi 5 that has support for an NVMe SSD and it works
pretty well: https://www.berrybase.at/argon-one-v3-m.2-case-fuer-raspberry-
pi-5-nvme
Thanks for the hint. I've learned now the keywords to search for:
"raspberrypi 5 nvme hat", the the "HAT" is the board to carry the M2/NVME storage.
Makarius
Last updated: Feb 01 2025 at 20:19 UTC