Ramana,

On 14 Oct 2013, at 14:41, Ramana Kumar <ram...@member.fsf.org> wrote:

> From what I remember, camlp5 and ocaml versioning is a nightmare... (though 
> it may be that HOL Light is a particularly strenuous application for it).
> One might find Alex Krauss's approach useful: 
> http://sourceforge.net/mailarchive/message.php?msg_id=29220282, if going at 
> the pa_j.ml file doesn't hack it one day.
> 
> 
I did install ocaml and camlp5 from source as Alex suggests, but it doesn't 
help in this case.  The problem is that pa_j.ml contains modified copies of 
various bits of the camlp5 source that have changed significantly.

The current situation seems to be that if you use the latest ocaml you have to 
use the latest camlp5. So I think if you want HOL Light to build out of the box 
you are pretty well forced to use a version of ocaml that is nearly 2 years old.

Regards,

Rob.


------------------------------------------------------------------------------
October Webinars: Code for Performance
Free Intel webinars can help you accelerate application performance.
Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from 
the latest Intel processors and coprocessors. See abstracts and register >
http://pubads.g.doubleclick.net/gampad/clk?id=60134071&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to