Stream: Coq Platform devs & users

Topic: 8.13+beta1 release


view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:06):

@Enrico Tassi : I did a smoke test with the result of the 8.13 installer. Results:

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:16):

for HB, these files are compiled (but not installed) as part of the build process. So the most recent version works.
For gappa/interval I don't know, I'm looking at it

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:27):

for interval, it's the installation process that breaks

$ ./remake.exe install -d
Building install
dir="$DESTDIRC:/bin/cygwin_coqplatform_8_13_0/home/IEUser/.opam/_coq-platform_.8.13.0+beta1/lib/coq/user-contrib/Interval"
mkdir -p $dir
for d in Eval Float Integral Interval Missing Poly Real; do mkdir -p $dir/$d; done
for f in Tactic Eval/Eval Eval/Prog Eval/Reify Eval/Tree Float/Basic Float/Generic Float/Generic_ops Float/Generic_proof Float/Specific_bigint Float/Specific_ops Float/Specific_sig Float/Specific_stdz Float/Sig Integral/Bertrand Integral/Integral Integral/Priority Integral/Refine Interval/Interval Interval/Interval_compl Interval/Float Interval/Float_full Interval/Transcend Interval/Univariate_sig Missing/Coquelicot Missing/MathComp Missing/Stdlib Poly/Basic_rec Poly/Bound Poly/Bound_quad Poly/Datatypes Poly/Taylor_model Poly/Taylor_model_sharp Poly/Taylor_poly Real/Taylor Real/Xreal Real/Xreal_derive Tactic_float Float/Primitive_ops; do cp src/$f.vo $dir/$f.vo; done
( cd src && find . -type d -name ".coq-native" -exec cp -RT "{}" "$dir/{}" \; )

Finished install

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:27):

dir is wrong

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:27):

@Enrico Tassi : yes, HB looks fine - it gets pretty far. I do these tests mostly to check if the stuff is there at all / works at all. For this getting over the Require commands is enough - I trust that the rest is tested elsewhere.

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:28):

Yes. I guess for gappa it is the same - Guillaume's make files are all similar.

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:28):

Can you fix the issue or should I look into it?

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:30):

This hack seems to fix it: ./remake.exe -d install DESTDIR="cygpath -u"

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:30):

let me try from a clean situation

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:31):

what is cygpath -u supposed to do ?

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:34):

You need to give a path as argument to cygpath.

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:35):

dir="$DESTDIRC:/bin/cygwin_coqplatform_8_13_0/home/IEUser/.opam/_coq-platform_.8.13.0+beta1/lib/coq/user-contrib/Interval"

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:38):

here @Guillaume Melquiond wanted to support DESTDIR, a standard way to have make install copy the files under a user provided path. When empty dir constains the usual path. I don't get why my hack worked (I wanted to turn the path into a unix one, but a pair of backticks are missing)

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:41):

So I've probably been allucinating

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:41):

;-)

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:41):

So how about ./remake.exe -d install DESTDIR="" ?

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:42):

I looked at the congigure.in and Remake.in files of interval and DESTDIR is not set anywhere. If it is then expanded with the variable name things go wild.

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:42):

But the windows path with forward slashes should work. Cygwin can handle this.

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:43):

This form of path is the common denominator between MinGW (opam) and cygwin (bash).

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:45):

I guess the real problem is that "$DESTDIR@COQUSERCONTRIB@/Interval" concatenates $DESTDIR with C: and this makes the variable name invalid.

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:46):

I guess "dir="$DESTDIR""@COQUSERCONTRIB@/Interval" might work.

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:48):

yes, this is the actual hack DESTDIRC=C ./remake.exe install -d

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:48):

(-d is for debug)

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:48):

note I set the variable name DESTDIRC that is DESTDIR + the C coming from the windows path ;-)

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:49):

let me try yout fix to the .in file

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:51):

But this only works if your install drive is C. Mine is typically T.

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:51):

I opted for this, which works: dir="${DESTDIR}@COQUSERCONTRIB@/Interval"

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:51):

Much better :-)

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:51):

yes my hack was orrible

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:52):

let me see if gappa has the same problem

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:53):

You know how the opam patch mechanism works?

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:54):

yes

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:55):

same problem for coq-gappa, I'll make an overlay with a patch for both

view this post on Zulip Enrico Tassi (Dec 07 2020 at 10:55):

BTW, do you know homebrew? any idea if we can force it to not clean (which started to fail?) https://dev.azure.com/coq/coq/_build/results?buildId=13834&view=logs&j=a5e52b91-c83f-5429-4a68-c246fc63a4f7&t=7d499b5d-1d92-5096-7919-3c7f8065da78

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:55):

Well if you use the coq platform to build the installer, you need to create patched opam packages

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:57):

Regarding homebrew: no - I don't use it (it makes your main system folder writable to the current user which I find not agreeable and which is very hard to fix). But I think I can find instruction son how to get around this and install it anyway.

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:58):

My advice would be to switch to MacPorts.

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 10:59):

I added a lot of MacPorts depext info in the last months. It likely did not work a year back, but now it should. Definitely Coq platform builds on a virgin Mac with MacPorts now.

view this post on Zulip Guillaume Melquiond (Dec 07 2020 at 14:10):

Oops, right. ${DESTDIR}@COQUSERCONTRIB@/Interval should have been the original code. It did not occur to me that @COQUSER...@ could start with something else than /.

view this post on Zulip Enrico Tassi (Dec 07 2020 at 14:19):

I've tested this trivial patch on both gappa and interval and it works

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 15:00):

@Enrico Tassi : good! Btw.: I just had a call with Andrew. The plan is to have a VST release this week. The master branch is fine for the beta.

view this post on Zulip Enrico Tassi (Dec 07 2020 at 15:00):

I've almost finished building an installer with compcert 3.8 full and vst master. Are you OK with that (see my previous message)

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 15:01):

You mean about the license of CompCert?

view this post on Zulip Enrico Tassi (Dec 07 2020 at 15:01):

oops, I never sent the message

view this post on Zulip Enrico Tassi (Dec 07 2020 at 15:02):

the example file says "compcert=o" but then I get "beta does not support open source variant". So I was not sure what you wanted to ship today

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 15:03):

The Windows installer should have the full version. This is agreed on with Xavier. As I wrote before the conditions are:

