Stream: CUDW 2020

Topic: WG: Coq Platform


view this post on Zulip Karl Palmskog (Nov 23 2020 at 01:40):

Although we have a Coq Platform stream, I'm setting up this topic for the Platform working group at CUDW.

view this post on Zulip Enrico Tassi (Nov 30 2020 at 10:38):

Plan:

view this post on Zulip Michael Soegtrop (Nov 30 2020 at 12:05):

What is missing from opam is a user friendly package name. E.g. for "coq-menhirlib" the synopsis is "A support library for verified Coq parsers produced by Menhir" which is not suitable as display name in the component selection list. But "coq-menhirlib" is not that nice either ...

view this post on Zulip Michael Soegtrop (Nov 30 2020 at 12:05):

For the tim beeing I will use the opam package name

view this post on Zulip Michael Soegtrop (Nov 30 2020 at 14:03):

@Enrico Tassi : I am AFK for an hour or so.

view this post on Zulip Enrico Tassi (Nov 30 2020 at 14:08):

ok

view this post on Zulip Enrico Tassi (Nov 30 2020 at 14:09):

So far I have

view this post on Zulip Michael Soegtrop (Nov 30 2020 at 15:52):

If you need help with the Coq platform scripts, please let me know. I have most of the NSIS input but need to improve the dependencies further. I will join Jason's Ph.D. defense now.

view this post on Zulip Enrico Tassi (Nov 30 2020 at 15:58):

I'm testing my last push on v8.13 on windows, it seems to compile

view this post on Zulip Enrico Tassi (Nov 30 2020 at 15:58):

I had to disable a few packages, but I've pinned most of them, I'll finish tomorrow

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 08:33):

@Andrej Dudenhefner : please ping me when you have time for a Coq platform discussion.

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 08:38):

@Enrico Tassi : how are things going? Do you need help with anything on the 8.13 branch? My plan is to create updated opam packages for CompCert and VST today - if this helps you, I can do it right away.

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

Hi, I have a few more packages to port before compcert and vst, so no hurry

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 08:50):

OK, let me know 2 hours before you need it. I will continue with the installer creator scripts then.

view this post on Zulip Andrej Dudenhefner (Dec 01 2020 at 08:59):

@Michael Soegtrop I'm available today from now up until 14:00 CET.

view this post on Zulip Enrico Tassi (Dec 01 2020 at 09:03):

@Cyril Cohen you told me you were working on a mathcomp 1.12 compatible release of some packages. I need suitable versions/hash for these packages

#PACKAGES="${PACKAGES} coq-mathcomp-bigenough.1.0.0"
#PACKAGES="${PACKAGES} coq-mathcomp-finmap.1.5.0"
#PACKAGES="${PACKAGES} coq-mathcomp-real-closed.1.1.1"

Hints?

view this post on Zulip Cyril Cohen (Dec 01 2020 at 09:11):

Not available yet

view this post on Zulip Cyril Cohen (Dec 01 2020 at 09:11):

Maybe tomorrow surely by the wnd of the week

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

@Andrej Dudenhefner : let's meet after the current sync up in a break out room.

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 09:23):

@Andrej Dudenhefner : The platform project os here: https://github.com/coq/platform

view this post on Zulip Andrej Dudenhefner (Dec 01 2020 at 10:36):

@Michael Soegtrop The Coq platform installed and opam list looks fine. I continued to build my current project but it failed: opam-failed.jpg

view this post on Zulip Yannick Forster (Dec 01 2020 at 10:48):

@Andrej Dudenhefner We had this problem in the lecture as well, but I was unable to fix it although spending some time on it

view this post on Zulip Yannick Forster (Dec 01 2020 at 10:48):

I think the issue is this line: https://github.com/MetaCoq/metacoq/blob/a64fa5052873e6b0725fa4e84931a51f9c2da2eb/template-coq/update_plugin.sh#L17

view this post on Zulip Yannick Forster (Dec 01 2020 at 10:49):

This patches the result of Coq's extraction, because there is a bug resulting in an ill-typed Ocaml program

view this post on Zulip Yannick Forster (Dec 01 2020 at 10:50):

But I'm not entirely sure: The patch applies to line 104 if I understand correctly, and your error occurs in line 204.

view this post on Zulip Yannick Forster (Dec 01 2020 at 10:50):

@Matthieu Sozeau might be able to help

view this post on Zulip Yannick Forster (Dec 01 2020 at 10:51):

Can you somehow inspect the generated ml file @Andrej Dudenhefner?

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 11:10):

@Andrej Dudenhefner @Yannick Forster : can you tell me under which circumstances this does build? E.g. does it require Coq master or Coq 8.12.1? It wouldn't be much of an issue to update to Coq 8.12.1. Maybe you can provide a shell script with opam install commands which does build from an empty switch on some platform.

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

@Andrej Dudenhefner : opam keeps the files of failed builds. If you need help with this, please let me know. You can also cd into the opam build folder of the package and do local incremental builds there.

view this post on Zulip Yannick Forster (Dec 01 2020 at 11:11):

We're in breakout room 1. The issue is that the patch is not applied due to having the wrong line endings

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 11:12):

I join

view this post on Zulip Yannick Forster (Dec 01 2020 at 11:14):

Here's the file: https://raw.githubusercontent.com/MetaCoq/metacoq/coq-8.11/template-coq/extraction.patch

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 11:26):

@Yannick Forster : regarding sed on Mac: it is as I remembered. The backup extension is obligatory on BSD with the inplace option.

view this post on Zulip Yannick Forster (Dec 01 2020 at 11:27):

Thanks!

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 11:31):

Did you manage to solve the problem?

view this post on Zulip Yannick Forster (Dec 01 2020 at 11:31):

No, but we're close :) It's a Windows line ending issue

view this post on Zulip Yannick Forster (Dec 01 2020 at 11:36):

Here's the patch file: https://gist.githubusercontent.com/yforster/b5596a32377f23c18344f5a04038c3a7/raw/cc7eb9d79c0e313c0b73943b5f3831e1abc54292/metacoq-lineendings.patch

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

@Michael Soegtrop Branch https://github.com/coq/platform/tree/v8.13 build here (on windows) disabling compcert and vst.
Only one package, which I commented out, has no 8.13-compatible version yet (coq-mathcomp-realclosed CC @Cyril Cohen ).
Commit messages like "pin foo version" mean that "foo" already has a tag (possibly even an opam package) for 8.13.
Commit messages like "pin foo hash version" mean that I could find a hash that works, that I did pick a "arbitrary" version and made an opam package for it in the overlay folder

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 11:40):

@Enrico Tassi : perfect, thanks!

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

This last class of commit is something I don't really like, this is why I did notify all upstream asking them to tag. See the linked issues in https://github.com/coq/coq/issues/12334

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 11:45):

@Yannick Forster : coq-metacoq is a metapackage without any sources. Which of the sub packages needs this patch?

view this post on Zulip Yannick Forster (Dec 01 2020 at 11:45):

coq-metacoq-template

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 11:45):

OK

view this post on Zulip Yannick Forster (Dec 01 2020 at 11:46):

Lets hope that suffices, depending on the build process every other metacoq package might need the patch as well because they all build from the same repo (but different subdirectories)

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 11:47):

Possibly checker needs it as well

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 11:48):

I think the other are safe (i.e. we're not recompiling template-coq in the others but using the one that is already installed)

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 11:49):

