Various users have reported the same problem over the last year or so, see
http://code.google.com/p/hol-light/issues/detail?id=2.
I have encountered the same problem using Camlp5 version 6.06 as Colin
Rowat also did recently. There seems to be a trend here, that all new
versions of camlp5 work with the HOL Light file pa_j_3.1x_6.02.2.ml, but do
_not_ work with HOL Light file pa_j_3.1x_6.xx.ml, though the Makefile uses
the latter as its default.
I have diffed these two files and see that the "6.02" file has a later
revision ID that it got from somewhere:
--- pa_j_3.1x_6.xx.ml 2012-07-01 20:30:43.000000000 -0700
+++ pa_j_3.1x_6.02.2.ml 2012-07-01 20:30:43.000000000 -0700
@@ -20,7 +20,7 @@
(*
------------------------------------------------------------------------- *)
(* camlp5r *)
-(* $Id: reloc.ml,v 6.15 2010-11-14 11:20:26 deraugla Exp $ *)
+(* $Id: reloc.ml,v 6.19 2011-02-17 10:20:50 deraugla Exp $ *)
Encouraged by this, I successfully tried the following edit to the Makefile:
--- Makefile (revision 146)
+++ Makefile (working copy)
@@ -56,10 +56,7 @@
then cp pa_j_${OCAML_VERSION}.ml pa_j.ml ; \
else if test ${CAMLP5_VERSION} = "6.02.1" ; \
then cp pa_j_3.1x_6.02.1.ml pa_j.ml; \
- else if test ${CAMLP5_VERSION} = "6.02.2" -o
${CAMLP5_VERSION} = "6.02.3" -o ${CAMLP5_VERSION} = "6.05" ; \
- then cp pa_j_3.1x_6.02.2.ml pa_j.ml; \
- else cp pa_j_3.1x_${CAMLP5_BINARY_VERSION}.xx.ml pa_j.ml;
\
- fi \
+ else cp pa_j_3.1x_6.02.2.ml pa_j.ml; \
fi \
fi
This change makes pa_j_3.1x_6.02.2.ml the default version of pa_j.ml,
bypassing special-case checks for every version since 6.02.1. Given recent
history of problems users are having with new versions of camlp5, I suggest
this as a change to the distribution Makefile.
If you accept this change you might wish to delete the file
pa_j_3.1x_6.xx.ml.
Regards,
Cris
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
