I have this problem again. Can anyone help?
% camlp5 -v
Camlp5 version 6.14 (ocaml 4.02.3)
hol-light % make
\
if test `ocamlc -version | cut -c1-3` = "3.0" ; \
then cp pa_j_`ocamlc -version | cut -c1-4`.ml pa_j.ml ; \
else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' |
cut -c1-6` = "6.02.1" ; \
then cp pa_j_3.1x_6.02.1.ml pa_j.ml; \
else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.'
| cut -c1-6` = "6.02.2" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.02.3" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut
-f1-3 -d'.' | cut -c1-6` = "6.03" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut
-f1-3 -d'.' | cut -c1-6` = "6.04" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut
-f1-3 -d'.' | cut -c1-6` = "6.05" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut
-f1-3 -d'.' | cut -c1-6` = "6.06" ; \
then cp pa_j_3.1x_6.02.2.ml pa_j.ml; \
else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.06" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.07" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.08" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.09" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.10" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.11" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
-d'.' | cut -c1-6` = "6.12" ; \
then cp pa_j_3.1x_6.11.ml pa_j.ml; \
else cp pa_j_3.1x_`camlp5 -v 2>&1 | cut -f3 -d' ' |
cut -c1`.xx.ml pa_j.ml; \
fi \
fi \
fi \
fi
if test `ocamlc -version | cut -c1-3` = "3.0" ; \
then ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo"
-I `camlp4 -where` pa_j.ml; \
else ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo
q_MLast.cmo" -I `camlp5 -where` pa_j.ml; \
fi
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])
File "pa_j.ml", line 1:
Error: Error while running external preprocessor
Command line: camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo 'pa_j.ml' >
/tmp/ocamlpp428d9c
Makefile:40: recipe for target 'pa_j.cmo' failed
make: *** [pa_j.cmo] Error 2
On 19 September 2014 at 09:38, Nela Cicmil <nela.cic...@dpag.ox.ac.uk>
wrote:
> Thanks again for everyone's replies.
>
> @Marco: After typing hol_light and waiting a few minutes for the warnings
> stop, HOL Light seems to be running fine by this Nix installation. Thank
> you!
>
> @Mark: I'm not sure why this combination isn't working for my Mac when
> Ocaml, camlp5 and HOL Light are installed individually. I removed and
> re-downloaded HOL Light via svn, checked the ocaml & camlp5 versions again
> in the hol_light directory, used make clean followed by make, and the same
> error appeared (copied in below).
>
> @Ramana: Thank you for pointing out the HOL Light Workbench link -
> actually I had come across it earlier via
> http://www.eng.utah.edu/~cs6110/install-hol-light.html - sorry I didn't
> to mention this in my original email. Unfortunately, this automated
> approach did not work for my Mac. I didn't make a record of the errors but
> as far as I remember the automated script installation of ocaml failed, so
> camlp5 installation failed and HOL Light did not run.
>
> In any case, I shall now press on with HOL Light as installed with Nix -
> thanks again.
>
> All the best,
> Nela
>
> hol_light nc$ ocaml -version
> The OCaml toplevel, version 4.01.0
> hol_light nc$ camlp5 -v
> Camlp5 version 6.11 (ocaml 4.01.0)
> hol_light nc$ make clean
> rm -f pa_j.ml pa_j.cmi pa_j.cmo hol hol.multivariate hol.sosa hol.card
> hol.complex;
> hol_light nc$ make
> \
> if test `ocamlc -version | cut -c1-3` = "3.0" ; \
> then cp pa_j_`ocamlc -version | cut -c1-4`.ml pa_j.ml ; \
> else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' |
> cut -c1-6` = "6.02.1" ; \
> then cp pa_j_3.1x_6.02.1.ml pa_j.ml; \
> else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
> -d'.' | cut -c1-6` = "6.02.2" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut
> -f1-3 -d'.' | cut -c1-6` = "6.02.3" -o `camlp5 -v 2>&1 | cut -f3 -d' ' |
> cut -f1-3 -d'.' | cut -c1-6` = "6.03" -o `camlp5 -v 2>&1 | cut -f3 -d' ' |
> cut -f1-3 -d'.' | cut -c1-6` = "6.04" -o `camlp5 -v 2>&1 | cut -f3 -d' ' |
> cut -f1-3 -d'.' | cut -c1-6` = "6.05" -o `camlp5 -v 2>&1 | cut -f3 -d' ' |
> cut -f1-3 -d'.' | cut -c1-6` = "6.06" ; \
> then cp pa_j_3.1x_6.02.2.ml pa_j.ml; \
> else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
> -d'.' | cut -c1-6` = "6.06" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
> -d'.' | cut -c1-6` = "6.07" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
> -d'.' | cut -c1-6` = "6.08" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
> -d'.' | cut -c1-6` = "6.09" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
> -d'.' | cut -c1-6` = "6.10" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
> -d'.' | cut -c1-6` = "6.11" ; \
> then cp pa_j_3.1x_6.11.ml pa_j.ml; \
> else cp pa_j_3.1x_`camlp5 -v 2>&1 | cut -f3 -d' ' |
> cut -c1`.xx.ml pa_j.ml; \
> fi \
> fi \
> fi \
> fi
> if test `ocamlc -version | cut -c1-3` = "3.0" ; \
> then ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo"
> -I `camlp4 -where` pa_j.ml; \
> else ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo
> q_MLast.cmo" -I `camlp5 -where` pa_j.ml; \
> fi
> File "pa_j.ml", line 112, characters 72-74:
> Error: This expression has type (string * MLast.ctyp) list
> but an expression was expected of type
> ('a * MLast.ctyp) list Ploc.vala
> make: *** [pa_j.cmo] Error 2
> hol_light nc$
>
>
>
> ----
> Nela Cicmil, D.Phil
> Dept. Physiology, Anatomy & Genetics,
> University of Oxford
> ________________________________________
> From: "Mark Adams" [m...@proof-technologies.com]
> Sent: 17 September 2014 17:05
> To: Nela Cicmil; magg...@math.unifi.it
> Cc: hol-info@lists.sourceforge.net
> Subject: Re: [Hol-info] advice on installing Ocaml, camlp5 & HOL Light on
> Mac OS X 10.8.5?
>
> Nela,
>
> These versions should definitely work together.
>
> Just realised - what you presumably did is first try the HOL Light 'make'
> using other versions of OCaml or Camlp5. So what you needed to do was
> first
> do
> make clean
> before doing
> make
>
> I would be very surprised if this doesn't work.
>
> Mark.
>
> on 17/9/14 1:14 PM, Nela Cicmil <nela.cic...@dpag.ox.ac.uk> wrote:
>
> > @ Mark: I used the svn download command only this week so probably it
> has
> > the most recent version of HOL Light. On svn download, I get the output
> > "Checked out revision 198", and the CHANGES document inside the hol_light
> > directory is dated 9th Sept 2014. Here are my ocaml and camlp5 versions:
> >
> > hol_light nc$ ocaml -version
> > The OCaml toplevel, version 4.01.0
> > hol_light nc$ camlp5 -v
> > Camlp5 version 6.11 (ocaml 4.01.0)
> >
> > @ Ramana: I'm looking into the pa_j*.ml files, but it's not clear to me
> how
> > to write one to work with the ocaml version 4.01.0/camlp5 v 6.11 combo.
> >
> > Thanks!
> >
> > Best wishes,
> > Nela
> >
> > ----
> > Nela Cicmil, D.Phil
> > Dept. Physiology, Anatomy & Genetics,
> > University of Oxford
> > ________________________________________
> > From: marco.magg...@gmail.com [marco.magg...@gmail.com] on behalf of
> Marco
> > Maggesi [magg...@math.unifi.it]
> > Sent: 17 September 2014 08:15
> > To: Mark Adams
> > Cc: Nela Cicmil; hol-info@lists.sourceforge.net
> > Subject: Re: [Hol-info] advice on installing Ocaml, camlp5 & HOL Light on
> > Mac OS X 10.8.5?
> >
> > Hi Nela,
> >
> > I use the Nix package manager (http://nixos.org/nix/) and it works well
> for
> > me. I use Nix both on Max and on Linux. It is nice because it makes the
> > installation of HOL Light completely independent from the versions of
> ocaml,
> > camlp5 (or any other software indeed) installed in your machine.
> >
> > If you want to try, here is what you have to do:
> >
> > 1. Install Nix. Follow the instructions from the nix manual
> > (http://nixos.org/nix/manual). Basically you have to type the following
> > four commands in a terminal:
> >
> >
> > $ bash <(curl https://nixos.org/nix/install)
> > source /usr/local/etc/profile.d/nix.sh
> >
> >
> > nix-channel --add http://nixos.org/channels/nixpkgs-unstable
> > nix-channel --update
> >
> > 2
> > .
> > Then you can install HOL Light with a single command (no need to install
> > OCaml or Camlp5)
> >
> >
> > nix-env -i hol_light
> >
> > For more serious work you probably need to use checkpointing which is
> > available only on Linux. For this I use a NixOS (http://nixos.org)
> > VirtualBox appliance. Do not esitate to ask for more details if you are
> > interested.
> >
> > Best,
> > Marco
> >
> > 2014-09-17 5:50 GMT+02:00 "Mark Adams"
> > <m...@proof-technologies.com<mailto:m...@proof-technologies.com>>:
> > Hi Nela,
> >
> > There have been various problems over the years, but I get no problems
> with
> > recent versions of HOL Light (downloaded since May 2014, including SVN
> > version 197 downloaded in mid-August) with OCaml 4.01.0 and Camlp5 6.11
> > running on Fedora 17.
> >
> > Do you know the HOL Light SVN version (or otherwise, what date did you
> > download)?
> >
> > And can you please check your OCaml and Camlp5 versions by executing the
> > following from the same terminal window from which you are trying the HOL
> > Light make?:
> > ocaml -version
> > camlp5 -v
> >
> > Mark.
> >
> > on 16/9/14 4:45 PM, Nela Cicmil
> > <nela.cic...@dpag.ox.ac.uk<mailto:nela.cic...@dpag.ox.ac.uk>> wrote:
> >
> >> Dear HOL Light users,
> >>
> >> Would anyone be able to please advise me on how to install HOL Light on
> my
> >> Mac? It's a MacBook Pro OS X 10.8.5 Intel core i5.
> >>
> >> My trouble is that I can't seem to get compatible versions of Ocaml,
> > camlp5
> >> and HOL Light installed on my system, mainly because the Ocaml version
> > that
> >> comes with OPAM, v 4.01.0, seems to be too recent to run with the
> slighter
> >> older camlp5 versions compatible with HOL Light.
> >>
> >> Has anyone recently installed HOL Light on a Mac, and has advice on
> which
> >> versions of Ocaml and camlp5 to install, and which procedure to use to
> >> install them? In particular, is it possible to install an older version
> of
> >> Ocaml, e.g. v 3.12, using OPAM?
> >>
> >> The specific issues I've encountered are detailed below. Any advice
> would
> > be
> >> much appreciated.
> >>
> >> Thank you,
> >>
> >> Best wishes,
> >> Nela
> >> ----
> >> Nela Cicmil, D.Phil
> >> Dept. Physiology, Anatomy & Genetics,
> >> University of Oxford
> >> ----
> >>
> >> After various attempts to install Ocaml on the Mac, I installed (using
> >> homebrew) the latest version of OPAM, which comes with Ocaml version
> > 4.01.0.
> >> On basic testing at the terminal, Ocaml seemed to be working fine. I
> then
> >> installed camlp5 version 6.11, using ./configure --transitional mode,
> and
> >> that seemed to be running fine as well. When I then attempted to install
> > HOL
> >> Light, using the svn checkout
> http://hol-light.googlecode.com/svn/trunk/
> >> hol_light procedure, and got the following error on "make":
> >>
> >> File "pa_j.ml<http://pa_j.ml>", line 112, characters 72-74:
> >> Error: This expression has type (string * MLast.ctyp) list
> >> but an expression was expected of type
> >> ('a * MLast.ctyp) list Ploc.vala
> >> make: *** [pa_j.cmo] Error 2
> >>
> >> - On reading various previous posts, it seemed that the latest versions
> of
> >> camlp5 could be at fault. I attempted to install older versions of
> camlp5,
> >> version 6.02.0 and 5.15, but I got the following error on ./configure
> >> --transitional:
> >>
> >> Sorry: the compatibility with ocaml version "4.01.0"
> >> is not yet implemented. Please report.
> >> Information: directory ocaml_stuff/4.01.0 is missing.
> >> Configuration failed.
> >>
> >> - With campl5 version 6.06 it's the following error (I'm not sure what
> the
> >> preprocessor is here):
> >>
> >>>> Fatal error: OCaml and preprocessor have incompatible versions
> >> Fatal error: exception Misc.Fatal_error
> >> make[2]: *** [versdep.cmo] Error 2
> >> make[1]: *** [core] Error 2
> >> make: *** [world.opt] Error 2
> >>
> >> - So then I attempted to install an earlier version of Ocaml, version
> >> 3.12.1, in the hope that it would be compatible with the earlier
> versions
> > of
> >> camlp5. This did not seem possible with OPAM so I downloaded the
> original
> >> source distribution tar.gz from http://ocaml.org/releases/3.12.1.html.
> I
> >> believe my system has the necessary dependencies in the form of Xcode
> > 5.11,
> >> gcc and gnumake running. However, the "make world" installation command
> >> exits on the following error:
> >>
> >> make coldstart
> >> cd byterun; make all
> >> gcc -DCAML_NAME_SPACE -O -fno-defer-pop -no-cpp-precomp -Wall
> >> -D_FILE_OFFSET_BITS=64 -D_REENTRANT -c -o interp.o interp.c
> >> clang: error: unknown argument: '-fno-defer-pop'
> >> [-Wunused-command-line-argument-hard-error-in-future]
> >> clang: note: this will be a hard error (cannot be downgraded to a
> warning)
> >> in the future
> >> make[2]: *** [interp.o] Error 1
> >> make[1]: *** [coldstart] Error 2
> >> make: *** [world] Error 2
> >>
> >>
> >>
> >
>
> ----------------------------------------------------------------------------
> >> --
> >> Want excitement?
> >> Manually upgrade your production database.
> >> When you want reliability, choose Perforce.
> >> Perforce version control. Predictably reliable.
> >>
> >
>
> http://pubads.g.doubleclick.net/gampad/clk?id=157508191&iu=/4140/ostg.clktrk
> >> _______________________________________________
> >> hol-info mailing list
> >> hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
> >> https://lists.sourceforge.net/lists/listinfo/hol-info
> >>
> >>
> >>
> >
> >
> >
>
> ----------------------------------------------------------------------------
> > --
> > Want excitement?
> > Manually upgrade your production database.
> > When you want reliability, choose Perforce
> > Perforce version control. Predictably reliable.
> >
>
> http://pubads.g.doubleclick.net/gampad/clk?id=157508191&iu=/4140/ostg.clktrk
> > _______________________________________________
> > hol-info mailing list
> > hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
> >
>
> ------------------------------------------------------------------------------
> Slashdot TV. Video for Nerds. Stuff that Matters.
>
> http://pubads.g.doubleclick.net/gampad/clk?id=160591471&iu=/4140/ostg.clktrk
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
