Is there a job building it? I found instructions on how to sign the dmg, but not where to find the dmg.
No, there is no longer a macOS packaging infrastructure. See https://github.com/coq/coq/pull/13310
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?
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?
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.
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).
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.
Oh, and I'm forgetting the issue that we had no renewal process for the signing key.
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.
I’d worry more about supporting the Coq platform and opam install coqide
...
... but IIUC the latter should be broken as well?
(users are _not_ pinning ancient gtks)
And users of coqide on mac do exist and post (to my surprise, I’ve seen such claims here / on discourse)
OTOH, opam install coqide
just worked here (with some prodding for buggy conf-
packages)
maybe the new gtk doesn’t support the old mac, or maybe lablgtk got fixed?
I think CoqIDE is not the main object. I would like a .app with coqc and coqidetop. That is enough for vscoq.
that needn't be a .app
, nor does it need notarization probably
skipping coqide avoids (1) needing an old gtk (2) using Homebrew for pinning
(don't quote me on notarization etc., I don't develop native OSX apps, but I can download binaries with wget
just fine)
but for users for which opam
is a barrier, I'd fear this setup change might still be disruptive.
You can install Coq with coqidetop
via Homebrew if you don't use opam.
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.
We should do a WG at the CUDW
I managed to successfully build a coqide app using the azure script (and homebrew packages) without trouble.
So at least we know we can distribute one without too much trouble.
I guess the easiest solution then is to get access to the new os x box
To give an happy ending to this thread, it seems we have a working solution!
https://github.com/coq/coq/pull/13476
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).
I had already improved it last time, but this was not sufficient.
Did you manage to sign it remotely via SSH?
Or are you still going through the VNC server?
Would you mind making a call on renater and share your screen?
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.
@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.
ok
the Unix password to log in the VM (you have to ask it via a secured channel to a past release manager)
@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)?
C11A 5053 569A 7C8C 1758 E311 2505 33CC A29B 764F
ping @Enrico Tassi
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...
OK
I guess the problem is that the version found on the keyservers does not contain the inria address.
I'm having a hard time with Thunderbird's new integrated PGP support.
With Enigmail, I could just use the gpg
command line to manage my keybase.
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?
ping @Enrico Tassi
yes, use fettunta
sorry, I'm "at" a talk
:ok:
E-mail sent.
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)
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.
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.
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: May 31 2023 at 16:01 UTC