Théo Zimmermann (Jun 07 2020 at 15:17): Théo Zimmermann (Jun 07 2020 at 15:17):Could some macOS users test the installer for the v8.12 branch that can be downloaded from this page? https://dev.azure.com/coq/coq/_build/results?buildId=10328&view=artifacts&type=publishedArtifacts
Usual things to check in CoqIDE (from the top of my head):
Karl Palmskog (Jun 07 2020 at 15:30):I remember doing similar tests for Windows for 8.11.0 and struggling to figure out all the actions that should be tried. Maybe make an issue about writing this down somewhere?
Karl Palmskog (Jun 07 2020 at 16:08):in particular, I think one should test opening a file in the middle of a nontrivial compiled third-party project (to see that _CoqProject, or equivalent when compiled by dune works)
Emilio Jesús Gallego Arias (Jun 08 2020 at 14:43):@Hugo Herbelin has been testing quite a few packages in the past, maybe he would be interested.
Hugo Herbelin (Jun 08 2020 at 14:59):It does not work. I have a "dyld: Symbol not found: _NSPasteboardTypeURL" error when running coqide (but coqtop works). No time to investigate now. Full message is:
dyld: Symbol not found: _NSPasteboardTypeURL
Referenced from: /Applications/CoqIDE_8.12+alpha.app/Contents/MacOS/../Resources/lib/libgdk-3.0.dylib
Expected in: /System/Library/Frameworks/AppKit.framework/Versions/C/AppKit
in /Applications/CoqIDE_8.12+alpha.app/Contents/MacOS/../Resources/lib/libgdk-3.0.dylib
Trace/BPT trap
Thanks a lot for testing Hugo, what's your OSX version @Hugo Herbelin
Hugo Herbelin (Jun 08 2020 at 15:40):10.11.1
Hugo Herbelin (Jun 08 2020 at 18:29):10.11 is 5 years old. I don't know which versions you want to target. Here, the code is produced using Azure's 10.14 (iiuc), which apparently produces a different format of executable (or, most probably, a format with new features). Maybe adding export MACOSX_DEPLOYMENT_TARGET=10.11 in the Azure script may help (or the same with whatever "deployment" version you want to target).
Théo Zimmermann (Jun 09 2020 at 09:53):This variable is already set: https://github.com/coq/coq/blob/3080a8e9500b854344b3df5840feefd15ef0cbd1/azure-pipelines.yml#L56
Théo Zimmermann (Jun 09 2020 at 09:54):It is quite surprising that this installer is not working for you but the one for v8.11 that you tested relatively recently was working (after this variable was set).
Théo Zimmermann (Jun 09 2020 at 09:55):Oh actually, this variable was not added very recently (coq/coq#10186).
Théo Zimmermann (Jun 09 2020 at 09:55):But still, I'm puzzled by this.
Emilio Jesús Gallego Arias (Jun 09 2020 at 12:49):lablgtk versions are the same right?
Théo Zimmermann (Jun 09 2020 at 12:56):The only difference between v8.11 and v8.12 in the Azure pipeline packaging job is:
@@ -87,6 +98,7 @@ jobs:
- script: |
eval $(opam env)
+ export OCAMLPATH=$(pwd):"$OCAMLPATH"
make -j "$NJOBS" test-suite PRINT_LOGS=1
displayName: 'Run Coq Test Suite'
Bizarre :S
Théo Zimmermann (Jun 09 2020 at 12:57):Homebrew is pinned. The macOS image is fixed.
Théo Zimmermann (Jun 09 2020 at 12:58):The OCaml and findlib versions are pinned but not the version of lablgtk!
Emilio Jesús Gallego Arias (Jun 09 2020 at 13:02):Yup we should try to see if there is a difference in gtk / lablgtk
Théo Zimmermann (Jun 09 2020 at 13:24):lablgtk 3.1.0 was released end of January 2020. If the macOS installer for Coq 8.11.1 works on @Hugo Herbelin's machine, then that's not it.
Emilio Jesús Gallego Arias (Jun 09 2020 at 13:34):Could be the case that 8.12 is using some more features, for example in the completion. IMHO anyways we should ping.
Emilio Jesús Gallego Arias (Jun 09 2020 at 13:35):But yeah, we need someone else to try the package
Anton Trunov (Jun 09 2020 at 13:48):I tried the actions mentioned by @Théo Zimmermann. It worked for me on macOS 10.15.4 "Catalina".
Anton Trunov (Jun 09 2020 at 13:48):macOS complained about missing signature before opening CoqIDE, though.
Théo Zimmermann (Jun 09 2020 at 13:49):Yeah, that's normal.
Hugo Herbelin (Jun 09 2020 at 14:06):Théo Zimmermann said:
lablgtk 3.1.0 was released end of January 2020. If the macOS installer for Coq 8.11.1 works on Hugo Herbelin's machine, then that's not it.
Actually, 8.11.1 does not work either (same error).
Théo Zimmermann (Jun 09 2020 at 14:09):Oh OK, and does 8.11.0 work for you? (It was released after the 3.1.0 release but very likely built before.)
Hugo Herbelin (Jun 09 2020 at 15:18):The dmg for 8.11.0 works. Note that it does not have the same libgdk-3.0.dylib as in 8.11.1 and that this file does not mention the _NSPasteboardTypeURL symbol for 8.11.0. (It mentions instead a symbol called _NSURLPboardType which is apparently deprecated since MacOS 10.14.) Sorry no time for further investigations at the moment.
Hugo Herbelin (Jun 09 2020 at 21:02):What (only) matters is probably the version of gtk installed on the Azure pipeline (apparently gtk+3-3.24.11.mojave.bottle.tar.gz according to recent builds) which is not anymore compatible with MacOS 10.11.1 and suspectingly not compatible with 10.12 either, based on the fact that _NSPasteboardTypeURL arrived in 10.13. Is there a way to know what version of gtk was installed on the Azure pipeline at the time of 8.11.0 for comparison? (In any case, there is no bug involved)
Théo Zimmermann (Jun 10 2020 at 08:44):The macOS image was upgraded from macOS-10.13 to macOS-10.14 between 8.11.0 and 8.11.1. So I think this can explain the change of version of gtk+.
Maxime Dénès (Jun 11 2020 at 19:43):Is it a good idea to do it in a minor release, though? Isn't it under our control?
Théo Zimmermann (Jun 12 2020 at 07:02):This was coq/coq#11803. Apparently the previous image was deprecated and scheduled to be removed just 12 days after. So no choice but to backport.
Théo Zimmermann (Jun 12 2020 at 07:03):But the PR was thoroughly tested. Initially it broke macOS 10.11.1 and then a later version fixed it.
Théo Zimmermann (Jun 12 2020 at 07:03):So since then something else must have changed to make it break again.
Théo Zimmermann (Jul 24 2020 at 14:21):The release candidate for 8.12.0 is 558e8ea. If some macOS users are around, it would be great if you could test the generated macOS installer from https://dev.azure.com/coq/coq/_build/results?buildId=11089&view=artifacts&type=publishedArtifacts. Cf. the top of this thread for a list of usual things to check.
Tadeusz Litak (Jul 24 2020 at 15:20):Théo Zimmermann said:
The release candidate for 8.12.0 is
558e8ea. If some macOS users are around, it would be great if you could test the generated macOS installer from https://dev.azure.com/coq/coq/_build/results?buildId=11089&view=artifacts&type=publishedArtifacts. Cf. the top of this thread for a list of usual things to check.
Mojave 10.14.6 here. Almost all actions (open/modify/step/till end/save) seem to work. Query menu doesn't seem to do anything, but in earlier versions of Coq+CodIDE doesn't seem any better for me (never use CoqIDE, so I hardly ever test those things)
Enrico Tassi (Jul 24 2020 at 15:25):For the queries, you should select some text, like "nat" and then Query -> Print
Enrico Tassi (Jul 24 2020 at 15:26):Or hit f1 and there write Print nat
Enrico Tassi (Jul 24 2020 at 15:26):And thanks for testing!
Tadeusz Litak (Jul 24 2020 at 15:30):selecting "nat" Query -> Print does do the job. For F1, it clashes with brightness key on Mac keyboard :slight_smile: this is why I never got to use it, I guess (apart from using Aquamacs + PG in general). But after switching keys to standard function keys, it works perfectly fine.
Tadeusz Litak (Jul 24 2020 at 15:31):You're welcome! I didn't know that there is such a shortage of Mac testers.
Last updated: Oct 13 2024 at 01:02 UTC