Stream: Coq devs & plugin devs

Topic: OSX package build


view this post on Zulip Emilio Jesús Gallego Arias (Jul 17 2020 at 09:05):

I'm opening this topic to address the problems we are having with https://github.com/coq/coq/pull/12672 , in particular the build of the OSX packages is failing due to brew problems; @Théo Zimmermann and myself are having some trouble debugging it as we are not OSX users; @Paolo Giarrusso did look a bit into it, @Paolo Giarrusso , would you mind summarizing / pushing the fix you discussed in the 8.12 thread?

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 09:18):

in a hurry; but in short, it seems the scripts “freeze” Homebrew formulas from last year, but still use Homebrew from this year.

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 09:21):

That’s as-if you used the latest opam, but opam repos from last year, except it’s an unsupported config.

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 09:22):

Looking at it again, has somebody tried _ignoring_ the failure and continuing? It seems all required packages are actually installed; in particular, ruby@2.6 is _not_ a dependency of adwaita-icon-theme.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 17 2020 at 09:24):

@Paolo Giarrusso thanks for the summary; how should that work so we get reproducible builds? If we update the pointer to the formulas we get some failure related to gtk; maybe someone would like to have a look into it?

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 09:24):

My other ideas were: 1) stop “freezing” Homebrew — instead, find out which gtk version was installed, and “inline” its installation script 2) maybe try freezing _both_ formulas and brew (by checking out an old version of the brew repo), but that’s more fragile because Brew likes to update itself.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 17 2020 at 09:24):

Ignoring the failure could work indeed, hard to know myself

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 09:25):

sticking to the old formula snapshot.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 17 2020 at 09:25):

Stopping the freeze is a bit dangerous as we would get random versions and we'd like the CI to be reproducible at least a bit

view this post on Zulip Emilio Jesús Gallego Arias (Jul 17 2020 at 09:25):

I'd be OK I guess to bump every once in a while

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 09:25):

I was aiming to _not_ upgrade gtk for this release (that’s hard and dangerous)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 17 2020 at 09:26):

It seems the update is just a minor version tho?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 17 2020 at 09:26):

Let me try ignoring the brew error tho

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 09:26):

please try :-)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 17 2020 at 09:27):

But we wouldn't mind having a more up to date formulas, if the current ones are > 1 year old

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 09:27):

re gtk, all I know is the bump didn’t “just work”

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 09:27):

re stopping the freeze, I meant to _not_ install gtk libraries via brew at all. For the other packages, the exact versions didn’t seem to matter as much.

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 09:27):

The underlying issue is that this use of Brew is unsupported.

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 09:28):

so after this release you might need something else.

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 09:30):

_actually_, longer-term it might be worth asking _on the brew forum_ (not as an issue).

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 09:30):

(Homebrew maintainers seem more tolerant of questions on the forum)

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 09:35):

I should be going, but yet another medium-term idea: you could “vendor” older version of a Formula, by creating your own tap (like your own opam repo)— and that’s totally supported. So if you need, dunno, gtk3.11 instead of the new gtk 3.42, you’d just create a gtk3-coq formula, by copy-pasting the old gtk formula that you have pinned.

view this post on Zulip Paolo Giarrusso (Jul 17 2020 at 16:44):

I should be able to execute that last idea, but probably not for the release.
Have you tried ignoring the brew error? I don't see logs for that in https://github.com/coq/coq/pull/12672.

view this post on Zulip Michael Soegtrop (Jul 17 2020 at 16:58):

I have quite a bit of experience building Coq on macOS with MacPorts, but not su much with homebrew (which does security wise a few rather questionable things).

view this post on Zulip Paolo Giarrusso (Jul 18 2020 at 02:18):

Mac lets you install as non-root anyway; but that’s an old debate. On the new one: with MacPorts, can you freeze ports so that what’s installed in CI only changes when the coq team decides?

view this post on Zulip Paolo Giarrusso (Jul 18 2020 at 02:19):

Because on Brew that’s surely hard.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 18 2020 at 11:43):

Regarding ports vs brew, I have no idea myself; I think most of us are on linux [and Hugo is on quite old OSX version unfortunately] so we'll be happy to change the setup in the way OSX users/devs suggest I think.


Last updated: Oct 21 2021 at 21:03 UTC