Stream: Coq devs & plugin devs

Topic: CI: OSX installer

Enrico Tassi (Nov 24 2020 at 13:50):

Is there a job building it? I found instructions on how to sign the dmg, but not where to find the dmg.

Théo Zimmermann (Nov 24 2020 at 14:19):

No, there is no longer a macOS packaging infrastructure. See https://github.com/coq/coq/pull/13310

Enrico Tassi (Nov 24 2020 at 17:32):

I'm trying to log in to the osx slave, but the username/pwd I find in the instructions do not work. Is it known?

Théo Zimmermann (Nov 24 2020 at 18:16):

I can try to log again in the osx slave to see if I can guide you, but what are you trying to achieve anyway?

Théo Zimmermann (Nov 24 2020 at 18:18):

FYI the slave is on a quite old version of macOS. When I signed the 8.12.0 release with it, I couldn't even test it because our infrastructure generated it for more recent versions.

Théo Zimmermann (Nov 24 2020 at 18:18):

OTOH, there is now a (physical) macOS machine located in your team with a more recent version and which should be usable to do any debugging (though I haven't yet succeeded in connecting to it).

Théo Zimmermann (Nov 24 2020 at 18:22):

Anyway, the macOS packaging infrastructure has always been a mess but it was bound to become worse and worse: we relied on code that nobody understands anymore in Makefile.ide, we relied on Homebrew to get system dependencies even if it's badly suited for pinning packages, we had discovered that we had to rely on an older version of gtk+ (and thus an older pin) because of issues, we didn't notarize the installer which made it raise frightening warnings for macOS >= 10.15, etc.

Théo Zimmermann (Nov 24 2020 at 18:22):

Oh, and I'm forgetting the issue that we had no renewal process for the signing key.

Enrico Tassi (Nov 24 2020 at 18:25):

Théo Zimmermann said:

I can try to log again in the osx slave to see if I can guide you, but what are you trying to achieve anyway?

I wanted to see if the scripts from the platform can work. I don't know the name of the machine you talk about, I know I have an account, but I never used it.

Paolo Giarrusso (Nov 24 2020 at 19:17):

I’d worry more about supporting the Coq platform and opam install coqide...

Paolo Giarrusso (Nov 24 2020 at 19:17):

... but IIUC the latter should be broken as well?

Paolo Giarrusso (Nov 24 2020 at 19:17):

(users are _not_ pinning ancient gtks)

Paolo Giarrusso (Nov 24 2020 at 19:19):

And users of coqide on mac do exist and post (to my surprise, I’ve seen such claims here / on discourse)

Paolo Giarrusso (Nov 24 2020 at 19:42):

OTOH, opam install coqide just worked here (with some prodding for buggy conf- packages)

Paolo Giarrusso (Nov 24 2020 at 19:43):

maybe the new gtk doesn’t support the old mac, or maybe lablgtk got fixed?

Enrico Tassi (Nov 24 2020 at 20:27):

I think CoqIDE is not the main object. I would like a .app with coqc and coqidetop. That is enough for vscoq.

Paolo Giarrusso (Nov 25 2020 at 02:41):

that needn't be a .app, nor does it need notarization probably

Paolo Giarrusso (Nov 25 2020 at 02:41):

skipping coqide avoids (1) needing an old gtk (2) using Homebrew for pinning

Paolo Giarrusso (Nov 25 2020 at 02:43):

(don't quote me on notarization etc., I don't develop native OSX apps, but I can download binaries with wget just fine)

Paolo Giarrusso (Nov 25 2020 at 02:46):

but for users for which opam is a barrier, I'd fear this setup change might still be disruptive.

Théo Zimmermann (Nov 25 2020 at 08:14):

You can install Coq with coqidetop via Homebrew if you don't use opam.

Enrico Tassi (Nov 25 2020 at 08:39):

For binary packages in general I would just follow the experiment with snap which is pretty much related to the platform scripts we have today: you build an opam root in /abspath and you make a tarball/dmg/snap out of it. You use opam to build it, and some users may use opam to extend it, but if you are not into tooling you can just double click to install. Embedding CoqIDE if possible is a plus, but not mandatory IMO. Adding batteries is also easy. The root will be largish, it will carry the ocaml compiler for example (good for native), but whw cares, this is hos "apps" are today.

I don't think we need a lot of makefile trickery to do that, even on osx.

Signatures, notarization... this is another story but we can't even tackle this problem if we don't have a binary to begin with. We have 1.5 month before the final, I think it is worth trying.

Théo Zimmermann (Nov 25 2020 at 08:48):

We should do a WG at the CUDW

Matthieu Sozeau (Nov 25 2020 at 17:10):

I managed to successfully build a coqide app using the azure script (and homebrew packages) without trouble.

Matthieu Sozeau (Nov 25 2020 at 17:11):

So at least we know we can distribute one without too much trouble.

Matthieu Sozeau (Nov 25 2020 at 17:56):

I guess the easiest solution then is to get access to the new os x box

Enrico Tassi (Nov 25 2020 at 20:42):

To give an happy ending to this thread, it seems we have a working solution!
https://github.com/coq/coq/pull/13476

Théo Zimmermann (Nov 27 2020 at 13:46):

FWIW I'm currently running through the process of signing the macOS installer for 8.12.1 and improving the wiki page as I advance through the steps (to make it much clearer).

Théo Zimmermann (Nov 27 2020 at 13:46):

I had already improved it last time, but this was not sufficient.

Pierre-Marie Pédrot (Nov 27 2020 at 13:46):

Did you manage to sign it remotely via SSH?

Pierre-Marie Pédrot (Nov 27 2020 at 13:47):

Or are you still going through the VNC server?

Enrico Tassi (Nov 27 2020 at 13:49):

Would you mind making a call on renater and share your screen?

Théo Zimmermann (Nov 27 2020 at 13:59):

Still going through the VNC server. I have added a note on the wiki that I don't know how to log in via SSH.

Théo Zimmermann (Nov 27 2020 at 14:00):

@Enrico Tassi Sorry, I'm only seeing your message now and I'm almost done, but given that I have added details everywhere I thought they were missing on the wiki page, I'd rather have you follow it and tell me where it's still unclear.

Enrico Tassi (Nov 27 2020 at 14:00):

ok

Enrico Tassi (Nov 27 2020 at 14:12):

the Unix password to log in the VM (you have to ask it via a secured channel to a past release manager)

Théo Zimmermann (Nov 27 2020 at 14:30):

@Enrico Tassi Can you confirm that I should use this SSH key? Can I send the encrypted mail to your debian.org e-mail (the SSH key doesn't seem to be associated with your inria.fr e-mail)?

Théo Zimmermann (Nov 27 2020 at 14:30):

C11A 5053 569A 7C8C 1758 E311 2505 33CC A29B 764F

Théo Zimmermann (Nov 27 2020 at 14:46):

ping @Enrico Tassi

Enrico Tassi (Nov 27 2020 at 14:51):

This is a PGP key, but yes. Here I do have the inria address:

gares@ollypat:~/COQ/backports-8.13$ gpg --list-key A29B764F
pub   rsa4096 2010-10-29 [SC]
      C11A5053569A7C8C1758E311250533CCA29B764F
uid           [ultimate] Enrico Tassi <gareuselesinge@debian.org>
uid           [ultimate] Enrico Tassi <gares@fettunta.org>
uid           [ultimate] Enrico Tassi <Enrico.Tassi@inria.fr>
sub   rsa4096 2010-10-29 [E]

Hum...

Théo Zimmermann (Nov 27 2020 at 14:52):

OK

Théo Zimmermann (Nov 27 2020 at 14:53):

I guess the problem is that the version found on the keyservers does not contain the inria address.

Théo Zimmermann (Nov 27 2020 at 14:54):

I'm having a hard time with Thunderbird's new integrated PGP support.

Théo Zimmermann (Nov 27 2020 at 14:54):

With Enigmail, I could just use the gpg command line to manage my keybase.

Théo Zimmermann (Nov 27 2020 at 14:57):

So basically, I do not know how to add your inria.fr identity to this key. So can I use any of the two other e-mail addresses?

Théo Zimmermann (Nov 27 2020 at 15:18):

ping @Enrico Tassi

Enrico Tassi (Nov 27 2020 at 15:23):

yes, use fettunta

Enrico Tassi (Nov 27 2020 at 15:23):

sorry, I'm "at" a talk

Théo Zimmermann (Nov 27 2020 at 15:39):

:ok:

Théo Zimmermann (Nov 27 2020 at 15:43):

E-mail sent.

Paolo Giarrusso (Nov 27 2020 at 18:09):

You can install Coq with coqidetop via Homebrew if you don't use opam.

(please don’t, you shouldn’t upgrade Coq just because Homebrew said so)

Théo Zimmermann (Nov 28 2020 at 15:45):

Oh that's a good point against using Homebrew to install Coq. Though, it technically is just as good an argument not to use any system package manager (like Arch Linux's). Only Nix and opam give you the full control that upgrading at your own pace requires.

Théo Zimmermann (Nov 28 2020 at 15:46):

That being said, for beginners, using always the latest stable Coq should provide a perfectly acceptable experience. Especially because migrating small code base from one version to the next should have a very little cost, especially if you fix warnings when you see them.

Paolo Giarrusso (Nov 29 2020 at 02:12):

any system package manager

Install a new Ubuntu LTS and your Coq won't be broken for 5 years, tho it might get backported fixed. Still a bad idea, but you'll be burned less often.

Last updated: Dec 07 2023 at 07:39 UTC