Stream: Coq devs & plugin devs

Topic: Testing the signed installers for 8.12.0


view this post on Zulip Théo Zimmermann (Jul 27 2020 at 11:58):

The signed installers for 8.12.0 have been uploaded to a draft release on GitHub. Anyone who is in the @coq/contributors team should be able to download them. It would be much appreciated if some of you could test that everything is in order (in particular w.r.t the signatures).

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 12:00):

In particular, we are doing something that is a bit odd, which is to sign the macOS installer on a macOS 10.12 whereas since Coq 8.11.1, our installer is only compatible with macOS 10.13 and up, which means that we are signing the installer on a machine which cannot run it.

view this post on Zulip Paolo Giarrusso (Jul 27 2020 at 14:40):

I get the following:

“CoqIDE_8.12.0.app” can’t be opened because Apple cannot check it for malicious software.
This software needs to be updated. Contact the developer for more information.

The usual workaround (right-click + open) seems to work – CoqIDE icons are fine (should test the code better).

I've seen this before on other apps, I suspect this might be about notarization?

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 14:47):

@Paolo Giarrusso Is this something new from 8.12? I.e., did it produce fewer warnings with 8.11.X?

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 14:52):

Unfortunately, I had already clicked on the published button before seeing your answer, but I will delay a bit the announcement on Discourse / Coq-Club, to understand if this is something usual or problematic.

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 15:33):

Some other macOS user is welcome to answer this question as well. Is there a regression regarding the Apple warnings that you have to bypass (more warnings than in 8.11) or is this about the same?

view this post on Zulip Karl Palmskog (Jul 27 2020 at 15:35):

ping @Tadeusz Litak who helped out with macOS testing before.

view this post on Zulip Paolo Giarrusso (Jul 27 2020 at 15:42):

I switched to Mac 10.15 Catalina, which is stricter on this front than 10.14

view this post on Zulip Paolo Giarrusso (Jul 27 2020 at 15:42):

I can luckily still check on 10.14

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 15:43):

OK, that might be it. Apple is getting worse by the day.

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 15:44):

We should start to explore how to get into the App Store I guess.

view this post on Zulip Tadeusz Litak (Jul 27 2020 at 16:08):

Karl Palmskog said:

ping Tadeusz Litak who helped out with macOS testing before.

As I said, I'm still on 10.14.6 (though thinking of switching to 10.15) and I had no problems on Friday. Is there something else I can/should test now then?

view this post on Zulip Karl Palmskog (Jul 27 2020 at 16:10):

@Tadeusz Litak as per above, we are looking for reports of what happens when using the signed executable (e.g., what warnings are shown). Théo went through a quite laborious signing process since Friday.

view this post on Zulip Tadeusz Litak (Jul 27 2020 at 16:25):

is it this one:

https://github.com/coq/coq/releases/tag/V8.12.0

or shall I use again the link posted on Friday?

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 16:25):

Yes, this one.

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 16:26):

It is signed, so it should (normally) show fewer warnings than the one you tried on Friday.

view this post on Zulip Théo Winterhalter (Jul 27 2020 at 17:22):

I tried on Catalina as well, and I have the same warnings for both 8.11.1 and 8.12.

view this post on Zulip Théo Winterhalter (Jul 27 2020 at 17:24):

I think this can be scary to casual users because most programs don't do this. You have something in between where it says "It has been downloaded from the internet, are you sure you want to open?" but here it doesn't offer it unless you do "right click — open", by default it just tells you not to use it.

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 17:44):

@Théo Winterhalter OK, thanks for the additional feedback. I think this will do for now, but we should definitely address this for subsequent releases.

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 17:45):

Unfortunately, I cannot say I understand much of these issues, so it would be immensely appreciated if someone could open an issue summarizing briefly the kind of thing (notarization?) that we'd need to do to address this.

view this post on Zulip Tadeusz Litak (Jul 27 2020 at 18:10):

I don't see any new problems on 10.14.6 since Friday. Indeed, this time I didn't even have to manually enable opening in security settings, which seems to be the improvement in question. The problem flagged by other users does seem Catalina-specific; I wouldn't be surprised if Apple is indeed trying to force everybody to use the App Store. Ah, progress!

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

IIUC notarization doesn't force to use the app store, it's one more step beyond the signature

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

but the warning looks different (and maybe a bit scarier) than the old one

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

(for unsigned packages)

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

and the fact that it doesn't offer to open is also the same hoop as unsigned packages

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

Here are the official docs — basically, notarization is an alternative to submitting to the app store, that does some of the same security checks, but without App Review. It does require submitting the software to Apple:
https://developer.apple.com/documentation/xcode/notarizing_macos_software_before_distribution

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

OTOH, what's this? > In macOS 10.15 and later, apps can load quarantined plug-ins — those downloaded from the internet or transferred with AirDrop — only if the plug-in is notarized

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

Hm, IIUC downloading via opam/wget/etc does not quarantine a plugin, so it's not an actual problem

view this post on Zulip Tadeusz Litak (Jul 28 2020 at 16:02):

@Théo Winterhalter or @Paolo Giarrusso , would you be willing then to open this issue that @Théo Zimmermann is asking for? You two tested the installer on Catalina and ran into problems. Especially Paolo has already gone into some detail of what's actually going on. I am not going to do it myself, as without upgrading my OS I cannot reproduce the issue (but I do believe Paolo's summary).

Edit: it seems this ended up outside the testing installer topic and now I see no obvious way of moving the message there. I still have to get the hang of this strange Zulip client. Is moving messages between topics only something that admins can do?

view this post on Zulip Théo Zimmermann (Jul 28 2020 at 16:12):

No this is something that you should be able to do yourself as well, but it might be a limitation of your client. I'll fix this for you.

view this post on Zulip Théo Winterhalter (Jul 28 2020 at 17:05):

Tadeusz Litak said:

Théo Winterhalter or Paolo Giarrusso , would you be willing then to open this issue that Théo Zimmermann is asking for?

I don't really mind, but I have no clue about this stuff so I would rather have someone with more knowledge do it.

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

Sorry, I did it

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

https://github.com/coq/coq/issues/12760

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

had forgotten to post here

view this post on Zulip Théo Winterhalter (Jul 28 2020 at 17:52):

Thanks!


Last updated: Oct 21 2021 at 21:03 UTC