Stream: Coq Platform devs & users

Topic: 2021.02 fix release


view this post on Zulip Michael Soegtrop (Aug 25 2021 at 16:19):

Since a few days the Windows build is broken cause Cygwin removed the old binutils package I used for patching the broken current package, but now they have a new one which appears to work. I also need to look into Ubuntu failures.

Is there anything else known which needs fixing in 2021.02?

view this post on Zulip Emilio Jesús Gallego Arias (Aug 25 2021 at 16:53):

I dunno what needs to be done, but I'd be great if the package problem could be fixed quickly as it is making Coq's CI fail [and I understand that's a super easy fix]

view this post on Zulip Michael Soegtrop (Aug 25 2021 at 17:17):

I was super busy the last weeks and I am not up to date. What is the package problem?

view this post on Zulip Enrico Tassi (Aug 25 2021 at 17:22):

About the (platform/Coq) release I think we should really chat at the next Coq call, if @Guillaume Melquiond is available, so that we can set up a plan.

view this post on Zulip Michael Soegtrop (Aug 25 2021 at 18:02):

When is it ? The Wiki says "after the summer holidays" ...

view this post on Zulip Matthieu Sozeau (Aug 26 2021 at 12:48):

I guess we should resume next week (sept 1st)

view this post on Zulip Michael Soegtrop (Aug 26 2021 at 14:54):

@Emilio Jesús Gallego Arias : I am working on fixing the Coq Platform CI issues (there was a very recent Windows issue which is fixed and a then it doesn't seem to work on Ubuntu 20 (the CI machines recently switched) - some basic OCaml issue. I still don't know what the "packaging" issue is you mentioned - can you please clarify / point me to relevant CI logs?

view this post on Zulip Michael Soegtrop (Aug 26 2021 at 17:50):

Just wanted to state the Coq Platform has issues with opam 2.1.0 - this is the reason it fails on Ubuntu in CI. On Windows we use a special MinGW version which is older. Nut sure why the Mac CI doesn't use opam 2.1.0 though need to check. The incompatibility is depext, which has been integrated into 2.1.0.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 26 2021 at 17:54):

The problem in Coq's CI is the missing package, see any CI log such as https://gitlab.com/coq/coq/-/jobs/1538227382

view this post on Zulip Michael Soegtrop (Aug 27 2021 at 09:24):

@Emilio Jesús Gallego Arias : ah ok, that is fixed in the Coq Platform 2021.02 branch (https://github.com/coq/platform/pull/123).

view this post on Zulip Emilio Jesús Gallego Arias (Aug 27 2021 at 09:55):

Does this mean that Coq's CI is fixed too?

view this post on Zulip Michael Soegtrop (Aug 27 2021 at 13:05):

As far as I can see yes - I didn't see CI failing for this reason in the last 24 hours.

view this post on Zulip Guillaume Melquiond (Aug 30 2021 at 09:28):

I am back from vacations and, if there is a Coq call Wednesday, I should be able to attend. (Assuming I have no surprise meeting scheduled hidden in the humongous stack of emails I have yet to sift through.)

view this post on Zulip Emilio Jesús Gallego Arias (Aug 30 2021 at 18:09):

Michael Soegtrop said:

As far as I can see yes - I didn't see CI failing for this reason in the last 24 hours.

@Michael Soegtrop see for example https://github.com/coq/coq/pull/14515/checks?check_run_id=3464879153

view this post on Zulip Emilio Jesús Gallego Arias (Aug 30 2021 at 18:09):

CI seems to be still failing all over the place

view this post on Zulip Emilio Jesús Gallego Arias (Aug 30 2021 at 18:18):

Indeed, not a single job succeeded

view this post on Zulip Emilio Jesús Gallego Arias (Aug 30 2021 at 21:33):

@Michael Soegtrop I had a look and it turns out that what we test in Coq's CI is a branch called dev-ci , I'm unsure what the idea is here, but that branch has diverged significantly from the main one in the platform scripts @Enrico Tassi

view this post on Zulip Enrico Tassi (Aug 31 2021 at 07:17):

Hum, yes the branching scheme is changing, I don't know if the new model (monobranch) is in place yet or not.

view this post on Zulip Michael Soegtrop (Aug 31 2021 at 10:01):

@Emilio Jesús Gallego Arias : ah yes, I forgot. The usual Coq Platform branch builds specific pics of everything - this is not very useful for Coq's CI. So there is an extra branch which builds the opam dev packages of everything.

Since it is a bit of a pain to maintain both, I am working on a new Coq Platform branch which supports different versions of Coq, inlcuding the dev-ci version. This will come within a few days (currently busy with doing fixes caused by changes in opam).

I guess it should be quick to cherry pick the Cygwin fixes in the dev-ci branch for the time beeing.

view this post on Zulip Michael Soegtrop (Aug 31 2021 at 12:08):

@Emilio Jesús Gallego Arias : I cherry picked the 3 relevant commits from 2021.02 to dev-ci. This should work now (Coq Platform CI on this is still running, so I don't know).

With the "multi-version" branch this should be better - the main issue we have in Coq Platform is that we can't run (easily) daily CI on several branches, so dev-ci is untested on Coq Platform side. With the multi-version branch, we can regularly test the dev variant as well.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2021 at 12:15):

Thanks! I'm gonna update the Coq's CI branch too and see how it goes

view this post on Zulip Michael Soegtrop (Aug 31 2021 at 12:22):

Just to make sure: the "multi-version" branch is not yet released, but should come soon.

view this post on Zulip Michael Soegtrop (Aug 31 2021 at 12:28):

@Théo Zimmermann @Enrico Tassi I fixed 2021.02 so that it works with recent cygwin and recent opam. I don't see other things to fix, so I plan to tag and publish this is 2021.02.3.

2021.09 I plan to do based on the multi-version branch - I think it would be OK then to just add 8.14 as variant to 2021.09, since this wouldn't touch any of the existing versions. In the 8.13 variant I would update all packages to the latest ones which work with 8.13 (e.g. update VST).

I am unsure what to do with the 8.12 and earlier variants. Should the package versions be frozen to whatever it was back then, or should we also try to update them to the latest which works on 8.12 ...? Or should we have both, say 8.12-original and 8.12-updated?

view this post on Zulip Michael Soegtrop (Aug 31 2021 at 12:29):

The same would then of cause apply to 8.13 as well, although for 8.13 the situation is slightly different since 8.14 is not yet there, so 8.13 is still the latest Coq.

view this post on Zulip Michael Soegtrop (Aug 31 2021 at 13:45):

@Emilio Jesús Gallego Arias : the dev-ci Windows builds pass now except coq-interval.dev which I guess is somehow normal with the move to Flocq 4. Please let me know if I shall remove it or if you patch the version (the dev-ci branch as special mechanisms to pin package versions from the command line). The Ubuntu build probably needs some updates on the CI script side.

view this post on Zulip Michael Soegtrop (Aug 31 2021 at 13:46):

Regarding the "updated picks in the multi-variant" question: I guess the answer is that 8.13 will come with two picks, one from 2021.02 and one from 2021.09. All other versions have only one pick, because there was only one official platform release for them.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2021 at 14:00):

@Michael Soegtrop my own build failed with https://github.com/coq/coq/pull/12425/checks?check_run_id=3472736478#step:4:1630

Error:  The sources of the following couldn't be obtained, aborting:
          - coq.dev
          - coqide.dev

The regular runner succeeded tho https://gitlab.com/coq/coq/-/jobs/1549277449 , so it seems that coq-interval.dev somehow is not affected or tested in Coq's Ci.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2021 at 14:00):

Gonna have a look thanks

view this post on Zulip Michael Soegtrop (Aug 31 2021 at 17:43):

@Emilio Jesús Gallego Arias : I somehow can't find the error text you pasted in the first log you linked ...

Regarding the succeeding build: this has -extent=i (=IDE, see platform-windows.bat ) which means it only builds Coq and CoqIDE. In Coq Platform CI I test -extent=f(=FULL) which builds a lot more.

It makes sense to test only Coq and CoqIDE in the Coq Platform Windows build of Coq CI, since one can expect that other packages don't depend that much on the OS.

In the Coq Platform Dev CI it makes sense to test everything, so that we are warned in advance if stuff breaks.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2021 at 18:38):

I understood everything and made things work I think, thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2021 at 18:39):

Still, the CI run is a bit heavy, I will open some issues discussing caching and mention you on the relevant ones, thanks!

view this post on Zulip Michael Soegtrop (Sep 02 2021 at 08:42):

@Théo Zimmermann, @Enrico Tassi, @Jim Fehrle : I am about to make a patch release of 2021.02 from the current 2021.02 branch - it fixes the issues with Cygwin binutils and with the integration of depext in opam 2.1.0 (it is still compatible with older opam). Since I am mostly testing on Mac these days, it would be great if someone with Linux or Windows background also has a look (of cause I test there as well + CI, but not as much as on Mac).

view this post on Zulip Enrico Tassi (Sep 02 2021 at 12:02):

I can test the snap. I've just started a workflow https://github.com/coq/platform/actions/runs/1194069552 which will produce a snap of the current 2021.02 branch

view this post on Zulip Michael Soegtrop (Sep 02 2021 at 13:04):

@Enrico Tassi : great, this would help. I test the plain script on the major platforms.

Btw.: Is gappa disabled in snap for some reason?

view this post on Zulip Enrico Tassi (Sep 02 2021 at 13:08):

I don't know how gappa works

view this post on Zulip Enrico Tassi (Sep 02 2021 at 13:09):

do you mean: is gappa available via coq-prover.gappa ?

view this post on Zulip Enrico Tassi (Sep 02 2021 at 13:09):

if so, no but we can add it.

view this post on Zulip Enrico Tassi (Sep 02 2021 at 13:25):

The snap seems to work fine and the few fixes are there (eg the .desktop entry starts coqide correctly)

view this post on Zulip Michael Soegtrop (Sep 02 2021 at 13:43):

There is a test file in the smoke test kit, assuming gappa is installed (there is a Coq plugin calling the gappa executable).
I had the impression that it is explicitly excluded in snap because there was a bug that Coq didn't compile if gappa was not included because Coq now requires GMP, which gappa also happens to install, but Coq not. So no gappa, no Coq. I fixed this meanwhile. In the older version the prerequisites of gappa have always been installed regardless if gappa was requested or not, so that this did hide the missing dependency of Coq. (btw.: this is mostly about unattended installations - for attended installations opam would ask the user, but in CI there is nobody to answer, so Coq Platform does the things where opam might ask questions upfront with "unsafe-yes").

view this post on Zulip Michael Soegtrop (Sep 02 2021 at 13:44):

I don't think a shortcut link to the gappa executable is required as long as the plugin works, but @Guillaume Melquiond might have a different opinion on that.

view this post on Zulip Guillaume Melquiond (Sep 02 2021 at 13:48):

No, that seems fine. As for the plugin, as long as gappa is in the PATH, it should work fine. (Does Snap adjust it so that binaries are visible from other binaries?)

view this post on Zulip Enrico Tassi (Sep 02 2021 at 14:40):

problem: gappa is not there, stripped out by the usual cleanup line (recall clightgen). I'll fix that.

view this post on Zulip Enrico Tassi (Sep 02 2021 at 14:50):

https://github.com/coq/platform/pull/127
but it will take me more time to test it.

view this post on Zulip Michael Soegtrop (Sep 02 2021 at 15:21):

We are not in a hurry, but we should get things ready and well tested before the autumns semester starts anywhere in the world.

view this post on Zulip Théo Zimmermann (Sep 02 2021 at 15:28):

The Fall semester is already well started in many US universities I believe...

view this post on Zulip Enrico Tassi (Sep 02 2021 at 16:21):

By chance I also found another bug in the snap, which requires a little patch which I'm testing. The home plug does not let one read (nor write) hidden files and Coq create a .x.aux file next to each x.vo. I don't know if things changed recently (I had to remove the old snap), or if I tested things the wrong way (e.g. granting extra rights to the snap locally). Anyway, this may require a silly patch on 8.14 as well, since we don't protect open_out with a try-with in aux_file.ml.

view this post on Zulip Enrico Tassi (Sep 03 2021 at 14:49):

OK, I managed to run the smoke test (which includes gappa tests) on the snap from this branch: https://github.com/coq/platform/pull/127
but each invocation of coqc prints:

Warning: Cannot open directory /usr/games/. [cannot-open-dir,filesystem]
Warning: Cannot open directory /bin/. [cannot-open-dir,filesystem]
Warning: Cannot open directory /sbin/. [cannot-open-dir,filesystem]
Warning: Cannot open directory /usr/sbin/. [cannot-open-dir,filesystem]

Any ideas why coqc would look there? Otherwise I'll dig myself

view this post on Zulip Guillaume Melquiond (Sep 03 2021 at 14:50):

Could it be that they are in $PATH but do not exist?

view this post on Zulip Guillaume Melquiond (Sep 03 2021 at 14:54):

if System.is_in_system_path "csdp" then lazy () else lazy (raise CsdpNotFound)

view this post on Zulip Enrico Tassi (Sep 03 2021 at 16:05):

thanks, I think I found the culprit, but I'll need to rebuild the snap to really test it

view this post on Zulip Enrico Tassi (Sep 03 2021 at 20:20):

So apparently snap sets a PATH which contains /usr/games which does not exists on my system. Hence the warnings. While I add COQBIN I could also remove non existing entries... or I could patch coq to not complain about bogus PATH...

view this post on Zulip Enrico Tassi (Sep 03 2021 at 20:22):

Coq platform PR 127 makes the snap pass the smoke test. I should add a CI step testing this, but it is not super easy either (since the build is inside a container). Locally I had to download the one built on OSX and run the snap on it....

view this post on Zulip Paolo Giarrusso (Sep 04 2021 at 13:29):

or I could patch coq to not complain about bogus PATH...

Assuming say bash accepts bogus PATH entries, that'd be a (low-priority) bugfix in Coq... Does Coq even need an execvp reimplementation?

view this post on Zulip Jim Fehrle (Sep 05 2021 at 04:07):

Michael Soegtrop said:

Théo Zimmermann, Enrico Tassi, Jim Fehrle : I am about to make a patch release of 2021.02 from the current 2021.02 branch - it fixes the issues with Cygwin binutils and with the integration of depext in opam 2.1.0 (it is still compatible with older opam). Since I am mostly testing on Mac these days, it would be great if someone with Linux or Windows background also has a look (of cause I test there as well + CI, but not as much as on Mac).

What exactly needs to be tested on windows? As you probably saw, I've had problem building on windows Lawley.

view this post on Zulip Jim Fehrle (Sep 05 2021 at 04:09):

I meant Lately...

view this post on Zulip Michael Soegtrop (Sep 05 2021 at 13:09):

@Jim Fehrle : download the Coq platform from (https://github.com/coq/platform) - branch 2021.02 is default - and run coq_platform_make_windows.bat and follow the instructions. If this doesn't work, it is a bug and we should investigate it asap (probably best with a screen sharing session).

view this post on Zulip Michael Soegtrop (Sep 06 2021 at 09:27):

@Enrico Tassi, @Jim Fehrle : how are things going? I wanted to release the update soon.

view this post on Zulip Enrico Tassi (Sep 06 2021 at 09:42):

https://github.com/coq/platform/pull/127 makes gappa work, but you still have the warnings because of the confinement mode. In particular the cleanup code for the path is not helping. snap is putting in the path stuff like /usr/games, but from the snap I can't ls that directory nor run any file in it. Similarly /bin is there, and I can run ls (from there) but I can't ls /bin. So I'm afraid the only way out is to comment out the warning in Coq.

view this post on Zulip Michael Soegtrop (Sep 06 2021 at 09:53):

@Enrico Tassi : since it has been like this before and it is not a serious / blocking issue, I would say we simply go for it. So we merge pull 127 and I release (after some final tests)?

view this post on Zulip Michael Soegtrop (Sep 06 2021 at 09:54):

I also want to make progress with 2021.09, but I wanted to wait for 2021.02, so that I can merge over all fixes in one coordinated action.

view this post on Zulip Enrico Tassi (Sep 06 2021 at 10:08):

let this CI round finish, so that I can try the snap on the last commit. The I agree, this issue is not blocking.

view this post on Zulip Enrico Tassi (Sep 06 2021 at 10:54):

OK, I've tested the snap and it works OK for me

view this post on Zulip Enrico Tassi (Sep 06 2021 at 10:54):

I'm not very happy with the second patch, since it simply disable the warning

view this post on Zulip Enrico Tassi (Sep 06 2021 at 10:55):

I don't know if opam patches can be made "optional" and be applied only in the snap

view this post on Zulip Enrico Tassi (Sep 06 2021 at 10:55):

probably yes but I did not try

view this post on Zulip Michael Soegtrop (Sep 06 2021 at 12:24):

Yes, you can apply to everything in opam the same conditional syntax - essentially everything are lists of strings with optional conditions after each string.

view this post on Zulip Michael Soegtrop (Sep 06 2021 at 12:24):

Shall I have a look?

view this post on Zulip Enrico Tassi (Sep 06 2021 at 12:40):

yes please, the two patches I add are just for the snap

view this post on Zulip Michael Soegtrop (Sep 06 2021 at 12:57):

Hmm - thinking about it there is one catch: how would I detect with opam rules that I am building snap ...

view this post on Zulip Michael Soegtrop (Sep 06 2021 at 12:57):

It is not an OS distribution like Ubuntu or Windows.

view this post on Zulip Enrico Tassi (Sep 06 2021 at 13:18):

right. maybe we can do, as part of the snap build process, opam var --global snap=true and then use patches: [ "foo.patch" {snap} ] as a filter in the opam file

view this post on Zulip Enrico Tassi (Sep 06 2021 at 13:19):

see https://opam.ocaml.org/doc/Manual.html#Filters , but I have not tried

view this post on Zulip Enrico Tassi (Sep 06 2021 at 13:22):

here it is https://snapcraft.io/docs/parts-environment-variables, the platform script could set that opam variable whenever SNAPCRAFT_PROJECT_NAME is set

view this post on Zulip Enrico Tassi (Sep 06 2021 at 13:23):

I'll give it a try

view this post on Zulip Enrico Tassi (Sep 06 2021 at 13:27):

ok, I did push a commit. let's see from the log if the patches are only applied when building the snap.

view this post on Zulip Enrico Tassi (Sep 06 2021 at 15:07):

ok, it seems to work. the snap has the (now optional) patches applied.

view this post on Zulip Michael Soegtrop (Sep 06 2021 at 16:04):

Fine, so shall I merge?

view this post on Zulip Jim Fehrle (Sep 06 2021 at 16:47):

Michael Soegtrop said:

Enrico Tassi, Jim Fehrle : how are things going? I wanted to release the update soon.

I haven't gotten to try it--just got back from vacation late Saturday night and this is a major 3 day holiday weekend here in the States (Labor Day). But I'll try it soon.

view this post on Zulip Jim Fehrle (Sep 06 2021 at 18:16):

Not working at all for me:

  1. I don't see any recent update to the 2021.02 branch:
$ git remote -v
origin  https://github.com/jfehrle/platform.git (fetch)
origin  https://github.com/jfehrle/platform.git (push)
upstream        https://github.com/coq/platform.git (fetch)
upstream        https://github.com/coq/platform.git (push)
$ git branch
* 2021.02
  8.14+debugger-preview
  stale_cygwin
$ git fetch
$ git pull
Already up to date.
$ git log
commit 464e1a83005ddc73e53caca382a2a5d026f785fa (HEAD -> 2021.02, origin/HEAD, origin/2021.02)
Merge: 036b901 c78c01e
Author: Théo Zimmermann <theo.zimmermann@inria.fr>
Date:   Wed Aug 11 10:31:35 2021 +0200

    Merge pull request #119 from pedroqueiroga/fix-ininstall-typo

    Fixes typo in `shell_scripts/install_opam.sh`
  1. When I try it anyway, the .bat file fails with:
--2021-09-06 10:42:56--  http://mirrors.kernel.org/sourceware/cygwin/x86_64/release/mingw64-x86_64-binutils/mingw64-x86_64-binutils-2.35.1-1.tar.xz
Resolving mirrors.kernel.org (mirrors.kernel.org)... 2001:19d0:306:6:0:1994:3:14, 198.145.21.9
Connecting to mirrors.kernel.org (mirrors.kernel.org)|2001:19d0:306:6:0:1994:3:14|:80... connected.
HTTP request sent, awaiting response... 404 Not Found
2021-09-06 10:42:56 ERROR 404: Not Found.

ERROR coq_platform_make_windows.bat failed
  1. The install process is a bit circular: I need git to pull the platform, while I normally get git by installing cygwin. Then the .bat file installs/updates cygwin. (And after the first few failures, I've tended to install a fresh cygwin each time.) This makes me uneasy.

I'm still quite tired from my vacation (290 miles of cycling), so maybe I'm not doing the right thing.

view this post on Zulip Théo Zimmermann (Sep 06 2021 at 18:26):

@Jim Fehrle You should probably run git branch --set-upstream-to=upstream/2021.02 before pulling in your 2021.02 branch. BTW, to avoid the circularity, you can also download the tarball from the branch. This should also work in principle.

view this post on Zulip Jim Fehrle (Sep 06 2021 at 18:41):

(deleted)

view this post on Zulip Michael Soegtrop (Sep 06 2021 at 20:39):

@Jim Fehrle : does it work now?

view this post on Zulip Jim Fehrle (Sep 07 2021 at 02:12):

I was able to build/install the full platform for 2021.02 and run coqide. ("n" for the CompCert option). Is this likely to build if I point to the Coq 8.14+alpha branch?

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 07:38):

Jim Fehrle said:

I was able to build/install the full platform for 2021.02 and run coqide. ("n" for the CompCert option). Is this likely to build if I point to the Coq 8.14+alpha branch?

From past experience, I would say no. But I anyway plan to do 2021.09 now, which supports multiple versions and I plan to add a 8.14 preview version. Also I have a good application for your debugger now and also plan to make your branch work. I guess it should work next weekend.

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 12:22):

@Enrico Tassi @Théo Zimmermann : I did some more minor improvements and manually tested it on the major platforms (Windows 64, MacOS BigSur, Ubuntu 20) with fresh systems (so that also the system setup part is tested). I plan to tag and release in an hour or so.

view this post on Zulip Enrico Tassi (Sep 07 2021 at 12:23):

if you need help with the snap procedure, just tell me

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 12:24):

