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

from hol-light.

from hol-light.

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

from hol-light.

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

from hol-light.

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

from hol-light.

Yeah! It works. Thank you very much.

from hol-light.