Stream: Coq users

Topic: Local Coq CI


view this post on Zulip Andrej Dudenhefner (Mar 24 2021 at 13:12):

I'm trying to execute Coq's CI locally. The problem is that make ci-quickchick both uses make commands (for which it relies on opam) and make install commands for which it needs superuser rights. Therefore, make ci-quickchick aborts by permission denied and sudo make ci-quickchick gets confused with opam switches (says cannot find ocaml). If I by hand use make and sudo make install for individual dependencies it works out, but is quite tedious essentially to do make ci-quickchick by hand inserting sudo whenever install is used. Is there some easy fix?

view this post on Zulip Gaëtan Gilbert (Mar 24 2021 at 13:18):

it shouldn't need superuser

view this post on Zulip Gaëtan Gilbert (Mar 24 2021 at 13:22):

otoh it's installing quickchick to opam which I don't like
you can try changing make install to make install-plugin in the ci-quickchick.sh, maybe that will help

view this post on Zulip Andrej Dudenhefner (Mar 24 2021 at 13:25):

In a simpler case: make ci-relation_algebra compiles fine, but then complains install: cannot change permissions of ‘/usr/local/lib/coq//user-contrib/RelationAlgebra/’: No such file or directory and Makefile.coq:531: recipe for target 'install' failed-

view this post on Zulip Gaëtan Gilbert (Mar 24 2021 at 13:26):

you're not supposed to use the ci targets with an arbitrary coq
locally compiled coqs (not installed) only

view this post on Zulip Andrej Dudenhefner (Mar 24 2021 at 13:27):

I see, so my initial step to compile and install the master branch was a mistake.

view this post on Zulip Gaëtan Gilbert (Mar 24 2021 at 13:31):

y


Last updated: Feb 01 2023 at 11:04 UTC