@Enrico: I guess I will - you sent me notes some time ago, but I am not sure I can find them ...

view this post on Zulip Enrico Tassi (Sep 07 2021 at 12:31):

I'm afraid they were "oral notes" ;-)

view this post on Zulip Enrico Tassi (Sep 07 2021 at 12:33):

anyway, once you tag you have to run a workflow manually for the snap job, and answer yes to the "upload to the store" question.

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 13:04):

I just did the tag - let me see if I can manage to run the Snap pipeline ...

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 13:07):

Seems to be easy enough. I guess when it is finished I download the artifact and attach it to the release?

view this post on Zulip Enrico Tassi (Sep 07 2021 at 13:13):

no, you go to https://snapcraft.io/coq-prover/listing and fiddle with the channels. The new snap is going to show up in the edge one, it is up to you to move it to the stable one

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 13:13):

Ah, OK, I remember - need to create a notes file for that.

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 13:14):

Also I guess I should learn how to test these. Do you have a shell 2 liner for Ubuntu?

view this post on Zulip Enrico Tassi (Sep 07 2021 at 13:14):

sudo snap install --dangerous /tmp/coq-prover_2021-02-1_amd64.snap

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 13:15):

I guess this is for non official releases (locally downloaded packages).

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 13:15):

And I guess I do sudo apt-get install snap first?

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 13:16):