view this post on Zulip Enrico Tassi (Dec 07 2020 at 15:04):

ok, then.

view this post on Zulip Enrico Tassi (Dec 07 2020 at 15:04):

I'll finish the build, test the license thing, and then send the installer to the guys that sign it

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 15:04):

The installer ist mostly intended for people who just want to try things out and CompCert may be used for commercial evaluation purposes.

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 15:04):

Perfect, thanks!

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 15:05):

Btw.: I also want to do a 8.12.1 Platform release. Can the installer also be signed? Who would take care of this?

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 15:07):

@Enrico Tassi : you sent the message in the CUDW thread :-) We should change the example file until the open source variant exists.

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 15:07):

But as I said, the installer should always be full version.

view this post on Zulip Enrico Tassi (Dec 07 2020 at 15:08):

sorry, I'm receiving too many interrupts today

view this post on Zulip Enrico Tassi (Dec 07 2020 at 15:08):

all good then

view this post on Zulip Théo Zimmermann (Dec 07 2020 at 16:28):

Michael Soegtrop said:

Btw.: I also want to do a 8.12.1 Platform release. Can the installer also be signed? Who would take care of this?

It should be someone at Inria who sends the request as the 8.12 RM. I could do it or let @Enrico Tassi do it since he's already sent a mail to them today.

view this post on Zulip Enrico Tassi (Dec 07 2020 at 16:31):

I can do it tomorrow. I only need to know:

view this post on Zulip Théo Zimmermann (Dec 07 2020 at 16:41):

Let's use GitHub releases on the platform repo.

view this post on Zulip Théo Zimmermann (Dec 07 2020 at 16:43):

And if the Windows installer for the 8.13 release is actually the platform installer, it could also be released on the platform repo, with a link from the Coq release. WDYT?

view this post on Zulip Enrico Tassi (Dec 07 2020 at 17:54):

I don't know, it's still a bit unclear to me how to organize the two releases, the beta period, etc...

view this post on Zulip Théo Zimmermann (Dec 07 2020 at 20:07):

To me too. You have been an exceptional release manager, but I don't think it will happen with the same tight schedule every time.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2020 at 20:15):

Congrats on the 8.13+beta release @Enrico Tassi [and all that helped him], incredible work indeed!

view this post on Zulip Enrico Tassi (Dec 07 2020 at 20:37):

Thanks guys, it means a lot to me.

But being timely is not the point I'm confused about. The beta, early or late it does not change much. My feeling is that the beta testing period give us little back. I failed to see a flood of bugreports in the past. For example in 8.12+beta1 there was a serious ssreflect bug that anybody would have noticed after playing with it 10 minutes (myself included), but It was only reported after the final. The same happened with notation regressions in the past. At the same time, Cyril is still not using 8.12.x for example because he knows a few bugs only 8.12.2 will solve! (just to make an example).

IMO, but for a few PHDs eager to feel the bleeding edge, no final user dares trying the beta. It may still make sense to make a beta tag, to synchronize with developers of plugins. Half of them did tag in less than 48h after I asked them. A handful are still working on a release for 8.13, mainly because they depend on other plugins/developments. This seems to be the expected time it takes to consolidate the platform.

If my feeling is close to reality, then maybe we should turn the beta release into a softer checkpoint (eg, developers don't need an easy installer, polished released notes...). Then, after the final, we may need to release hotfixes super fast, to deal with unexpected regressions, so the release pipeline must be well greased. Even if it is not the case, as it was this time (both win and mac installers were broken, CI de-synchronized with the platform), it took 2 weeks to repair the thing (and now it will rest for 30 days...)

To cut it short, maybe tagging the beta should be the first step of the 1 month long release process, not the end of the first half.

view this post on Zulip Théo Zimmermann (Dec 07 2020 at 20:44):

Your feeling is confirmed by download data:
Check the following query at this address: https://developer.github.com/v4/explorer/

query {
  repository(owner: "coq", name: "coq") {
    releases(first: 100, orderBy: {field: CREATED_AT, direction: DESC}) {
      nodes {
        name
        releaseAssets(first: 100) {
          nodes {
            name
            downloadCount
          }
        }
      }
    }
  }
}

view this post on Zulip Théo Zimmermann (Dec 07 2020 at 20:48):

I totally agree that greasing the release pipeline to make little cost, frequent patch-level releases is the way to go. The work on the platform is the most important step in this direction (the release process doesn't contain much more difficulties than this).

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 20:51):

I think we should see how things work out with the platform - it is hard to foresee how difficult it will be. But I am sure it will make things smoother to decouple the core Coq release and the platform release.

view this post on Zulip Michael Soegtrop (Dec 07 2020 at 20:52):

Regarding the 8.12 release: I am not yet finished with testing - likely tomorrow. I also wanted to finish a proper script to create a smoke test kit. With some feedback from the opam team I meanwhile have some good ideas how to do it.

view this post on Zulip Enrico Tassi (Dec 07 2020 at 20:56):

I've just built the installer out of commit 2ed6a8ce9c977853569e44229b4cda49ee9d878a donwload installer 8.12.1, if it is OK, then I can send it to Inria for signing tomorrow. Otherwise just ping me when you have a new commit to build.

view this post on Zulip Enrico Tassi (Dec 07 2020 at 20:56):

(when the wheels are greased... )

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 07:07):

@Enrico Tassi should we advertise the 8.12 branch and ask developers to use it? If some 8.12.1 bugs are only fixed in 8.12.2 and affect @Cyril Cohen , he could try as soon as fixes are merged.
For myself, I personally packaged and used branches (with backports) for both 8.11 and 8.12 (for different reasons), so I don't think it's that scary.

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 07:09):

In the recent experience doesn't seem that CI covers that well IDE usage and error messages, but that's harder to test, so while it's a problem it's still an improvement...

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 07:10):

OTOH I've never tried master, and I don't expect that to be so stable; at least, random libraries aren't ported to it (while libraries in CI are).

view this post on Zulip Enrico Tassi (Dec 08 2020 at 07:32):

I think not using a version that is broken for you is normal, you can't ask users to work on a patch (as a general rule). I mentioned that to stress that pushing point releasing quickly can help users adopt a new Coq versions sooner.

view this post on Zulip Karl Palmskog (Dec 08 2020 at 07:35):