We will see. I create the opam patch package - if you have this as template it should be easy to do.

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 11:49):

Alternatively, changing the metacoq-checker opam file to do make -C checker would solve this

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 11:54):

@Enrico Tassi : I think it is OK for a beta and in the future even for a Coq release. One of the reasons for having teh platform is to solve the hen and egg problem. The intended procedure is:

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 11:56):

@Yannick Forster : I have some strange errors when opam tries to retrieve the packages. We have lunch now. I will ping you after lunch.

view this post on Zulip Yannick Forster (Dec 01 2020 at 11:57):

Okay, I should be available all afternoon. Guten Appetit! ;)

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 12:55):

I pushed a commit to the v8.12 branch of Coq platform. To update the cygwin, just pull (or doanload a new zip) and run the batch file again. Alternatively you can just sync the opam folder with the opam folder in the ~/platform folder in the created cygwin.

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 12:55):

coq-metacoq-template.1.0~beta1+8.12 runs through now, but time seems to be missing.

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 12:57):

@Yannick Forster @Andrej Dudenhefner : can you explain what you want to achieve with the conf-time opam package dependenca? Time is usually a shell built in, so the which time as check in the conf-time package likely fails on many system.

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

I am AFK for on hour or so. In case you need further patches, it is easy:

The opam patch repo of the platform is a convenient way to get things working and also makes it easy to push thing supstream as soon as they work and are tested a bit.

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 13:13):

@Michael Soegtrop I think we need the unix time command

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 13:14):

@Michael Soegtrop but we don't really need it to build, if that's a problem on Windows

view this post on Zulip Yannick Forster (Dec 01 2020 at 13:24):

I remember we added the conf-time after @Karl Palmskog suggested it to @Matthieu Sozeau

view this post on Zulip Yannick Forster (Dec 01 2020 at 13:25):

Oh, Matthieu already answered, sorry. I was narrowed down to mentions in the Zulip view

view this post on Zulip Yannick Forster (Dec 01 2020 at 13:27):

Karl might still be able to help: We need time to have MetaCoq work correctly. Either we get rid of this dependency, or we install metacoq via a patched opam file on the long run in Coq platform and accept that certain things won't work

view this post on Zulip Yannick Forster (Dec 01 2020 at 13:28):

So it should be a general issue for packages depending on conf-time. Maybe coq-platform should just install time in Cygwin?

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 13:40):

We can easily remove the reliance on time

view this post on Zulip Yannick Forster (Dec 01 2020 at 13:42):

Maybe that's the way to go then

view this post on Zulip Karl Palmskog (Dec 01 2020 at 13:51):

we needed conf-time as a dependency because it was the only way to get clean-slate Linux builds to work. One middle ground would be to add it as a test dependency.

view this post on Zulip Karl Palmskog (Dec 01 2020 at 13:52):

then you can run time-based build if you pass the testing option to opam

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

It would help if you could point me to the command line you use with time. I understand that you use features, which are not included in the shell version of time.

view this post on Zulip Karl Palmskog (Dec 01 2020 at 14:37):

@Michael Soegtrop they use the timing feature with coq_makefile, where one passes TIMECMD or it defaults to some OS-specific stuff

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

I see, so you need time to be not a shell built in so that you can pass it as command in TIMECMD, but you don't need fancy features of it, e.g. computing the max working set of a process tree.

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 16:41):

@Yannick Forster @Andrej Dudenhefner : actually depext does work fine on cygwin. So what you have to do is:

opam depext coq-metacoq
opam install coq-metacoq

The platform setup scripts call opam depext for the packages which need it. In my tests I did opam depext conf-time, but giving meta-coq should also work. Now I get:

#=== ERROR while compiling coq-metacoq-checker.1.0~beta1+8.12 =================#
# context     2.0.7 | win32/x86_64 | ocaml-variants.4.07.1+mingw64c | https://coq.inria.fr/opam/released#2020-12-01 04:40
# path        ~/.opam/_coq-platform_.8.12.0+beta1/.opam-switch/build/coq-metacoq-checker.1.0~beta1+8.12
# command     T:\bin\cygwin_coqplatform_8_12_0\bin\make.exe -j16 checker
# exit-code   2
# env-file    ~/.opam/log/coq-metacoq-checker-265544-a71bb4.env
# output-file ~/.opam/log/coq-metacoq-checker-265544-a71bb4.out
### output ###
# Error: The implementation gen-src/cRelationClasses.ml
# [...]
#        File "gen-src/cRelationClasses.mli", line 107, characters 0-46:
#          Expected declaration
#        File "gen-src/cRelationClasses.ml", line 204, characters 4-18:
#          Actual declaration
# make[3]: *** [Makefile.plugin:664: gen-src/cRelationClasses.cmx] Error 2
# make[3]: *** Waiting for unfinished jobs....
# make[2]: *** [Makefile.plugin:339: all] Error 2
# make[2]: Leaving directory '/home/Michael/.opam/_coq-platform_.8.12.0+beta1/.opam-switch/build/coq-metacoq-checker.1.0~beta1+8.12/template-coq'
# make[1]: *** [Makefile:20: plugin] Error 2
# make[1]: Leaving directory '/home/Michael/.opam/_coq-platform_.8.12.0+beta1/.opam-switch/build/coq-metacoq-checker.1.0~beta1+8.12/template-coq'
# make: *** [Makefile:51: template-coq] Error 2

Is this the same issue as in coq-metacoq-template?

view this post on Zulip Yannick Forster (Dec 01 2020 at 16:42):

Yes, it's the same issue, and it can be fixed the same way

view this post on Zulip Yannick Forster (Dec 01 2020 at 16:44):

This might mean there's something wrong with the coq-metacoq-checker package though: Do we really need to recompile template-coq when installing the checker package? @Matthieu Sozeau? That means we're somewhat quadratic in the number of subprojects

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 16:44):

Do you want to give it a try - I would be interested to know how easy/difficult you find the opam patch repo to use - or shall I do it?

view this post on Zulip Yannick Forster (Dec 01 2020 at 16:44):

I can do it

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 16:46):

OK, fine. Please let me know how it goes.

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 16:47):

@Andrej Dudenhefner : can we review your issue with coq-gappa? I just tried it and it did work fine for me. I would be interested to inspect the log files.

view this post on Zulip Andrej Dudenhefner (Dec 01 2020 at 16:49):

@Michael Soegtrop Yes, where can I find the log files?

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 16:50):

@Andrej Dudenhefner let's have a quick breakout session

view this post on Zulip Andrej Dudenhefner (Dec 01 2020 at 16:50):

OK.

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 16:51):

Room 7 ...

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 17:12):

I had a discussion with @Andrej Dudenhefner on the default path for the cygwin installation on Windows (currently C:\bin\cygwin_coqplatform_8_12_0). Andrej doesn't find this very agreeable. What would be the preference of others?
I can also make the batch file such that it suggests a few options one can select by entering a number or enter a path if none is given on the command line.

view this post on Zulip Andrej Dudenhefner (Dec 01 2020 at 17:13):

(in particular, C:\bin is a folder that under Windows can be occupied/polluted by something else entirely)

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

Yes but I would think that most people/SW create a subfolder under C:\bin and do not put stuff directly there. I use C:\bin for everything which is more command line stuff than a Windows app (say ffmpeg, imagemagick, ...).

