Re: [Hol-info] Trouble building HOL light
Mark, Thanks for the info and the pointers to your excellent HOL Zero documentation. On 15 Oct 2013, at 14:03, Mark Adams wrote: > … > I think the warnings you get may be from superfluous #load directives in > your adapted 'pa_j.ml' file, so comment out the following two lines in the > adapted 'pa_o.ml' file and everything should go smoothly: > #load "pa_extend.cmo";; > #load "q_MLast.cmo";; > Unfortunately, that doesn't make the warnings of away. Regards, Rob. -- October Webinars: Code for Performance Free Intel webinars can help you accelerate application performance. Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from the latest Intel processors and coprocessors. See abstracts and register > http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Trouble building HOL light
Oops. That last email contains an error in the detail. The HOL Light adaption of 'plexer.ml' and 'pa_o.ml' is called 'pa_j.ml'. Mark. on 15/10/13 2:29 PM, Mark Adams wrote: > Hi Rob, > > Yes, you not only need a sufficiently recent version of Camlp5 for your > version of OCaml, you also need to create a sufficiently recent > adapted-for-HOL-Light version of pa_j.ml (adapted from Camlp5 source code > files etc/). You are right that you can work out what adaptions to do by > diffing corresponding older versions of the unadapted and adapted Camlp5 > files. These Camlp5 files are 'lib/lexer.ml' and 'etc/pa_o.ml', but the > adaption for HOL Light is combined into one file called 'pa_o.ml'. Note > that Camlp5 6.07 or later is required for OCaml 4.00, and Camlp5 6.11 or > later is required for OCaml 4.01. > > I think the warnings you get may be from superfluous #load directives in > your adapted 'pa_j.ml' file, so comment out the following two lines in the > adapted 'pa_o.ml' file and everything should go smoothly: > #load "pa_extend.cmo";; > #load "q_MLast.cmo";; > > Note that HOL Zero (also implemented in OCaml) does a similar thing to HOL > Light, in that it uses Camlp5 to adjust the OCaml lexical syntax for HOL > quotations (although in HOL Light there are also changes to the OCaml > syntax). Installation works smoothly for HOL Zero for all versions of > OCaml. Also, the HOL Zero distribution has relatively detailed comments in > Section 2 of INSTALL and Section 2 of 'etc/README', if you want to > understand a little more about what is going on. > > Mark. > > on 14/10/13 2:07 PM, Rob Arthan wrote: > >> >> On 14 Oct 2013, at 12:53, Rob Arthan wrote: >> >>> Can anyone help me with building HOL light? I get the following when I > run >> make: >>> >>> File "pa_j.ml", line 1918, characters 35-43: >>> While expanding quotation "str_item": >>> Parse error: antiquot "_" or antiquot "" or [ident] expected after 'type' >> (in >>> [str_item]) >>> Error while running external preprocessor >>> Command line: camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo 'pa_j.ml' > >> /var/folders/8_/t3z32dh14tzfb_4lvdq8q5frgn/T/ocamlppbd42df >>> >>> I am using ocaml version 4.01.0 and camlp5 version 6.11 and svn rev 174 > of >> the HOL light source. >>> >>> Regards, >>> >>> Rob. >> >> By comparing the camlp5 source with pa_j.ml, I got it and then HOL Light > to >> compile. I can provide a patch if anyone wants it, but it still gives >> warnings, so it really needs attention from someone who understands it. > It >> seems a shame that this involves so much copy/paste/tweak re-use of the >> camlp5 source. >> >> Regards, >> >> Rob. >> >> > >> -- >> October Webinars: Code for Performance >> Free Intel webinars can help you accelerate application performance. >> Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most >> from >> the latest Intel processors and coprocessors. See abstracts and register > >> > http://pubads.g.doubleclick.net/gampad/clk?id=60134071&iu=/4140/ostg.clktrk >> ___ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info >> >> >> > > > > -- > October Webinars: Code for Performance > Free Intel webinars can help you accelerate application performance. > Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most > from > the latest Intel processors and coprocessors. See abstracts and register > > http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- October Webinars: Code for Performance Free Intel webinars can help you accelerate application performance. Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from the latest Intel processors and coprocessors. See abstracts and register > http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Trouble building HOL light
Hi Rob, Yes, you not only need a sufficiently recent version of Camlp5 for your version of OCaml, you also need to create a sufficiently recent adapted-for-HOL-Light version of pa_j.ml (adapted from Camlp5 source code files etc/). You are right that you can work out what adaptions to do by diffing corresponding older versions of the unadapted and adapted Camlp5 files. These Camlp5 files are 'lib/lexer.ml' and 'etc/pa_o.ml', but the adaption for HOL Light is combined into one file called 'pa_o.ml'. Note that Camlp5 6.07 or later is required for OCaml 4.00, and Camlp5 6.11 or later is required for OCaml 4.01. I think the warnings you get may be from superfluous #load directives in your adapted 'pa_j.ml' file, so comment out the following two lines in the adapted 'pa_o.ml' file and everything should go smoothly: #load "pa_extend.cmo";; #load "q_MLast.cmo";; Note that HOL Zero (also implemented in OCaml) does a similar thing to HOL Light, in that it uses Camlp5 to adjust the OCaml lexical syntax for HOL quotations (although in HOL Light there are also changes to the OCaml syntax). Installation works smoothly for HOL Zero for all versions of OCaml. Also, the HOL Zero distribution has relatively detailed comments in Section 2 of INSTALL and Section 2 of 'etc/README', if you want to understand a little more about what is going on. Mark. on 14/10/13 2:07 PM, Rob Arthan wrote: > > On 14 Oct 2013, at 12:53, Rob Arthan wrote: > >> Can anyone help me with building HOL light? I get the following when I run > make: >> >> File "pa_j.ml", line 1918, characters 35-43: >> While expanding quotation "str_item": >> Parse error: antiquot "_" or antiquot "" or [ident] expected after 'type' > (in >> [str_item]) >> Error while running external preprocessor >> Command line: camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo 'pa_j.ml' > > /var/folders/8_/t3z32dh14tzfb_4lvdq8q5frgn/T/ocamlppbd42df >> >> I am using ocaml version 4.01.0 and camlp5 version 6.11 and svn rev 174 of > the HOL light source. >> >> Regards, >> >> Rob. > > By comparing the camlp5 source with pa_j.ml, I got it and then HOL Light to > compile. I can provide a patch if anyone wants it, but it still gives > warnings, so it really needs attention from someone who understands it. It > seems a shame that this involves so much copy/paste/tweak re-use of the > camlp5 source. > > Regards, > > Rob. > > > -- > October Webinars: Code for Performance > Free Intel webinars can help you accelerate application performance. > Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most > from > the latest Intel processors and coprocessors. See abstracts and register > > http://pubads.g.doubleclick.net/gampad/clk?id=60134071&iu=/4140/ostg.clktrk > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- October Webinars: Code for Performance Free Intel webinars can help you accelerate application performance. Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from the latest Intel processors and coprocessors. See abstracts and register > http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Trouble building HOL light
Ramana, On 14 Oct 2013, at 14:41, Ramana Kumar wrote: > From what I remember, camlp5 and ocaml versioning is a nightmare... (though > it may be that HOL Light is a particularly strenuous application for it). > One might find Alex Krauss's approach useful: > http://sourceforge.net/mailarchive/message.php?msg_id=29220282, if going at > the pa_j.ml file doesn't hack it one day. > > I did install ocaml and camlp5 from source as Alex suggests, but it doesn't help in this case. The problem is that pa_j.ml contains modified copies of various bits of the camlp5 source that have changed significantly. The current situation seems to be that if you use the latest ocaml you have to use the latest camlp5. So I think if you want HOL Light to build out of the box you are pretty well forced to use a version of ocaml that is nearly 2 years old. Regards, Rob. -- October Webinars: Code for Performance Free Intel webinars can help you accelerate application performance. Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from the latest Intel processors and coprocessors. See abstracts and register > http://pubads.g.doubleclick.net/gampad/clk?id=60134071&iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Trouble building HOL light
>From what I remember, camlp5 and ocaml versioning is a nightmare... (though it may be that HOL Light is a particularly strenuous application for it). One might find Alex Krauss's approach useful: http://sourceforge.net/mailarchive/message.php?msg_id=29220282, if going at the pa_j.ml file doesn't hack it one day. On Mon, Oct 14, 2013 at 2:07 PM, Rob Arthan wrote: > > On 14 Oct 2013, at 12:53, Rob Arthan wrote: > > > Can anyone help me with building HOL light? I get the following when I > run make: > > > > File "pa_j.ml", line 1918, characters 35-43: > > While expanding quotation "str_item": > > Parse error: antiquot "_" or antiquot "" or [ident] expected after > 'type' (in > > [str_item]) > > Error while running external preprocessor > > Command line: camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo 'pa_j.ml' > > /var/folders/8_/t3z32dh14tzfb_4lvdq8q5frgn/T/ocamlppbd42df > > > > I am using ocaml version 4.01.0 and camlp5 version 6.11 and svn rev 174 > of the HOL light source. > > > > Regards, > > > > Rob. > > By comparing the camlp5 source with pa_j.ml, I got it and then HOL Light > to compile. I can provide a patch if anyone wants it, but it still gives > warnings, so it really needs attention from someone who understands it. It > seems a shame that this involves so much copy/paste/tweak re-use of the > camlp5 source. > > Regards, > > Rob. > > -- > October Webinars: Code for Performance > Free Intel webinars can help you accelerate application performance. > Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most > from > the latest Intel processors and coprocessors. See abstracts and register > > http://pubads.g.doubleclick.net/gampad/clk?id=60134071&iu=/4140/ostg.clktrk > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > -- October Webinars: Code for Performance Free Intel webinars can help you accelerate application performance. Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from the latest Intel processors and coprocessors. See abstracts and register > http://pubads.g.doubleclick.net/gampad/clk?id=60134071&iu=/4140/ostg.clktrk___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Trouble building HOL light
On 14 Oct 2013, at 12:53, Rob Arthan wrote: > Can anyone help me with building HOL light? I get the following when I run > make: > > File "pa_j.ml", line 1918, characters 35-43: > While expanding quotation "str_item": > Parse error: antiquot "_" or antiquot "" or [ident] expected after 'type' (in > [str_item]) > Error while running external preprocessor > Command line: camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo 'pa_j.ml' > > /var/folders/8_/t3z32dh14tzfb_4lvdq8q5frgn/T/ocamlppbd42df > > I am using ocaml version 4.01.0 and camlp5 version 6.11 and svn rev 174 of > the HOL light source. > > Regards, > > Rob. By comparing the camlp5 source with pa_j.ml, I got it and then HOL Light to compile. I can provide a patch if anyone wants it, but it still gives warnings, so it really needs attention from someone who understands it. It seems a shame that this involves so much copy/paste/tweak re-use of the camlp5 source. Regards, Rob. -- October Webinars: Code for Performance Free Intel webinars can help you accelerate application performance. Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from the latest Intel processors and coprocessors. See abstracts and register > http://pubads.g.doubleclick.net/gampad/clk?id=60134071&iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Trouble building HOL light
Can anyone help me with building HOL light? I get the following when I run make: File "pa_j.ml", line 1918, characters 35-43: While expanding quotation "str_item": Parse error: antiquot "_" or antiquot "" or [ident] expected after 'type' (in [str_item]) Error while running external preprocessor Command line: camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo 'pa_j.ml' > /var/folders/8_/t3z32dh14tzfb_4lvdq8q5frgn/T/ocamlppbd42df I am using ocaml version 4.01.0 and camlp5 version 6.11 and svn rev 174 of the HOL light source. Regards, Rob. -- October Webinars: Code for Performance Free Intel webinars can help you accelerate application performance. Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from the latest Intel processors and coprocessors. See abstracts and register > http://pubads.g.doubleclick.net/gampad/clk?id=60134071&iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
