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