Dear Bill, At Mon, 21 Jan 2013 22:21:51 -0600, Bill Richter wrote: > > Marko, as Ramana said, you're having a ocaml/campl5 problem. You didn't say > which HOL Light version you're using. I reccommend the latest subversion. > That might fix the problem. If not, read John Harrison's post > http://sourceforge.net/mailarchive/message.php?msg_id=29268458 > You didn't say which OS you're using. I'm using Scientific Linux, and John > changed the makefile to use > pa_j_3.1x_6.02.2.ml
the hol-light version was the latest svn. I now tried all pa_j_3.1x_6*.ml files as pa_j.ml. I get the same error message with all of them. > John also recommended Alex Krauss's script > https://bitbucket.org/akrauss/hol-light-workbench/ I also tried the script after the above didn't work. It does not provide sufficient insulation against the OCaml/Camlp5 installed in /usr and eventually executes: ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I +camlp5 pa_j.ml Error while loading "/usr/lib/ocaml/camlp5/pa_lexer.cmo": interface mismatch on Grammar. File "pa_j.ml", line 1, characters 0-1: Error: Preprocessor error explicitly executing ocamlc -c -pp "camlp5r \ ~/src/hol-light-workbench/ocaml/lib/ocaml/camlp5/pa_lexer.cmo \ ~/src/hol-light-workbench/ocaml/lib/ocaml/camlp5/pa_extend.cmo \ ~/src/hol-light-workbench/ocaml/lib/ocaml/camlp5/q_MLast.cmo" -I \ +camlp5 pa_j.ml succeeded in getting past this point. I have made a change to the setup script and hope it will be pulled up. Best regards, Marko
pgpGFUuaZFFam.pgp
Description: PGP signature
------------------------------------------------------------------------------ Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS, MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft MVPs and experts. ON SALE this month only -- learn more at: http://p.sf.net/sfu/learnnow-d2d
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
