Stream: Coq Platform devs & users

Topic: opam depext in opam-coq-archive CI


view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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?).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Dec 30 2020 at 11:57):

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

view this post on Zulip 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).

view this post on Zulip Michael Soegtrop (Dec 30 2020 at 12:58):

Even on fast machines it can take a few minutes.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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:

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.

view this post on Zulip Michael Soegtrop (Dec 30 2020 at 17:01):

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

  - 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

view this post on Zulip Enrico Tassi (Dec 30 2020 at 17:08):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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: Jan 29 2023 at 19:02 UTC