Email Gateway (Oct 03 2020 at 14:43): Email Gateway (Oct 03 2020 at 14:43):From: Makarius <makarius@sketis.net>
Here is an intermediate report on the state of support for the ARM64 platform,
according to Isabelle/694d0a315d0a.
Presently, its main hardware representative is my new Raspberry Pi 4B (4 CPU
cores at 1.5 GHz, 8 GB RAM), running Ubuntu Linux 20.04 LTS. I've purchased
that for a bit less than 100 EUR; a suitable micro SD storage card needs to be
added (e.g. 128 GB for 20 EUR).
The most relevant Isabelle components already include arm64-linux parts, but
jdk is still missing. This works e.g. via the Ubuntu package "openjdk-11-jdk"
and the following $ISABELLE_HOME_USER/etc/settings:
ISABELLE_JDK_HOME="/usr/lib/jvm/java-11-openjdk-arm64"
An alternative is to download/unpack JDK 11 from https://adoptopenjdk.net
(platform aarch64) and point to that directory. I will include that in the
next official update of the jdk component, probably at the end of October.
Now most Isabelle/Scala tools should work properly, as well as Isabelle/ML
based on the existing interpreter by David Matthews for that platform: it is
approx. 50-100 times slower than the standard code-generator for x86_64.
Consequently, "isabelle jedit" might require some hours to build the Scala
jars + ML logic image for HOL (while ZF only requires minutes). To reduce
heat, it might require to disable the display and run "isabelle build -b HOL"
first via ssh.
At this stage we can already use sledgehammer with prover "e", e.g. in
$ISABELLE_HOME/src/HOL/Metis_Examples/BigO.thy on many of the metis proofs.
This requires some patience, but it is fun to see it all work on this tiny
little device.
Overall the experiment is not just for fun: Apple might ship fancy new ARM
MacBooks within a few months.
So we need to think about collecting some money for David Mattews to produce a
proper code generator for Poly/ML eventually. People who have some ideas
should contact me or David via private mail.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 03 2020 at 20:29):From: Makarius <makarius@sketis.net>
I have now found a beta version of Pi OS 64bit:
https://downloads.raspberrypi.org/raspios_arm64/images
Pi OS appears to support this special hardware better than Ubuntu, e.g.
graphics and CPU power regulation (less heating).
Consequently, I have rebuilt the polyml component in Isabelle/3e84f4e9651a; it
now works both with Pi OS (Debian 10) and Ubuntu 20.04.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 04 2020 at 19:16):From: Makarius <makarius@sketis.net>
Here are some timings for Isabelle/3e84f4e9651a on Pi OS 64bit beta (Debian 10.6):
Finished Pure (0:07:01 elapsed time, 0:07:01 cpu time, factor 1.00)
Finished HOL (3:04:18 elapsed time, 8:52:18 cpu time, factor 2.89)
Finished HOL-Word (0:28:07 elapsed time, 1:33:39 cpu time, factor 3.33)
Finished HOLCF (0:11:18 elapsed time, 0:26:53 cpu time, factor 2.38)
It is good to see that our huge HOL image already works on this tiny machine,
with interpreted Poly/ML.
HOL-Analysis and HOL-Library failed, due some to odd timeouts and missing z3
for arm64-linux.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 04 2020 at 14:52):From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
Hi,
I was revisiting this thread about the arm64 backend for Poly/ML.
Unfortunately, I don't have any ideas about the funding but more of a
technical remark. When implementing a new backend, I think one should
think about using LLVM due to the following reasons:
It supports amd64 and arm64 (and more).
It comes with useful tooling including a debugger and a profiler.
On the other hand, I am not very well versed about the costs and
benefits of using LLVM as a backend for a functional language. Haskell
has an LLVM backend [1] that seems to work quite well [2] which
confirms that it can work.
Kind regards,
Lukas
[1]
https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/backends/llvm
[2]
https://andreaspk.github.io/posts/2019-08-25-Opinion%20piece%20on%20GHC%20backends.html
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 04 2020 at 17:29):From: Florian Märkl <isabelle-dev@florianmaerkl.de>
Hello,
I am planning to write my Master's thesis at TUM in the coming summer
semester and I wonder whether implementing this backend for Poly/ML
would be a fitting topic for this.
I have recently bought myself a PineBook Pro, which is a small aarch64
laptop, maybe slightly faster than a Raspberry Pi 4, and I have actually
been using this as my main laptop for a few months now.
I use it mostly for programming C and Haskell, but could also play
around with Isabelle a bit and can confirm that the only blocker there
seems to be that it is just unbearably slow, so I do have some
motivation to fix this.
About GHC's llvm backend, I can also confirm that it indeed works very
well, with the main issue being the fact that llvm is generally quite
big and resource-hungry.
In fact, while compiling GHC itself and many other Haskell libraries
(which I had to do all by myself because Arch Linux ARM, which I use,
does not provide any Haskell packages), I ran out of memory multiple
times, had to reduce concurrency and eventually set up a Raspberry Pi 4
with 8GB of RAM and a lot of swap space as an external build server for
this. For reference, a build of GHC takes about one full night.
This blog post also mentions that it would still be desirable to have a
native arm backend in GHC:
https://www.haskell.org/ghc/blog/20200515-ghc-on-arm.html
So I think this is an important aspect, especially considering that
Isabelle compiles code on the fly while using it. However I don't know
how much ML code is actually being compiled during a usual Isabelle
session, so I can't say how strongly this will affect the experience in
the end.
On the other hand, there are of course the obvious benefits of llvm,
including that it already has a huge set of well-tested optimization
passes, and even if these optimizations won't fit as well to ML as they
do to classic imperative languages, in the worst case, it would be
degraded to a simple code generator for arbitrary architectures and some
language-specific optimization could be done before translating to LLVM IR.
It would be nice if someone from Prof. Nipkow's or related chairs could
give me some feedback whether this could theoretically fit for a
Master's thesis.
Florian
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 05 2020 at 11:48):From: David Matthews <dm@prolingua.co.uk>
Llvm has come up as a suggestion a number of times. I did look at it
some years ago as a possible back-end for Poly/ML and came to the
conclusion that it wouldn't work in the way that was needed. I read the
blog post about GHC and thought it was interesting that they still felt
the need to have their own back-end as well.
The problem I could see was that Llvm seems to have its own ideas about
data representation and that wouldn't fit with the way Poly/ML works
especially in Isabelle. I could see a possible use for it as a back-end
when Poly/ML was batch-compiling some ML code to be executed as a
separate program.
However, interactive theorem proving in Isabelle is more like
manipulating data structures some of whose elements happen to be blobs
of executable code. This fits with the view of a functional language in
which functions are just another kind of value. The Poly/ML compiler,
just another function in the environment, builds code in the heap and if
the heap is saved to disc only then will the code be written out. That
is quite different from the conventional view of a compiler.
I'm quite happy to provide any information needed if someone wants to
look at an Llvm back-end but I don't see it working with Isabelle.
David
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 23 2024 at 12:29 UTC