from coq-community side, beta periods have generally been so short we barely have had time to get betas into CI for testing. Best use of betas in my mind is as a coordination mechanism for releases of Coq projects to coincide with the point release. For example, once the beta is out, I would feel comfortable doing a release of AAC Tactics for 8.13, and this release can go into the Coq Platform, etc.

view this post on Zulip Enrico Tassi (Dec 08 2020 at 08:33):

@Michael Soegtrop : for your info I plan to make a PR to erase the windows job and instead build a "minimal" platform today

view this post on Zulip Théo Zimmermann (Dec 08 2020 at 08:57):

Just for clarification, there is no plan for a 8.12.2 release. I think Enrico used the name as a joke.

view this post on Zulip Enrico Tassi (Dec 08 2020 at 09:24):

Didn't know that. I seriously thought that there were a few fixes pending.

view this post on Zulip Enrico Tassi (Dec 08 2020 at 09:24):

Sorry for the confusion

view this post on Zulip Théo Zimmermann (Dec 08 2020 at 09:56):

No worries. We decided about it in a Coq Call, but if there really are important fixes that should be backported to v8.12, we could change the plans...

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

I would need to know what they are though, because I never heard about these important issues that would still not be fixed in 8.12.

view this post on Zulip Cyril Cohen (Dec 08 2020 at 10:48):

As of now, even though mathcomp compiles with 8.12. Some notations break so badly that I deem it unusable in an interactive way, it least for end users

view this post on Zulip Cyril Cohen (Dec 08 2020 at 10:48):

https://github.com/coq/coq/pull/13436#issuecomment-733653527

view this post on Zulip Cyril Cohen (Dec 08 2020 at 10:48):

Maybe I should have openned an issue instead of making this comment.

view this post on Zulip Cyril Cohen (Dec 08 2020 at 10:50):

I will open the issue ASAP

view this post on Zulip Théo Zimmermann (Dec 08 2020 at 11:14):

A comment would have been fine if you had mentioned me. But in this case I didn't see the comment at all.

view this post on Zulip Cyril Cohen (Dec 08 2020 at 11:18):

I wouldn't have known who to mention, is there such a thing as an @coq/release-managers-8.12 ?

view this post on Zulip Cyril Cohen (Dec 08 2020 at 11:20):

@Théo Zimmermann actually, I thought that it had been taken care of by @Enrico Tassi but I think I was mistaken...

view this post on Zulip Théo Zimmermann (Dec 08 2020 at 11:23):

It was backported to 8.13 by Enrico.

view this post on Zulip Théo Zimmermann (Dec 08 2020 at 11:24):

Indeed, there is no such team, though you have release manager information in https://github.com/coq/coq/wiki/Release-Plan and in the changelog.

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

Yup indeed we just missed that problem, should be OK to backport the fix.

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 16:51):

@Enrico Tassi I assumed 8.12-master would have a fix.

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 16:52):

And if all of 8.12 is not good enough for a library as crucial as math-comp, that seems bad, and it might warrant a _blameless_ postmortem.

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 16:52):

basically, finding out what's wrong in the QA process

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 16:53):

again, not to blame people but to prevent it in the future

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 16:55):

FWIW, I use nothing from math-comp, but I use ssreflect so had problems with 8.12.0. So I'm a semi-disinterested party.

view this post on Zulip Théo Zimmermann (Dec 08 2020 at 18:43):

FTR, no the release branch has nothing that is not in the 8.12.1 release. I've added the topic of a potential 8.12.2 release to the program of the next Coq Call.

view this post on Zulip Enrico Tassi (Dec 08 2020 at 20:05):

Paolo Giarrusso said:

basically, finding out what's wrong in the QA process

I've just received the signed windows binary for 8.13. I'll send the announcement in a moment. You'll find there the only culprit I can find (hence the request for testing).

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 20:05):

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 20:07):

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 20:09):

to answer the 2nd question (from this code): the infrastructure is there.

view this post on Zulip Enrico Tassi (Dec 08 2020 at 20:10):

The infrastructure, yes. The tests ... no ;-)

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 20:11):

"What would it take to fix that" is left as an "easy" exercise for the reader. /s

view this post on Zulip Cyril Cohen (Dec 08 2020 at 20:12):

Well I added one of them recently, but since it was not done historically, we should add a bunch of them.
(EDIT link updated)

view this post on Zulip Cyril Cohen (Dec 08 2020 at 20:12):

Manpower is of the essence

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 20:16):

testing prereleases for 8.x.1 and 8.x.0 should also be encouraged, but for 8.x.1 it _might_ be easier.

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 20:17):

if you want me to try 8.x.0 "for real" it must be in my daily work, and for that you must coordinate with the ecosystem.

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 20:19):

some of my deps test against master, but some of my code uses metacoq which took a bit longer.

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 20:20):

dunno if that's _the_ blocker but it's probably _one_ obstacle; I think Scala's release process explicitly coordinates with OS maintainers exactly to this end, and I don't know if the resources are there.

view this post on Zulip Enrico Tassi (Dec 08 2020 at 21:47):

You have a crystal ball, the message I did +1 is essentially what I want to propose tomorrow at the Coq call.

view this post on Zulip Michael Soegtrop (Dec 09 2020 at 08:42):

@Enrico Tassi : did you just take my CI runner session?

view this post on Zulip Michael Soegtrop (Dec 09 2020 at 08:52):

My view on this is that the Coq 8.13.beta release should mostly be tested by package maintainers - especially platform package maintainers, so that the creation of package releases for 8.13.0 is a quicky and easy process.

view this post on Zulip Enrico Tassi (Dec 09 2020 at 08:53):

no, I'm busy the whole day with other things FYI

view this post on Zulip Enrico Tassi (Dec 09 2020 at 08:55):

@Paolo Giarrusso @Michael Soegtrop this is my drawing of the current release process and of the one I'll propose this afternoon release-coq.pdf

view this post on Zulip Enrico Tassi (Dec 09 2020 at 08:55):

without the sound it may not be super explicit, but I really gotta to do other stuff now

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

There's no 32bit Windows installer for 8.13?

view this post on Zulip Enrico Tassi (Dec 09 2020 at 13:04):

I did not build it (not even tried, but the scripts do support it)

