[do not merge] math-comp-school-2022

[gares]

https://mathcomp-schools.gitlabpages.inria.fr/2022-12-school/

TODO:

• mczify
• algebra-tactics

[MSoegtropIMC]

@gares : FYI: the macOS build is currently broken (since an update of macOS on the Github runners) - In case you did this PR to create installers I would have to do something to fix it (it is tricky, I need a machine with the specific OS).

[gares]

Thanks for the heads up. Well, yes, a dmg would help. The school starts on the 5/12. In any case I have a jscoq setup, so I hope it won't be necessary, but I'm not 100% sure yet.

[MSoegtropIMC]

OK - I likely have some time on Friday to fix it.

[gares]

@MSoegtropIMC do you have any hints? I do have a spare mac here, I can investigate a little myself.

[MSoegtropIMC]

@gares : it will likely be tricky to fix (that's the reason it is setting broken since 2 weeks). We use a python based tool called macpack to analyse the shared library dependencies of executables and to patch the executables such that they search the shared libraries under a new (relative) path). This tool broke with an update of macOS on the GitHub runners.

[MSoegtropIMC]

I already prepared a mac with the exact same macOS version github is using, but didn't have time to look into it after that.

[gares]

@MSoegtropIMC I did found the problem, see the last commit. The script is not calling the right macpack!
It calls a mono binary instead:

/Library/Frameworks/Mono.framework/Versions/Current/Commands/macpack

I tried to call the python one but I failed, on my PC this is where pip installs binaries, but I guess it is not the same on OSX:

macos/create_installer_macos.sh: line 153: .local/bin/macpack: No such file or directory

If you can just tell me where the python script is, I think I can fix the installer here.

[MSoegtropIMC]

@gares : great!

The path also depends on the MacPorts vs Homebrew question. The machine I have here is MacPorts. There it is:

$HOME/Library/Python/3.10/bin/macpack

It might be different on Homebrew. It will also depend on the python version ...

It might be wise to run

pip3 show --files macpack

und use awk (or whatever) to get the install path. The output is:

Name: macpack
Version: 1.0.3
Summary: Makes a macOS binary redistributable by searching the dependency tree and copying/patching non-system libraries.
Home-page: https://github.com/chearon/macpack
Author: Caleb Hearon
Author-email: caleb@chearon.net
License: UNKNOWN
Location: /Users/msoegtrop/Library/Python/3.10/lib/python/site-packages
Requires: 
Required-by: 
Files:
  ../../../bin/macpack
  macpack-1.0.3.dist-info/DESCRIPTION.rst
  macpack-1.0.3.dist-info/INSTALLER
  macpack-1.0.3.dist-info/METADATA
  macpack-1.0.3.dist-info/RECORD
  macpack-1.0.3.dist-info/REQUESTED
  macpack-1.0.3.dist-info/WHEEL
  macpack-1.0.3.dist-info/entry_points.txt
  macpack-1.0.3.dist-info/metadata.json
  macpack-1.0.3.dist-info/top_level.txt
  macpack/__init__.py
  macpack/__pycache__/__init__.cpython-310.pyc
  macpack/__pycache__/dependency.cpython-310.pyc
  macpack/__pycache__/patcher.cpython-310.pyc
  macpack/dependency.py
  macpack/patcher.py
  tmp/__init__.py
  tmp/__pycache__/__init__.cpython-310.pyc
  tmp/__pycache__/patcher.cpython-310.pyc
  tmp/patcher.py

One has to combine the path after Location: and the path of bin/macpack.

[MSoegtropIMC]

P.S.: Using Pip together with package managers can be quite contrived. MacPorts also has many usually pip installed packages as MacPorts packages, und this is the preferred method. Packages really installed with pip are installed outside of the MacPorts realm to make sure the MacPorts installation is not messed up by pip.

[MSoegtropIMC]

@gares: somehow all my comments got lost because I commented on commits which got deleted.

A short summary:

• On Mac you have usually several pythons - the system supplied one and a Homwbrew / macPorts supplied one.
• The library path in the git logs looks like the python you call is the system python.
• On my mac there is a system supplied python3 and pip3 but no system supplied python
• The yaml file installs macpack with pip3
• A Homebrew supplied python (the yaml file installs one - probably useless) is usually not in the path - it is intended mostly for homebrews internal use
• The python3 depext opam packages likely do something so that a Homebrew installed python3 is accessible, so things might change after the opam environment is active

In summary: you might want to check which pip3 and python3 is in the path when macpack is installed - best do this in the yaml file where macpack is installed.

[gares]

I pushed one last attempt using pip3 show, but if it does not work I'll give up, you seem to know better how to continue the patch. How do developers manage to survive on this OS is still a mistery to me ;-)

[MSoegtropIMC]

OK, I can take it from here. It is a big help to know the root cause (using the wrog macpack). I will do this in a separate PR on master.

Regarding living on macOS: I am using MacPorts and reasonably happy with it. But since HomeBrew is preinstalled on the GitHub runners and many people use it, CI uses HomeBrew.

The real mess indeed is that the system doesn't come with a package manager for such things so that two independent systems came to existence, and we need to support both. On the other hand the Python supplied with macOS should be fine since a few years.

[gares]

last run failed because I was too naïve concatenating the strings I guess. Good luck!

[MSoegtropIMC]

I did a PR: #311. It did work locally in a very similar environment.

[MSoegtropIMC]

@gares : Two notes:

• when you are finished, some feedback on the use of Coq Platform for creating custom installers would be nice, e.g. the documentation on this.
• I wonder if we should have a "show more" entry in the package list selection and actually add such special package lists to main. The rationale is that maybe lectures are recorded and people might want to follow it even a few years later. The original installers might not work then any more (think of the Ubuntu OCaml incompatibility issue), but compiling from sources should. I would put them in a separate sub folder of the package lists folder.

[gares]

I skimmed the doc and I did not take notes, sorry for that.
IIRC the part about tuning the package selection was OK.
The I believe it focuses more on building the thing on your machine rather than just opening a PR (and removing unnecessary jobs).

It was very easy, but I'm not the best "tester" since I already know too much on the infrastructure I'm afraid.

[gares]

OK, I've the installers.

I did test the snap, and CoqIDE has no icons. Tons of

(coqide:439770): Gtk-WARNING **: 18:36:48.853: Error loading theme icon 'document-save' for stock: Icon 'document-save' not present in theme Adwaita

Is it a known issue?

[MSoegtropIMC]

You mean no icons in the Mac installer?

[MSoegtropIMC]

Ah sorry, you wrote snap ...

[MSoegtropIMC]

It did work last time I looked into it.

[gares]

OK, so I'll debug it myself, it's probably just a missing package in the image.

[gares]

@MSoegtropIMC On my PC icons are missing (even with the official snap). Setting GTK debug:

loading theme icon 'window-close' for stock: Icon 'window-close' not present in theme Adwaita
Gtk-Message: 17:15:28.494: looking up icon image-missing for scale 1
Gtk-Message: 17:15:28.496: looking up icon window-close for scale 1
Gtk-Message: 17:15:28.496: 	lookup name: window-close
Gtk-Message: 17:15:28.496: look up icon dir /snap/coq-prover/30/data-dir/icons/Adwaita/8x8/emblems
Gtk-Message: 17:15:28.496: get icon suffix: 0
Gtk-Message: 17:15:28.496: look up icon dir /snap/coq-prover/30/gnome-platform/usr/share/icons/Adwaita/8x8/emblems
Gtk-Message: 17:15:28.496: get icon suffix: 0
Gtk-Message: 17:15:28.496: look up icon dir /snap/coq-prover/30/gnome-platform/usr/share/icons/Adwaita/16x16/actions
Gtk-Message: 17:15:28.496: get icon suffix: 0
Gtk-Message: 17:15:28.496: look up icon dir /snap/coq-prover/30/gnome-platform/usr/share/icons/Adwaita/16x16/apps
Gtk-Message: 17:15:28.496: get icon suffix: 0
Gtk-Message: 17:15:28.496: look up icon dir /snap/coq-prover/30/data-dir/icons/Adwaita/16x16/devices
Gtk-Message: 17:15:28.496: get icon suffix: 0
Gtk-Message: 17:15:28.496: look up icon dir /snap/coq-prover/30/gnome-platform/usr/share/icons/Adwaita/16x16/devices
Gtk-Message: 17:15:28.496: get icon suffix: 0
Gtk-Message: 17:15:28.496: look up icon dir /snap/coq-prover/30/data-dir/icons/Adwaita/16x16/emblems
Gtk-Message: 17:15:28.496: get icon suffix: 0
Gtk-Message: 17:15:28.496: look up icon dir /snap/coq-prover/30/gnome-platform/usr/share/icons/Adwaita/16x16/emblems
Gtk-Message: 17:15:28.497: get icon suffix: 0
Gtk-Message: 17:15:28.497: look up icon dir /snap/coq-prover/30/gnome-platform/usr/share/icons/Adwaita/16x16/emotes
Gtk-Message: 17:15:28.497: get icon suffix: 0
Gtk-Message: 17:15:28.497: look up icon dir /snap/coq-prover/30/data-dir/icons/Adwaita/16x16/mimetypes
Gtk-Message: 17:15:28.497: get icon suffix: 0
Gtk-Message: 17:15:28.497: look up icon dir /snap/coq-prover/30/gnome-platform/usr/share/icons/Adwaita/16x16/mimetypes
Gtk-Message: 17:15:28.497: get icon suffix: 0
Gtk-Message: 17:15:28.497: look up icon dir /snap/coq-prover/30/data-dir/icons/Adwaita/16x16/places
Gtk-Message: 17:15:28.497: get icon suffix: 0
Gtk-Message: 17:15:28.497: look up icon dir /snap/coq-prover/30/data-dir/icons/Adwaita/16x16/status
Gtk-Message: 17:15:28.497: get icon suffix: 0
Gtk-Message: 17:15:28.497: look up icon dir /snap/coq-prover/30/gnome-platform/usr/share/icons/Adwaita/16x16/status
Gtk-Message: 17:15:28.497: get icon suffix: 0
Gtk-Message: 17:15:28.497: look up icon dir /snap/coq-prover/30/data-dir/icons/Adwaita/22x22/devices
Gtk-Message: 17:15:28.497: get icon suffix: 0
Gtk-Message: 17:15:28.497: look up icon dir /snap/coq-prover/30/gnome-platform/usr/share/icons/Adwaita/22x22/devices
Gtk-Message: 17:15:28.497: get icon suffix: 0
Gtk-Message: 17:15:28.497: look up icon dir /snap/coq-prover/30/data-dir/icons/Adwaita/22x22/emblems
Gtk-Message: 17:15:28.497: get icon suffix: 0
Gtk-Message: 17:15:28.497: look up icon dir /snap/coq-prover/30/gnome-platform/usr/share/icons/Adwaita/22x22/emblems
Gtk-Message: 17:15:28.497: get icon suffix: 0
Gtk-Message: 17:15:28.497: look up icon dir /snap/coq-prover/30/data-dir/icons/Adwaita/22x22/mimetypes
Gtk-Message: 17:15:28.497: get icon suffix: 0
Gtk-Message: 17:15:28.497: look up icon dir /snap/coq-prover/30/gnome-platform/usr/share/icons/Adwaita/22x22/mimetypes
Gtk-Message: 17:15:28.497: get icon suffix: 0
Gtk-Message: 17:15:28.497: look up icon dir /snap/coq-prover/30/data-dir/icons/Adwaita/22x22/places
Gtk-Message: 17:15:28.497: get icon suffix: 0
Gtk-Message: 17:15:28.497: look up icon dir /snap/coq-prover/30/data-dir/icons/Adwaita/22x22/status
Gtk-Message: 17:15:28.497: get icon suffix: 0
...

The icons are in theory "superposed" because of the gnome "extension" but apparently are not found. Are we fiddling with GTK data pats?

[gares]

@MSoegtropIMC last commit fixes the issue, at least locally. Let's see the package built by CI...

[MSoegtropIMC]

@gares : thanks! Please also do a PR vs. main.