[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