Re: [Caml-list] ocamlc compiles hello world, ocamlopt not

[Benedikt Meurer <benedikt.meurer@googlemail.com>]

On Jan 17, 2013, at 0:17 , Gabriel Scherer <gabriel.scherer@gmail.com> wrote:

> Benedikt, let me jump on the occasion to provide more pointers you
> might be interested in:
> 
> - Raphaël Amiard, a student at Paris 6 university, recently worked on
> translating OCaml byte into LLVM:
> https://github.com/raph-amiard/CamllVM ; I have not seen a definite
> comparison with Colin's and Benoit's work, but they appear to hit the
> same kind of issues (performance degradation of exceptions, handling
> GC roots that are passed in registers)

Yeah, I've seen that earlier on the mailinglist.

> - VeriML is a research language for writing tactics and proof
> assistants; developed at Yale during Antonis Stampoulis recently
> finished thesis ( http://www.cs.yale.edu/homes/stampoulis/ ); they
> have a HOL-like mode of interaction, where the user-interface to the
> prover is directly a toplevel (forked from OCaml's toplevel), and they
> use OCamlJIT2 to provide good performances within this model.

That sounds interesting. And it would certainly benefit from a trace-based JITter. :-)

Benedikt