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
Umm, seems strange
You can do fine strace debug using
dune build -p coq-core && strace dune install coq-core
from a pristine tree
sorry, dune build coq-core.install
if you want to experiment
the install file is a standard "opam install file"
dune install is just a small command for example to help windows users process this files, etc...
@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
the problem you are seeing is indeed due to us not testing sudo make install
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
to solve your issue for now, do
make world && dune build coq-core.install && sudo make install
until we ensure world
does build coq-core.install too
Ah, great, thanks!
this is by the way pretty hard to tet
to test
in the dune system, it holds by construction
so that's good, but in general testing commands with sudo vs without sudo is hard
let me know if that change fixes your problem
so I push it to master
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.
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
Sorry @Jason Gross , the workaround I submitted here is incomplete
see the PR for the right one, but the set of *.install files has to match what dune install does
so that is
from https://github.com/coq/coq/pull/14233
coq-core.install coqide-server.install and coqide.install if building with -ide yes
see the comments in the PR / commit , but indeed this bug arose due to the rewrite
and the quite different model between the organization of old targets and the organization of new ones
actually, it could be a good idea to forbid make install
to do any build
a simple check to see if the corresponding .install
files are in place would help to provide a nice error message
I started this code under the old dune mode where dune install
would build things, but that was abandoned upstream
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!
I'm using that too in elpi's CI and I'm happy with it. It is very close to the platform scripts btw.
Hm, but opam install coq.8.13.1
does not install coqchk
Oh, wait, no, I just forgot to eval $(opam env)
. It's annoying that I have to run that in every step
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 13 2024 at 01:02 UTC