Théo Zimmermann (Jun 24 2020 at 11:16): Théo Zimmermann (Jun 24 2020 at 11:16):This is the topic to ask questions to the Coq developers during the discussion session.
Théo Zimmermann (Jul 06 2020 at 09:06):This session will start in one hour.
Théo Zimmermann (Jul 06 2020 at 09:06):After Jean-Christophe's talk.
Théo Zimmermann (Jul 06 2020 at 09:07):Start asking questions for the Coq developers as soon as you want.
Théo Zimmermann (Jul 06 2020 at 09:18):@Michael Soegtrop If you want to participate with the Coq devs to make a quick recap of the status of the platform, let us know and we can add you to the panelists.
Emilio Jesús Gallego Arias (Jul 06 2020 at 09:20):Please feel free to raise your hand in the Zoom session in Zoom and ask questions using audio
Michael Soegtrop (Jul 06 2020 at 09:33):@Théo Zimmermann : yes, sure
Michael Soegtrop (Jul 06 2020 at 09:37):I am right now in my lab and I don't have a camera on my workstation - should I move to the reading room where I have a web camera?
Matthieu Sozeau (Jul 06 2020 at 09:39):@Michael Soegtrop I guess that would be nicer to see you indeed :)
Gaëtan Gilbert (Jul 06 2020 at 09:50):zoom seems to need a reload every few minutes for me or I stop hearing its sound x_x
Théo Zimmermann (Jul 06 2020 at 09:51):Only since you are a panelist?
Gaëtan Gilbert (Jul 06 2020 at 09:51):it didn't happen yesterday
that's all I know
Michael Soegtrop (Jul 06 2020 at 09:54):@Théo Zimmermann I can't join any more - it says I need the panel link to join. Can you temporarily remove me from the panel until I joined?
Théo Zimmermann (Jul 06 2020 at 09:55):OK let's try that.
Théo Zimmermann (Jul 06 2020 at 09:55):Oh in fact I see you are already there
Michael Soegtrop (Jul 06 2020 at 09:58):Théo Zimmermann said:
Oh in fact I see you are already there
Yes, zoom changed its mind on a second try ...
Michael Soegtrop (Jul 06 2020 at 10:07):@Théo Zimmermann : I can't start video - it says the host has stopped it
Chantal Keller (Jul 06 2020 at 10:10):Q. on Coq 8.12: which changes are relevant when implementing an OCaml plugin?
Bas Spitters (Jul 06 2020 at 10:17):https://github.com/coq/coq/wiki/Future+plans
Karl Palmskog (Jul 06 2020 at 10:19):Q: when will we get a nice (and up-to-date) "Coq Team" person listing/presentation so we know who to praise/blame (without git)?
Chantal Keller (Jul 06 2020 at 10:20):Q. How does the Coq Platform interact with Coq Community? Will developments in Coq Community be automatically integrated in the Coq Platform?
Hugo Herbelin (Jul 06 2020 at 10:23):@Karl Palmskog : There is https://github.com/coq/coq/wiki/Coq-development-team (I don't know how up-to-date it is exactly).
Chantal Keller (Jul 06 2020 at 10:24):Thanks for the answer
Karl Palmskog (Jul 06 2020 at 10:24):@Hugo Herbelin I guess I was thinking of something similar to this: https://leanprover-community.github.io/meet.html
Chantal Keller (Jul 06 2020 at 10:25):Q. on native arrays: what is the status? Will they be integrated in Coq-8.13?
Karl Palmskog (Jul 06 2020 at 10:28):Q: What's the core devs' opinions on the Stdlib development? Should it grow more or be or just be maintained? Should Coq itself be "partial" to Stdlib, given that there are (arguably) other libraries of similar status?
Michael Soegtrop (Jul 06 2020 at 10:29):@Chantal Keller : one more not on this: it might happen that we have two levels of the Coq Platform - a level one with commonly used developments and tight release schedules and maintenance requirements and a level two with an extended set of developments and relaxed inclusion and maintenance criteria.
Chantal Keller (Jul 06 2020 at 10:31):Thanks a lot Maxime, I will be happy to provide benchmarks!
Andrej Dudenhefner (Jul 06 2020 at 10:31):Q: Does vscoq have a release schedule / roadmap? The TODO file was updated 4 years ago.
Bas Spitters (Jul 06 2020 at 10:36):@Hugo Herbelin mentioned coq-extlib.
I could imagine that https://github.com/coq-community/coq-ext-lib/commits/master and stdlibpp could be merged. They have similar goals and similar design principles. extlib does not seem to be too active anymore. Q: would this be a good idea?
Robbert Krebbers (Jul 06 2020 at 10:41):RE contributions to "standard libraries", issues and merge requests for std++ are always welcome, by anyone, at https://gitlab.mpi-sws.org/iris/stdpp
Karl Palmskog (Jul 06 2020 at 10:41):the problem of students/enthusiasts contributing to Stdlib: any changes will be visible only in the next Coq release, which may be 6 months away. This can probably be pretty frustrating and might be discouraging.
Samuel Hym (Jul 06 2020 at 10:41):Q: What are the current plans / roadmap about IDEs?
Enrico Tassi (Jul 06 2020 at 10:42):@Karl Palmskog Why? And what time frame would not be, in your opinion?
Cyril Cohen (Jul 06 2020 at 10:43):The panel of yesterday never entered stdlib topic :-( (my mistake too)
Paolo Giarrusso (Jul 06 2020 at 10:43):@Enrico Tassi With external libraries, your contributions are available as soon as the external library is released, and potentially also on older Coq releases :-)
Karl Palmskog (Jul 06 2020 at 10:44):Enrico Tassi said:
Karl Palmskog Why? And what time frame would not be, in your opinion?
say you have an "experimental" library like Lean's Mathlib where people just add new stuff. Is there any reason not to release once every 1-2 months? This means contributors get immediate recognition and others can use their results.
Matthieu Sozeau (Jul 06 2020 at 10:44):@Cyril Cohen oh, right, my bad!
Emilio Jesús Gallego Arias (Jul 06 2020 at 10:45):@Maxime Dénès where is the roadmap for the document server?
Théo Zimmermann (Jul 06 2020 at 10:45):Karl Palmskog said:
Enrico Tassi said:
Karl Palmskog Why? And what time frame would not be, in your opinion?
say you have an "experimental" library like Lean's Mathlib. Is there any reason not to release once every 1-2 months? This means contributors get immediate recognition and others can use their results.
Stdlib is not the only place people can contribute. But having stdlib be "experimental" makes no sense to me.
Matthieu Sozeau (Jul 06 2020 at 10:45):It's somewhere on github IIRC
Karl Palmskog (Jul 06 2020 at 10:46):Théo Zimmermann said:
Stdlib is not the only place people can contribute. But having stdlib be "experimental" makes no sense to me.
Right, this is why I don't think we should encourage new users to contribute to Stdlib as a first option.
Emilio Jesús Gallego Arias (Jul 06 2020 at 10:46):I mean, there is only the branch? No design / RFC?
Michael Soegtrop (Jul 06 2020 at 10:46):Is the version of VSCoq offered by the plugin manager current or should I use a GIT version?
Paolo Giarrusso (Jul 06 2020 at 10:46):The "document manager" PR for VSCode is https://github.com/coq-community/vscoq/pull/140
Emilio Jesús Gallego Arias (Jul 06 2020 at 10:46):IIRC commit didn't say a lot on the approach used
Reynald Affeldt (Jul 06 2020 at 10:46):People may maybe not agree on one naming convention but working with more than two naming conventions is frustrating. :-(
Evgeny Makarov (Jul 06 2020 at 10:47):What's the current status of the documentation for writing the OCaml side of a Coq tactic? Would you recommend trying to understand how to write OCaml code for Coq for a person who is familiar only with Coq, for example, as a university term/diploma project?
Paolo Giarrusso (Jul 06 2020 at 10:47):IME, you only notice the frustration once you learn to expect a naming convention, which takes some time with a library using one...
Emilio Jesús Gallego Arias (Jul 06 2020 at 10:48):@Evgeny Makarov you have Yves' Coq plugin tutorial
Andrej Dudenhefner (Jul 06 2020 at 10:48):Thank you for the detailed answer @Maxime Dénès .
Would it it be possible to more often update the plugin in the vscode store. v0.3.1 is half a year old.
Emilio Jesús Gallego Arias (Jul 06 2020 at 10:48):it is distributed with Coq these days
Maxime Dénès (Jul 06 2020 at 10:49):@Andrej Dudenhefner Yes, I was planning to make a release, unfortunately my planning was a bit disturbed by the health crisis, but I hope to do one soon. I integrated a few external contributions some weeks ago, that it would be nice to ship.
Paolo Giarrusso (Jul 06 2020 at 10:50):Link to new manual, with link to plugin tutorial: https://coq.github.io/doc/v8.12/refman/using/libraries/writing.html
Robbert Krebbers (Jul 06 2020 at 10:52):Question: Related to the question in the other channel, what's the rough ETA on unification? (I know it's super hard, so I'm not pushing :))
Michael Soegtrop (Jul 06 2020 at 10:52):Regarding plugins: I can do most of the things I need to do in Ltac2 or MetaCoq - the missing thing is to write / read files and call external programs. Doing a PR on this I found that adding this is highly controversial, but one could have some sandbox type of file IO.
Andrej Dudenhefner (Jul 06 2020 at 10:55):Q: Is WSL (Windows) something that is actively considered as standard way to use Coq on Windows? With the recent WSL2 it way much simpler to install and use Coq+Vscode+opam.
Karl Palmskog (Jul 06 2020 at 10:55):Q: regarding high level documentation on Coq's trusted base ("what do I have to trust to trust Coq theorems"): is this something that can/should be in the manual? I think we established that the wiki page on this was obsolete.
Guillaume Melquiond (Jul 06 2020 at 10:55):Q: How does UIP interact with kernel computations, e.g. vm/native_compute?
Théo Zimmermann (Jul 06 2020 at 10:58):sure!
Théo Zimmermann (Jul 06 2020 at 11:00):I think this stdlib discussion warrants a new dedicated thread BTW :wink:
Cyril Cohen (Jul 06 2020 at 11:00):I could hand-pick messages and put them in the new topic
Cyril Cohen (Jul 06 2020 at 11:00):give me 1min
Reynald Affeldt (Jul 06 2020 at 11:03):With the recent WSL2 it way much simpler to install and use Coq+Vscode+opam.
What has become easier with WSL2? (Because it was already pretty simple with WSL1...) (I do not have a Windows machine to check it by myself now.)
Théo Zimmermann (Jul 06 2020 at 11:04):At some point WSL required dev mode. But this has probably changed before WSL2.
Karl Palmskog (Jul 06 2020 at 11:04):Q: how do we establish clear boundaries on what are the responsibilities of the core devs vs. the community? Should this be documented? For example, I'm not sure it's obvious that OPAM packages for Coq releases/betas are handled by the community.
Andrej Dudenhefner (Jul 06 2020 at 11:05):@affeldt-aist it ran (for the first time) as described for native linux systems and did so in a faction of the time of wsl1.
Enrico Tassi (Jul 06 2020 at 11:05):Here my snap "experiment": https://github.com/gares/coq-opam-snap
Emilio Jesús Gallego Arias (Jul 06 2020 at 11:06):Thanks @Enrico Tassi , let's open a ticket and try to get the CI to build it.
Chantal Keller (Jul 06 2020 at 11:06):Thanks! :clap: for the development of Coq
Théo Zimmermann (Jul 06 2020 at 11:06):Karl Palmskog said:
Q: regarding high level documentation on Coq's trusted base ("what do I have to trust to trust Coq theorems"): is this something that can/should be in the manual? I think we established that the wiki page on this was obsolete.
Yes. This was kind of the goal of the Core language chapter in the 8.12 manual.
Emilio Jesús Gallego Arias (Jul 06 2020 at 11:06):IMHO there is no conflict with the platform, at some point if the platfrom wants to take over they can just copy the code
Emilio Jesús Gallego Arias (Jul 06 2020 at 11:06):it would make still sense to have a snap for master with the basic things
Cyril Cohen (Jul 06 2020 at 11:07):Cyril Cohen said:
I could hand-pick messages and put them in the new topic
Done > Please followup here for Stdlib contributions discussions.
Please tell me if I forgot a message.
Emilio Jesús Gallego Arias (Jul 06 2020 at 11:07):@Gaëtan Gilbert I'm not sure we answered Guillaume question about UIP
Enrico Tassi (Jul 06 2020 at 11:08):I absolutely don't recall how to build it. The only "trick" is that I name the package/binaries after the version of Coq, so that you can install multiple version of Coq alongside. IIRC I also bundle opam, so that you can install extra atuff inside the snap (a posteriori, and that is not really needed for teaching)
Michael Soegtrop (Jul 06 2020 at 11:08):Emilio Jesús Gallego Arias said:
IMHO there is no conflict with the platform, at some point if the platfrom wants to take over they can just copy the code
I would say having a snap package of core Coq in Coq CI is a prerequisite for having a Coq Platform snap package.
Cyril Cohen (Jul 06 2020 at 11:08):Thanks for this very nice session.
Andrej Dudenhefner (Jul 06 2020 at 11:10):@affeldt-aist @Maxime Dénès
the only thing with WSL2 I needed to do in addition was to set the actual binpath in the vscoq plugin. This was strange since that was already on PATH in the linux subsystem, but vscoq was not able to find coqtop (maybe it still was my mistake).
Enrico Tassi (Jul 06 2020 at 11:10):Oh, now I recall the main trick: opam roots are not relocatable, so you have to build the root in the same place where it will be installed, which would be /snap/.../. This is a bit of a hack, but worked fine.
Matthieu Sozeau (Jul 06 2020 at 11:10):Karl Palmskog said:
Q: how do we establish clear boundaries on what are the responsibilities of the core devs vs. the community? Should this be documented? For example, I'm not sure it's obvious that OPAM packages for Coq releases/betas are handled by the community.
I think it should be documented indeed, so we know who does what. We don't have anything about this in the release manual?
Emilio Jesús Gallego Arias (Jul 06 2020 at 11:11):Enrico Tassi said:
Oh, now I recall the main trick: opam roots are not relocatable, so you have to build the root in the same place where it will be installed, which would be /snap/.../. This is a bit of a hack, but worked fine.
Actually that has improved quite a bit, but still a problem indeed. Let's move the discussion to its own thread tho [this is getting Gitterish :)]
Cyril Cohen (Jul 06 2020 at 11:11):Emilio Jesús Gallego Arias said:
Enrico Tassi said:
Oh, now I recall the main trick: opam roots are not relocatable, so you have to build the root in the same place where it will be installed, which would be /snap/.../. This is a bit of a hack, but worked fine.
Actually that has improved quite a bit, but still a problem indeed. Let's move the discussion to its own thread tho [this is getting Gitterish :)]
That was my main reason for switching to nix btw.
Matthieu Sozeau (Jul 06 2020 at 11:12):Karl Palmskog said:
Q: regarding high level documentation on Coq's trusted base ("what do I have to trust to trust Coq theorems"): is this something that can/should be in the manual? I think we established that the wiki page on this was obsolete.
We should certainly revisit this page indeed. We could also give much more details about what's been formalized / where so people can know which parts of the theory are more or less cutting-edge.
Karl Palmskog (Jul 06 2020 at 11:12):Matthieu Sozeau said:
Karl Palmskog said:
Q: how do we establish clear boundaries on what are the responsibilities of the core devs vs. the community? Should this be documented? For example, I'm not sure it's obvious that OPAM packages for Coq releases/betas are handled by the community.
I think it should be documented indeed, so we know who does what. We don't have anything about this in the release manual?
I think there is something about what developers/RMs will do, but not anything explicit about what the community can/should help out with
Matthieu Sozeau (Jul 06 2020 at 11:13):Ok
Théo Zimmermann (Jul 06 2020 at 11:14):Andrej Dudenhefner said:
affeldt-aist Maxime Dénès
the only thing with WSL2 I needed to do in addition was to set the actual binpath in the vscoq plugin. This was strange since that was already on PATH in the linux subsystem, but vscoq was not able to find coqtop (maybe it still was my mistake).
There is a VsCode extension that helps with this it seems. See: https://github.com/coq/coq/wiki/Installation%20of%20Coq%20on%20Windows#front-end-setup-in-wsl
Karl Palmskog (Jul 06 2020 at 11:15):I mean, this could even be something that could live in coq-community --- "at every release, coq-community members should (1) submit opam packages, (2) help out with marketing the new release and assist users to upgrade, (3) ..."
Matthieu Sozeau (Jul 06 2020 at 11:17):Karl Palmskog said:
I mean, this could even be something that could live in coq-community --- "at every release, coq-community members should (1) submit opam packages, (2) help out with marketing the new release and assist users to upgrade, (3) ..."
That sounds right. @Théo Zimmermann do you think we can formally add this to coq-community's responsibilities?
Gaëtan Gilbert (Jul 06 2020 at 11:24):Guillaume Melquiond said:
Q: How does UIP interact with kernel computations, e.g. vm/native_compute?
Currently only the "lazy" default kernel reduction understands SProp and the special reduction behaviour of UIP
VM and native reduce matches without the special reduction
Théo Zimmermann (Jul 06 2020 at 11:51):Matthieu Sozeau said:
Karl Palmskog said:
I mean, this could even be something that could live in coq-community --- "at every release, coq-community members should (1) submit opam packages, (2) help out with marketing the new release and assist users to upgrade, (3) ..."
That sounds right. Théo Zimmermann do you think we can formally add this to coq-community's responsibilities?
FWIW Karl is just as much an admin of coq-community as I am.
Matthieu Sozeau (Jul 06 2020 at 12:07):Right, I was more talking to you from the other side as you documented the release process of Coq and are currently performing one :)
Yannick Forster (Jul 07 2020 at 13:23):@Maxime Dénès I think you yesterday mentioned that there is work on native well-founded recursion, in the context where you explained the situation around native integers. Is this native wf recursion a feature independently of integers?
Last updated: Jun 01 2023 at 11:01 UTC