John, your fix worked, on both a 32 bit and a 64 bit Dell running Scientific Linux! My Tarksi code runs with ocaml 3.12.1 & camlp5!
I think the current Makefile will end up using "pa_j_3.1x_6.xx.ml" That's what happened, and that's partly because camlp5 -v 2>&1 | cut -f3 -d' ' | cut -c1 => 6 You could try manually copying one of the more recent versions then doing "make", e.g: make clean cp pa_j_3.1x_6.02.2.ml pa_j.ml make Make works fine! We take the else fork ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I +camlp5 pa_j.ml which is obviously the one we want, and not the camlp4r fork. BTW I first thought #use "hol.ml";; didn't work, and I was going to mail you the transcript, which included File "/home/richter/HOL/hol_light/system.ml", line 31, characters 0-13: Error: Unbound value set_jrh_lexer But I looked at it, and realized I was in the wrong directory, and I reset the variable export HOLLIGHT_DIR=/home/richter/hol_light I guess it pays to look at the error message :) I set the other variable, but I'm not sure that was needed: export CAMLP5LIB=$HOME/HOL-Light/lib/ocaml/camlp5 On the 64 bit machine I've never set it. -- Best, Bill ------------------------------------------------------------------------------ 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