view this post on Zulip Enrico Tassi (Dec 09 2020 at 13:06):

I really don't know how relevant it is today. In the past @Andrew Appel was using it. If it is still the case I can try to build it (and publish it, at least for the final).

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

Yes, I also had in mind the use case of @Andrew Appel.

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

But you can also use the query I shared above to check how much this installer was downloaded for previous versions.

view this post on Zulip Enrico Tassi (Dec 09 2020 at 13:19):

There are downloads, way less than the 64 bit one, but not 0 either.
Let's use the windows NT page cache cleanup strategy (you remove a page, not caring if it was used recently or not, at worse you get a page fault) ;-)

The 32 bit version was not really used because of 32 bit hardware, but because it was using less memory on some workloads. Maybe it's not relevant anymore, and users that were used to that installer did continue to use it because of habit, or just clicked on the first .exe in the list. Maybe it is still relevant, and in that case we will put it back. Let's see if people ask for it.

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

image.png

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

Let's see if people ask for it.

Sounds as a good strategy to me!

view this post on Zulip Enrico Tassi (Dec 09 2020 at 13:31):

There is a singularity in V8.10.0, @Vincent Laporte do you by any chance remember if you added the 32 bit installer "later" to the assets that time?

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

We can add a createdAt field to this query. Then we learn that the two Windows installers were added at the same time.

view this post on Zulip Andrew Appel (Dec 09 2020 at 13:41):

I continue to use the 32-bit Windows version of Coq, simply because it's significantly faster than the 64-bit version. The reason, as usual, is that twice as many pointers fit into the same-size cache, and Coq is mostly memory bound. If I'm the only user, then perhaps it doesn't make sense to maintain this version just for me. It's a pity that everyone else in the world is burning twice as many watts as necessary to do their Coq proofs...

view this post on Zulip Enrico Tassi (Dec 09 2020 at 13:43):

Well, It's @Michael Soegtrop that maintains the scripts, I don't know if the 32 bit variant has a maintenance cost or not. I'm running them now, see you in 4 hours ;-)

view this post on Zulip Enrico Tassi (Dec 09 2020 at 13:52):

We can add a createdAt field to this query.

It was created at the very same time of the other assets. Mystery not solved.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 09 2020 at 14:07):

@Andrew Appel support for 32bit versions of Coq is planned to be continued .

view this post on Zulip Michael Soegtrop (Dec 09 2020 at 14:28):

@Enrico Tassi : the 32 bit option is there, but I can't say I tested it. But of cause it is the plan to support it. In case you have issues with the 32 bit option, please let me know.

view this post on Zulip Enrico Tassi (Dec 09 2020 at 14:31):

It's crunching fine so far, it's compiling coq-vst right now. I'll post a link to download the installer soon, so that you can test it now (before putting it on github I need to go trough the signature bureaucracy which takes 1 day...)

view this post on Zulip Michael Soegtrop (Dec 09 2020 at 14:35):

Good, I will smoke test it today and also see if it indeed produces 32 bit apps (there is a small risk that the ARCH flag gets lost on the way ...)
Can you can please start a console of the generated cygwin and run "uname -m" there?

view this post on Zulip Michael Soegtrop (Dec 09 2020 at 14:35):

Btw.: I plan to add a file to the platform repo which contains information on what has been actually tested.

view this post on Zulip Michael Soegtrop (Dec 09 2020 at 14:36):

Do you think I should add an interactive question for 32/64 bit in case no command line argument is given?

view this post on Zulip Enrico Tassi (Dec 09 2020 at 14:37):

I think I made a mistake. I did the flag to purge the opam switch, but I did not purge the cygwin (and its folder name does not contain $ARCH.

view this post on Zulip Enrico Tassi (Dec 09 2020 at 14:37):

and I did pass -arch=32

view this post on Zulip Enrico Tassi (Dec 09 2020 at 14:38):

I'll fix the script to put the architecture in the name of the generated cygwin

view this post on Zulip Michael Soegtrop (Dec 09 2020 at 14:38):

You need a 32 bit cygwin to compile 32 bit stuff. Otherwise it gets really tricky. The reason is that some DLLs in Windows have magic overlays and it depends on the architecture of the exe accessing them which file you get.

view this post on Zulip Enrico Tassi (Dec 09 2020 at 14:39):

are you OK with the proposed "fix"?

view this post on Zulip Enrico Tassi (Dec 09 2020 at 14:39):

the default should be C:\cygwin$ARCH_coq_platform

view this post on Zulip Enrico Tassi (Dec 09 2020 at 14:40):

and not C:\cygwin_coq_platform. That would have just worked I believe

view this post on Zulip Michael Soegtrop (Dec 09 2020 at 14:40):

Yes, that's fine.

view this post on Zulip Michael Soegtrop (Dec 09 2020 at 14:41):

Of cause I guess few people will do both and if so also can give a manual name.

view this post on Zulip Michael Soegtrop (Dec 09 2020 at 14:41):

But it doesn't hurt to have it in the default - two chars more make no difference and it is clearer what it is.

view this post on Zulip Michael Soegtrop (Dec 09 2020 at 14:43):

Another option would be to check the architecture of the target cygwin if it exists and abort if not. I might like this more ... There is an area in the batch file which e.g. checks if there is a platform folder in the cygwin.

view this post on Zulip Michael Soegtrop (Dec 09 2020 at 14:44):

I mean abort if the architecture does not match the -arch argument.

view this post on Zulip Michael Soegtrop (Dec 09 2020 at 14:44):

That would also work in case people do give custom names.

view this post on Zulip Enrico Tassi (Dec 09 2020 at 14:59):

something went wrong, "opam" is not installed (but I see it download opam64.something). Coq Call now.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 10 2020 at 13:50):

@Enrico Tassi , sorry I did review the release notes so late, IMHO we would like to add changes in the default garbage collector for OCaml >= 4.11 in the main summary notes, as this can be relevant for many users, WDYT?

view this post on Zulip Enrico Tassi (Dec 10 2020 at 13:51):

I'm ok with that, submit a PR and put it in the 8.13.0 milestone

view this post on Zulip Emilio Jesús Gallego Arias (Dec 10 2020 at 13:57):

Thanks @Enrico Tassi , will submit a one-line addition then.

