[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


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,




More information about the isabelle-dev mailing list