Stream: Coq Platform devs & users

Topic: opam depext in opam-coq-archive CI

Michael Soegtrop (Dec 30 2020 at 11:33):

@Karl Palmskog : I don't know if you have seen my comment in (https://github.com/coq/opam-coq-archive/pull/1537). This PR fails because the CI of opam-coq-archive doesn't call depext. I guess for pure Coq packages this is fine, but gappa has a lengthy list of depext packages.

Do you think it would be feasible / OK to have depext in opam-coq-archive CI? If not I can remove the gappa.dev package and keep it forver in the opam patch repo of the Coq Platform master branch. The release package is in the main opam repo and passes CI fine there on many platforms (they call opam depext).

Karl Palmskog (Dec 30 2020 at 11:51):

@Michael Soegtrop adding depext just because of gappa seems unncessary. Why not just add the required Debian packages into the CI config like Enrico suggested?

Michael Soegtrop (Dec 30 2020 at 11:54):

You mean add these packages in the CI config for all packages? This might be more wasteful than calling opam depext for all installed packages. If I remember right gappa has a few dependencies which take a while to install (boost?).

Michael Soegtrop (Dec 30 2020 at 11:56):

But as I said, if this is problematic, I see no issue in keeping the gappa package forever in the Coq Platform Master patch repo. For the release branches there is no issue, since gappa is in the opam main (not coq) repo.

Karl Palmskog (Dec 30 2020 at 11:56):

every CI run in the opam archive builds Coq, so almost any binary package installation will be a drop in the bucket

Michael Soegtrop (Dec 30 2020 at 11:57):

You don't install boost regularly I guess ;-)

Michael Soegtrop (Dec 30 2020 at 12:58):

(boost is about 13.000 C header files and this makes even binary instalations quite slow - depending on how many sanity checks the package manager does per file).

Michael Soegtrop (Dec 30 2020 at 12:58):

Even on fast machines it can take a few minutes.

Michael Soegtrop (Dec 30 2020 at 14:58):

@Karl Palmskog : I thought aboit this and I don't like the idea of adding the packages to CI a lot. There will likely come more of this (Z3 for Coq-hammer, ...) and I like the platform independent way of depext. Adding depext is a one time effort for many packages.

Karl Palmskog (Dec 30 2020 at 15:00):

can you coordinate with Enrico if you want to add depext stuff? I think he was the last person to fiddle with those scripts. What I don't want to happen is for regular CI jobs to fail due to scripting issues that were added for Gappa, which almost nobody uses

Karl Palmskog (Dec 30 2020 at 15:01):

or in other words, I would rather have a working CI that fails for some packages with obscure dependencies than a faulty CI tailored for packages with such dependencies.

Michael Soegtrop (Dec 30 2020 at 16:09):

I think it doesn't make a lot of sense to handle complicated dependencies for each package and each CI system separately.
So the options I see are:

• use depext in opam-coq-archive CI
• keep the packages which need extra dependencies in the Coq Platform patch repo

I am fine with either way - your choice. I don't think that handling depext will be complicated. It should be one command to install it and one to run it. It should only fail if depext entries are bogus. Sure I can align with @Enrico Tassi on this topic as you suggest.

Michael Soegtrop (Dec 30 2020 at 17:01):

@Enrico Tassi: I had a quick look at the CI scripts. A few questions:

• opam seems to be initialized before it is installed:

  - test -e $OPAM_ROOT_CACHE || scripts/opam-coq-init
  - curl -L https://github.com/ocaml/opam/releases/download/${OPAM_VERSION}/opam-${OPAM_VERSION}-x86_64-linux >/usr/local/bin/opam

• It is not clear to me when test -e $OPAM_ROOT_CACHE fails or what to do to reinit opam. If we add depext it would make most sense to do it once.
• There is a duplicate and different yaml key opam-build:any:. Which one is the correct?
• The script opam-coq-install-remove has set -e but checks for errors with if [ $? != 0 ]; then - do I miss something?

Enrico Tassi (Dec 30 2020 at 17:08):

• There is a "cache", which contains an opam root (with many switches, IIRC, one per compiler), the cache is used to generate a pristine root for each package we try
• opam is not in the cache, so we install it every time, while we init the opam root only if it is not there yet.
• the double entry is a typo
• what I see is

set +e
echo Installing $PKG_NAME_VERSION
opam install "$PKG_NAME_VERSION" -y -v -v $EXTRA_OPAM_OPTION >> $LOG
if [ $? != 0 ]; then
  RC=1;
  FAILURES="$FAILURES $PKG_NAME_VERSION";
else
  SUCCESSES="$SUCCESSES $PKG_NAME_VERSION";
fi
echo Removing $PKG_NAME
opam remove "$PKG_NAME" -y >> $LOG
set -e

which seems correct about set +/- e

Enrico Tassi (Dec 30 2020 at 17:08):

The point is that we want to try all packages, even if one fails, and this is important since many PRs add/modify many packages.

Michael Soegtrop (Dec 30 2020 at 17:47):

@Enrico Tassi : Ah yes, I didn't see the inner set +e - this is fine then.

How can I clear the cache in case I want to add something (that is depext) to the tar file generated at the end of opam-coq-init? For Travis there are buttons in the settings section, but I couldn't find something similar for Gitlab.

What I still don't understand is the logic of running opam (in opam-coq-init) and one line later downloading a different opam. What is the point of doing it in this order rather than the other way around? Wouldn't the first step fail if there is no opam installed as yet?

Enrico Tassi (Dec 30 2020 at 18:10):

I don't know how the cache works in gitlab ci (originally the scripts were using travis)

Enrico Tassi (Dec 30 2020 at 18:10):

if the cache is there, then you don't run opam-coq-init. if it is not, then you install opam twice

Last updated: Jun 03 2023 at 05:01 UTC