feat: Allow automatic install of system dependencies (needs opam 2.1)

palmskog commented 2 years ago

Since all Docker images switched to opam 2.1, it might make sense to enable installing depext dependencies automatically (in this case, Debian system packages).

However, the current definition of the install task does not permit installing depext dependencies, since a simple -y/--yes does not suffice for system packages, instead one has to:

set OPAMCONFIRMLEVEL=unsafe-yes or --confirm-level=unsafe-yes to launch non interactive system package commands.

Note that Docker-Coq-Action users will still have to run sudo apt-get update -y -q somewhere before the dependency installation to get system packags, but this is already documented in the wiki. The --confirm-level=unsafe-yes is much more obscure to figure out and set manually, so I propose we set it by default here.

erikmd commented 2 years ago

Hi @palmskog, thanks for your suggestion!

LGTM (albeit users that override the install task won't benefit from the update, but I don't see a better solution)

Just 2 questions:

sudo apt-get update -y -q is documented indeed, but what about running it by default after opam update -y? the only drawback I see would be a small additional delay (several seconds or so), for the good cause!
can you also update the README.md?

https://github.com/coq-community/docker-coq-action/blob/e717ad9bc843f08ecbdf7d7f493b8704df3a79d7/README.md?plain=1#L76-L78

&

https://github.com/coq-community/docker-coq-action/blob/e717ad9bc843f08ecbdf7d7f493b8704df3a79d7/README.md?plain=1#L221-L223

palmskog commented 2 years ago

@erikmd I updated README.md to mention --confirm-level=unsafe-yes.

I would personally be in favor of having a sudo apt-get update -y -q, since this would seemingly would give out-of-the-box automatic installation of required system packages. I assume you mean like this:

startGroup "Install dependencies"
  opam pin add -n -y -k path $PACKAGE $WORKDIR
  opam update -y
  sudo apt-get update -y -q
  opam install --confirm-level=unsafe-yes -j 2 $PACKAGE --deps-only
endGroup

If this is what you had in mind, I can add it to this PR.

Finally, do we want to write about depext and confirm-level stuff in a sentence of two in README.md? It looks like the only official documentation is this page, so maybe we should link that?

erikmd commented 2 years ago

Hi @palmskog,

I updated README.md to mention --confirm-level=unsafe-yes.

Thanks.

I would personally be in favor of having a sudo apt-get update -y -q, since this would seemingly would give out-of-the-box automatic installation of required system packages. I assume you mean like this:
startGroup "Install dependencies"
  opam pin add -n -y -k path $PACKAGE $WORKDIR
  opam update -y
  sudo apt-get update -y -q
  opam install --confirm-level=unsafe-yes -j 2 $PACKAGE --deps-only
endGroup
If this is what you had in mind, I can add it to this PR.

Exactly! I agree with you that it's worth it to have this feature working "out-of-the-box"…

If you can add this line sudo apt-get update -y -q at the three places involved (action.yml + README.md), that'd be great!

Meanwhile, I think you should replace this line

https://github.com/coq-community/docker-coq-action/blob/e717ad9bc843f08ecbdf7d7f493b8704df3a79d7/README.md?plain=1#L663

with a commented-out version:

          # sudo apt-get update -y -q # this mandatory command is already run in install step

and likewise for:

https://github.com/coq-community/docker-coq-action/blob/e717ad9bc843f08ecbdf7d7f493b8704df3a79d7/.github/workflows/coq-demo.yml#L273

Finally, do we want to write about depext and confirm-level stuff in a sentence of two in README.md? It looks like the only official documentation is this page, so maybe we should link that?

Good idea: I suggest you add some sentences in this section:

https://github.com/coq-community/docker-coq-action#opam

and the link you suggest looks fine to me.

erikmd commented 2 years ago

BTW, which order looks best to you?

startGroup "Install dependencies"
  opam pin add -n -y -k path $PACKAGE $WORKDIR
  opam update -y
  sudo apt-get update -y -q
  opam install --confirm-level=unsafe-yes -j 2 $PACKAGE --deps-only
endGroup

or

startGroup "Install dependencies"
  sudo apt-get update -y -q
  opam pin add -n -y -k path $PACKAGE $WORKDIR
  opam update -y
  opam install --confirm-level=unsafe-yes -j 2 $PACKAGE --deps-only
endGroup

Maybe the second one?

palmskog commented 2 years ago

I like the second order best, and I tried this out in the bertrand project, CI log can be seen here.

Looks like it works fine, so I added the apt-get command and documentation with release notes link in d6a62ce.

erikmd commented 2 years ago

Looks very good to me. I'm going to squash-merge and doing a release.