How would I install an officially released snap package?

view this post on Zulip Enrico Tassi (Sep 07 2021 at 13:59):

sudo snap install coq-prover

view this post on Zulip Enrico Tassi (Sep 07 2021 at 14:00):

I thought snap was preinstalled on ubuntu, but maybe it is not the case.

view this post on Zulip Enrico Tassi (Sep 07 2021 at 15:15):

I see the snap is in uploaded to the store. Do you want me to publish it?

view this post on Zulip Enrico Tassi (Sep 07 2021 at 15:15):

It's "revision" 25

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 15:16):

Let me have a quick look myself first ...

view this post on Zulip Enrico Tassi (Sep 07 2021 at 15:17):

We can also put it in beta, then you can get it by passing --beta to snap (now you need to pass --edge, which is the channel populated by CI).

view this post on Zulip Enrico Tassi (Sep 07 2021 at 15:17):

ok

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 15:26):

Or to "candidate" I guess ...

view this post on Zulip Enrico Tassi (Sep 07 2021 at 15:28):

right

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 15:28):

OK, I promoted it to beta and candidate and will have a look.

view this post on Zulip Enrico Tassi (Sep 07 2021 at 15:30):

note that latest is not the only track, there is one for the 2021.02 series

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 15:31):

Ah OK ...