view this post on Zulip Enrico Tassi (Dec 01 2020 at 18:17):

Would c:\coq_platform\ be more safe?

view this post on Zulip Michael Soegtrop (Dec 01 2020 at 18:42):

That's what Andrej suggested.

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 21:04):

Yannick Forster said:

This might mean there's something wrong with the coq-metacoq-checker package though: Do we really need to recompile template-coq when installing the checker package? Matthieu Sozeau? That means we're somewhat quadratic in the number of subprojects

Indeed, but that's just for the checker. That's why I suggested using make -C checker in the opam file instead

view this post on Zulip Paolo Giarrusso (Dec 01 2020 at 22:53):

IIRC on Windows you'll want short-ish paths (C:\coq_platform is okay), Haskell-stack still run into the 256char limit for paths somewhat recently (so they used C:\stack)

view this post on Zulip Paolo Giarrusso (Dec 01 2020 at 22:54):

I'm not up-to-date nor a Windows user, but see e.g. https://github.com/commercialhaskell/stack/issues/3285 from 2017

view this post on Zulip Paolo Giarrusso (Dec 01 2020 at 22:56):

Oh okay there's also https://github.com/ocaml/dune/issues/2991 ?

view this post on Zulip Paolo Giarrusso (Dec 01 2020 at 22:59):

On paths, I'd also object to c:\bin, the old usual thing is c:\name_of_your_program; the new advice demands "C:\Program Files" (but path lengrh and spaces intefere)

view this post on Zulip Yannick Forster (Dec 02 2020 at 07:46):

@Matthieu Sozeau The opam file of the checker does call make -C checker. Or do you mean in the opam file of template-coq we should use make -C checker?

view this post on Zulip Michael Soegtrop (Dec 02 2020 at 08:25):

Regarding the name: OK, I will use C:\coq_platform as default then but also add a question to the batch file in case no path is given on the comman dline.

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

@Enrico Tassi : the base library also has a wrong dependency (on sexplib and jbuilder) which is not in the opam file:

$ opam list --required-by=base
# Packages matching: (installed | available) & required-by(base)
# Name            # Installed # Synopsis
dune              2.7.0b      Fast, portable, and opinionated build system
dune-configurator 2.7.1       Helper library for gathering system configuration
jbuilder          --          This is a transition package, jbuilder is now named dune. Use the dune
ocaml             4.07.1      The OCaml compiler (virtual package)
sexplib           --          Library for serializing OCaml values to and from S-expressions
sexplib0          v0.14.0     Library containing the definition of S-expressions and some base converters

Furthermore there is a longer cyclic dependency as follows:

33 sexplib parsexp
32 parsexp ppx_sexp_value
31 ppx_sexp_value ppx_sexp_conv
30 ppx_sexp_conv ppx_type_conv
29 ppx_type_conv ppx_metaquot
28 ppx_metaquot ppx_driver
27 ppx_driver ppx_optcomp
26 ppx_optcomp ppx_core
25 ppx_core ppx_ast
24 ppx_ast ppxlib
23 ppxlib stdio
22 stdio sexplib

Need to check which of these is wrong

view this post on Zulip Michael Soegtrop (Dec 02 2020 at 09:53):

The dependency parsexp ppx_sexp_value is not in the opam file.

view this post on Zulip Andrej Dudenhefner (Dec 02 2020 at 09:56):

Small remark for the windows installer (we had an additional metacoq installation problem): on windows coqc -where adds a carriage return which is problematic in configure scripts.
windows-coqc-where.jpg

view this post on Zulip Michael Soegtrop (Dec 02 2020 at 09:58):

@Andrej Dudenhefner : yes you need to filter the output of coqc -where with tr.

view this post on Zulip Michael Soegtrop (Dec 02 2020 at 09:59):

@Enrico Tassi : there is an interesting side to the wrong depenencies reported by opam: non of the wrong dependencies are installed. So if I use opam --required-by=xxx --installed, they go away.

view this post on Zulip Andrej Dudenhefner (Dec 02 2020 at 10:00):

@Michael Soegtrop today I also tried to reproduce the gappa bug, but everything went well.

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

e.g.

$ opam list --required-by=base
# Packages matching: (installed | available) & required-by(base)
# Name            # Installed # Synopsis
dune              2.7.0b      Fast, portable, and opinionated build system
dune-configurator 2.7.1       Helper library for gathering system configuration
jbuilder          --          This is a transition package, jbuilder is now named dune. Use the dune
ocaml             4.07.1      The OCaml compiler (virtual package)
sexplib           --          Library for serializing OCaml values to and from S-expressions
sexplib0          v0.14.0     Library containing the definition of S-expressions and some base converters

$ opam list --required-by=base --installed
# Packages matching: installed & required-by(base)
# Name            # Installed # Synopsis
dune              2.7.0b      Fast, portable, and opinionated build system
dune-configurator 2.7.1       Helper library for gathering system configuration
ocaml             4.07.1      The OCaml compiler (virtual package)
sexplib0          v0.14.0     Library containing the definition of S-expressions and some base converters

view this post on Zulip Michael Soegtrop (Dec 02 2020 at 10:01):

@Andrej Dudenhefner : thanks! please keep an eye open!

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

@Enrico Tassi : I will add --installed then and report this as a bug to opam.

view this post on Zulip Matthieu Sozeau (Dec 02 2020 at 10:13):

Yannick Forster said:

Matthieu Sozeau The opam file of the checker does call make -C checker. Or do you mean in the opam file of template-coq we should use make -C checker?

Hmm, I'm looking at a different version of metacoq then, that's why. We stopped making check checker plugin in the current 8.11 branch

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

@Enrico Tassi : the dependency script does work now. The highest level in the dependency tree (at level 12) has elpi :-)

view this post on Zulip Enrico Tassi (Dec 02 2020 at 10:17):

Eh... I know. Some of the dependencies of elpi are optional (even if the opam package does not say so). In particular the ppx stack is optional (in the old windows installer the only real dependency was "re"). We can make an overlay package if you like (to make the platform switch slim).

view this post on Zulip Enrico Tassi (Dec 02 2020 at 10:17):

So on windows build with the platform coqide works but you can't pass arguments to it because of https://github.com/coq/coq/pull/13546

view this post on Zulip Enrico Tassi (Dec 02 2020 at 10:18):

@Emilio Jesús Gallego Arias please give a look at that PR quickly

view this post on Zulip Enrico Tassi (Dec 02 2020 at 10:23):

It is sufficient to remove the ppx from the dependencies, the build system will figure out these libraries are not there and work around it.

view this post on Zulip Andrej Dudenhefner (Dec 02 2020 at 11:31):

@Michael Soegtrop after including @Yannick Forster 's patches for metacoq I was now able to install all the necessary dependencies under the coq platform (for Windows) and make the coq-library-undecidability project. Also vscode with vscoq work properly on the compiled files. So far everything is in order.

view this post on Zulip Michael Soegtrop (Dec 02 2020 at 12:48):

@Andrej Dudenhefner @Yannick Forster : can you please create a PR on Coq platform with the opam patches? Or is this already merged upstream?

view this post on Zulip Yannick Forster (Dec 02 2020 at 12:48):

No, it's on a branch of mine. Give me a minute

view this post on Zulip Yannick Forster (Dec 02 2020 at 12:51):

