Stream: Coq users

Topic: installing 32-bit ocaml fails


view this post on Zulip Notification Bot (Jul 21 2023 at 15:58):

A message was moved here from #jsCoq > jsCoq compilation by Paolo Giarrusso.

view this post on Zulip Paolo Giarrusso (Jul 21 2023 at 15:59):

Oh, that's a new problem — even _ocaml_ is failing to install

view this post on Zulip Paolo Giarrusso (Jul 21 2023 at 16:02):

I created a separate thread, but https://discuss.ocaml.org probably has more people qualified to help with this..

@Karl Palmskog can you move this to Coq users? I don't know if we can help, but if somebody can, it's less likely to be seen here.

view this post on Zulip Notification Bot (Jul 21 2023 at 16:08):

This topic was moved here from #jsCoq > installing 32-bit ocaml fails by Karl Palmskog.

view this post on Zulip Karl Palmskog (Jul 21 2023 at 16:15):

OK, moved this here from #jsCoq, I guess the big question is: should 32-bit OCaml even work these days? The Fatal error: exception Cmi_format.Error(_) looks worrying and fundamental.

view this post on Zulip Paolo Giarrusso (Jul 21 2023 at 16:21):

I agree; @Wiame Karmouni 's supervisor Mr. Bodin did manage, but they haven't explained why they're all using 32bit ocaml.

view this post on Zulip Paolo Giarrusso (Jul 21 2023 at 16:22):

cc @Martin Constantino–Bodin

view this post on Zulip Karl Palmskog (Jul 21 2023 at 16:25):

from what I remember it's a jsCoq requirement somewhere, but other people have used it since proof checking time is lower on 32-bit

view this post on Zulip Shachar Itzhaky (Jul 21 2023 at 16:52):

OCaml 4.12 did install in our CI (in Docker). I will have to check again. The Fatal error is a bit cryptic.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 21 2023 at 18:21):

Hi @Wiame Karmouni , that's indeed a very strange error, can you provide more details on your OS / hardware?

view this post on Zulip Martin Constantino–Bodin (Jul 24 2023 at 09:35):

Paolo Giarrusso said:

they haven't explained why they're all using 32bit ocaml.

We followed the advises on the build :smiling_face: We also got errors in the 64bits versions, so we thought that keeping to the one marked as non-experimental would be safer :smiling_face:

view this post on Zulip Martin Constantino–Bodin (Jul 24 2023 at 09:36):

By the way, I finally succeeded to compile everything, but it was in a fresh install (in a virtual machine) of the latest's Ubuntu.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2023 at 09:43):

Hi @Martin Constantino–Bodin , I'm glad everything worked fine in the end. Let us know if we should update the documentation in any way.

view this post on Zulip Martin Constantino–Bodin (Jul 24 2023 at 10:06):

Here is what I did on the virtual machine:

$ sudo apt install git make perl m4 npm curl mercurial darcs g++-multilib gcc-multilib libgmp-dev
$ sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) # Maybe with sudo? I'm no longer sure about this one.
$ opam init
$ # <git cloning and cd>
$ ./etc/toolchain-setup.sh --64
$ make coq
$ make jscoq

For most apt packages it was very clear which should be installed, apart from libgmp-dev: I think that it would be worthwhile adding a note about it in the documentation (especially if one should install a 32 bits version). I didn't find a 32 bits version of this package for this version of Ubuntu, so I switch to 64 bits despite the warning in the documentation.

view this post on Zulip grianneau (Jul 24 2023 at 13:00):

I had the same issue to find libgmp3-dev:i386, on Ubuntu one can add repositories for i386 packages:

dpkg --add-architecture i386

Last updated: Oct 13 2024 at 01:02 UTC