search

coq / platform

Multi platform setup for Coq, Coq libraries and tools
Creative Commons Zero v1.0 Universal
187 stars 47 forks source link

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

Open ghost opened 3 months ago

ghost commented 3 months ago

After copying the disk image to my applications folder and trying to open it I get the message: “Coq-Platform~8.18~mc2 [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:

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 commented 3 months ago

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

Capture d’écran 2024-05-06 à 20 25 31 Capture d’écran 2024-05-06 à 20 26 05
MSoegtropIMC commented 3 months ago

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 commented 3 months ago

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 commented 3 months ago

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 commented 3 months ago

See also https://github.com/coq/platform/issues/403.

rtetley commented 3 months ago

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 commented 3 months ago

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

MSoegtropIMC commented 3 months ago

@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 commented 3 months ago

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 commented 3 months ago

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 commented 3 months ago

Which MacOS do you have?

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

rtetley commented 3 months ago

13.4.1 (Ventura)

MSoegtropIMC commented 3 months ago

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 commented 3 months ago

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 commented 3 months ago

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

rtetley commented 3 months ago

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 commented 3 months ago

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 commented 2 months ago

This does not work for me.

MSoegtropIMC commented 1 month ago

Triage note: we will retest this in the next release