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?
in a hurry; but in short, it seems the scripts “freeze” Homebrew formulas from last year, but still use Homebrew from this year.
That’s as-if you used the latest opam, but opam repos from last year, except it’s an unsupported config.
Looking at it again, has somebody tried _ignoring_ the failure and continuing? It seems all required packages are actually installed; in particular, email@example.com is _not_ a dependency of adwaita-icon-theme.
@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?
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.
Ignoring the failure could work indeed, hard to know myself
sticking to the old formula snapshot.
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
I'd be OK I guess to bump every once in a while
I was aiming to _not_ upgrade gtk for this release (that’s hard and dangerous)
It seems the update is just a minor version tho?
Let me try ignoring the brew error tho
please try :-)
But we wouldn't mind having a more up to date formulas, if the current ones are > 1 year old
re gtk, all I know is the bump didn’t “just work”
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.
The underlying issue is that this use of Brew is unsupported.
so after this release you might need something else.
_actually_, longer-term it might be worth asking _on the brew forum_ (not as an issue).
(Homebrew maintainers seem more tolerant of questions on the forum)
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.
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.
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).
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?
Because on Brew that’s surely hard.
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: Dec 07 2023 at 09:01 UTC