8.13+beta1 release · Coq Platform devs & users

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

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

Enrico Tassi (Dec 07 2020 at 10:27):

$ ./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

Enrico Tassi (Dec 07 2020 at 10:27):

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.

Michael Soegtrop (Dec 07 2020 at 10:28):

Enrico Tassi (Dec 07 2020 at 10:30):

Michael Soegtrop (Dec 07 2020 at 10:31):

Michael Soegtrop (Dec 07 2020 at 10:34):

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"

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)

Enrico Tassi (Dec 07 2020 at 10:41):

Michael Soegtrop (Dec 07 2020 at 10:41):

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.

Michael Soegtrop (Dec 07 2020 at 10:42):

Michael Soegtrop (Dec 07 2020 at 10:43):

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

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.

Michael Soegtrop (Dec 07 2020 at 10:46):

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 ;-)

Enrico Tassi (Dec 07 2020 at 10:49):

Michael Soegtrop (Dec 07 2020 at 10:51):

Enrico Tassi (Dec 07 2020 at 10:51):

Michael Soegtrop (Dec 07 2020 at 10:51):

Enrico Tassi (Dec 07 2020 at 10:51):

Enrico Tassi (Dec 07 2020 at 10:52):

Michael Soegtrop (Dec 07 2020 at 10:53):

Enrico Tassi (Dec 07 2020 at 10:54):

Enrico Tassi (Dec 07 2020 at 10:55):

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

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.

Michael Soegtrop (Dec 07 2020 at 10:58):

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.

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 /.

Enrico Tassi (Dec 07 2020 at 14:19):

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.

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)

Michael Soegtrop (Dec 07 2020 at 15:01):

Enrico Tassi (Dec 07 2020 at 15:01):

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

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:

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

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.

Michael Soegtrop (Dec 07 2020 at 15:04):

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?

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.

Michael Soegtrop (Dec 07 2020 at 15:07):

Enrico Tassi (Dec 07 2020 at 15:08):

Théo Zimmermann (Dec 07 2020 at 16:28):

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.

Enrico Tassi (Dec 07 2020 at 16:31):

Théo Zimmermann (Dec 07 2020 at 16:41):

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?

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...

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.

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!

Enrico Tassi (Dec 07 2020 at 20:37):

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.

Théo Zimmermann (Dec 07 2020 at 20:44):

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

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).

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.

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.

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.

Enrico Tassi (Dec 07 2020 at 20:56):

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.

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...

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).

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.

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.

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

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.

Enrico Tassi (Dec 08 2020 at 09:24):

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...

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.

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

Cyril Cohen (Dec 08 2020 at 10:48):

Cyril Cohen (Dec 08 2020 at 10:50):

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.

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 ?

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...

Théo Zimmermann (Dec 08 2020 at 11:23):

Théo Zimmermann (Dec 08 2020 at 11:24):

Emilio Jesús Gallego Arias (Dec 08 2020 at 13:15):

Paolo Giarrusso (Dec 08 2020 at 16:51):

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.

Paolo Giarrusso (Dec 08 2020 at 16:52):

Paolo Giarrusso (Dec 08 2020 at 16:53):

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.

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.

Enrico Tassi (Dec 08 2020 at 20:05):

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).

Paolo Giarrusso (Dec 08 2020 at 20:05):

Paolo Giarrusso (Dec 08 2020 at 20:07):

Paolo Giarrusso (Dec 08 2020 at 20:09):

Enrico Tassi (Dec 08 2020 at 20:10):

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

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)

Cyril Cohen (Dec 08 2020 at 20:12):

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.

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.

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.

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.

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.

Michael Soegtrop (Dec 09 2020 at 08:42):

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.

Enrico Tassi (Dec 09 2020 at 08:53):

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

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

Théo Zimmermann (Dec 09 2020 at 10:49):

Enrico Tassi (Dec 09 2020 at 13:04):

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).

Théo Zimmermann (Dec 09 2020 at 13:11):

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.

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.

Théo Zimmermann (Dec 09 2020 at 13:24):

Théo Zimmermann (Dec 09 2020 at 13:25):

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?

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.

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...

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 ;-)

Enrico Tassi (Dec 09 2020 at 13:52):

Emilio Jesús Gallego Arias (Dec 09 2020 at 14:07):

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.

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...)

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?

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.

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?

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.