view this post on Zulip Enrico Tassi (Sep 07 2021 at 15:31):

and we should ask the admins to create a 2021.09 track as well

view this post on Zulip Enrico Tassi (Sep 07 2021 at 15:31):

I can take care of that (if .09 is final)

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 15:32):

Yes, it will be 2021.09 - should only be a few days of work. Since it is multi-version I release it first with 8.13 as release and 8.14 as preview and in 2021.09.1 we can put in the release 8.14.

view this post on Zulip Enrico Tassi (Sep 07 2021 at 15:37):

ok, so I'll ask for the creation of 2021.09

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 15:39):

Yes please. And I took some notes on the snap process ...

view this post on Zulip Enrico Tassi (Sep 07 2021 at 15:42):

https://forum.snapcraft.io/t/2021-09-track-creation-for-coq-prover/26451

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 16:00):

@Enrico Tassi : one thing I almost forgot: the Windows installers need to be signed by INRIA. Can you take care of this? You can use the artifacts from the "Set version" commit.

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 16:04):

Did we also sign the MacOS DMG?

view this post on Zulip Enrico Tassi (Sep 07 2021 at 16:04):

yes

view this post on Zulip Enrico Tassi (Sep 07 2021 at 16:04):

I'll do for windows

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 16:04):

and Mac?

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 16:04):

