Jason Gross (Apr 30 2021 at 21:03): 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
Emilio Jesús Gallego Arias (Apr 30 2021 at 21:19):Umm, seems strange
Emilio Jesús Gallego Arias (Apr 30 2021 at 21:19):You can do fine strace debug using
Emilio Jesús Gallego Arias (Apr 30 2021 at 21:19):dune build -p coq-core && strace dune install coq-core
Emilio Jesús Gallego Arias (Apr 30 2021 at 21:19):from a pristine tree
Emilio Jesús Gallego Arias (Apr 30 2021 at 21:20):sorry, dune build coq-core.install if you want to experiment
Emilio Jesús Gallego Arias (Apr 30 2021 at 21:20):the install file is a standard "opam install file"
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...
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
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
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
Emilio Jesús Gallego Arias (May 01 2021 at 18:01):to solve your issue for now, do
Emilio Jesús Gallego Arias (May 01 2021 at 18:02): make world && dune build coq-core.install && sudo make install
Emilio Jesús Gallego Arias (May 01 2021 at 18:02):until we ensure world does build coq-core.install too
Jason Gross (May 01 2021 at 18:03):Ah, great, thanks!
Emilio Jesús Gallego Arias (May 01 2021 at 18:03):this is by the way pretty hard to tet
Emilio Jesús Gallego Arias (May 01 2021 at 18:03):to test
Emilio Jesús Gallego Arias (May 01 2021 at 18:04):in the dune system, it holds by construction
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
Emilio Jesús Gallego Arias (May 01 2021 at 18:04):let me know if that change fixes your problem
Emilio Jesús Gallego Arias (May 01 2021 at 18:04):so I push it to master
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.
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
Sorry @Jason Gross , the workaround I submitted here is incomplete
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
Emilio Jesús Gallego Arias (May 03 2021 at 00:35):so that is
Emilio Jesús Gallego Arias (May 03 2021 at 00:35):from https://github.com/coq/coq/pull/14233
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
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
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
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
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
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
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!
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.
Jason Gross (May 03 2021 at 12:18):Hm, but opam install coq.8.13.1 does not install coqchk
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
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 13 2024 at 01:02 UTC