view this post on Zulip Andrew Appel (Dec 14 2020 at 14:21):

Emilio Jesús Gallego Arias said:

Andrew Appel support for 32bit versions of Coq is planned to be continued .

Will the 32-bit version appear on https://github.com/coq/coq/releases/tag/V8.13+beta1 so that I can test the install?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 14 2020 at 14:31):

That's the domain of windows packagers @Enrico Tassi @Michael Soegtrop

view this post on Zulip Enrico Tassi (Dec 14 2020 at 15:00):

Unfortunately the current platform scripts don't work I did not have time to repair them yet.

view this post on Zulip Enrico Tassi (Dec 14 2020 at 16:48):

@Michael Soegtrop I pushed 2 commit repairing the platform scripts on 32 bits. The cygwin installation and the opam root are now set up correctly (coqc.exe is a 80386 binay according to file). A couple of packages fail because they get the host wrong (gappa & co using remake). I'll try to build the installer as soon as all working Coq packages finish to compile.

view this post on Zulip Enrico Tassi (Dec 14 2020 at 17:07):

[ERROR] The compilation of gappa failed at "./configure CXXFLAGS=-I/opt/local/include --build=x86_64-pc-cygwin --host=x86_64-w64-mingw32 --target=x86_64-w64-mingw32
        --prefix=C:/cygwin32_coq_platform/home/IEUser/.opam/_coq-platform_.8.13.0+beta1".
[ERROR] The installation of dep-glib-compiled-schemas failed at "glib-compile-schemas /usr/x86_64-w64-mingw32/sys-root/mingw/share/glib-2.0/schemas/".
∗ installed dune.2.7.0b
[ERROR] The compilation of dep-gtksourceview3 failed at "./configure --build=x86_64-pc-cygwin --host=x86_64-w64-mingw32 --target=x86_64-w64-mingw32
        --prefix=/usr/x86_64-w64-mingw32/sys-root/mingw".

It seems the configure script is invoked with the wrong host/target values.

view this post on Zulip Michael Soegtrop (Dec 14 2020 at 17:37):

@Andrew Appel : I am about to make the first official release (8.12.1.0) and will then take care of the Windows 32 bit variant.

view this post on Zulip Enrico Tassi (Dec 14 2020 at 17:43):

FTR, also compcert fails for the same reason (host/target mixup)

view this post on Zulip Michael Soegtrop (Dec 14 2020 at 17:45):

@Enrico Tassi : thanks. I will start a test build and see what is going on.

view this post on Zulip Enrico Tassi (Dec 14 2020 at 17:57):

just in case, I pushed and tested on the 8.13 branch

view this post on Zulip Enrico Tassi (Dec 14 2020 at 17:57):

(only)

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 10:00):

@Enrico Tassi : I just reviewed you changes. There is one thing which confuses me: you are still using opam64. There is also an opam32 in the fdopen archive. I am a bit astonished that this does work at all with a 32 bit cygwin. I guess this opam is a MinGW app, so that it doesn't matter what cygwin one has. But still there might be differences in the handling of OCaml. Not sure. Maybe it is so that the opam32 is needed on a 32 bit Windows?

view this post on Zulip Enrico Tassi (Dec 15 2020 at 10:22):

I did not know, I've nothing against changing that.
Any ideas about the packages that fail? Could it be related to that?

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 10:31):

@Enrico Tassi : the packages failing for me are:

│ λ build   coq-compcert              3.8
│ λ build   dep-gtksourceview3        24.11
│ λ build   gappa                     1.3.5
│ ∗ install dep-glib-compiled-schemas 1.0

Do you get the same result?

For CompCert the issue might be that for 3.8 teh 64 bit variante is default and the configure might not allow to run a 64 bit compiler on a 32 bit OS. It might be worthwhile to test coq-compcert-32 instead. I don't think that a lot of people tried 64 bit compcert in a 32 bit build before.

For the others I will check.

view this post on Zulip Enrico Tassi (Dec 15 2020 at 10:33):

yes, I get the same results

view this post on Zulip Enrico Tassi (Dec 15 2020 at 10:34):

(as a consequence, coqide does not even start to build)

view this post on Zulip Enrico Tassi (Dec 15 2020 at 10:35):

Oh, and I did test the windows installer script, there was a minor issue which is solved, so it should work fine now (I don't recall if I told you already)

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 10:35):

The compiled schemas has a brutal

install: [ "glib-compile-schemas" "/usr/%{arch}%-w64-mingw32/sys-root/mingw/share/glib-2.0/schemas/" ]

in its opam file

view this post on Zulip Enrico Tassi (Dec 15 2020 at 10:36):

is %{arch}% set by opam?

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 10:36):

I guess so

view this post on Zulip Enrico Tassi (Dec 15 2020 at 10:36):

so maybe opam64 is the problem here

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 10:36):

$ opam var

<><> Global opam variables ><><><><><><><><><><><><><><><><><><><><><><><><><><>
arch              x86_64                                 # Inferred from system
jobs              16                                     # The number of parallel jobs set up in opam configuration
make              make                                   # The 'make' command to use
opam-version      2.0.7                                  # The currently running opam version
os                win32                                  # Inferred from system
os-distribution   cygwinports                            # Inferred from system
os-family         windows                                # Inferred from system
os-version        10.0.18362                             # Inferred from system
root              T:/bin/test_8_13_32/home/Michael/.opam # The current opam root directory
switch            _coq-platform_.8.13.0+beta1            # The identifier of the current switch
sys-ocaml-version                                        # OCaml version present on your system independently of

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 10:37):

Yes, so switching to opam32 might fix this.

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 10:37):

I will do a test build with this changed and see what happens.

view this post on Zulip Enrico Tassi (Dec 15 2020 at 10:37):

it seems you can also force it: https://opam.ocaml.org/doc/man/opam-var.html

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 10:38):

Yeah, well ... let me just change it.

view this post on Zulip Enrico Tassi (Dec 15 2020 at 10:38):

(to continue testing from there, I mean)

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 10:39):

I think I prefer to have two separate builds - it doesn't take that long.

view this post on Zulip Enrico Tassi (Dec 15 2020 at 11:11):

BTW, I found a bug in my changes:

The following recommended paths can be chosen by entering a number:
1  C:\cygwin"64"_coq.
2  C:\cygwin"64"_coq_platform.
3  C:\bin\cygwin"64"_coq_platform.

