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

palmskog · 2022-04-09T11:25:49Z

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.

…llow depexts

erikmd · 2022-04-09T12:05:10Z

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?

docker-coq-action/README.md

Lines 76 to 78 in e717ad9

    
           opam pin add -n -y -k path coq-proj folder 
        
           opam update -y 
        
           opam install -y -j 2 coq-proj --deps-only

&

docker-coq-action/README.md

Lines 221 to 223 in e717ad9

    
             opam pin add -n -y -k path $PACKAGE $WORKDIR 
        
             opam update -y 
        
             opam install -y -j 2 $PACKAGE --deps-only

…nstallation

palmskog · 2022-04-09T13:39:25Z

@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 · 2022-04-09T13:48:36Z

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

docker-coq-action/README.md

Line 663 in e717ad9

sudo apt-get update -y -q # Mandatory

with a commented-out version:

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

and likewise for:

docker-coq-action/.github/workflows/coq-demo.yml

Line 273 in e717ad9

sudo apt-get update -y -q

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 · 2022-04-09T13:50:59Z

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?

….yml and update documentation

palmskog · 2022-04-09T16:59:36Z

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 · 2022-04-09T17:26:52Z

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 · 2022-04-09T17:34:01Z

@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 · 2022-04-09T17:34:41Z

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

…efore_script example

palmskog · 2022-04-09T17:40:12Z

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

erikmd · 2022-04-09T17:51:06Z

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 · 2022-04-09T17:54:41Z

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:   "[email protected]"
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 · 2022-04-09T17:55:38Z

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 · 2022-04-09T17:56:33Z

Yes, see the end of my comment :)

Do you think gappa is a good example?

palmskog · 2022-04-09T17:58:46Z

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.

`custom_image / docker-coq / opam / auto install depexts`

erikmd · 2022-04-09T18:40:06Z

FYI I committed one such test in ece4f1b with:

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

feat: change from yes to unsafe-yes on dep install in action.yml to a…

7e883fe

…llow depexts

erikmd added the enhancement New feature or request label Apr 9, 2022

erikmd self-assigned this Apr 9, 2022

docs(README.md): document --confirm-level=unsafe-yes for dependency i…

5ea1fa5

…nstallation

feat: add apt-get update command to dependency installation in action…

d6a62ce

….yml and update documentation

erikmd changed the title ~~allow installs of dependencies with depexts~~ feat: Allow automatic install of system dependencies (needs opam 2.1) Apr 9, 2022

doc: comment out the now-redundant apt-get update command in custom b…

814026a

…efore_script example

test(coq-demo.yml): Add demo-6

ece4f1b

`custom_image / docker-coq / opam / auto install depexts`

erikmd merged commit e8a69bd into master Apr 9, 2022

erikmd deleted the depext-unsafe-yes branch April 9, 2022 18:58

erikmd mentioned this pull request Jun 20, 2022

feat: Drop support of ocaml_version: "minimal" #75

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

palmskog commented Apr 9, 2022

erikmd commented Apr 9, 2022

palmskog commented Apr 9, 2022

erikmd commented Apr 9, 2022 •

edited

Loading

erikmd commented Apr 9, 2022

palmskog commented Apr 9, 2022 •

edited

Loading

erikmd commented Apr 9, 2022

palmskog commented Apr 9, 2022 •

edited

Loading

erikmd commented Apr 9, 2022

palmskog commented Apr 9, 2022

erikmd commented Apr 9, 2022

erikmd commented Apr 9, 2022

palmskog commented Apr 9, 2022

erikmd commented Apr 9, 2022

palmskog commented Apr 9, 2022

erikmd commented Apr 9, 2022 •

edited

Loading

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

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

Conversation

palmskog commented Apr 9, 2022

erikmd commented Apr 9, 2022

palmskog commented Apr 9, 2022

erikmd commented Apr 9, 2022 • edited Loading

erikmd commented Apr 9, 2022

palmskog commented Apr 9, 2022 • edited Loading

erikmd commented Apr 9, 2022

palmskog commented Apr 9, 2022 • edited Loading

erikmd commented Apr 9, 2022

palmskog commented Apr 9, 2022

erikmd commented Apr 9, 2022

erikmd commented Apr 9, 2022

palmskog commented Apr 9, 2022

erikmd commented Apr 9, 2022

palmskog commented Apr 9, 2022

erikmd commented Apr 9, 2022 • edited Loading

erikmd commented Apr 9, 2022 •

edited

Loading

palmskog commented Apr 9, 2022 •

edited

Loading

palmskog commented Apr 9, 2022 •

edited

Loading

erikmd commented Apr 9, 2022 •

edited

Loading