Karl Palmskog (Nov 23 2020 at 01:40): 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.
Enrico Tassi (Nov 30 2020 at 10:38):Plan:
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 ...
Michael Soegtrop (Nov 30 2020 at 12:05):For the tim beeing I will use the opam package name
Michael Soegtrop (Nov 30 2020 at 14:03):@Enrico Tassi : I am AFK for an hour or so.
Enrico Tassi (Nov 30 2020 at 14:08):ok
Enrico Tassi (Nov 30 2020 at 14:09):So far I have
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.
Enrico Tassi (Nov 30 2020 at 15:58):I'm testing my last push on v8.13 on windows, it seems to compile
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
Michael Soegtrop (Dec 01 2020 at 08:33):@Andrej Dudenhefner : please ping me when you have time for a Coq platform discussion.
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.
Enrico Tassi (Dec 01 2020 at 08:45):Hi, I have a few more packages to port before compcert and vst, so no hurry
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.
Andrej Dudenhefner (Dec 01 2020 at 08:59):@Michael Soegtrop I'm available today from now up until 14:00 CET.
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?
Cyril Cohen (Dec 01 2020 at 09:11):Not available yet
Cyril Cohen (Dec 01 2020 at 09:11):Maybe tomorrow surely by the wnd of the week
Michael Soegtrop (Dec 01 2020 at 09:13):@Andrej Dudenhefner : let's meet after the current sync up in a break out room.
Michael Soegtrop (Dec 01 2020 at 09:23):@Andrej Dudenhefner : The platform project os here: https://github.com/coq/platform
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
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
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
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
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.
Yannick Forster (Dec 01 2020 at 10:50):@Matthieu Sozeau might be able to help
Yannick Forster (Dec 01 2020 at 10:51):Can you somehow inspect the generated ml file @Andrej Dudenhefner?
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.
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.
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
Michael Soegtrop (Dec 01 2020 at 11:12):I join
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
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.
Yannick Forster (Dec 01 2020 at 11:27):Thanks!
Matthieu Sozeau (Dec 01 2020 at 11:31):Did you manage to solve the problem?
Yannick Forster (Dec 01 2020 at 11:31):No, but we're close :) It's a Windows line ending issue
Yannick Forster (Dec 01 2020 at 11:36):Here's the patch file: https://gist.githubusercontent.com/yforster/b5596a32377f23c18344f5a04038c3a7/raw/cc7eb9d79c0e313c0b73943b5f3831e1abc54292/metacoq-lineendings.patch
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
Michael Soegtrop (Dec 01 2020 at 11:40):@Enrico Tassi : perfect, thanks!
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
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?
Yannick Forster (Dec 01 2020 at 11:45):coq-metacoq-template
Michael Soegtrop (Dec 01 2020 at 11:45):OK
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)
Matthieu Sozeau (Dec 01 2020 at 11:47):Possibly checker needs it as well
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)
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.
Matthieu Sozeau (Dec 01 2020 at 11:49):Alternatively, changing the metacoq-checker opam file to do make -C checker would solve this
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:
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.
Yannick Forster (Dec 01 2020 at 11:57):Okay, I should be available all afternoon. Guten Appetit! ;)
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.
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.
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.
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:
~/coq-platform/opam/packagesfiles in the package folderThe 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.
Matthieu Sozeau (Dec 01 2020 at 13:13):@Michael Soegtrop I think we need the unix time command
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
Yannick Forster (Dec 01 2020 at 13:24):I remember we added the conf-time after @Karl Palmskog suggested it to @Matthieu Sozeau
Yannick Forster (Dec 01 2020 at 13:25):Oh, Matthieu already answered, sorry. I was narrowed down to mentions in the Zulip view
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
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?
Matthieu Sozeau (Dec 01 2020 at 13:40):We can easily remove the reliance on time
Yannick Forster (Dec 01 2020 at 13:42):Maybe that's the way to go then
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.
Karl Palmskog (Dec 01 2020 at 13:52):then you can run time-based build if you pass the testing option to opam
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.
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
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.
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?
Yannick Forster (Dec 01 2020 at 16:42):Yes, it's the same issue, and it can be fixed the same way
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
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?
Yannick Forster (Dec 01 2020 at 16:44):I can do it
Michael Soegtrop (Dec 01 2020 at 16:46):OK, fine. Please let me know how it goes.
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.
Andrej Dudenhefner (Dec 01 2020 at 16:49):@Michael Soegtrop Yes, where can I find the log files?
Michael Soegtrop (Dec 01 2020 at 16:50):@Andrej Dudenhefner let's have a quick breakout session
Andrej Dudenhefner (Dec 01 2020 at 16:50):OK.
Michael Soegtrop (Dec 01 2020 at 16:51):Room 7 ...
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.
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)
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, ...).
Enrico Tassi (Dec 01 2020 at 18:17):Would c:\coq_platform\ be more safe?
Michael Soegtrop (Dec 01 2020 at 18:42):That's what Andrej suggested.
Matthieu Sozeau (Dec 01 2020 at 21:04):Yannick Forster said:
This might mean there's something wrong with the
coq-metacoq-checkerpackage though: Do we really need to recompiletemplate-coqwhen installing thecheckerpackage? 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
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)
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
Paolo Giarrusso (Dec 01 2020 at 22:56):Oh okay there's also https://github.com/ocaml/dune/issues/2991 ?
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)
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?
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.
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
Michael Soegtrop (Dec 02 2020 at 09:53):The dependency parsexp ppx_sexp_value is not in the opam file.
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
Michael Soegtrop (Dec 02 2020 at 09:58):@Andrej Dudenhefner : yes you need to filter the output of coqc -where with tr.
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.
Andrej Dudenhefner (Dec 02 2020 at 10:00):@Michael Soegtrop today I also tried to reproduce the gappa bug, but everything went well.
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
@Andrej Dudenhefner : thanks! please keep an eye open!
Michael Soegtrop (Dec 02 2020 at 10:02):@Enrico Tassi : I will add --installed then and report this as a bug to opam.
Matthieu Sozeau (Dec 02 2020 at 10:13):Yannick Forster said:
Matthieu Sozeau The
opamfile of the checker does callmake -C checker. Or do you mean in theopamfile oftemplate-coqwe should usemake -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
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 :-)
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).
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
Enrico Tassi (Dec 02 2020 at 10:18):@Emilio Jesús Gallego Arias please give a look at that PR quickly
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.
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.
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?
Yannick Forster (Dec 02 2020 at 12:48):No, it's on a branch of mine. Give me a minute
Yannick Forster (Dec 02 2020 at 12:51):I filed a PR agains the v8.12 branch: https://github.com/coq/platform/pull/42
Michael Soegtrop (Dec 02 2020 at 12:52):Thanks!
Michael Soegtrop (Dec 02 2020 at 12:52):@Enrico Tassi : is there a coqc command to get a less verbose version string?
Enrico Tassi (Dec 02 2020 at 12:53):yup
Enrico Tassi (Dec 02 2020 at 12:53):-print-version
Michael Soegtrop (Dec 02 2020 at 12:53):Perfect, thanks!
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.
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.
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...
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.
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.
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.
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
Enrico Tassi (Dec 02 2020 at 18:04):The version is in the path above.
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.
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 '\\\\' '/'.
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).
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!
Paolo Giarrusso (Dec 02 2020 at 19:54):does \ cause exciting “double quote” issues? :-|
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.
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
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.
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"
Enrico Tassi (Dec 03 2020 at 08:55):example ${CheckHiddenSectionDependency} ${Sec_elpi} ${Sec_dune}, elpi need dune to build, but not to run
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
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.
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
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}
]
The opam files need to be fixed.
Enrico Tassi (Dec 03 2020 at 08:59):I can improve that for sure
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 ...
Michael Soegtrop (Dec 03 2020 at 09:00):Maybe I am mixing it up with MacPorts or another packager.
Enrico Tassi (Dec 03 2020 at 09:00):I'll double check, IIRCyou can {build} and I do for {with-test}
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...
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.
Enrico Tassi (Dec 03 2020 at 09:07):Do you want me to work on this filtering by name feature?
Enrico Tassi (Dec 03 2020 at 09:08):(It's blocking for the release, IMO, 1.4G is not an option)
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.
Enrico Tassi (Dec 03 2020 at 09:13):ok ok, I'm at the rewrite rule WG now
Michael Soegtrop (Dec 03 2020 at 09:13):You can also enable compression (line 13+14 of Coq.nsi).
Michael Soegtrop (Dec 03 2020 at 09:14):But as I said, it takes ages to build then.
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.
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.
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 :( :(
Enrico Tassi (Dec 03 2020 at 14:23):I did add some support to slim packages https://github.com/coq/platform/commit/23135987b66c7b08ec263bdc16d7ef8d7d993eb6
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.
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)
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!
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.
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.
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.
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.
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.
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
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.
that warning is from Brew, and it means that depext on brew is likely breaking a bit, which might relate to your bug.
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.
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)
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).
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.
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.
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).
Enrico Tassi (Dec 04 2020 at 15:54):the NSIS script writes a coq_environment.txt
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.
Enrico Tassi (Dec 04 2020 at 16:07):Right.
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 ;-)
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)
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.
Michael Soegtrop (Dec 04 2020 at 16:22):@Enrico Tassi : is the Coq patch already in 8.13?
Enrico Tassi (Dec 04 2020 at 16:22):I think it was working with the old installed
Enrico Tassi (Dec 04 2020 at 16:23):no, but it's not strictly needed
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)
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
Michael Soegtrop (Dec 04 2020 at 16:24):I see. I think I anway put in the patch as opam patch
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
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.
Enrico Tassi (Dec 04 2020 at 16:25):ok, nevermind.
Michael Soegtrop (Dec 04 2020 at 16:25):So either you compile NSIS from sources after patching it, or you patch the binaries.
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.
Michael Soegtrop (Dec 04 2020 at 16:27):I look into creating groups now.
Michael Soegtrop (Dec 04 2020 at 16:27):Err - first the icons ...
Enrico Tassi (Dec 04 2020 at 16:29):Gotta go
Enrico Tassi (Dec 04 2020 at 16:30):Ciao
Michael Soegtrop (Dec 04 2020 at 16:30):Ciao. Talk on Monday?
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.
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.
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
Paolo Giarrusso (Dec 04 2020 at 19:31):(That’s true even if you were talking about something else)
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.
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).
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.
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.
Enrico Tassi (Dec 05 2020 at 16:21):I just did, and pushed 2 commits
Enrico Tassi (Dec 05 2020 at 16:21):the installer is now 160M and seems to work
Enrico Tassi (Dec 05 2020 at 16:22):thanks for the icons!
Michael Soegtrop (Dec 05 2020 at 16:22):Do you have time for a short chat what needs to be done for the release?
Enrico Tassi (Dec 05 2020 at 16:22):I'll test coq_makefile shortly
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?
Enrico Tassi (Dec 05 2020 at 16:23):yes
Michael Soegtrop (Dec 05 2020 at 16:23):Did you include compcert and VST?
Enrico Tassi (Dec 05 2020 at 16:23):no
Michael Soegtrop (Dec 05 2020 at 16:23):Ah OK. They should be included.
Enrico Tassi (Dec 05 2020 at 16:24):I don't know which vst tag to take
Enrico Tassi (Dec 05 2020 at 16:24):if you have it, please push
Michael Soegtrop (Dec 05 2020 at 16:24):You used the black list default to remove .cam and .cmo?
Enrico Tassi (Dec 05 2020 at 16:24):yes
Enrico Tassi (Dec 05 2020 at 16:24):also .o .cmxa .cmi .cmx
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).
Enrico Tassi (Dec 05 2020 at 16:24):all these are needed only if you build new plugins
Michael Soegtrop (Dec 05 2020 at 16:25):Yes and new plugins should be builded based on the opam based coq platform installation.
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.
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
Enrico Tassi (Dec 05 2020 at 16:27):yes. For the beta (due on monday) I think I'm good.
Enrico Tassi (Dec 05 2020 at 16:27):both would be nice, but I'm not blocked.
Enrico Tassi (Dec 05 2020 at 16:27):so no pressure
Michael Soegtrop (Dec 05 2020 at 16:27):OK, I see what I can do. I have a telco with Andrew on Monday.
Enrico Tassi (Dec 05 2020 at 16:28):for the final, I guess compcert and VST are needed.
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.
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)
Enrico Tassi (Dec 05 2020 at 16:28):hum, what does it change exactly?
Michael Soegtrop (Dec 05 2020 at 16:29):It changes which CompCert and VST ist installed under user-contrib and which under variant
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?)
Michael Soegtrop (Dec 05 2020 at 16:30):Likely yes, but sometimes there are unexpected details one needs to take care of.
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
Enrico Tassi (Dec 05 2020 at 16:31):I mean, coq_makefile should understand DESTDIR, IIRC
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.
Michael Soegtrop (Dec 05 2020 at 16:32):I also have this issue open about a -V option which would make this easier.
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?
Enrico Tassi (Dec 05 2020 at 16:33):I think I see 3 extra, finmap, realcosed and bigenough
Enrico Tassi (Dec 05 2020 at 16:33):finmap is being integrated in mathcomp proper, so yes
Michael Soegtrop (Dec 05 2020 at 16:34):Not sure how to interpret "yes" as answer on an "or" question ...
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.
Michael Soegtrop (Dec 05 2020 at 16:35):mczify is indeed important.
Enrico Tassi (Dec 05 2020 at 16:35):yes = is maintained
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
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.
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.
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.
Michael Soegtrop (Dec 05 2020 at 16:37):I see, so this way just a temporary situation - fine for a beta.
Michael Soegtrop (Dec 05 2020 at 16:37):What shall we do with the Windows build in CI?
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)
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?
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?
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.
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)
Enrico Tassi (Dec 05 2020 at 16:41):and we track it in Coq's ci as we track any other external project
Michael Soegtrop (Dec 05 2020 at 16:42):Maybe we should discuss this in the weekly Coq work group meeting.
Enrico Tassi (Dec 05 2020 at 16:42):good idea
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.
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
Enrico Tassi (Dec 05 2020 at 16:43):right now we are not too far, but some are missing
Michael Soegtrop (Dec 05 2020 at 16:43):Yes, stuff I added because I needed it and then didn't have time, sorry.
Michael Soegtrop (Dec 05 2020 at 16:43):But gappa is now easy to buil dvi aopam.
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.
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.
Enrico Tassi (Dec 05 2020 at 16:46):OK, no more rewrites
Enrico Tassi (Dec 05 2020 at 16:46):I have to go
Enrico Tassi (Dec 05 2020 at 16:46):thanks for all your help!
Michael Soegtrop (Dec 05 2020 at 16:47):I say thanks! Ciao.
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?
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.
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).
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" ?
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.
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"
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.
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.
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
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.
Cyril Cohen (Dec 06 2020 at 16:29):I should add them to the CI of Coq, you are right
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.
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
Michael Soegtrop (Dec 06 2020 at 20:05):@Cyril Cohen : OK, I leave these packages in the Coq platform then. Thanks for the clarification!
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.
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:
Enrico Tassi (Dec 07 2020 at 09:04):great
Michael Soegtrop (Dec 07 2020 at 09:05):If you need anything during teh release today, please let me know.
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)
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.
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
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.
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?
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)
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:
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...
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.
Michael Soegtrop (Dec 11 2020 at 17:22):Possibly you have run sudo chown -R ${USER}:admin /usr/local/* some time in the past?
Paolo Giarrusso (Dec 13 2020 at 00:40):Maybe; that sounds like a potential bug but many people describe this...
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.
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.
Paolo Giarrusso (Dec 13 2020 at 23:10):On the non-fresh system, have you run brew doctor?
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
Paolo Giarrusso (Dec 13 2020 at 23:12):and I _think_ brew doctor should warn about permission issues
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"
Paolo Giarrusso (Dec 13 2020 at 23:20):I've included a possible weaker suggestion in https://github.com/coq/platform/pull/43
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
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: Jun 10 2023 at 23:01 UTC