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.
I don't have signed it yet, I'd love to do so after a green flag
Oh so there will be a non-platform macOS installer for 8.13.0?
Yes, the platform one is not ready yet
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.
I'll try it
It works fine
I just installed by moving to applications as usual
And CoqIDE runs ok
I'll sign it after lunch
Enrico Tassi Works fine on my machine as well (macOS 11.1, "Big Sur").
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
/usr/bin, then an installer can do that; although perhaps this should just be an opt-in feature of CoqIDE?
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.
Thanks for the bugreport
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
nope, it does not work for a different reason. I'll try to fix it
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).
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
(but I'm on Catalina as well)
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
/usr/local in the output of
otool could be enough for a CI test.
why would a slave have things installed in
macports and brew populate these two paths with stuff like gtk that you also want to bundle.
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.
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).
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
This topic was moved by Théo Zimmermann to #VsCoq devs & users > Beginner's help
Last updated: Sep 23 2023 at 08:01 UTC