I am not sure of the previous package was signed

view this post on Zulip Enrico Tassi (Sep 07 2021 at 16:05):

for OSX: https://github.com/coq/coq/wiki/SigningReleases

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 16:09):

OK, I don't have the siganture password (and I think I shouldn't since it is an INRIA signature), so I fear you have to do that as well.

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 16:09):

Apparently the 2021.02.1 release was not signed for MacOS.

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 16:13):

I got the Windows installers - this was quick :-) Maybe we should change the name one day ...

view this post on Zulip Enrico Tassi (Sep 07 2021 at 16:16):

I got a mail that they downloaded it already.. but they did not send it back

view this post on Zulip Enrico Tassi (Sep 07 2021 at 16:16):

or maybe you are the anonymous downloader

view this post on Zulip Enrico Tassi (Sep 07 2021 at 16:16):

these are yet to be signed

view this post on Zulip Enrico Tassi (Sep 07 2021 at 16:17):

inria does not give me the key, I've to ask this team to sign the packages for me

view this post on Zulip Enrico Tassi (Sep 07 2021 at 16:17):

for windows I mean

view this post on Zulip Enrico Tassi (Sep 07 2021 at 16:17):

for OSX, I'll do it now, let's see

view this post on Zulip Michael Soegtrop (Sep 07 2021 at 16:19):

