Stream: Coq users

Topic: OSX users, please test


view this post on Zulip Enrico Tassi (Jan 07 2021 at 08:43):

I'm about to release Coq 8.13.0 and this is going to be the OSX installer https://dev.azure.com/coq/coq/_build/results?buildId=13980&view=artifacts&pathAsName=false&type=publishedArtifacts . If you read this message and you use OSX, would you mind trying this out? (does it install? does CoqIDE start?). I don't have a Mac to test it myself.

view this post on Zulip Enrico Tassi (Jan 07 2021 at 08:46):

I don't have signed it yet, I'd love to do so after a green flag

view this post on Zulip Théo Zimmermann (Jan 07 2021 at 09:02):

Oh so there will be a non-platform macOS installer for 8.13.0?

view this post on Zulip Enrico Tassi (Jan 07 2021 at 09:20):

Yes, the platform one is not ready yet

view this post on Zulip Enrico Tassi (Jan 07 2021 at 09:27):

I started porting the code ("inspired" by our makefiles) in a PR but I did not finish before the Christmas break.
@Michael Soegtrop wanted to make a nicer installer (a .pkg I guess) like the windows one, but I had no news.

So, for today, I'll publish the same artifact I published for the beta.

view this post on Zulip Théo Zimmermann (Jan 07 2021 at 09:47):

OK

view this post on Zulip Matthieu Sozeau (Jan 07 2021 at 10:48):

I'll try it

view this post on Zulip Matthieu Sozeau (Jan 07 2021 at 10:50):

It works fine

view this post on Zulip Matthieu Sozeau (Jan 07 2021 at 10:51):

I just installed by moving to applications as usual

view this post on Zulip Matthieu Sozeau (Jan 07 2021 at 10:51):

And CoqIDE runs ok

view this post on Zulip Enrico Tassi (Jan 07 2021 at 11:11):

thanks

view this post on Zulip Enrico Tassi (Jan 07 2021 at 11:11):

I'll sign it after lunch

view this post on Zulip Anton Trunov (Jan 07 2021 at 11:12):

Enrico Tassi Works fine on my machine as well (macOS 11.1, "Big Sur").

view this post on Zulip Shachar Itzhaky (Jan 09 2021 at 10:05):

IMHO If all you want is to distribute CoqIDE.app, then a .pkg installer is not really needed; a .dmg where you drag the app to "Applications" is a common idiom in macOS.
If you want to e.g. make links to coqc and coqtop in /usr/bin, then an installer can do that; although perhaps this should just be an opt-in feature of CoqIDE?

view this post on Zulip Shachar Itzhaky (Jan 09 2021 at 10:08):

Unrelated: seems like libgmp.10.dylib is missing and both CoqIDE and coqtop look for it in /usr/local/opt/gmp/lib, which I don't have.
I am running it on M1 (arm64) with Rosetta, but I think it may affect Intel users as well.

view this post on Zulip Enrico Tassi (Jan 09 2021 at 12:03):

Thanks for the bugreport

view this post on Zulip Enrico Tassi (Jan 11 2021 at 22:44):

This time the bundle contains the libgmp.10.dylib shared object, according to the logs. Would you be so kind to test the artifact? (if it works I'll sign it and publish it). Here it is: https://dev.azure.com/coq/coq/_build/results?buildId=13985&view=artifacts&pathAsName=false&type=publishedArtifacts

view this post on Zulip Enrico Tassi (Jan 12 2021 at 08:51):

nope, it does not work for a different reason. I'll try to fix it

view this post on Zulip Enrico Tassi (Jan 12 2021 at 10:01):

OK, I think I fixed it. https://dev.azure.com/coq/coq/_build/results?buildId=13986&view=artifacts&pathAsName=false&type=publishedArtifacts
It works on a Mac I could access to (catalina).

Note to self and other testers: if you don't (temporarily) chmod a-x /usr/local/ then the bundled CoqIDE may find libraries there which were not erroneously bundled in the .app (it was the case for libgmp.10.dylib I'm afraid).

view this post on Zulip Paolo Giarrusso (Jan 12 2021 at 12:11):

chmod a-x /usr/local fails due to permissions, but (a) CoqIDE works here (b) DYLD_PRINT_LIBRARIES=1 /Applications/CoqIDE_8.13.0.app/Contents/MacOS/coqide prints how libraries are resolved, and /usr/local doesn't appear there

view this post on Zulip Paolo Giarrusso (Jan 12 2021 at 12:12):

(but I'm on Catalina as well)

view this post on Zulip Paolo Giarrusso (Jan 12 2021 at 12:14):

And these commands might be scriptable:

otool -L /Applications/CoqIDE_8.13.0.app/Contents/MacOS/coqide
otool -L /Applications/CoqIDE_8.13.0.app/Contents/Resources/bin/*
/Applications/CoqIDE_8.13.0.app/Contents/Resources/bin/coqc:
    @loader_path/../lib/libgmp.10.dylib (compatibility version 15.0.0, current version 15.1.0)
    /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1252.250.1)

view this post on Zulip Enrico Tassi (Jan 12 2021 at 12:23):

Hum, thanks for the hint, grepping for /opt or /usr/local in the output of otool could be enough for a CI test.

view this post on Zulip Guillaume Melquiond (Jan 12 2021 at 13:23):

why would a slave have things installed in /opt or /usr/local?

view this post on Zulip Enrico Tassi (Jan 12 2021 at 13:34):

macports and brew populate these two paths with stuff like gtk that you also want to bundle.

view this post on Zulip Enrico Tassi (Jan 12 2021 at 13:36):

All the pointers to share libraries not in /usr/lib (hence not provided by macos itself) have to be rewritten to point inside the bundle. If you forget to do the rewriting (and hence bundling, since it's the same tool that does both) but you happen to have the library at sight... you app may just work on your machine, but not on a pristine one.

view this post on Zulip Enrico Tassi (Jan 12 2021 at 13:38):

see https://github.com/coq/coq/blob/3c3a3565b8416ddb65114140e7b3021bafa4347d/.github/workflows/ci.yml#L37

view this post on Zulip Enrico Tassi (Jan 12 2021 at 13:39):

It will be the same once the job for the osx installer will be moved to the platform, even if I think we will prefer macports to brew (and it will be the platform script to invoke it, not the ci script).

view this post on Zulip Guillaume Melquiond (Jan 12 2021 at 13:40):

I had understood the issue; the point I was missing is that Macports and Brew were actually using these directories; so yes, if the CI is using them, it makes sense

view this post on Zulip Notification Bot (Jan 14 2021 at 19:02):

This topic was moved by Théo Zimmermann to #VsCoq devs & users > Beginner's help


Last updated: Jan 28 2023 at 06:30 UTC