I filed a PR agains the v8.12 branch: https://github.com/coq/platform/pull/42

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

Thanks!

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

@Enrico Tassi : is there a coqc command to get a less verbose version string?

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

yup

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

-print-version

view this post on Zulip Michael Soegtrop (Dec 02 2020 at 12:53):

Perfect, thanks!

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

@Enrico Tassi : I pushed a first draft for the nsis installer script. I split it into two pieces - the first "windows/create_installer_windows.sh" extracts the information from opam and the second "windows/create_installer_windows_2.sh" creates the installer from that. I will later combine it, but since the first part takes considerable time it is easier to test this way. Both scripts are intended to be run from the coq-platform root folder in the created cygwin. The created installer still has a lot of defficiencies, but does something.

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

Ont thing: there are a few files I need which are not installed by opam, namely:

https://github.com/coq/coq/raw/v8.12/ide/coq.ico
https://github.com/coq/coq/raw/v8.12/LICENSE

Since these files don't change frequently I wget them, but a proper solution would be good.

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

I think I will rebase v8.13 on top of your commits so to have the scripts around and be able to run them in my VM, if it's OK for you.
BTW, I guess I need NSIS installed somewhere...

view this post on Zulip Michael Soegtrop (Dec 02 2020 at 16:03):

@Enrico Tassi : it is only one commit, so you can cherry pick it, but rebase should also work. I put it into 8.12, not master.
The scripts downloas NSIS - no need to install it anywhere.

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

Btw.: the opam folks say that the issue with --required-by is that it gives the requirements for all package versions, unless you give a package version. I also guess that this is faster when I give the package version. I can change that.

view this post on Zulip Andrej Dudenhefner (Dec 02 2020 at 17:06):

It is a little strange that coqc -where gives e.g. C:\bin\cygwin_coq_platform\home\user\.opam\_coq-platform_.8.12.0+beta1/lib/coq that contains both \ and / to navigate.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2020 at 17:12):

By the way I recommend you name the directory coq-platform-version as users may want to have several versions installed simultaneouly

view this post on Zulip Enrico Tassi (Dec 02 2020 at 18:04):

The version is in the path above.

view this post on Zulip Enrico Tassi (Dec 02 2020 at 18:05):

coqc -config is a bit of a mess on windows, but apparently paths with / in them still work fine.

view this post on Zulip Andrej Dudenhefner (Dec 02 2020 at 18:24):

but apparently paths with / in them still work fine.

To compile metacoq on windows the \ were problematic and we had to add tr '\\\\' '/'.

view this post on Zulip Michael Soegtrop (Dec 02 2020 at 18:27):

@Emilio Jesús Gallego Arias : you can use one coqplatform cygwin for several coq platform versions (different opam switches).

view this post on Zulip Michael Soegtrop (Dec 02 2020 at 18:29):

@Andrej Dudenhefner : all Windows C level system functions can handle both / and \ (even DOS could). Where it gets tricky is calling DOS command line tools, since the use / for options - they get frequently confused by /. Also some GUI tools get confused by /. But most stuff works fine with both. So I recommend to use in make files and other build systems always /. And always user relative paths!

view this post on Zulip Paolo Giarrusso (Dec 02 2020 at 19:54):

does \ cause exciting “double quote” issues? :-|

view this post on Zulip Michael Soegtrop (Dec 02 2020 at 20:01):

@Paolo Giarrusso : \ results in all sorts of issues. For this reason I wouldn't use it. Maybe we can do something about the back quotes in the Coq path.

view this post on Zulip Yannick Forster (Dec 03 2020 at 08:38):

Fixing the backquotes in the Coq path is probably the best solution for us. Currently MetaCoq's configure.sh script either configures the subprojects (which all have their own _CoqProject files) to depend on each other by using local paths, or configures them for an opam install to depend on installed packages - then we use coqc -where to find the path to put in the _CoqProjects. And that's where the \, \\, and \\\\ come in

view this post on Zulip Michael Soegtrop (Dec 03 2020 at 08:48):

@Yannick Forster : I see what I can do. I would think what coqc -where reports is what it is given during configure time and this should be easy to change in the opam file.

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

@Michael Soegtrop I managed to run the script and get an installer but it is too big. I believe that the script confuses "build dependencies" with "runtime dependencies"

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

example ${CheckHiddenSectionDependency} ${Sec_elpi} ${Sec_dune}, elpi need dune to build, but not to run

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

after fiddling with the installer, it seems 1/2 of the space (~700M) is taken by these

view this post on Zulip Michael Soegtrop (Dec 03 2020 at 08:56):

@Enrico Tassi : there are two things: first compression is off because it takes literally forever and then yes, it includes a lot of stuff which is only required for build put this is not always distinguished at opam level. Definitely there needs to be a package filtering. My strategy is to make first somethign that works and then strip it down.

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

ok, then I'll look at the script to see if it's easy to tell build dependencies

view this post on Zulip Michael Soegtrop (Dec 03 2020 at 08:57):

Well bat that is not what the opam file of elpi says:

depends: [
  "ocaml" {>= "4.04.0"}
  "camlp5" {< "7.99"}
  "ppxlib" {>= "0.12.0" & < "0.15.0"}
  "ocaml-migrate-parsetree" {>= "1.6.0"}
  "ppx_deriving"
  "re" {>= "1.7.2"}
  "ANSITerminal" {with-test}
  "cmdliner" {with-test}
  "dune" {>= "2.2.0"}
  "conf-time" {with-test}
]

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

The opam files need to be fixed.

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

I can improve that for sure

view this post on Zulip Michael Soegtrop (Dec 03 2020 at 09:00):

Hmm, I though there was a separate "depends-build" or so, but I can't find it right now ...

view this post on Zulip Michael Soegtrop (Dec 03 2020 at 09:00):

Maybe I am mixing it up with MacPorts or another packager.

view this post on Zulip Enrico Tassi (Dec 03 2020 at 09:00):

I'll double check, IIRCyou can {build} and I do for {with-test}

view this post on Zulip Enrico Tassi (Dec 03 2020 at 09:01):

I can look at that, gappa also pulls in "c++", if it's true it's all inlined...

view this post on Zulip Michael Soegtrop (Dec 03 2020 at 09:02):

Anyway - for the time beeing the idea is to have a package and/or file name filter. We can make a cleaner solution later. For the time beeing, as I said let's first do something that works and then strip it down.

view this post on Zulip Enrico Tassi (Dec 03 2020 at 09:07):

Do you want me to work on this filtering by name feature?

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