Truth is, I don't know how escaping/variable-expansion works in .bat files

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 11:19):

Truth is, I don't know how escaping/variable-expansion works in .bat files

Quotes are generally kept when expanding variables. You need to say %~VAR% to strip quotes (afair). Better is to not use quotes unless there is a good reason.

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 11:21):

The opam32 gives false positives with my virus scanner btw. It is a dual engine scanner so this is not that incommon and it is a single engine hit. That is my scanner is two scanners in one and one says it is a virus, one says not. I reported it to the manufacturer.

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 11:53):

Interestingly the arch variable is x86_64 even with opam32 on a 32 bit cygwin. So I will follow your advice now and change it.

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 12:52):

@Enrico Tassi : unfortunately the opam version available for MinGW doesn't have a command line option to change variables, so one has to resort to awk the config file - I did it in .opam/<switch>/.opam-switch/config.switch. The immediatly failing packages except compcert work then. I guess for compcert one has to use the 32-bit variant - the 64 bit variant fails with a 32 bit system.

view this post on Zulip Enrico Tassi (Dec 15 2020 at 12:53):

Great. Btw, I'd like COQREGTEST support on unix too. Can I add it? Any caveat? better ideas?

view this post on Zulip Enrico Tassi (Dec 15 2020 at 12:54):

see also: https://github.com/coq/platform/pull/44

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 13:05):

@Enrico Tassi : COQREGTEST shouldn't apply on unix. It won't ask anything if you give command line options for all parameters. The Windows version has an extra question cause of all the configurable paths, which easyily for wrong. COQREGTEST applies to this one question only.

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 13:05):

coq-compcert-32 does build, btw.

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 13:06):

The problem is that coq-compcert-32 is not installed under user-contrib and only found with proper -Q -R options. Maybe we should have a variant which does install to the default location.

view this post on Zulip Enrico Tassi (Dec 15 2020 at 13:12):

I'm currently getting questions from the opam installer. Maybe it's the only place where COQREGTEST should be honored?
I could install it beforehand, but I'd rather test that code path too, no?

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 13:15):

Ah, the where to install question? Yes, it would make sense to disable that. On the other hand on a reg test machine it would be expected that opam is already installed and only a switch is created.

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 13:46):

@Enrico Tassi : just wanted to let you know that I am preparing a push to fix the 32 bit stuff - just to avoid double work.

view this post on Zulip Enrico Tassi (Dec 15 2020 at 13:52):

ok, it's all yours. I'm on PR about CI now

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 14:10):

@Andrew Appel : there is one issue with a 32 bit installer: 64 bit CompCert does not compile on 32 bit platforms - at least not easily (it might work if one installs a cross compiler). Since with CompCert 3.8 the default is 64 bit, so that CompCert-32 gets installed to a non standard location, which needs -R/-Q options. Do you think we should have an opam CompCert package, which installs the 32 bit variant in the default location?

view this post on Zulip Enrico Tassi (Dec 15 2020 at 14:23):

@Michael Soegtrop does this ring a bell?(from https://github.com/coq/platform/runs/1557448505?check_suite_focus=true )

========== CONFIGURE CYGWIN USER ACCOUNT ==========
        1 file(s) copied.
Copying skeleton files.
These files are for the users to personalise their cygwin experience.

They will never be overwritten nor automatically updated.

'./.bashrc' -> '/home/runneradmin//.bashrc'
'./.bash_profile' -> '/home/runneradmin//.bash_profile'
'./.inputrc' -> '/home/runneradmin//.inputrc'
'./.profile' -> '/home/runneradmin//.profile'
/cygdrive/c/cygwin64_coq_platform/var/tmp/configure_profile.sh: line 2: $'\r': command not found
/cygdrive/c/cygwin64_coq_platform/var/tmp/configure_profile.sh: line 4: $'\r': command not found
/cygdrive/c/cygwin64_coq_platform/var/tmp/configure_profile.sh: line 6: $'\r': command not found
/cygdrive/c/cygwin64_coq_platform/var/tmp/configure_profile.sh: line 10: $'\r': command not found
/cygdrive/c/cygwin64_coq_platform/var/tmp/configure_profile.sh: line 12: $'\r': command not found
/cygdrive/c/cygwin64_coq_platform/var/tmp/configure_profile.sh: line 15: $'\r': command not found

The problematic lines are the empty ones, and I don't see \r in that file.
I'm running the main .bat file from cmd.exe (no administrative cygwin).

view this post on Zulip Andrew Appel (Dec 15 2020 at 14:33):

Michael Soegtrop said:

Andrew Appel : there is one issue with a 32 bit installer: 64 bit CompCert does not compile on 32 bit platforms - at least not easily (it might work if one installs a cross compiler). Since with CompCert 3.8 the default is 64 bit, so that CompCert-32 gets installed to a non standard location, which needs -R/-Q options. Do you think we should have an opam CompCert package, which installs the 32 bit variant in the default location?

@Michael Soegtrop : I'm not sure I understand the issue. Perhaps telephone me to explain.

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 15:04):

@Enrico Tassi : possibly someone messed up the file by checking it out to a repo where some sort of line ending translation goes on. The \r is simply the carriage return at the end of each line in a CR-LF terminated file. So open in VSCode, at the bottom right slect LF and save.

view this post on Zulip Enrico Tassi (Dec 15 2020 at 15:06):

According to vscode the file is clean, and the problem is only about some lines. I was wondering if copy.exe does silly things. Or maybe it's the "checkout action" we are using on github CI... I'll google

view this post on Zulip Enrico Tassi (Dec 15 2020 at 15:06):

ah ah: https://github.com/actions/checkout/issues/135

view this post on Zulip Andrew Appel (Dec 15 2020 at 15:47):

VST 2.7 is now ready for Coq Platform release. I have tagged the master branch as v2.7 in github.

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 16:05):

@Andrew Appel : thanks - I will update the opam packages in the coq platform and release them to the main coq opam repo if all goes well later today.

view this post on Zulip Michael Soegtrop (Dec 20 2020 at 17:41):