Ah OK, a misunderstanding then - likely I was the downloader

view this post on Zulip Enrico Tassi (Sep 07 2021 at 16:59):

uff, I get an error:

bin/Coq_Platform_2021.02.2.app: the main executable or Info.plist must be a regular file (no symlinks, etc.)

I've to go now

view this post on Zulip Enrico Tassi (Sep 07 2021 at 16:59):

it seems to come from codesign

view this post on Zulip Enrico Tassi (Sep 08 2021 at 08:17):

@Michael Soegtrop if the problem is the symlink one (I can of recall you changing this) then I can hack it (replace the symlink by the symlinked) and get a signed dmg

view this post on Zulip Michael Soegtrop (Sep 08 2021 at 08:20):

I darkly remember that we had this issue before and did the same hack before. So yes, please go ahead. I will try to fix it properly in 2021.09.

view this post on Zulip Enrico Tassi (Sep 08 2021 at 08:53):

here the dmg signed https://filesender.renater.fr/?s=download&token=d05bae48-f840-4db4-8a70-28d5ee9be2f3 (but not tested)

view this post on Zulip Michael Soegtrop (Sep 08 2021 at 09:40):

@Enrico Tassi : the signed package does not work - even when opened with override. MacOS complains that it can't be scanned for malicious software but there seems to be more to it.