Thanks a lot @palmskog for your help on this!

palmskog commented 2 years ago

@erikmd but I noticed now I missed your suggestions to comment out the sudo apt-get lines in the documentation and coq-demo.yml. I'll try to fix this in the next 10-20 min.

erikmd commented 2 years ago

Ah OK! no worries, I can do the merge later on tonight

palmskog commented 2 years ago

OK, documentation update on sudo apt-get done now in 814026a, please merge at your convenience (i.e., no hurry on my side).

erikmd commented 2 years ago

OK thanks @palmskog.

Just before merging, I believe I'll add a small unit test in the docker-coq-action CI testsuite.

Namely, a package that would rely on a system package such as gmp(?)

erikmd commented 2 years ago

FTR, given the following command:

$ opam search --depends-on=conf-gmp
# Packages matching: depends-on(conf-gmp)
# Name                 # Installed # Synopsis
bap-std                --          The Binary Analysis Platform Standard Library
bitwuzla               --          SMT solver for QF_AUFBVFP
bitwuzla-bin           --          Bitwuzla SMT solver executable
bitwuzla-c             --          SMT solver for AUFBVFP (C API)
comby                  --          A tool for structural code search and replace that supports ~every lan
conf-gmp-powm-sec      --          Virtual package relying on a GMP lib with constant-time modular expone
conf-mpfr              --          Virtual package relying on library MPFR installation
coq-coqprime-generator --          Certificate generator for prime numbers in Coq
gappa                  --          Tool intended for formally proving properties on numerical programs de
gmp-ecm                --          GMP-ECM library for the Elliptic Curve Method (ECM) for integer factor
goblint                --          Static analysis framework for C
lutin                  --          Lutin: modeling stochastic reactive systems
mlgmp                  --          Interface of GNU MP and MPFR
mlgmpidl               --          OCaml interface to the GMP library
numerix                --          Big integer library, written by Michel Quercia. Compares well to GMP.
polka                  --          Polka: convex polyhedron library by Bertrand Jeannet (now part of apro
sail                   --          Sail is a language for describing the instruction semantics of process
secp256k1-internal     --          Bindings to secp256k1 internal functions (generic operations on the cu
yices2                 --          Yices2 SMT solver binding
z3                     --          Z3 solver
zarith                 --          Implements arithmetic and logical operations over arbitrary-precision

zarith could have been a good choice, but it is already installed in Docker-Coq images!

so… let's stick to gappa as an example, which also depends on conf-mpfr:

$ opam show gappa.1.4.0

<><> gappa: information on all versions <><><><><><><><><><><><><><><><><><><><>
name         gappa
all-versions 1.3.5  1.4.0

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><><><>
version       1.4.0
repository    default
url.src:      "https://gitlab.inria.fr/gappa/gappa/-/archive/gappa-1.4.0.tar.gz"
url.checksum: "sha512=d5ed841fc8def27ae3973c97d9a242e2fe4997888d3a8c2d46029aab2c5311ec5d0df3a0780fc88eead20d6aa4b34122c9bb8d290f3a2b4886488f34602d43c7"
homepage:     "https://gitlab.inria.fr/gappa/gappa"
bug-reports:  "https://gitlab.inria.fr/gappa/gappa/-/issues"
dev-repo:     "git+https://gitlab.inria.fr/gappa/gappa.git"
authors:      "Guillaume Melquiond"
maintainer:   "7895506+MSoegtropIMC@users.noreply.github.com"
license:      "CeCILL"
depends:      "conf-g++" {build}
              "conf-autoconf" {build}
              "conf-automake" {build}
              "conf-gmp"
              "conf-mpfr"
              "conf-boost"
              "conf-bison" {build}
              "conf-flex" {build}
synopsis      Tool intended for formally proving properties on numerical programs dealing with
              floating-point or fixed-point arithmetic

palmskog commented 2 years ago

A unit test sounds like a good idea. However, isn't gmp already installed as a system package, since Coq needs it (via zarith). My suggestion would be to add something to the unit test that depends on conf-zlib, such as camlzip.

erikmd commented 2 years ago

Yes, see the end of my comment :)

Do you think gappa is a good example?

palmskog commented 2 years ago

gappa could be a good example, but it has a lot of conf-* dependencies, so it might take a while to run. So I'd go with gappa if running time is not a concern, and camlzip otherwise.

erikmd commented 2 years ago

FYI I committed one such test in ece4f1be42a31b3093e9aacfb5721e787488152e with:

The test passed and the timing is reasonable (GHA log), so that looks good to go.

coq-community / docker-coq-action

feat: Allow automatic install of system dependencies (needs opam 2.1) #74