@Enrico Tassi : FYI: I pushed a commit which allows to build 32 bit CompCert on 64 bit cygwin and vice versa. I tested that this actually works. The CompCert put in the variants folder works fine without extra env vars. But please note that there is one more piece missing: one has to install the correspondign toolchain in cygwin - I did this manually so far.

view this post on Zulip Enrico Tassi (Dec 20 2020 at 18:19):

OK, I'm on CI & co.
Btw if you have build failures on 8.13 and mtac2 this is the problem: https://github.com/Mtac2/Mtac2/issues/310 and this is a workaround: https://github.com/coq/platform/pull/49/commits/99f084549f636cceaf7a031b1526fb2ec6840dae

view this post on Zulip Michael Soegtrop (Dec 20 2020 at 18:46):

Thanks for the Mtac2 hint. Also coq-gappa is failing btw (gappa itself is fine).

view this post on Zulip Michael Soegtrop (Dec 20 2020 at 19:51):

@Enrico Tassi : one more note: the 64 bit variants of the v2.7 tag of VST fails to build - I see what I can do about this.

view this post on Zulip Michael Soegtrop (Dec 20 2020 at 22:43):

@Enrico Tassi : CompCert builds now both in 32 and 64 bit on both 32 and 64 bit cygwin. VST should also work - I just forgot to remove a patch I merged upstream. I committed a fix, but didn't have time to test it locally. Will do tomorrow.

view this post on Zulip Enrico Tassi (Dec 21 2020 at 09:04):

I've rebased the ci PR (#46) on top, and pushed in v8.13 some cleanup commits. I will let the CI branch run, if it is green I'll merge. After that any pull request and any push will be checked by CI (only on the v8.13 branch, if you want that on 8.12 you need to backport).

view this post on Zulip Michael Soegtrop (Dec 21 2020 at 11:42):

@Enrico Tassi : you changed the parameter parsing such that variables are set to __unset__ if not passed. This is not compatible with the rest of the script which checks if variables are defined and asks for them if not.

view this post on Zulip Michael Soegtrop (Dec 21 2020 at 11:42):

Should we change this so that variables are not defined if not defined, or should we check for defined as __unset__ if not defined?

view this post on Zulip Michael Soegtrop (Dec 21 2020 at 11:44):

Hmm, I had a quick look and will change it such that I check of __unset__.

view this post on Zulip Michael Soegtrop (Dec 21 2020 at 12:05):

Sorry, I found it. Your scripts alomst work as is, just a = instead of == for an equality check in check_value_range. I will push a fix.

view this post on Zulip Enrico Tassi (Dec 21 2020 at 12:16):

thanks.

view this post on Zulip Enrico Tassi (Dec 21 2020 at 12:20):

BTW, I did push another little commit which helped me debug mtac2 failure, apparently opam keeps the logs of packages that fail, so I cat them completely (otherwise you only see a few lines)

view this post on Zulip Enrico Tassi (Dec 21 2020 at 12:21):

The snap package is almost ok. I still don't get how it is larger than the windows one (it's essentially a filesystem compressed with xz...), and I'm waiting for snapcraft to accept a package called 'coq'...

view this post on Zulip Enrico Tassi (Dec 21 2020 at 12:22):

I started doing an osx package, it does not work yet and I think I'll have to use macpack (a python script) since using ldd (otool -L) from the shell is a pain.

view this post on Zulip Enrico Tassi (Dec 21 2020 at 12:25):

All 3 packages use some "filtering of unneeded files". I guess we should factor that out. The windows one is more sophisticated, since it is a real installer, and not just a "blob". On osx one could also make an .apk with similar features I guess, right now I'm trying to "redo" the silly .dmg we currently provide.

view this post on Zulip Enrico Tassi (Dec 21 2020 at 12:28):

Last (I get to leave now), the stublibs we keep on windows are useless if coq/coqide are compiled in native mode (that C code is linked in), so we can strip further. I don't know why I thought they were needed.

BTW: If you want to add to the 8.13 branch a ci entry for windows 32 bits, please do (just copy paste the other job, the -bits flag is local to the windows job).

view this post on Zulip Enrico Tassi (Dec 21 2020 at 12:29):

(you can do it in a PR and see if CI likes it)

view this post on Zulip Michael Soegtrop (Dec 21 2020 at 12:38):

@Enrico Tassi : thanks for all the work! Regarding Mac: I have some time to look into a more feature rich installer over the holidays. What I also want to look into is to have a MinGW CompCert. But now at least mixing 32 and 64 bit CompCert and Cygwin works (well hopefully - final tests are running).

view this post on Zulip Michael Soegtrop (Dec 22 2020 at 12:05):

@Enrico Tassi : I merged all of your changes in 8.13 to master except the picking. I first want to merge CI back to the 8.12 branch. Then I will update the picking to what you have in 8.13.
So now master and v8.13 are content wise identical except version numbers, picking and the opam dev repo. I did quite a bit of squashing, though, so the history is quite different.

view this post on Zulip Enrico Tassi (Dec 22 2020 at 12:17):

ok, great. for master, I belive CI should be a bit different, see the ci branch which is still a WIP: it generates opam package for the(Coq) dev version of each package.

view this post on Zulip Michael Soegtrop (Dec 22 2020 at 13:08):

Yes, but currently master is still on 8.12. It is an extra step (to be done soon) to switch the master branch to test master. I will have a look at your opam package creation magic. My plan was more to have manually created master packages in the Coq platform local patch repo or on coq extra dev.

view this post on Zulip Enrico Tassi (Dec 22 2020 at 13:35):

We can do that, but I tried something more automatic: I use Coq's metadata for project in CI to fetch upstream opam file (with hopefully up to date external deps) and I patch it with the current commit being tested in Coq. The idea is to run a job which is close to the one run by Coq.

view this post on Zulip Michael Soegtrop (Dec 22 2020 at 13:42):

Makes sense. I would just recommend to take packages from the coq platform local patch repo with highest priority in the search. Then anything which is broken else where can be fixed and tested locally first before pushing the package upstream.

view this post on Zulip Michael Soegtrop (Dec 22 2020 at 13:45):

Btw.: I think teh next step would be to finish the smoke test test kit generator. Would you run the smoke test test kit generator in each CI run (it is a bit time consuming) or check in the test kit (test files + scripts to run them all). Would you do this differently on master and release branches?

view this post on Zulip Enrico Tassi (Dec 22 2020 at 13:53):