view this post on Zulip Enrico Tassi (Sep 08 2021 at 10:29):

well, I can't really help to debug this. My only change was to rm coqide; cp ../wherever/coqide .

view this post on Zulip Enrico Tassi (Sep 08 2021 at 10:30):

If you want try a new one and sign it yourself, instructions are here https://github.com/coq/coq/wiki/SigningReleases and the passwords, well, I can give them to you

view this post on Zulip Michael Soegtrop (Sep 08 2021 at 12:48):

Yes, I guess this is best - can you please send me the password via email?

I wonder if I should publish the unsigned installer meanwhile - the 2021.02.1 was also unsigned and on Mac this is not that bad - one has to open the App once from Finder with open - I can put a remark in the release notes.

view this post on Zulip Théo Zimmermann (Sep 08 2021 at 12:59):

Michael Soegtrop said:

Yes, I guess this is best - can you please send me the password via email?

PGP-encrypted e-mail I guess then :smile:

view this post on Zulip Michael Soegtrop (Sep 08 2021 at 13:09):

Sure, although I guess PGP security suffered a bit from Corona - no key signing parties any more ... in Germany we meanwhile have an email system where you authenticate with your electronic ID card - quite convenient.

view this post on Zulip Enrico Tassi (Sep 08 2021 at 13:13):

I think we already tried to exchange a PGP encrypted email, I found an email exchange where your tell me that pub key is not on public servers... Anyway, how do I get your pub key?

view this post on Zulip Michael Soegtrop (Sep 08 2021 at 13:15):

I will send you a signed email a bit later and post the fingerprint in a private message here.


Last updated: Jan 30 2023 at 10:03 UTC