Unable to run Coq-Platform after following instructions for disk image installation on MacBook Air M1 16GB Sonoma 14.4.1

[ghost]

After copying the disk image to my applications folder and trying to open it I get the message: “Coq-Platform8.18mc2 [or whatever version of the disk image I've downloaded] is damaged and can’t be opened. You should move it to the Bin."

This happens both with:

• MacOS (arm) installer for Coq 8.18.0 with MathComp 1.18 (default) (https://github.com/coq/platform/releases/download/2023.11.0/Coq-Platform-release-2023.11.0-version.8.18.2023.11-MacOS-arm64.dmg), and
• MacOS (arm) installer for Coq 8.18.0 with MathComp 2.1 (incomplete) (https://github.com/coq/platform/releases/download/2023.11.0/Coq-Platform-release-2023.11.0-version.8.18.mc2-MacOS-arm64.dmg)

Same for if I command click, right click or control click and then click open. Have removed the platform and tried to reinstall a few times but no luck.

Also, no luck installing by building from sources. I get error messages when trying to build a couple of the packages.

[tcosmo]

I get the exact same issue on MacBook Pro M3 Max 36 Go with Sonoma 14.2.1 :(

Verification gets stuck 2/3 of the way, then Macos says to eject the dmg

[MSoegtropIMC]

That's weird - apparently something with the signing went wrong. INRIA has new procedures here, but both me and @rtetley tested the installers and it did work for us. Meanwhile please use the install from sources method. Please note that relation-algebra currently fails on MacOS >= 14.3 (14.2 should be fine as far as I have heard).

[ghost]

That's weird - apparently something with the signing went wrong. INRIA has new procedures here, but both me and @rtetley tested the installers and it did work for us. Meanwhile please use the install from sources method. Please note that relation-algebra currently fails on MacOS >= 14.3 (14.2 should be fine as far as I have heard).

I am also unable to build from source. Off of the top of my head, I get error messages about gappa not being built with 4 make jobs, or something like this. Also, even though I already have command line tools installed, I am prompted halfway through that command line tools needs to update to use m4 command or something like this. Perhaps something to do with C or C++ tooling?

[MSoegtropIMC]

This sounds like a configuration problem of your package manager - either homebrew or MacPorts (both are well tested) - and/or XCode. All similar reports I had in the past could be solved by fixing the package manager (worst case to reinstall it from scratch). I am not aware that XCode misconfiguration leads to such effects, but it cannot be excluded.

But if you don't need gappa, it should not hurt that its build failed. All opam packages which did install properly are usable.

[MSoegtropIMC]

See also #403.

[rtetley]

It seems file upload is not working. On my local computer the signed files are working perfectly fine but once I upload and re-download them I get the same error... I've tried re-uploading them with no success. @MSoegtropIMC any ideas what I could be doing wrong ?

[MSoegtropIMC]

Can you send me the signed files again via the INRIA fiel transfer service? I will check.

[MSoegtropIMC]

@rtetley : there are some rumors that Sonoma strictly requires notarisation, so you need to look into this.

As far as I can see we both tested it with older versions of MacOS, which did work, then both updated to Sonoma and now it doesn't work any more. As far as I can tell all versions of the signed file you ever signed or uploaded are binary identical.

[MSoegtropIMC]

On the other hand older, not yet notarised Cq installers (say 8.16 or 8.17) do still work, so there might be something specific about the signature Sonoma does not like. Possibly it depends on the date on which the app has been signed. Possibly if it has been signed before some critical date it works even on Sonoma.

[rtetley]

But I haven't updated my machine ? And when I use the file locally (before upload to github) it works, once I upload it and I re-download it, it crashes with the same error as above.

[MSoegtropIMC]

Which MacOS do you have?

MacOS might distinguish between files you created locally and you downloaded from the internet.

[rtetley]

13.4.1 (Ventura)

[MSoegtropIMC]

OK. I was on 12.7.1 before I updated. So a possibility is that it did work for me because my MacOS was so old and it did work for you because you created the file locally.

[rtetley]

I downloaded the dmgs from the same archive I sent you, and it works. I really think there is something wrong with the upload on github. Also, the signed executables were not created locally, the signing process at Inria works through a remote machine.

[MSoegtropIMC]

But you can easily see that the files are identical (your favourite comparison program or compute a hash)

[rtetley]

I agree with you... Maybe I messed up and used the wrong file. I'll try again. Still the error message I get (corrupted file) is weird.

[ghost]

This solution worked for me and might work for others: after opening the coq platform .dmg and dragging to applications folder, you find you get the message about the app being damaged and should be dragged to the bin. I went to Settings > Privacy and Security > Full Disk Access. From there, I needed to give coq platform full disk access (just have to click a button). Then I could open coq platform and ide without issue.

[rongcuid]

This does not work for me.

[MSoegtropIMC]

Triage note: we will retest this in the next release