A message was moved here from #jsCoq > jsCoq compilation by Paolo Giarrusso.
Oh, that's a new problem — even _ocaml_ is failing to install
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.
This topic was moved here from #jsCoq > installing 32-bit ocaml fails by Karl Palmskog.
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.
I agree; @Wiame Karmouni 's supervisor Mr. Bodin did manage, but they haven't explained why they're all using 32bit ocaml.
cc @Martin Constantino–Bodin
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
OCaml 4.12 did install in our CI (in Docker). I will have to check again. The Fatal error
is a bit cryptic.
Hi @Wiame Karmouni , that's indeed a very strange error, can you provide more details on your OS / hardware?
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:
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.
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.
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.
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