(It's blocking for the release, IMO, 1.4G is not an option)

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

@Enrico: sure - it would definitely help to think about how to do the filtering. Before you implement it, you should wait for my next release, though. Should not be more than 1 hour from now.

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

ok ok, I'm at the rewrite rule WG now

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

You can also enable compression (line 13+14 of Coq.nsi).

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

But as I said, it takes ages to build then.

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

@Enrico Tassi : just a small status update: NSIS 2.51 has bugs which stop me from doing what I want (short of very complicated hacks), so I had to update to the latest version. This seems to have the one blocking bg resolved - further investigating.

view this post on Zulip Michael Soegtrop (Dec 03 2020 at 11:12):

@Enrico Tassi : I pushed a new version (to the v8.12 branch). The main difference is that the dependency management when selecting or deselcting packages now works smoothly (better also than in the legacy installer). Maybe you can try it with mathcomp, where you know the dependencies. The management of hidden dependencies (the majority) is also going on when packages are selected or deselcted, so that the install size is correct. All in all it is a fairly tricky business, but I would say it is correct now.

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

By the way you should not add {build} to dune in opam as while packages don't need dune to run, they need to be rebuilt when dune version changes for the metadata (ppx etc...) to be correctly versioned. There is work in having a stable format but it's not there yet :( :(

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

I did add some support to slim packages https://github.com/coq/platform/commit/23135987b66c7b08ec263bdc16d7ef8d7d993eb6

view this post on Zulip Enrico Tassi (Dec 03 2020 at 14:24):

the installer is now half in size. it still does not work since some dll are missing (freetype, gtk, ...). I guess this is expected.

view this post on Zulip Enrico Tassi (Dec 03 2020 at 14:42):

I don't recall if you had plans on how to fix this or not (hence I can add an ad hoc list)

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

ldd .../coqide seems to work on cygwin, it gives me the DDLs in the cygwin installation, we could just copy those!

view this post on Zulip Enrico Tassi (Dec 03 2020 at 17:19):

This commit https://github.com/coq/platform/commit/fa99d4da9d8ef4432778d9f995b9de37b5c0a2c9 makes the installer ship a CoqIDE that runs.
Icons are not there.
If you enable lzma, then the installer is 190M which is OK.

view this post on Zulip Michael Soegtrop (Dec 03 2020 at 18:00):

Thanks, I will do some more tweaking and add the icons. I also thought about tracking down the conf-opam packages to system packages and get the file list from there and filter these. Btw.: the icon scheme is huge - I used to heavily filter it.

view this post on Zulip Enzo Crance (Dec 03 2020 at 18:34):

Hello. I have successfully installed the Coq Platform on macOS Catalina. Here are some details about how it went:

First the specs of my machine:

macOS 10.15.6
Xcode 11.4.1
Homebrew 2.6.0-68-g5ad9496
opam 2.0.6
install with 16GB RAM and 4 threads
yes to CompCert and VST

The script must have run a brew upgrade on all my installed packages or something, because a failed upgrade on an unrelated package made it fail. I had to relaunch the shell script and it resumed from where it had stopped.

Three packages were not installed: conf-gtk3, conf-gtksourceview3, and cairo2. The reason is libpng missing for the latter, thus a cairo.h include failing when compiling C files in the former.

At the end, I have a working coqc and coqtop which I have tried on a few files of mine (some stdlib handling and proofs with the Flocq floating-point arithmetic library). I have performed a full install, so if you need further testing, for example if you have a suggestion to test CompCert and VST, please tell me and I would be happy to help.

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

@Enzo Crance : thanks for testing and reporting - since I myself use MacPorts, there is not much testing on homebrew. The update is possibly done by opam depext - I don't do it explicitly.
I can check about the libpng. You are saying that cairo fails cause of this? This looks like a dependency issue in Homebrew, but one could possibly fix it on opam level by adding a libpng dependency. It might take a few iterations, though.

view this post on Zulip Michael Soegtrop (Dec 03 2020 at 21:14):

@Enrico Tassi : I made one more committ (https://github.com/coq/platform/commit/a0269e3ab27719cf09a25d9dc2f9a588c5d63dc0) which enhances the auto select/deselect of dependencies (only one message with a list of all packages and auto-changed packages are marked bold (sticky).

I also added the license text for CompCert and VST.

What is still missing is a larger dialog box and the icons for CoqIDE. About the latter we should have a quick discussion tomorrow.

view this post on Zulip Enzo Crance (Dec 03 2020 at 22:22):

I think I made a mistake in what I said earlier. The 2 conf-* packages depend on cairo, not cairo2, and opam install fails because of this line:

# Package 'libpng', required by 'cairo', not found

Concerning cairo2, it fails for the include reason I wrote about, and I am not sure what to conclude about it. Maybe opam does not call brew install cairo. Here is the explicit error message, so that the information is reliable:

#=== ERROR while compiling cairo2.0.6.1 =======================================#
# context     2.0.6 | macos/x86_64 | ocaml-base-compiler.4.07.1 | https://opam.ocaml.org/#9f32db57
# path        ~/.opam/_coq-platform_.8.12.0+beta1/.opam-switch/build/cairo2.0.6.1
# command     ~/.opam/opam-init/hooks/sandbox.sh build dune build -p cairo2 -j 4
# exit-code   1
# env-file    ~/.opam/log/cairo2-41502-1872ec.env
# output-file ~/.opam/log/cairo2-41502-1872ec.out
### output ###
# compiling c program:
# [...]
#  | };
#  |
# run: cc -Wno-implicit-function-declaration -O2 -fno-strict-aliasing -fwrapv  -I/usr/include/cairo -I /Users/cloudyhug/.opam/_coq-platform_.8.12.0+beta1/lib/ocaml -o /var/folders/0x/430g858n2z703mtpghf256y40000gn/T/ocaml-configuratorec3ecd/c-test-2/test.o -c /var/folders/0x/430g858n2z703mtpghf256y40000gn/T/ocaml-configuratorec3ecd/c-test-2/test.c
# -> process exited with code 1
# -> stdout:
# -> stderr:
#  | /var/folders/0x/430g858n2z703mtpghf256y40000gn/T/ocaml-configuratorec3ecd/c-test-2/test.c:2:10: fatal error: 'cairo.h' file not found
#  | #include <cairo.h>
#  |          ^~~~~~~~~
#  | 1 error generated.
# Error: failed to compile program

Here is the result for opam depext on these 3 packages:

# Detecting depexts using vars: arch=x86_64, os=macos, os-distribution=homebrew, os-family=homebrew
cairo2: cairo pkg-config
conf-gtk3: expat gtk+3 pkg-config
conf-gtksourceview3: gtksourceview3 libxml2 pkg-config

And finally, libpng seems to be installed on my machine...

$ brew info libpng
libpng: stable 1.6.37 (bottled), HEAD

view this post on Zulip Paolo Giarrusso (Dec 03 2020 at 23:12):

I use Coq and Homebrew. Here's what I get from opam depext conf-cairo:

$ opam depext conf-cairo
# Detecting depexts using vars: arch=x86_64, os=macos, os-distribution=homebrew, os-family=homebrew
# The following system packages are needed:
cairo
pkg-config
Warning: Calling `brew list` to only list formulae is deprecated! Use `brew list --formula` instead.
# All required OS packages found.

view this post on Zulip Paolo Giarrusso (Dec 03 2020 at 23:12):

that warning is from Brew, and it means that depext on brew is likely breaking a bit, which might relate to your bug.

view this post on Zulip Paolo Giarrusso (Dec 03 2020 at 23:13):

IME, Homebrew can remove deprecated features really quickly. And when they do, if your code breaks, you (= opam-depext) get to keep the pieces.

view this post on Zulip Paolo Giarrusso (Dec 03 2020 at 23:14):

(and don't dare ask them on their github bug tracker, that's their TODO list — but they created separate forums for open discussion)

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

@Enzo Crance : This is a bit confusing. From which opam command does the "# Package 'libpng', required by 'cairo', not found" come from? I have:

~$ opam list --required-by cairo2 --recursive
# Packages matching: (installed | available) & rec-required-by(cairo2)
# Name                   # Installed # Synopsis
base-bigarray            base
base-num                 --          Num library distributed with the OCaml compiler
base-ocamlbuild          --          OCamlbuild binary and libraries distributed with the OCaml compiler
base-threads             base
base-unix                base
cairo2                   0.6.1       Binding to Cairo, a 2D Vector Graphics Library
camlp4                   --          Camlp4 is a system for writing extensible parsers for programming languages
conf-cairo               1           Virtual package relying on a Cairo system installation
conf-expat               --          Virtual package relying on an expat system installation
conf-libX11              --          Virtual package relying on an Xlib system installation
conf-m4                  1           Virtual package relying on m4
conf-pkg-config          1.3         Virtual package relying on pkg-config installation
conf-which               1           Virtual package relying on which
csexp                    1.3.2       Parsing and printing of S-expressions in Canonical form
dune                     2.7.1       Fast, portable, and opinionated build system
dune-configurator        2.7.1       Helper library for gathering system configuration
dune-private-libs        --          Private libraries of Dune
graphics                 --          The OCaml graphics library
jbuilder                 --          This is a transition package, jbuilder is now named dune. Use the dune
lablgtk                  --          OCaml interface to GTK+
num                      1.3         The Num library for arbitrary-precision integer and rational arithmetic
ocaml                    4.07.1      The OCaml compiler (virtual package)
ocaml-base-compiler      4.07.1      Official release 4.07.1
ocaml-config             1           OCaml Switch Configuration
ocaml-secondary-compiler 4.08.1-1    OCaml 4.08.1 Secondary Switch Compiler
ocaml-system             --          The OCaml compiler (system version, from outside of opam)
ocaml-variants           --          current trunk
ocamlbuild               0.14.0      OCamlbuild is a build system with builtin rules to easily build most OCaml projects.
ocamlfind                1.8.1       A library manager for OCaml
ocamlfind-secondary      1.8.1       ocamlfind support for ocaml-secondary-compiler
result                   1.5         Compatibility Result module
~$ opam list --required-by cairo --recursive
# Packages matching: (installed | available) & rec-required-by(cairo)
# Name              # Installed # Synopsis
base-num            --          Num library distributed with the OCaml compiler
base-ocamlbuild     --          OCamlbuild binary and libraries distributed with the OCaml compiler
cairo               --          Binding to Cairo, a 2D Vector Graphics Library
camlp4              --          Camlp4 is a system for writing extensible parsers for programming languages
conf-autoconf       0.1         Virtual package relying on autoconf installation
conf-cairo          1           Virtual package relying on a Cairo system installation
conf-expat          --          Virtual package relying on an expat system installation
conf-m4             1           Virtual package relying on m4
conf-pkg-config     1.3         Virtual package relying on pkg-config installation
conf-which          1           Virtual package relying on which
lablgtk             --          OCaml interface to GTK+
num                 1.3         The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.07.1      The OCaml compiler (virtual package)
ocaml-base-compiler 4.07.1      Official release 4.07.1
ocaml-config        1           OCaml Switch Configuration
ocaml-system        --          The OCaml compiler (system version, from outside of opam)
ocaml-variants      --          current trunk
ocamlbuild          0.14.0      OCamlbuild is a build system with builtin rules to easily build most OCaml projects.
ocamlfind           1.8.1       A library manager for OCaml

There is no libpng in the required by list. Do these commands give different results for you (this is possible, dependencies may depend on platform).

view this post on Zulip Enzo Crance (Dec 04 2020 at 12:32):

Hello @Michael Soegtrop. I have the same output as yours. I just found an error randomly running opam depext on some of these names:

$ opam depext cairo
# Detecting depexts using vars: arch=x86_64, os=macos, os-distribution=homebrew, os-family=homebrew
[ERROR] No solution for cairo: The following dependencies couldn't be met:
          - cairo → ocaml < 4.06.0
              base of this switch (use `--unlock-base' to force)
Command failed: opam list --readonly --external  '--resolve=cairo' returned 20

Maybe this could be linked to the issue... I must tell I am confused too.

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

@Enzo Crance : but we need cairo2, not cairo, as far as I can tell. cairo should not be in the dependency list of what you install. Maybe we can have a screen sahring session after the daily recap today.

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

https://github.com/coq/platform/commit/eaf3468d6e8d07fac7ed1cafe8bd147ab831f6f4 this seems to almost work (testing right now, since the EOL were wrong).

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

the NSIS script writes a coq_environment.txt

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

@Enrico Tassi : you wrote the file has OCaml string escapes. Doesn't this mean you have to do backslash expansion, or alternatively replace the back slashes with forward slashes. INSTDIR will for sure contain backward slashes. The commented out OCaml blocks show hot to do this and you might need to put in some of the commented out includes at the top.

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

Right.

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

I'll fix a couple of other things and then pass you the ball. You seem to have already macros for doubling \ but I don't know how to call it ;-)

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

done: I pushed an amended commit to v8.13 which creates a file in the right place with the right contents up to escaping which I leave to you (I've to go now)

view this post on Zulip Enrico Tassi (Dec 04 2020 at 16:22):

I still have to test if one can reasonably use "coq_makefile" from the installer in a fresh cygwin.

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

@Enrico Tassi : is the Coq patch already in 8.13?

view this post on Zulip Enrico Tassi (Dec 04 2020 at 16:22):

I think it was working with the old installed

view this post on Zulip Enrico Tassi (Dec 04 2020 at 16:23):

no, but it's not strictly needed

view this post on Zulip Enrico Tassi (Dec 04 2020 at 16:23):

COQLIB is already set to the place where the binary is (if the value is a file which does not exist)

view this post on Zulip Enrico Tassi (Dec 04 2020 at 16:23):

the value of OCAMLFIND (as used by coq_makefile) is wrong, but if your project is only made of .v file it's not a problem

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

I see. I think I anway put in the patch as opam patch

view this post on Zulip Enrico Tassi (Dec 04 2020 at 16:24):

sure, I tested it and it did work, but I hope I'll merge it in the Coq v8.13 branch soon

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

Btw.: chaging the dialog size is complicated. Essentially the dialogs are built in as Windows resources in a pre built NSIS template binary.

view this post on Zulip Enrico Tassi (Dec 04 2020 at 16:25):

ok, nevermind.

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

So either you compile NSIS from sources after patching it, or you patch the binaries.

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

The latter seems to be what most people are doing - there seems to be a special tool for it, but it is UI based and not easy to automate.

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

I look into creating groups now.

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

Err - first the icons ...

view this post on Zulip Enrico Tassi (Dec 04 2020 at 16:29):

Gotta go

view this post on Zulip Enrico Tassi (Dec 04 2020 at 16:30):

Ciao

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

Ciao. Talk on Monday?

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

Sure, but I will be releasing, not much free time I'm afraid. If you manage to do icons it will be very helpful. If not I'll hack something.

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

I commited a patch which does teh icons, but I think I need to do some them recompile in addition. I added two generic functions to add DLLs using ldd and to add files from a cygwin package, both with a regexp filter. They might be useful.
The installer I get is fairly large - 270MB compressed. The 8.12.0 official was 200 MB. The 8.12.1 is smaller but obviosuly broken. If I diff the folders, the main differences are bytecode files, which are fairly large and I can think be removed, and a lot of .cmo and .cma files.

view this post on Zulip Paolo Giarrusso (Dec 04 2020 at 19:30):

“Bytecode executables” (coqtop.byte?) are usually useless except for debugging... moving them to a separate package might make sense at some point

view this post on Zulip Paolo Giarrusso (Dec 04 2020 at 19:31):

(That’s true even if you were talking about something else)

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

@Paolo Giarrusso : the idea is that people who want to use a debugger use the base coq platform, not the installer. The installer is for quick mass installation especially for students and people who want to give it a try.

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

Yes, I think we can remove all .cm* but for . cmxs which are the ones loaded by Coq (for plugins).

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

@Enrico Tassi : OK, I will remove the .cm* files except .cmxs - should be easy now. I made a few more commits for cleanup and e.g. removing the bytecode files. The LZMA filesize is now 235MB, which is not that much larger than 8.12.0 (200 MB). Btw.: with bzip2 compression of the same data I get 311MB, so the LZMA seems worthwhile, even if it takes a while.

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

@Enrico Tassi I will update also the v813 branch today, unless you say you are workin gon it.

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

I just did, and pushed 2 commits

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

the installer is now 160M and seems to work

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:22):

thanks for the icons!

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

Do you have time for a short chat what needs to be done for the release?

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:22):

I'll test coq_makefile shortly

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

160M seems a bit small - the 8.12.0 was 200. Did you already remove the cma and cmo files?

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:23):

yes

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

Did you include compcert and VST?

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:23):

no

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

Ah OK. They should be included.

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:24):

I don't know which vst tag to take

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:24):

if you have it, please push

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

You used the black list default to remove .cam and .cmo?

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:24):

yes

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:24):

also .o .cmxa .cmi .cmx

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

Ah OK, if the issue is that there is no CompCert 3.8 and VST tag yet, I can make one today (at least a preliminary beta).

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:24):

all these are needed only if you build new plugins

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

Yes and new plugins should be builded based on the opam based coq platform installation.

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

I think this split into an installer for the masses and a separate dev envitronment for the pros greatly simplifies the whole thing.

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

So what remains to be done for the relase? I guess:
Prio 1: CompCert 3.8 and matching VST
Prio 2: package grouping

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:27):

yes. For the beta (due on monday) I think I'm good.

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:27):

both would be nice, but I'm not blocked.

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:27):

so no pressure

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

OK, I see what I can do. I have a telco with Andrew on Monday.

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:28):

for the final, I guess compcert and VST are needed.

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

One issue is that Xavier wants the 64 version to be the default from 3.8 on.

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:28):

and also proper tags for all the other addons (we are not bad, I tinky 6 top are missing)

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:28):

hum, what does it change exactly?

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

It changes which CompCert and VST ist installed under user-contrib and which under variant

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:29):

(I recall your wish to install 2 variant side by side, but using 64 seems simple no?)

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

Likely yes, but sometimes there are unexpected details one needs to take care of.

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:30):

ok. there is a way to divert the installation of packages compiled with coq_makefile, but compcert is not, dunno vst

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

I mean, coq_makefile should understand DESTDIR, IIRC

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

Well one can always give -Q options to direct CompCert and/or VST to a different folder.

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

I also have this issue open about a -V option which would make this easier.

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

Another thing: are all mathcomp packages long term maintained or are some more expirimental and shoul dnot be in the platform?

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

I think I see 3 extra, finmap, realcosed and bigenough

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

finmap is being integrated in mathcomp proper, so yes

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

Not sure how to interpret "yes" as answer on an "or" question ...

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:35):

the other two, I don't know, I think I can summon @Cyril Cohen to answer. I'd say yes.
We did also bring the platform to the attention of @Kazuhiko Sakaguchi for mczify, we all want that thing to be in a good state.

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

mczify is indeed important.

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:35):

yes = is maintained

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:36):

IIRC the problem with mczify is tht 8.12 support is not super good, much better in 8.13, so even if the package is part of both platforms, it is not really the same thing

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

I just saw a commit from you which looked like you excluded 2 packages for 8.13, but I didn't look at it, just the commit message. That's why I ask.

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:37):

now they should be back. I think realclosed had no mathcomp 1.12 compatible release, yet. Now it has.

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

Well it wouldn't be a big deal to start having it in 8.13. It is less problematic to add new stuff. The other way around would be worse.

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

I see, so this way just a temporary situation - fine for a beta.

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

What shall we do with the Windows build in CI?

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:38):

but it should be enabled now (I did rewrite the history of the branch a few times)

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

Remove it or strip it down to the bare minimum or replace it with coq platform in CI?

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:39):

Good question, I don't know yet. For sure the current job (and script) should go.
For the rest I don't know, because I don't know what is the plan for the platform itself.
Do you plan to have a CI on Coq master or not?

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:40):

In the very short term, I propose to add a job that compile the platform on coq master with just coq and coqide.

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:41):

I don't know what you use the master branch of the platform for... but that could be its role (point to coq.dev, comment all the other packages out)

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:41):

and we track it in Coq's ci as we track any other external project

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

Maybe we should discuss this in the weekly Coq work group meeting.

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:42):

good idea

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

I think it wouldn't be hard to have in Coq CI something which takes whatever fraction of the platform desired. I mean build Coq platform as we build any other Coq derivative project in CI.

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:42):

I think that ideally Coq's CI should also track all platform packages that have a .ml part, and possibly also the ones which are pure .v

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:43):

right now we are not too far, but some are missing

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

Yes, stuff I added because I needed it and then didn't have time, sorry.

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

But gappa is now easy to buil dvi aopam.

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

OK. so I start to work on CompCert and VST for 8.13 now. I will do this right on the 8.13 branch, so please refrain from history rewrites there.

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:45):

I think the main issue is not that some jobs were missing. It's that we (coq devs) don't all see CI the same way, so we don't necessarily follow the same practices. Adding the job you did add to windows only was very easy, but someone should have asked you to do it (or do it himself) earlier.

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:46):

OK, no more rewrites

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:46):

I have to go

view this post on Zulip Enrico Tassi (Dec 05 2020 at 16:46):

thanks for all your help!

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

I say thanks! Ciao.

view this post on Zulip Cyril Cohen (Dec 05 2020 at 18:54):

Enrico Tassi said:

the other two, I don't know, I think I can summon Cyril Cohen to answer. I'd say yes.
We did also bring the platform to the attention of Kazuhiko Sakaguchi for mczify, we all want that thing to be in a good state.

Could you state the question in a concise way?

view this post on Zulip Michael Soegtrop (Dec 05 2020 at 20:11):

@Cyril Cohen : my question was if all packages of mathcomp are in a state of fully maintained release or if some packages are experimental, so that such packages should not be included in the Coq platform. The question is not if today all packages are say compatible to 8.13, the question is if there are plans to maintain all mathcomp packages say for 8.14 and 8.15.

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

@Enrico Tassi : I created opam packages for CompCert 3.8 (no open source variant as yet) and bumped the version in the 8.13 branch. So CompCert should work no (the full variant).

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

It works here. I don't know the license of compcert. is the full version "redistributable in binary format" ?

view this post on Zulip Michael Soegtrop (Dec 06 2020 at 09:23):

@Enrico Tassi : the compcert license is in essence that it may be used for research and commercial evaluation purposes, but not for commercial production purposes. It doesn't distinguish between binary and source (afair). Xavier agreed a longer while back to include it in the Coq installer provided that it is not selected by default and that the full license is displayed and must be agreed on in case it is selected. This should work. It would of cause be nice to have two mutually exclusive packages for compcert and compcert-open source, but this is tricky from the opam side.

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

@Cyril Cohen : btw: as far as I can see these mathcomp packages, which are included in the platform, are not in Coq CI:

PACKAGES="${PACKAGES} coq-mathcomp-bigenough.1.0.0"
PACKAGES="${PACKAGES} coq-mathcomp-finmap.1.5.0"
PACKAGES="${PACKAGES} coq-mathcomp-real-closed.1.1.1"

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

It would of cause be nice to have two mutually exclusive packages for compcert and compcert-open source, but this is tricky from the opam side.

The nicest solution IMHO wouldn't be mutually exclusive package, but rather a non-open-source package that depends on the open source one.

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

@Théo Zimmermann : indeed, that would be most reasonable, but is also tricky. Either it would need a substantial restructuring of CompCert or one simply overwrites the open source part with the same files from the non open source part.

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

Cyril Cohen said:

Enrico Tassi said:

the other two, I don't know, I think I can summon Cyril Cohen to answer. I'd say yes.
We did also bring the platform to the attention of Kazuhiko Sakaguchi for mczify, we all want that thing to be in a good state.

Could you state the question in a concise way?

@Cyril Cohen : the coq platform currently includes finmap, bigenough and realclosed. Do you plan to maintain these? See the third point of this paragraph: https://github.com/coq/platform/blob/master/charter.md#package-inclusion-process

view this post on Zulip Cyril Cohen (Dec 06 2020 at 16:28):

@Michael Soegtrop @Enrico Tassi Yes I plan to maintain these three packages on the long term, until they get integrated fully and completely with mathcomp core.

view this post on Zulip Cyril Cohen (Dec 06 2020 at 16:29):

I should add them to the CI of Coq, you are right

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

I knew the plan was this one for finmap. Glad it's also the plan for the other 2 pkgs.

view this post on Zulip Paolo Giarrusso (Dec 06 2020 at 17:46):

@Michael Soegtrop > one simply overwrites the open source part with the same files from the non open source part.

sounds too fragile, if it even works today with sandboxing

view this post on Zulip Michael Soegtrop (Dec 06 2020 at 20:05):

@Cyril Cohen : OK, I leave these packages in the Coq platform then. Thanks for the clarification!

view this post on Zulip Michael Soegtrop (Dec 06 2020 at 20:08):

@Paolo Giarrusso : yes, that's the reason why this are currently separate mutually exclusive packages.

Yet another option would be to have the open source part required by VST and the compcert/clightgen executables and libraries as separate packages but not the additional .vo files for CompCert. I am not sure if anybody uses .vo files of CompCert, which are not in the interface - which is open source. But as is the makefile of CompCert supports neither of this.

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

@Enrico Tassi : I did the following changes over the weekend on the Coq Platform 8.13 branch:

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

great

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

If you need anything during teh release today, please let me know.

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

w.r.t. the beta, I plan to tag before lunch, then I'll make an opam package and build the installer from that.
(BTW This morning I did test the coq_makefile from the installer and it works fine)

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

Good. I am currently building an installer from the status quo and plan to do some smoke tests of the delivered add ons. It would help if you could do a little smoektest and mathcomp - you know that much better than I do. A few mathcomp smoke test files would be good to have.

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

After the release I'll add to Coq CI a job for the platform building only Coq and CoqIDE against the master branch, and also the 2 mathcomp related packages that we don't track right now

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

Sounds good. Can we then remove the legacy Windows build scripts? I guess it would be my call to make a PR for that. Has been a while - if I remember right I started this for Coq 8.6.
Btw.: we should switch comunication back to the main Coq platform topic.

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

I'm testing gappa/interval fixes, and I noticed that the example file you pushed does -compcert=o but then fails saying that beta + opensource are not supported. So maybe we did not fully understand each other.
By tonight I plan to put on Coq's gihub an installer for windows. I was planning to put in there everything that builds. Are you OK with this? Should I chose -compcert=f and -vst=n? Or you want me to just have coq+coqide in there and leave to you a release of the platform including all the rest?

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

BTW, I did push a fix for compcert 3.8 opam packages (in case you are pushing them upstream already)

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

@Enzo Crance : you had some issues with Coq platform and homebrew. I did run some tests meanwhile. I must say that homebrew looks generally a bit fragile. What did help me to get Coq platform installed is the following procedure:

brew uninstall $(brew list)
sudo chown -R ${USER}:admin /usr/local/*
./coq_platform_make.sh (fails in depext step)
./coq_platform_make.sh (succeeds)

The first step kills of cause also everything else you have installed via homebrew - I found this step required because without the chwon step, pkg-config installation fails and if you install other packages without having pkg-config upfront, they are not properly registered. The second step is definitely not nice, but not much worse than what homebrew anyway does to the security of your system. I will put some notes on this in the platform repo. I must say their argumentation is not completely off but not completely solid either.

homebrew seems to have a few flaws:

view this post on Zulip Paolo Giarrusso (Dec 10 2020 at 18:45):

@Michael Soegtrop I'm confused on that code. (EDIT: it _seems_) a Homebrew /usr/local is user-writable unless something else screws with its permissions...

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

@Paolo Giarrusso : on a freshly installed macOS there is stuff in /usr/local and Homebrew makes only parts of this writable during installation - it shows a list of which folders it makes writable. But then it tries to write to other folders as well.

view this post on Zulip Michael Soegtrop (Dec 11 2020 at 17:22):

Possibly you have run sudo chown -R ${USER}:admin /usr/local/* some time in the past?

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 00:40):

Maybe; that sounds like a potential bug but many people describe this...

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

Actually I tried it with an absolute plain VM image and there it worked. Usually I use a developer VM image with e.g. XCode preinstalled. I will adjust my Mac Readme accordingly.

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

@Paolo Giarrusso : can you do me a favor and review the file https://github.com/coq/platform/blob/v8.12/README_macOS.md if the information given there on MacPorts and Homebrew matches your experience.

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 23:10):

On the non-fresh system, have you run brew doctor?

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 23:11):

I don't remember needing retries on brew install — except that brew install implies brew update so is network-sensitive

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 23:12):

and I _think_ brew doctor should warn about permission issues

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 23:13):

anyway, "Homebrew doesn't seem to have fully working dependency management" seems likely to be "too strong"

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

I've included a possible weaker suggestion in https://github.com/coq/platform/pull/43

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 23:23):

I can confirm that sudo chown root /usr/local/share/; sudo chmod 755 /usr/local/share/ gets noticed by brew doctor:

$ brew doctor
Please note that these warnings are just used to help the Homebrew maintainers
with debugging if you file an issue. If everything you use Homebrew for is
working fine: please don't worry or file an issue; just ignore this. Thanks!

Warning: The following directories are not writable by your user:
/usr/local/share

You should change the ownership of these directories to your user.
  sudo chown -R $(whoami) /usr/local/share

And make sure that your user has write permission.
  chmod u+w /usr/local/share

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 23:24):

both changes are needed to create trouble because I'm starting from

$ ll /usr/local/share -d
drwxrwxr-x 70 pgiarrusso admin 2240 Nov 29 15:27 /usr/local/share/

Last updated: Oct 16 2021 at 07:02 UTC