> 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'?
Thank you Bill. Yes, 'make' completes, giving at least the following error messages/warnings: (i) "inventing type variables" [a warning rather than an error] (ii) various .ml files have already been loaded [again, this seems non-fatal] (iii) the pattern matching is not exhaustive message [I'm not able to suggest the severity of this message] > 1) If your warning doesn't cause any trouble, don't worry about it > until John Harrison comes back and can deal with it. I'm not experienced enough with HOL Light to know whether it's fully functional, but it does now avoid the errors that I encountered earlier when trying to use definitions in sets.ml. Thus, it may be reasonable to conclude that I have now successfully built HOL Light. > What are you using HOL Light in order to do? I'd like to code up an early auction theory result due to Vickrey as a worked example for a PhD workshop I'm giving next month. > 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/ Thank you - I'd not known about Alex' script. If it seems that I don't have a proper installation, I'll try that. Best, and thank you again, Colin ------------------------------------------------------------------------------ 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
