search

jrh13 / hol-light

The HOL Light theorem prover
Other
435 stars 79 forks source link

make error #64

Open wdmjun opened 3 years ago

wdmjun commented 3 years ago

File "pa_j.ml", line 413, characters 6-24: 413 | | MtFun loc x1 x2 x3 → ^^^^^^^^^^^^^^^^^^ Error: The constructor MtFun expects 3 argument(s), but is applied here to 4 argument(s) make: *** [Makefile:49: pa_j.cmo] Error 2

I received this error when running make in ~/hol-light.

wdmjun commented 3 years ago

This was on Debian Sid.

wdmjun commented 3 years ago

I compiled camlp5 from source. I now get the same error as #62.

maggesi commented 3 years ago

You need to pick up a good combination of ocaml and camlp5 versions. The one that I'm using right now is the following: ocaml 4.05 camlp5 7.10 there many other possibile combinations.

With opam, you can use the following instructions:

opam switch create 4.05.0
eval `opam env`
opam pin add camlp5 7.10
opam install num camlp5
wdmjun commented 3 years ago

Worked for me. Much thanks.

asr commented 2 years ago

You need to pick up a good combination of ocaml and camlp5 versions. The one that I'm using right now is the following: ocaml 4.05 camlp5 7.10 there many other possibile combinations.

With opam, you can use the following instructions:

opam switch create 4.05.0
eval `opam env`
opam pin add camlp5 7.10
opam install num camlp5

I had the same problem on Ubuntu 20.04, ocaml 4.08.1 and camlp5 7.11. The above instructions also worked for me. @wdmjun, thanks!