I agree about the priority (but I did not implement that yet).

I would do it at every run. If you look at the CI job, I've already separated the smoke one (on windows). GH actions gives us 6h per job, it takes 2.30h to build the windows installer (1h for linux/osx, but I did not do any smoke test job there, maybe there is no need to separate it).

view this post on Zulip Enrico Tassi (Dec 22 2020 at 13:55):

I don't expect (but myabe I'm wrong) the dev activity of the platform to be hindered by a "slow" CI (It's a bit different on Coq).

view this post on Zulip Enrico Tassi (Dec 22 2020 at 13:56):

I imagine CI as mostly cron-triggered, once a day, on the routine.

view this post on Zulip Michael Soegtrop (Dec 26 2020 at 17:13):

@Enrico Tassi : I thought a bit about this and wonder if we shouldn't have separate branches for tracking Coq CI and master/dev. I think both woul dhelp to keep things under control, so we should have both.

view this post on Zulip Michael Soegtrop (Dec 27 2020 at 20:25):

@Enrico Tassi : I did a large rupdate on the master branch. All packages now build dev versions (with currently quite a few local .dev packages, these will all go upstream). Currently all works except CoqIDE and VST.

view this post on Zulip Michael Soegtrop (Dec 27 2020 at 20:26):

As mentioned I think your work on tracking Coq's CI should go into a seprate branch and I would keep both long term.

view this post on Zulip Enrico Tassi (Dec 27 2020 at 21:08):

I'll try to have a look at it, it's not so clear to me what the two branches would really test and why both are interesting to have.

view this post on Zulip Michael Soegtrop (Dec 27 2020 at 22:31):

The main reasoning is that I want to have an overview on the state of the package master branches independent of a possible deviating picking in Coq's CI. I guess frequently both will be the same. It gets interesting when they are not the same. The master branch is now a plain build of the master branches of all packages.

view this post on Zulip Enrico Tassi (Dec 28 2020 at 10:09):

Well, I guess it's just not clear what the regular .dev package should point to. For example in coq-elpi my development branch (master) tracks a coq stable release, but Coq's ci tracks the branch coq-master in which I merge master from time to time. Maybe we should "standardise" *.ci.dev as the one for Coq's master and .dev as the other one (or viceversa) and some projects may have just one if the two things coincide.

Btw, master fails on OSX

view this post on Zulip Enrico Tassi (Dec 28 2020 at 10:09):

https://github.com/coq/platform/runs/1614788316

view this post on Zulip Michael Soegtrop (Dec 28 2020 at 16:24):

@Enrico Tassi : yes - I fix is on the way. One of these Linux/BSD sed incompatibilities. I think one should make a point and add -E to sed where one finds it without it and adjust the RE. Usually I keep what I find but issues with macOS are frequent, and anyway the -E syntax is much nicer.

view this post on Zulip Karl Palmskog (Dec 29 2020 at 17:58):

@Michael Soegtrop I thought we already discussed the issue with 8.13-only packages in released opam repo?

view this post on Zulip Karl Palmskog (Dec 29 2020 at 17:58):

we already have: https://github.com/coq/opam-coq-archive/projects/1

view this post on Zulip Michael Soegtrop (Dec 29 2020 at 22:51):

@Karl Palmskog : yes, this was silly. I started to merge the CompCert package since it is needed for the VST package - both also work with older Coq. And then I thought why not merge others ...

view this post on Zulip Michael Soegtrop (Dec 29 2020 at 22:53):

@Enrico Tassi : FYI : Windows CI is failing on the 8.13 branch. At a first glance it looks like a change in cygwin - I guess they removed python2 from the standard delivery, which is needed by the gtksourceview build. Let's see how the nightly build on master ends.

view this post on Zulip Théo Zimmermann (Dec 30 2020 at 06:40):

This change is also affecting the Windows CI builds in the Coq repository.

view this post on Zulip Théo Zimmermann (Dec 30 2020 at 06:42):

The green Windows CI job didn't last long :'(

view this post on Zulip Michael Soegtrop (Dec 30 2020 at 08:58):

It is likely easy to fix - one just has to add the package. The Coq Platform cron master job also failed (the same commit passed before). I will do a local test now.

view this post on Zulip Michael Soegtrop (Dec 30 2020 at 09:51):

At first glance it is not easy to fix - cygwin restructred the python packages and as it looks messed it up on the way - by default there are now 4 additional python packages but there is no python any more ... A hack around this might be to create the symlink /usr/bin/python manually.

view this post on Zulip Michael Soegtrop (Dec 30 2020 at 10:16):

@Théo Zimmermann : a ln -s -f /usr/bin/python2 /usr/bin/python somewhere at the beginning of the build script should fix this - in local tests it got past the failing package with this.

view this post on Zulip Théo Zimmermann (Dec 30 2020 at 10:29):

Thanks!

view this post on Zulip Théo Zimmermann (Dec 30 2020 at 10:33):

Actually @Michael Soegtrop, I'm surprised by this fix. Doesn't it mean that ideally, it's gtksourceview that should be fixed to call python2 explicitly? In today's world, having the default python be python3 is pretty normal and expected.

view this post on Zulip Michael Soegtrop (Dec 30 2020 at 10:46):

As far as I know for gtksourceview it doesn't matter if it is python2 or python3 - I think the code is written in a compatible way. It just needs any python to be known as "python". I selected python2 because this is what it was on cygwin until a few days ago.
But I can check what happens if I link python to python3.8 instead and then choose that.

view this post on Zulip Michael Soegtrop (Dec 30 2020 at 10:47):

Btw: this package is only built on cygwin because the cygwin supplied package is outdated.

view this post on Zulip Théo Zimmermann (Dec 30 2020 at 11:04):

Ah, then I should update the comment I put in https://github.com/coq/coq/pull/13692! I wrongly assumed that you were replacing the python link to python3 by a link to python2 (because of the -f option).

view this post on Zulip Michael Soegtrop (Dec 30 2020 at 11:19):

@Théo Zimmermann : I just have the -f option in my script because the script might be rerun and I was too lazy to write a check if the symlink is there.

view this post on Zulip Théo Zimmermann (Dec 30 2020 at 11:20):

I see thanks!


Last updated: Jan 30 2023 at 10:03 UTC