[isabelle-dev] Experimental support for arm64-linux
Lukas Stevens
lukas.stevens+isabelle-users at in.tum.de
Wed Nov 4 15:52:07 CET 2020
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
More information about the isabelle-dev
mailing list