Create custom snap installer

[LasseBlaauwbroek]

For a course, we would like to create a custom installer of the platform (with additional packages). For windows, creating a installer exe is well-documented. It is currently not clear to me how I would create a custom snap installer for linux/macos.

Is this a scenario that is/could/should be supported?

[MSoegtropIMC]

For snap the process of building snap is integrated into CI - it uses the github action "snapcore/action-build". So there don't exist offline scripts which do this, although it might not be complicated to create them. The script for creating the snap control yaml file is available in the paltform - just not the script to run snap itself. I am not a snap expert and have no idea if this is complicated once one has the snap control yaml file.

Anyway I guess the easiest ways to do this are:

• configure your fork of Coq Platform so that it runs github CI actions and enable CI runs for you modified branch (say add "lecture-*" under on: push: branches: in .github/workflows/snap.yml - possibly reduce the build matrix to what you really need. I am not sure how this is with Mac and Windows runners these days - I guess there are meanwhile free shared runners.
• Do a draft PR here for your modified platform (stating that this is just for building).

The advantage of these methods is that you get all installers (Mac, Windows, Snap) with a single git push. Note, though, that the Mac installers don't work at all without signing. If you need the signing scripts for Mac, please let me know.

If you need help, with method 1, I can prototype it on my fork and document it.

[LasseBlaauwbroek]

Thanks @MSoegtropIMC, I'll try this out and report back.

[MSoegtropIMC]

Please note that I just merged a snap related PR from @gares to main - you should base your work on this.

[LasseBlaauwbroek]

I need to create images based on Coq 8.14. Can I do that with the master branch?

[LasseBlaauwbroek]

Ah never mind, I see that I can just select the correct package pick. Apparently this has changed since I last created images last year :-)

[MSoegtropIMC]

Yes, @gares just reworked it. 8.14.1 is currently default for snap, btw.:

platform/.github/workflows/ubuntu.yml

Line 31 in 3beca37

default: 8.14~2022.01

[LasseBlaauwbroek]

@MSoegtropIMC I'm working on it now, and it seems to be going reasonably well (I've not yet managed to produce any artifacts, but probably soon). You say that you have a way to sign MacOS binaries? If so, I'm definitely interested.

[MSoegtropIMC]

@LasseBlaauwbroek : I can supply scripts which work locally on a Mac, but you would have to have your own signing key as Apple developer (and a Mac).

[LasseBlaauwbroek]

Ah, okay, I don't have a Mac, and I'm not in the developer program, so I guess we'll do without MacOS binaries for now. Thanks anyway.

[LasseBlaauwbroek]

I'm actually meeting quite a few problems in getting binaries for any of the platforms (most of them seem to be related to installation errors of packages, not coq-platform itself). I remember this being much easier a year ago, apparently the OCaml ecosystem has seen some regressions.

I've managed to hack together some binaries that are good enough for the purposes of our course, so my immediate need is satisfied. However, in the longer term, it would be nice if I could test my Tactician package with Coq platform. For this purpose, I've set up a fork here: https://github.com/coq-tactician/platform. Most of the tests are currently failing for one reason or another. Specifically for the Snap package, dose3 is inexplicably failing to compile even though it succeeds in the Ubuntu target (see here https://github.com/coq-tactician/platform/runs/5134182512?check_suite_focus=true). Currently I don't know how to debug this because the only method of creating a snap package that is provided is through Github actions. Just for the purposes of debugging alone, it would be nice if I could create a Snap package on my local machine.

[gares]

I did follow this: https://snapcraft.io/docs/snapcraft-overview and I do use multipass (lxc is too complex to set up).
Once you have snapcraft installed you run linux/crate_snapcraft_yaml.sh and then snapcraft build --debug .

[Zimmi48]

Note, though, that the Mac installers don't work at all without signing.

Is this really true? It used to be the case that you could still run an unsigned macOS application (by right-clicking and clicking Open, something that is anyway needed today on recent macOS versions because the application is not notarized).

[LasseBlaauwbroek]

Thanks @gares, I'll try this out. It may be useful to document this process in the platform readme.

[MSoegtropIMC]

