Stream: Coq users

Topic: Testing the macOS installer


view this post on Zulip 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):

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 08 2020 at 15:10):

Thanks a lot for testing Hugo, what's your OSX version @Hugo Herbelin

view this post on Zulip Hugo Herbelin (Jun 08 2020 at 15:40):

10.11.1

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Théo Zimmermann (Jun 09 2020 at 09:55):

Oh actually, this variable was not added very recently (coq/coq#10186).

view this post on Zulip Théo Zimmermann (Jun 09 2020 at 09:55):

But still, I'm puzzled by this.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2020 at 12:49):

lablgtk versions are the same right?

view this post on Zulip 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'

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2020 at 12:57):

Bizarre :S

view this post on Zulip Théo Zimmermann (Jun 09 2020 at 12:57):

Homebrew is pinned. The macOS image is fixed.

view this post on Zulip Théo Zimmermann (Jun 09 2020 at 12:58):

The OCaml and findlib versions are pinned but not the version of lablgtk!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2020 at 13:35):

But yeah, we need someone else to try the package

view this post on Zulip 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".

view this post on Zulip Anton Trunov (Jun 09 2020 at 13:48):

macOS complained about missing signature before opening CoqIDE, though.

view this post on Zulip Théo Zimmermann (Jun 09 2020 at 13:49):

Yeah, that's normal.

view this post on Zulip 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).

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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+.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jun 12 2020 at 07:03):

So since then something else must have changed to make it break again.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Enrico Tassi (Jul 24 2020 at 15:25):

For the queries, you should select some text, like "nat" and then Query -> Print

view this post on Zulip Enrico Tassi (Jul 24 2020 at 15:26):

Or hit f1 and there write Print nat

view this post on Zulip Enrico Tassi (Jul 24 2020 at 15:26):

And thanks for testing!

view this post on Zulip 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.

view this post on Zulip 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: Feb 01 2023 at 13:03 UTC