Stream: Coq workshop 2020

Topic: [M] Session with the Coq developers


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

This is the topic to ask questions to the Coq developers during the discussion session.

view this post on Zulip Théo Zimmermann (Jul 06 2020 at 09:06):

This session will start in one hour.

view this post on Zulip Théo Zimmermann (Jul 06 2020 at 09:06):

After Jean-Christophe's talk.

view this post on Zulip Théo Zimmermann (Jul 06 2020 at 09:07):

Start asking questions for the Coq developers as soon as you want.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Jul 06 2020 at 09:33):

@Théo Zimmermann : yes, sure

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Jul 06 2020 at 09:39):

@Michael Soegtrop I guess that would be nicer to see you indeed :)

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Jul 06 2020 at 09:51):

Only since you are a panelist?

view this post on Zulip Gaëtan Gilbert (Jul 06 2020 at 09:51):

it didn't happen yesterday
that's all I know

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Jul 06 2020 at 09:55):

OK let's try that.

view this post on Zulip Théo Zimmermann (Jul 06 2020 at 09:55):

Oh in fact I see you are already there

view this post on Zulip 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 ...

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

@Théo Zimmermann : I can't start video - it says the host has stopped it

view this post on Zulip Chantal Keller (Jul 06 2020 at 10:10):

Q. on Coq 8.12: which changes are relevant when implementing an OCaml plugin?

view this post on Zulip Bas Spitters (Jul 06 2020 at 10:17):

https://github.com/coq/coq/wiki/Future+plans

view this post on Zulip 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)?

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Chantal Keller (Jul 06 2020 at 10:24):

Thanks for the answer

view this post on Zulip 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

view this post on Zulip Chantal Keller (Jul 06 2020 at 10:25):

Q. on native arrays: what is the status? Will they be integrated in Coq-8.13?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Chantal Keller (Jul 06 2020 at 10:31):

Thanks a lot Maxime, I will be happy to provide benchmarks!

view this post on Zulip Andrej Dudenhefner (Jul 06 2020 at 10:31):

Q: Does vscoq have a release schedule / roadmap? The TODO file was updated 4 years ago.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Samuel Hym (Jul 06 2020 at 10:41):

Q: What are the current plans / roadmap about IDEs?

view this post on Zulip Enrico Tassi (Jul 06 2020 at 10:42):

@Karl Palmskog Why? And what time frame would not be, in your opinion?

view this post on Zulip Cyril Cohen (Jul 06 2020 at 10:43):

The panel of yesterday never entered stdlib topic :-( (my mistake too)

view this post on Zulip 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 :-)

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Jul 06 2020 at 10:44):

@Cyril Cohen oh, right, my bad!

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 10:45):

@Maxime Dénès where is the roadmap for the document server?

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Jul 06 2020 at 10:45):

It's somewhere on github IIRC

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 10:46):

I mean, there is only the branch? No design / RFC?

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Jul 06 2020 at 10:46):

The "document manager" PR for VSCode is https://github.com/coq-community/vscoq/pull/140

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 10:46):

IIRC commit didn't say a lot on the approach used

view this post on Zulip 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. :-(

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 10:48):

@Evgeny Makarov you have Yves' Coq plugin tutorial

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 10:48):

it is distributed with Coq these days

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 :))

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (Jul 06 2020 at 10:55):

Q: How does UIP interact with kernel computations, e.g. vm/native_compute?

view this post on Zulip Théo Zimmermann (Jul 06 2020 at 10:58):

sure!

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

I think this stdlib discussion warrants a new dedicated thread BTW :wink:

view this post on Zulip Cyril Cohen (Jul 06 2020 at 11:00):

I could hand-pick messages and put them in the new topic

view this post on Zulip Cyril Cohen (Jul 06 2020 at 11:00):

give me 1min

view this post on Zulip 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.)

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

At some point WSL required dev mode. But this has probably changed before WSL2.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Jul 06 2020 at 11:05):

Here my snap "experiment": https://github.com/gares/coq-opam-snap

view this post on Zulip 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.

view this post on Zulip Chantal Keller (Jul 06 2020 at 11:06):

Thanks! :clap: for the development of Coq

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 11:07):

@Gaëtan Gilbert I'm not sure we answered Guillaume question about UIP

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Jul 06 2020 at 11:08):

Thanks for this very nice session.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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 :)]

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Jul 06 2020 at 11:13):

Ok

view this post on Zulip 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

view this post on Zulip 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) ..."

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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: Feb 06 2023 at 05:03 UTC