Enrico Tassi (Jan 07 2021 at 08:43): 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.
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
Théo Zimmermann (Jan 07 2021 at 09:02):Oh so there will be a non-platform macOS installer for 8.13.0?
Enrico Tassi (Jan 07 2021 at 09:20):Yes, the platform one is not ready yet
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.
Théo Zimmermann (Jan 07 2021 at 09:47):OK
Matthieu Sozeau (Jan 07 2021 at 10:48):I'll try it
Matthieu Sozeau (Jan 07 2021 at 10:50):It works fine
Matthieu Sozeau (Jan 07 2021 at 10:51):I just installed by moving to applications as usual
Matthieu Sozeau (Jan 07 2021 at 10:51):And CoqIDE runs ok
Enrico Tassi (Jan 07 2021 at 11:11):thanks
Enrico Tassi (Jan 07 2021 at 11:11):I'll sign it after lunch
Anton Trunov (Jan 07 2021 at 11:12):Enrico Tassi Works fine on my machine as well (macOS 11.1, "Big Sur").
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?
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.
Enrico Tassi (Jan 09 2021 at 12:03):Thanks for the bugreport
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
Enrico Tassi (Jan 12 2021 at 08:51):nope, it does not work for a different reason. I'll try to fix it
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).
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
Paolo Giarrusso (Jan 12 2021 at 12:12):(but I'm on Catalina as well)
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)
Hum, thanks for the hint, grepping for /opt or /usr/local in the output of otool could be enough for a CI test.
Guillaume Melquiond (Jan 12 2021 at 13:23):why would a slave have things installed in /opt or /usr/local?
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.
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.
Enrico Tassi (Jan 12 2021 at 13:38): 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).
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
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: Sep 23 2023 at 08:01 UTC