OCaml, originally known as Objective Caml, is the main implementation of the Caml programming language, created by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy and others in 1996. OCaml extends the core Caml language with object-oriented constructs. It is a free open source project managed and principally maintained by INRIA.
OCaml’s toolset includes an interactive toplevel interpreter, a bytecode compiler, and an optimizing native code compiler. It has a large standard library that makes it useful for many of the same applications as Python or Perl, as well as robust modular and object-oriented programming constructs that make it applicable for large-scale software engineering. OCaml is the successor to Caml Light. The acronym CAML originally stood for Categorical Abstract Machine Language, although OCaml abandons this abstract machine.
Functional Languages are, in general, more academic due to their performance costs. OCaml, however, puts some focus on performance although this means, on average, about 50% of the performance of a decent C Compiler.
COQ is a math library, also developed by INRIA, and much of the code is reused from OCaml source code. The only assembly code I could find were some registry locations defined by architecture type. This was in the coq_interp.c file
Looking around the Coq source code, I was unable to find anywhere that these definitions were used! So i appealed to the COQ community. The answer I got back is that the code was brought over from the OCaml VM, which already has the source code updated for Arm64 and it just needs to be brought over to AArch64
https://github.com/ocaml/ocaml/blob/trunk/byterun/interp.c#L107
#ifdef __aarch64__
#define PC_REG asm(“%x19”)
#define SP_REG asm(“%x20”)
#define ACCU_REG asm(“%x21”)
#define JUMPTBL_BASE_REG asm(“%x22”)
#endif
So it looked like this wasn’t exactly something that needed to be tackled. I looked on……
Moshe's Linaro Journey 