[isabelle-dev] Experimental support for arm64-linux

[David Matthews]

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