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).
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.
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?
@Paolo Giarrusso Is this something new from 8.12? I.e., did it produce fewer warnings with 8.11.X?
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.
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?
ping @Tadeusz Litak who helped out with macOS testing before.
I switched to Mac 10.15 Catalina, which is stricter on this front than 10.14
I can luckily still check on 10.14
OK, that might be it. Apple is getting worse by the day.
We should start to explore how to get into the App Store I guess.
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?
@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.
is it this one:
https://github.com/coq/coq/releases/tag/V8.12.0
or shall I use again the link posted on Friday?
Yes, this one.
It is signed, so it should (normally) show fewer warnings than the one you tried on Friday.
I tried on Catalina as well, and I have the same warnings for both 8.11.1 and 8.12.
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.
@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.
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.
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!
IIUC notarization doesn't force to use the app store, it's one more step beyond the signature
but the warning looks different (and maybe a bit scarier) than the old one
(for unsigned packages)
and the fact that it doesn't offer to open is also the same hoop as unsigned packages
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
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
Hm, IIUC downloading via opam/wget/etc does not quarantine a plugin, so it's not an actual problem
@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?
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.
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.
Sorry, I did it
https://github.com/coq/coq/issues/12760
had forgotten to post here
Thanks!
Last updated: Oct 13 2024 at 01:02 UTC