Michael Soegtrop (Aug 25 2021 at 16:19): 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?
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]
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?
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.
Michael Soegtrop (Aug 25 2021 at 18:02):When is it ? The Wiki says "after the summer holidays" ...
Matthieu Sozeau (Aug 26 2021 at 12:48):I guess we should resume next week (sept 1st)
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?
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.
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
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).
Emilio Jesús Gallego Arias (Aug 27 2021 at 09:55):Does this mean that Coq's CI is fixed too?
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.
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.)
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
Emilio Jesús Gallego Arias (Aug 30 2021 at 18:09):CI seems to be still failing all over the place
Emilio Jesús Gallego Arias (Aug 30 2021 at 18:18):Indeed, not a single job succeeded
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
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.
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.
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.
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
Michael Soegtrop (Aug 31 2021 at 12:22):Just to make sure: the "multi-version" branch is not yet released, but should come soon.
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?
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.
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.
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.
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.
Emilio Jesús Gallego Arias (Aug 31 2021 at 14:00):Gonna have a look thanks
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.
Emilio Jesús Gallego Arias (Aug 31 2021 at 18:38):I understood everything and made things work I think, thanks!
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!
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).
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
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?
Enrico Tassi (Sep 02 2021 at 13:08):I don't know how gappa works
Enrico Tassi (Sep 02 2021 at 13:09):do you mean: is gappa available via coq-prover.gappa ?
Enrico Tassi (Sep 02 2021 at 13:09):if so, no but we can add it.
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)
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").
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.
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?)
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.
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.
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.
Théo Zimmermann (Sep 02 2021 at 15:28):The Fall semester is already well started in many US universities I believe...
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.
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
Guillaume Melquiond (Sep 03 2021 at 14:50):Could it be that they are in $PATH but do not exist?
Guillaume Melquiond (Sep 03 2021 at 14:54):if System.is_in_system_path "csdp" then lazy () else lazy (raise CsdpNotFound)
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
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...
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....
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?
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.
Jim Fehrle (Sep 05 2021 at 04:09):I meant Lately...
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).
Michael Soegtrop (Sep 06 2021 at 09:27):@Enrico Tassi, @Jim Fehrle : how are things going? I wanted to release the update soon.
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.
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)?
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.
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.
Enrico Tassi (Sep 06 2021 at 10:54):OK, I've tested the snap and it works OK for me
Enrico Tassi (Sep 06 2021 at 10:54):I'm not very happy with the second patch, since it simply disable the warning
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
Enrico Tassi (Sep 06 2021 at 10:55):probably yes but I did not try
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.
Michael Soegtrop (Sep 06 2021 at 12:24):Shall I have a look?
Enrico Tassi (Sep 06 2021 at 12:40):yes please, the two patches I add are just for the snap
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 ...
Michael Soegtrop (Sep 06 2021 at 12:57):It is not an OS distribution like Ubuntu or Windows.
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
Enrico Tassi (Sep 06 2021 at 13:19):see https://opam.ocaml.org/doc/Manual.html#Filters , but I have not tried
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
Enrico Tassi (Sep 06 2021 at 13:23):I'll give it a try
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.
Enrico Tassi (Sep 06 2021 at 15:07):ok, it seems to work. the snap has the (now optional) patches applied.
Michael Soegtrop (Sep 06 2021 at 16:04):Fine, so shall I merge?
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.
Jim Fehrle (Sep 06 2021 at 18:16):Not working at all for me:
$ 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`
--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
I'm still quite tired from my vacation (290 miles of cycling), so maybe I'm not doing the right thing.
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.
Jim Fehrle (Sep 06 2021 at 18:41):(deleted)
Michael Soegtrop (Sep 06 2021 at 20:39):@Jim Fehrle : does it work now?
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?
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.
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.
Enrico Tassi (Sep 07 2021 at 12:23):if you need help with the snap procedure, just tell me
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 ...
Enrico Tassi (Sep 07 2021 at 12:31):I'm afraid they were "oral notes" ;-)
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.
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 ...
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?
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
Michael Soegtrop (Sep 07 2021 at 13:13):Ah, OK, I remember - need to create a notes file for that.
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?
Enrico Tassi (Sep 07 2021 at 13:14):sudo snap install --dangerous /tmp/coq-prover_2021-02-1_amd64.snap
Michael Soegtrop (Sep 07 2021 at 13:15):I guess this is for non official releases (locally downloaded packages).
Michael Soegtrop (Sep 07 2021 at 13:15):And I guess I do sudo apt-get install snap first?
Michael Soegtrop (Sep 07 2021 at 13:16):How would I install an officially released snap package?
Enrico Tassi (Sep 07 2021 at 13:59):sudo snap install coq-prover
Enrico Tassi (Sep 07 2021 at 14:00):I thought snap was preinstalled on ubuntu, but maybe it is not the case.
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?
Enrico Tassi (Sep 07 2021 at 15:15):It's "revision" 25
Michael Soegtrop (Sep 07 2021 at 15:16):Let me have a quick look myself first ...
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).
Enrico Tassi (Sep 07 2021 at 15:17):ok
Michael Soegtrop (Sep 07 2021 at 15:26):Or to "candidate" I guess ...
Enrico Tassi (Sep 07 2021 at 15:28):right
Michael Soegtrop (Sep 07 2021 at 15:28):OK, I promoted it to beta and candidate and will have a look.
Enrico Tassi (Sep 07 2021 at 15:30):note that latest is not the only track, there is one for the 2021.02 series
Michael Soegtrop (Sep 07 2021 at 15:31):Ah OK ...
Enrico Tassi (Sep 07 2021 at 15:31):and we should ask the admins to create a 2021.09 track as well
Enrico Tassi (Sep 07 2021 at 15:31):I can take care of that (if .09 is final)
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.
Enrico Tassi (Sep 07 2021 at 15:37):ok, so I'll ask for the creation of 2021.09
Michael Soegtrop (Sep 07 2021 at 15:39):Yes please. And I took some notes on the snap process ...
Enrico Tassi (Sep 07 2021 at 15:42):https://forum.snapcraft.io/t/2021-09-track-creation-for-coq-prover/26451
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.
Michael Soegtrop (Sep 07 2021 at 16:04):Did we also sign the MacOS DMG?
Enrico Tassi (Sep 07 2021 at 16:04):yes
Enrico Tassi (Sep 07 2021 at 16:04):I'll do for windows
Michael Soegtrop (Sep 07 2021 at 16:04):and Mac?
Michael Soegtrop (Sep 07 2021 at 16:04):I am not sure of the previous package was signed
Enrico Tassi (Sep 07 2021 at 16:05):for OSX: https://github.com/coq/coq/wiki/SigningReleases
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.
Michael Soegtrop (Sep 07 2021 at 16:09):Apparently the 2021.02.1 release was not signed for MacOS.
Michael Soegtrop (Sep 07 2021 at 16:13):I got the Windows installers - this was quick :-) Maybe we should change the name one day ...
Enrico Tassi (Sep 07 2021 at 16:16):I got a mail that they downloaded it already.. but they did not send it back
Enrico Tassi (Sep 07 2021 at 16:16):or maybe you are the anonymous downloader
Enrico Tassi (Sep 07 2021 at 16:16):these are yet to be signed
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
Enrico Tassi (Sep 07 2021 at 16:17):for windows I mean
Enrico Tassi (Sep 07 2021 at 16:17):for OSX, I'll do it now, let's see
Michael Soegtrop (Sep 07 2021 at 16:19):Ah OK, a misunderstanding then - likely I was the downloader
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
Enrico Tassi (Sep 07 2021 at 16:59):it seems to come from codesign
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
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.
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)
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.
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 .
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
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.
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:
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.
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?
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: Jun 03 2023 at 05:01 UTC