Enrico Tassi (Dec 09 2020 at 14:37):

Enrico Tassi (Dec 09 2020 at 14:38):

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.

Enrico Tassi (Dec 09 2020 at 14:39):

Enrico Tassi (Dec 09 2020 at 14:40):

Michael Soegtrop (Dec 09 2020 at 14:40):

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.

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.

Michael Soegtrop (Dec 09 2020 at 14:44):

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.

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?

Enrico Tassi (Dec 10 2020 at 13:51):

Emilio Jesús Gallego Arias (Dec 10 2020 at 13:57):

Andrew Appel (Dec 14 2020 at 14:21):

Emilio Jesús Gallego Arias (Dec 14 2020 at 14:31):

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.

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.

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".

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.

Enrico Tassi (Dec 14 2020 at 17:43):

Michael Soegtrop (Dec 14 2020 at 17:45):

Enrico Tassi (Dec 14 2020 at 17:57):

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?

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?

Michael Soegtrop (Dec 15 2020 at 10:31):

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

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.

Enrico Tassi (Dec 15 2020 at 10:33):

Enrico Tassi (Dec 15 2020 at 10:34):

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)

Michael Soegtrop (Dec 15 2020 at 10:35):

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

Enrico Tassi (Dec 15 2020 at 10:36):

Michael Soegtrop (Dec 15 2020 at 10:36):

Enrico Tassi (Dec 15 2020 at 10:36):

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

Michael Soegtrop (Dec 15 2020 at 10:37):

Enrico Tassi (Dec 15 2020 at 10:37):

Michael Soegtrop (Dec 15 2020 at 10:38):

Enrico Tassi (Dec 15 2020 at 10:38):

Michael Soegtrop (Dec 15 2020 at 10:39):

Enrico Tassi (Dec 15 2020 at 11:11):

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.

Michael Soegtrop (Dec 15 2020 at 11:19):

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.

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.

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.

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.

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?

Enrico Tassi (Dec 15 2020 at 12:54):

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.

Michael Soegtrop (Dec 15 2020 at 13:05):

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.

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?

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.

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.

Enrico Tassi (Dec 15 2020 at 13:52):

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?

Enrico Tassi (Dec 15 2020 at 14:23):

========== 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).

Andrew Appel (Dec 15 2020 at 14:33):

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

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.

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

Enrico Tassi (Dec 15 2020 at 15:06):

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.

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.

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.

Enrico Tassi (Dec 20 2020 at 18:19):

Michael Soegtrop (Dec 20 2020 at 18:46):

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

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.

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.

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).

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.

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?

Michael Soegtrop (Dec 21 2020 at 11:44):

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.

Enrico Tassi (Dec 21 2020 at 12:16):

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)

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'...

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.

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.

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).

Enrico Tassi (Dec 21 2020 at 12:29):

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).

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.

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.

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.

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.

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.

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?

Enrico Tassi (Dec 22 2020 at 13:53):

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).

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).

Enrico Tassi (Dec 22 2020 at 13:56):

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.

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.

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.

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.

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.

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.

Enrico Tassi (Dec 28 2020 at 10:09):

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.

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?

Karl Palmskog (Dec 29 2020 at 17:58):

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 ...

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.

Théo Zimmermann (Dec 30 2020 at 06:40):

Théo Zimmermann (Dec 30 2020 at 06:42):

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.

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.

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.

Théo Zimmermann (Dec 30 2020 at 10:29):

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.

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.

Michael Soegtrop (Dec 30 2020 at 10:47):

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

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).

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.

Stream: Coq Platform devs & users

Topic: 8.13+beta1 release

Michael Soegtrop (Dec 07 2020 at 10:06):

Enrico Tassi (Dec 07 2020 at 10:16):

Enrico Tassi (Dec 07 2020 at 10:27):

Enrico Tassi (Dec 07 2020 at 10:27):

Michael Soegtrop (Dec 07 2020 at 10:27):

Michael Soegtrop (Dec 07 2020 at 10:28):

Michael Soegtrop (Dec 07 2020 at 10:28):

Enrico Tassi (Dec 07 2020 at 10:30):

Enrico Tassi (Dec 07 2020 at 10:30):

Michael Soegtrop (Dec 07 2020 at 10:31):

Michael Soegtrop (Dec 07 2020 at 10:34):

