Stream: Coq devs & plugin devs

Topic: make install on Mac


view this post on Zulip Jason Gross (Apr 30 2021 at 21:03):

Is make install on MacOS to /usr/local supposed to require sudo? It didn't used to, but since the Dune PR, it errors with

Installing /usr/local/doc/coq-core/LICENSE
Error: mkdir: /usr/local/doc: Permission denied

without sudo

view this post on Zulip Emilio Jesús Gallego Arias (Apr 30 2021 at 21:19):

Umm, seems strange

view this post on Zulip Emilio Jesús Gallego Arias (Apr 30 2021 at 21:19):

You can do fine strace debug using

view this post on Zulip Emilio Jesús Gallego Arias (Apr 30 2021 at 21:19):

dune build -p coq-core && strace dune install coq-core

view this post on Zulip Emilio Jesús Gallego Arias (Apr 30 2021 at 21:19):

from a pristine tree

view this post on Zulip Emilio Jesús Gallego Arias (Apr 30 2021 at 21:20):

sorry, dune build coq-core.install if you want to experiment

view this post on Zulip Emilio Jesús Gallego Arias (Apr 30 2021 at 21:20):

the install file is a standard "opam install file"

view this post on Zulip Emilio Jesús Gallego Arias (Apr 30 2021 at 21:20):

dune install is just a small command for example to help windows users process this files, etc...

view this post on Zulip Jason Gross (May 01 2021 at 17:58):

@Emilio Jesús Gallego Arias could you help debug this at https://github.com/coq/coq/pull/14231 (https://github.com/coq/coq/pull/14231/checks#step:6:3061)? Btw, make install is also broken with sudo, which I think is at the root of https://github.com/coq/coq/issues/14228

view this post on Zulip Emilio Jesús Gallego Arias (May 01 2021 at 18:00):

the problem you are seeing is indeed due to us not testing sudo make install

view this post on Zulip Emilio Jesús Gallego Arias (May 01 2021 at 18:01):

that is the problem, I didn't notice in your first bug report; I'll ensure that the make-based vo build system does respect the build / install boundary, that's trivial to do , but I just inherited the old targets for world

view this post on Zulip Emilio Jesús Gallego Arias (May 01 2021 at 18:01):

to solve your issue for now, do

view this post on Zulip Emilio Jesús Gallego Arias (May 01 2021 at 18:02):

make world && dune build coq-core.install && sudo make install

view this post on Zulip Emilio Jesús Gallego Arias (May 01 2021 at 18:02):

until we ensure world does build coq-core.install too

view this post on Zulip Jason Gross (May 01 2021 at 18:03):

Ah, great, thanks!

view this post on Zulip Emilio Jesús Gallego Arias (May 01 2021 at 18:03):

this is by the way pretty hard to tet

view this post on Zulip Emilio Jesús Gallego Arias (May 01 2021 at 18:03):

to test

view this post on Zulip Emilio Jesús Gallego Arias (May 01 2021 at 18:04):

in the dune system, it holds by construction

view this post on Zulip Emilio Jesús Gallego Arias (May 01 2021 at 18:04):

so that's good, but in general testing commands with sudo vs without sudo is hard

view this post on Zulip Emilio Jesús Gallego Arias (May 01 2021 at 18:04):

let me know if that change fixes your problem

view this post on Zulip Emilio Jesús Gallego Arias (May 01 2021 at 18:04):

so I push it to master

view this post on Zulip Jason Gross (May 01 2021 at 18:20):

Test running at https://github.com/coq/coq/pull/14231/checks?check_run_id=2483373930 and https://github.com/mit-plv/fiat-crypto/runs/2483370989?check_suite_focus=true, but there's a bit of a backlog on fiat-crypto. I'm about to head out, but I am optimistic that it will work.

view this post on Zulip Jason Gross (May 03 2021 at 00:21):

Running dune build coq-core.install seems to make things worse, as now sudo make install fails with

DUNE      sources
COQDEP    VFILES
DUNE      sources
DUNE      _build/default/coqide-server.install
    ocamlopt ide/coqide/idetop.exe
ld: warning: directory not found for option '-L/opt/local/lib'
File "_none_", line 1:
Error: Error on dynamically loaded library: dllzarith.so: dlopen(dllzarith.so, 10): image not found
make[1]: *** [_build/default/coqide-server.install] Error 1

view this post on Zulip Emilio Jesús Gallego Arias (May 03 2021 at 00:35):

Sorry @Jason Gross , the workaround I submitted here is incomplete

view this post on Zulip Emilio Jesús Gallego Arias (May 03 2021 at 00:35):

see the PR for the right one, but the set of *.install files has to match what dune install does

view this post on Zulip Emilio Jesús Gallego Arias (May 03 2021 at 00:35):

so that is

view this post on Zulip Emilio Jesús Gallego Arias (May 03 2021 at 00:35):

from https://github.com/coq/coq/pull/14233

view this post on Zulip Emilio Jesús Gallego Arias (May 03 2021 at 00:36):

coq-core.install coqide-server.install and coqide.install if building with -ide yes

view this post on Zulip Emilio Jesús Gallego Arias (May 03 2021 at 00:36):

see the comments in the PR / commit , but indeed this bug arose due to the rewrite

view this post on Zulip Emilio Jesús Gallego Arias (May 03 2021 at 00:37):

and the quite different model between the organization of old targets and the organization of new ones

view this post on Zulip Emilio Jesús Gallego Arias (May 03 2021 at 00:37):

actually, it could be a good idea to forbid make install to do any build

view this post on Zulip Emilio Jesús Gallego Arias (May 03 2021 at 00:37):

a simple check to see if the corresponding .install files are in place would help to provide a nice error message

view this post on Zulip Emilio Jesús Gallego Arias (May 03 2021 at 00:38):

I started this code under the old dune mode where dune install would build things, but that was abandoned upstream

view this post on Zulip Jason Gross (May 03 2021 at 00:53):

I've decided to switch to using https://github.com/avsm/setup-ocaml + installing Coq via opam, and I'm hopeful this will be more robust. Thanks for the pointers though!

view this post on Zulip Enrico Tassi (May 03 2021 at 07:18):

I'm using that too in elpi's CI and I'm happy with it. It is very close to the platform scripts btw.

view this post on Zulip Jason Gross (May 03 2021 at 12:18):

Hm, but opam install coq.8.13.1 does not install coqchk

view this post on Zulip Jason Gross (May 03 2021 at 12:19):

Oh, wait, no, I just forgot to eval $(opam env). It's annoying that I have to run that in every step

view this post on Zulip Ali Caglayan (May 03 2021 at 12:32):

I'm also annoyed by having to eval everytime, but there are some workarounds here: https://github.com/ocaml/opam/issues/57


Last updated: Oct 16 2021 at 01:03 UTC