HOL light installation problem on macos

[dcr2828]

I am trying to install Hol light on macos. I downloaded the hol-light package and typed ¨make¨ but I got the following error:

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' > /var/folders/sy/0_3rx36s29d7zb8504hj9fkm0000gn/T/ocamlpp5d527d

make: *** [pa_j.cmo] Error 2

I use camlp5 version 7.10 and ocaml version 4.05

I would be glad of any advice.

[binghe]

Hi, the following combination works for me on Mac OS X 10.15:

        OCaml version 4.07.1

	Camlp5 parsing version 7.08

My advice is that you should never directly install OCaml but first install "opam" from MacPorts (not Homebrew) and then use opam to install the above working combinations of OCaml and camlp5. (Maybe the "num" package should be also installed.) The following is a output of my opam list command:

# Packages matching: installed
# Name         # Installed              # Synopsis
base-bigarray  base
base-threads   base
base-unix      base
camlp5         7.08                     pinned to version 7.08
conf-m4        1                        Virtual package relying on m4
num            1.3                      The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml          4.07.1                   The OCaml compiler (virtual package)
ocaml-config   1                        OCaml Switch Configuration
ocaml-variants 4.07.1+force-safe-string Official release 4.07.1, with safe string forced globally
ocamlfind      1.8.1                    A library manager for OCaml

[dcr2828]

Thank you for this. I will switch to the versions of ocaml and camlp5 you mention via opam. I have now also noticed that hol.ml apparently needs the checkpointing programme ckpt. How do I install this on macos? Or is there an alternative? Damian

…

On 14 Oct 2021, at 1:51 pm, Chun Tian ***@***.***> wrote: Hi, the following combination works for me on Mac OS X 10.15: OCaml version 4.07.1 Camlp5 parsing version 7.08 My advice is that you should never directly install OCaml but first install "opam" from MacPorts (not Homebrew) and then use opam to install the above working combinations of OCaml and camlp5. (Maybe the "num" package should be also installed.) The following is a output of my opam list command: # Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base camlp5 7.08 pinned to version 7.08 conf-m4 1 Virtual package relying on m4 num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.07.1 The OCaml compiler (virtual package) ocaml-config 1 OCaml Switch Configuration ocaml-variants 4.07.1+force-safe-string Official release 4.07.1, with safe string forced globally ocamlfind 1.8.1 A library manager for OCaml — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#66 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AWB4DWEEDWAELTE2LRAUOILUG3G67ANCNFSM5F7RZ5XQ>. Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

[dcr2828]

I have now switched to the suggested versions of OCaml and Camlp5 but still no joy. There is also another error (which was already there before):

Error while loading "/opt/local/lib/ocaml/camlp5/pa_lexer.cmo": /opt/local/lib/ocaml/camlp5/pa_lexer.cmo is not a bytecode object file.
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' > /var/folders/sy/0_3rx36s29d7zb8504hj9fkm0000gn/T/ocamlpp7dd892

Note that I run macos 11.6.

Here is what opam list gives for me

Packages matching: installed

Name # Installed # Synopsis

base-bigarray base
base-threads base
base-unix base
camlp5 7.08 pinned to version 7.08
num 1.4 The legacy Num library for arbitrary-precision integer and
ocaml 4.07.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.07.1 Official release 4.07.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.1 A library manager for OCaml

[binghe]

I have now switched to the suggested versions of OCaml and Camlp5 but still no joy. There is also another error (which was already there before):

Error while loading "/opt/local/lib/ocaml/camlp5/pa_lexer.cmo": /opt/local/lib/ocaml/camlp5/pa_lexer.cmo is not a bytecode object file. 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' > /var/folders/sy/0_3rx36s29d7zb8504hj9fkm0000gn/T/ocamlpp7dd892

You should completely uninstall ocaml and camlp5 from MacPorts. (Try port uninstall camlp5 and maybe more.) The folder "/opt/local/lib/ocaml" doesn't exist in Mac my system. If you execute which camlp5, it should return something like this (instead of "/opt/local/..."):

$ which camlp5
/Users/binghe/.opam/hol-light/bin/camlp5

To help camlp5 correctly finding its libraries, I have the following lines in my .bashrc, you can also try:

alias ocaml='ocaml -safe-string -I `camlp5 -where` camlp5o.cma'

if command -v opam 1>/dev/null 2>&1; then
    eval $(opam env)
fi

[binghe]

Thank you for this. I will switch to the versions of ocaml and camlp5 you mention via opam. I have now also noticed that hol.ml apparently needs the checkpointing programme ckpt. How do I install this on macos? Or is there an alternative? Damian
…

The purpose of ckpt (checkpoint) is to save the OCaml running process with all the loaded HOL theories into a file, so that later you can quickly load that file into memory, to save the long time loading everything again, starting from use "hol.ml";;. However, I don't think any such "checkpoint" program is still available today, especially for Mac OS X (the version you are using is even the latest).

If you really want this feature, I would recommend you to try to install a Linux virtual machine (by VMware Fusion, VirtualBox or Parallels Desktop) and run hol-light inside this Linux VM. In this way, you never need to shut down your OCaml process, as you can just suspend the entire Linux VM instead. This VM suspension facility can be seen as a special "checkpoint" for the entire operation system, as it indeed write everything from the memory to a disk file which can be later loaded back.

Hope this helps, (although I know very little about hol-light itself).

Chun

[dcr2828]

Yeah! It works. Thank you very much.