Indeed I think we should have a script which just does it (including checking prerequisites).

[MSoegtropIMC]

Note, though, that the Mac installers don't work at all without signing.

Is this really true? It used to be the case that you could still run an unsigned macOS application (by right-clicking and clicking Open, something that is anyway needed today on recent macOS versions because the application is not notarized).

Yes, it is really true, at least for macOS BigSur+. You can still run non-notarized apps using the right click open thing, but you can't run unsigned apps.

[MSoegtropIMC]

@LasseBlaauwbroek : I just wanted to ask what the outcome of this was. Can you please summarize what from your point of view is missing?

[LasseBlaauwbroek]

The outcome of this was mostly negative, but as far as I can see not particularly because of the platform. I tried Enrico's suggestions (and followed some other snap tutorials) but I'm unable to create a local snap build as of now. My laptop actually crashes during the generation of the Coq package, but as far as I can tell this is because of some virtualization issue that has little to do with the platform. (Note that I'm also experiencing issues for the MacOS and Windows CI target, currently the only thing that works is the Ubuntu target; but again this seems to be mostly because of issues with upstream Opam packages and a baffling bug on Windows, nothing immediately related to the platform.) For now I've given up on creating a full platform build, but I'll no doubt get back to that someday.

Specifically the question of creating a custom snap package, I think it would be enough if @gares comments/suggestions in this thread on how to locally generate a snap package would be put in a README somewhere. Perhaps together with some useful links to the snapcraft documentation/tutorials.

Apart from the documentation issue, I think this can be closed.

[LasseBlaauwbroek]

If you are interested in the CI failures, see below. Any suggestions on how to resolve any of it would be appreciated: https://github.com/coq-tactician/platform/actions

[MSoegtropIMC]

So "https://github.com/coq-tactician/platform" is a clone of Coq Platform 2022.01 and you just changed the pick files and the picks to build in the github action files? Are there other changes? This should be fairly easy to do provided the pick files themselves work.

[LasseBlaauwbroek]

I Indeed added some custom picks and enabled them in the CI.
But I also upgraded OCaml to 4.12 to make MacOS happy due to ocaml-opam/ocaml-mccs#33. Additionally I removed the use of the mingw repo for Windows (not sure exactly why anymore).

For Windows and Snap, upstream packages are still failing, which does not seem to have anything to do with Coq Platform.
For MacOS I'm getting lots of errors like

##### Copy system shared libraries #####
Copying shared libraries for _dmg/Coq_Platform_2022.01.0.app/Contents/Resources/bin/coqtacticworker.opt ...
Some of the paths in the dependency tree could not be resolved
Maybe you already bundled coqtacticworker.opt?
Could not resolve /usr/lib/libSystem.B.dylib
Could not resolve /usr/lib/libSystem.B.dylib

My best guess is that this is due to my Coq packages overwriting the standard library. But I've not investigated this further yet.

[MSoegtropIMC]

The Windows build will definitely fail if you remove the MinGW repo.

Let me take one of your pick files and build them locally and see what happens. If the picks build locally, they should also build in CI.

The Mac library issues shouldn't have anything to do with overwriting standard library files.

I will have a look after the 2022.03 release, since this has nothing to do with the release.

[LasseBlaauwbroek]

Yeah, the removal of the MinGW repo may have been a mistake (but it was also not working before the removal).

Note that my pick files do not build locally for me either. There are just a bunch of upstream problems that I've been unable to resolve on any platform apart from Linux (it used to work last year which is very annoying; there have been several regressions in the OCaml ecosystem).

Note that I don't expect you to resolve any of that, most of these issues seem to be outside of the platform. (But if you want to take a look that would of course still be appreciated.) The only bug that might be directly related to the platform are the MacOS errors.

[MSoegtropIMC]

I can definitely have a look.

The MacOS issue might be related to this change in macOS:

https://developer.apple.com/documentation/macos-release-notes/macos-big-sur-11_0_1-release-notes

Search for "dynamic linker cache".

But the Platform shared library copier should be able to detect that this is a system library and need not be copied to the installer (it tries to copy libraries from MacPorts or HomeBrew). I will see.