Enrico Tassi (Dec 07 2020 at 10:35):

Enrico Tassi (Dec 07 2020 at 10:38):

Enrico Tassi (Dec 07 2020 at 10:41):

Enrico Tassi (Dec 07 2020 at 10:41):

Michael Soegtrop (Dec 07 2020 at 10:41):

Michael Soegtrop (Dec 07 2020 at 10:42):

Michael Soegtrop (Dec 07 2020 at 10:42):

Michael Soegtrop (Dec 07 2020 at 10:43):

Michael Soegtrop (Dec 07 2020 at 10:45):

Michael Soegtrop (Dec 07 2020 at 10:46):

Enrico Tassi (Dec 07 2020 at 10:48):

Enrico Tassi (Dec 07 2020 at 10:48):

Enrico Tassi (Dec 07 2020 at 10:48):

Enrico Tassi (Dec 07 2020 at 10:49):

Michael Soegtrop (Dec 07 2020 at 10:51):

Enrico Tassi (Dec 07 2020 at 10:51):

Michael Soegtrop (Dec 07 2020 at 10:51):

Enrico Tassi (Dec 07 2020 at 10:51):

Enrico Tassi (Dec 07 2020 at 10:52):

Michael Soegtrop (Dec 07 2020 at 10:53):

Enrico Tassi (Dec 07 2020 at 10:54):

Enrico Tassi (Dec 07 2020 at 10:55):

Enrico Tassi (Dec 07 2020 at 10:55):

Michael Soegtrop (Dec 07 2020 at 10:55):

Michael Soegtrop (Dec 07 2020 at 10:57):

Michael Soegtrop (Dec 07 2020 at 10:58):

Michael Soegtrop (Dec 07 2020 at 10:59):

Guillaume Melquiond (Dec 07 2020 at 14:10):

Enrico Tassi (Dec 07 2020 at 14:19):

Michael Soegtrop (Dec 07 2020 at 15:00):

Enrico Tassi (Dec 07 2020 at 15:00):

Michael Soegtrop (Dec 07 2020 at 15:01):

Enrico Tassi (Dec 07 2020 at 15:01):

Enrico Tassi (Dec 07 2020 at 15:02):

Michael Soegtrop (Dec 07 2020 at 15:03):

Enrico Tassi (Dec 07 2020 at 15:04):

Enrico Tassi (Dec 07 2020 at 15:04):

Michael Soegtrop (Dec 07 2020 at 15:04):

Michael Soegtrop (Dec 07 2020 at 15:04):

Michael Soegtrop (Dec 07 2020 at 15:05):

Michael Soegtrop (Dec 07 2020 at 15:07):

Michael Soegtrop (Dec 07 2020 at 15:07):

Enrico Tassi (Dec 07 2020 at 15:08):

Enrico Tassi (Dec 07 2020 at 15:08):

Théo Zimmermann (Dec 07 2020 at 16:28):

Enrico Tassi (Dec 07 2020 at 16:31):

Théo Zimmermann (Dec 07 2020 at 16:41):

Théo Zimmermann (Dec 07 2020 at 16:43):

Enrico Tassi (Dec 07 2020 at 17:54):

Théo Zimmermann (Dec 07 2020 at 20:07):

Emilio Jesús Gallego Arias (Dec 07 2020 at 20:15):

Enrico Tassi (Dec 07 2020 at 20:37):

Théo Zimmermann (Dec 07 2020 at 20:44):

Théo Zimmermann (Dec 07 2020 at 20:48):

Michael Soegtrop (Dec 07 2020 at 20:51):

Michael Soegtrop (Dec 07 2020 at 20:52):

Enrico Tassi (Dec 07 2020 at 20:56):

Enrico Tassi (Dec 07 2020 at 20:56):

Paolo Giarrusso (Dec 08 2020 at 07:07):

Paolo Giarrusso (Dec 08 2020 at 07:09):

Paolo Giarrusso (Dec 08 2020 at 07:10):

Enrico Tassi (Dec 08 2020 at 07:32):

Karl Palmskog (Dec 08 2020 at 07:35):

Enrico Tassi (Dec 08 2020 at 08:33):

Théo Zimmermann (Dec 08 2020 at 08:57):

Enrico Tassi (Dec 08 2020 at 09:24):

Enrico Tassi (Dec 08 2020 at 09:24):