unix.cmxa file and theards package nonexistant

[Stiephen]

Hello,
I'm trying to install UniMath and I'm facing to the following issues with Ocaml files and Opam packages:

Error: Cannot find file /usr/local/lib/ocaml/unix.cmxa
COQMKTOP -o bin/coqtop.opt
ocamlfind: Package 'threads.posix' not found - required by 'threads'
make[2]: *** [bin/coqtop.opt] Error 2
make[2]: Leaving directory '/Users/stiph/UniMath/sub/coq'
make[1]: *** [submake] Error 2
make[1]: Leaving directory '/Users/stiph/UniMath/sub/coq'
make: *** [sub/coq/bin/coq_makefile] Error 2

I'm not very use to this kind of installation but, from my rechearch, there doesn't exist a threads.posix package and I don't know how to create the unix.cmxa file. Do you have any advise?

I'm on macOS Mojave 10.14.6 and have installed OCaml 4.07.1+flambda via Opam.

[dra27]

What's the output of which ocamlc and ocamlc -vnum?

[Stiephen]

Here is what I get:

MacBook-Air-de-Stiephen:~ stiph$ which ocamlc
/Users/stiph/.opam/with-coq/bin/ocamlc
MacBook-Air-de-Stiephen:~ stiph$ ocamlc -vnum
4.07.1

[rjbou]

You have an compiler installed via an opam switch with-coq that try to use your system libraries. Can you share output of opam env, env | grep CAML_LD_LIBRARY_PATH, and opam list base-* --installed?

[Stiephen]

Yes, from opam env I get:

MacBook-Air-de-Stiephen:~ stiph$ opam env
OPAM_SWITCH_PREFIX='/Users/stiph/.opam/with-coq'; export OPAM_SWITCH_PREFIX;
CAML_LD_LIBRARY_PATH='/Users/stiph/.opam/with-coq/lib/stublibs:Updated by package ocaml'; export CAML_LD_LIBRARY_PATH;
OCAML_TOPLEVEL_PATH='/Users/stiph/.opam/with-coq/lib/toplevel'; export OCAML_TOPLEVEL_PATH;
PATH='/Users/stiph/.opam/with-coq/bin:/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin:/Library/TeX/texbin'; export PATH;

Then from env | grep CAML_LD_LIBRARY_PATH:

MacBook-Air-de-Stiephen:~ stiph$ env | grep CAML_LD_LIBRARY_PATH
CAML_LD_LIBRARY_PATH=/Users/stiph/.opam/with-coq/lib/stublibs:Updated by package ocaml

And from opam list base-* --installed:

MacBook-Air-de-Stiephen:~ stiph$ opam list base-* --installed
# Packages matching: installed & name-match(base-*)
# Name        # Installed # Synopsis
base-bigarray base
base-threads  base
base-unix     base

[rjbou]

The env is not well updated, maybe related to #4841. How did you install the switch & the failing package?

[Stiephen]

I followed the installation INSTALL_OPAM.md for macOS and did the part "with OCaml 4.07.1+flambda". Everything went fine, except for installing camlp5 I get the following error:

The following actions will be performed:
  ∗ install conf-perl-string-shellquote 1       [required by camlp5]
  ∗ install conf-perl-ipc-system-simple 1       [required by camlp5]
  ∗ install camlp5                      8.00.02
===== ∗ 3 =====

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫 
⬇ retrieved camlp5.8.00.02  (cached)
[ERROR] The compilation of conf-perl-ipc-system-simple.1 failed at "perl -MIPC::System::Simple -e 1".
[ERROR] The compilation of conf-perl-string-shellquote.1 failed at "perl -MString::ShellQuote -e 1".

#=== ERROR while compiling conf-perl-string-shellquote.1 ======================#
# context     2.1.0 | macos/x86_64 | ocaml-variants.4.07.1+flambda | git+https://github.com/ocaml/opam-repository.git
# path        ~/.opam/with-coq/.opam-switch/build/conf-perl-string-shellquote.1
# command     ~/.opam/opam-init/hooks/sandbox.sh build perl -MString::ShellQuote -e 1
# exit-code   2
# env-file    ~/.opam/log/conf-perl-string-shellquote-10637-5a9e53.env
# output-file ~/.opam/log/conf-perl-string-shellquote-10637-5a9e53.out
### output ###
# Can't locate String/ShellQuote.pm in @INC (you may need to install the String::ShellQuote module) (@INC contains: /Library/Perl/5.18/darwin-thread-multi-2level /Library/Perl/5.18 /Network/Library/Perl/5.18/darwin-thread-multi-2level /Network/Library/Perl/5.18 /Library/Perl/Updates/5.18.4 /System/Library/Perl/5.18/darwin-thread-multi-2level /System/Library/Perl/5.18 /System/Library/Perl/Extras[...]
# BEGIN failed--compilation aborted.


#=== ERROR while compiling conf-perl-ipc-system-simple.1 ======================#
# context     2.1.0 | macos/x86_64 | ocaml-variants.4.07.1+flambda | git+https://github.com/ocaml/opam-repository.git
# path        ~/.opam/with-coq/.opam-switch/build/conf-perl-ipc-system-simple.1
# command     ~/.opam/opam-init/hooks/sandbox.sh build perl -MIPC::System::Simple -e 1
# exit-code   2
# env-file    ~/.opam/log/conf-perl-ipc-system-simple-10637-0ee1a4.env
# output-file ~/.opam/log/conf-perl-ipc-system-simple-10637-0ee1a4.out
### output ###
# Can't locate IPC/System/Simple.pm in @INC (you may need to install the IPC::System::Simple module) (@INC contains: /Library/Perl/5.18/darwin-thread-multi-2level /Library/Perl/5.18 /Network/Library/Perl/5.18/darwin-thread-multi-2level /Network/Library/Perl/5.18 /Library/Perl/Updates/5.18.4 /System/Library/Perl/5.18/darwin-thread-multi-2level /System/Library/Perl/5.18 /System/Library/Perl/Extra[...]
# BEGIN failed--compilation aborted.

And for the env, could it be because the compiler asked me to run the command eval $(opam env --switch=with-coq) to update the current shell environment?

[rjbou]

camlp5 error is not the same than library unix/thread error. Do you still have the first one ?

And for the env, could it be because the compiler asked me to run the command eval $(opam env --switch=with-coq) to update the current shell environment?

If opam ask you that, is to synchronise your terminal with opam environment. Since opam 2.0, opam installs a shell hook that automatically synchronise your terminal, you should had some related question about this step when you did opam init. You can launch opam init --reinit to reconfigure.

On camlp5 error, it is because of external dependencies: camlp5 depends on some perl external (system) dependencies. I see that you use opam 2.1.0, it handle automatically external dependencies, but there is no defined dependencies for MacOS for conf-perl* packages. @kit-ty-kate @mseri do you know who to ping for that?
In the meanwhile, you need to install IPC::System::Simple and String::ShellQuote perl modules in your system.

[Stiephen]

Yes, I still have the same error.

I have successfully installed IPC::System::Simple and String::ShellQuote using this stack overflow post and ActivatePerl. After that I was able to install correctly campl5, so the campl5 error is gone but the original error still there.

[Stiephen]

In the end, I removed UniMath and reinstalled it and it worked perfectly. Thanks you very much for your help.