[PATCH] Fragile include for camlp4/camlp5

[GoogleCodeExporter]

I installed OCaml 4.00.0 and camlp5 using GODI a while back. Today, I checked 
out the hol-light sources, but when I tried building them I got the following 
error:

File "pa_j.ml", line 13, characters 0-10:
Error: Unbound module Pcaml
make: *** [pa_j.cmo] Error 2

After a bit of searching, I found that ocamlc treats the `-I +foo` argument as 
`-I /usr/lib/ocaml/foo`:
http://stackoverflow.com/questions/3848897/unbound-modules-in-ocaml

As it turns out, GODI installs camlp5 in a non-standard location. On this 
machine (Ubuntu 12.04.1 x86), `which camlp5` returns:
/opt/godi/bin/camlp5

So, I tweaked the Makefile a bit to make it more robust (see the attached 
diff). camlp4 and camlp5 both support the "-where" option, so I've used that 
within backticks along with the -I option when invoking ocamlc. This makes it 
so camlp4/camlp5 will be included properly no matter where it's installed on 
the system.

Cheers,
Jack

Original issue reported on code.google.com by [email protected] on 14 Feb 2013 at 9:22

Attachments:

• hol-light.diff

[GoogleCodeExporter]

Thanks very much Jack! I will roll this change into the next revision,
which I hope to get done this weekend.

Original comment by [email protected] on 23 Mar 2013 at 9:42

[GoogleCodeExporter]

Hi: I have OCaml 4.00.1, and used the command
 svn checkout http://hol-light.googlecode.com/svn/trunk/ hol-light-read-only
to download HOL light.

When I type 
make
to build it, it get the error message:

File "pa_j.ml", line 1918, characters 35-43:
While expanding quotation "str_item":
Parse error: antiquot "_" or antiquot "" or [ident] expected after 'type' (in
  [str_item])
File "pa_j.ml", line 1:
Error: Preprocessor error
make: *** [pa_j.cmo] Error 2

Can anyone help?
Thanks.....Neil

Original comment by [email protected] on 12 Oct 2013 at 7:02

[NikolasTzimoulis]

I'm getting this error and the patch can't be applied to my makefile (seems like it has been already incorporated?). Any advice?