Colin, let me see if I understand. You hacked the Makefile so that you use (as I did) pa_j_3.1x_6.02.2.ml And then `make' succeeds, but you get a warning `pattern-matching is not exhaustive'? If so, then I suggest
1) If your warning doesn't cause any trouble, don't worry about it until John Harrison comes back and can deal with it. What are you using HOL Light in order to do? 2) See why the Makefile doesn't automatically use pa_j_3.1x_6.02.2.ml as it does for me on Scientific Linux. John changed the Makefile (I'd guess) so that SL would use automatically use pa_j_3.1x_6.02.2.ml. Maybe Ubuntu is different, and nyou need a different version of pa_j.ml. See if John's May 15 post to me helps http://sourceforge.net/mailarchive/message.php?msg_id=29268458 where he also suggested I use (which I didn't) cp pa_j_3.1x_6.02.1.ml pa_j.ml make and Alex Krauss's script https://bitbucket.org/akrauss/hol-light-workbench/ -- 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
