Théo Zimmermann (Jun 24 2020 at 11:14): Théo Zimmermann (Jun 24 2020 at 11:14):This is the topic to ask questions to the panelists on libraries.
Bas Spitters (Jun 29 2020 at 20:05):We have an excellent line up:
Andrej Bauer
@Cyril Cohen
@Robbert Krebbers (Gitter import)
Guilluame Melquiond
Anders Mortberg
@Karl Palmskog
If anyone has questions for the panel, please post them in this thread before, during or after the discussion.
Bas Spitters (Jun 30 2020 at 09:03):Provocative statement by Andrej Bauer, do we want to build Yahoo or Google?
https://github.com/formalabstracts/formalabstracts/issues/44
Cyril Cohen (Jun 30 2020 at 14:21):Bas Spitters said:
We have an excellent line up:
Andrej Bauer
Cyril Cohen
Robbert Krebbers (Gitter import)
Guilluame Melquiond
Anders Mortberg
Karl PalmskogIf anyone has questions for the panel, please post them in this thread before, during or after the discussion.
Hi @Bas Spitters , just so you know, names containing the string "Gitter import" here are accounts that have not been claimed by the user: you tagged Robbert Krebbers (Gitter import) he will never be notified
Bas Spitters (Jun 30 2020 at 15:36):Thanks, but I will not have another way to reach Robbert here then?
Cyril Cohen (Jun 30 2020 at 15:38):Bas Spitters said:
Thanks, but I will not have another way to reach Robbert here then?
@Bas Spitters Robbert did not join Zulip so far
Paolo Giarrusso (Jun 30 2020 at 20:20):I just pinged Robbert privately
Robbert Krebbers (Jul 01 2020 at 07:52):Here I am.
Cyril Cohen (Jul 04 2020 at 16:46):It would be nice if the other panelists could also join zulip...
Cyril Cohen (Jul 04 2020 at 16:50):@Bas Spitters do you intend to invite them too?
Anders Mörtberg (Jul 04 2020 at 19:54):Cyril Cohen said:
It would be nice if the other panelists could also join zulip...
Hi Cyril and everyone else, I'm also here :-)
Bas Spitters (Jul 04 2020 at 20:25):Done!
Andrej Bauer (Jul 05 2020 at 08:04):Hi.
Emilio Jesús Gallego Arias (Jul 05 2020 at 08:36):Hi @Andrej Bauer !
Bas Spitters (Jul 05 2020 at 09:00):Only 39 people here. Should the stream be announced more widely?
Gaëtan Gilbert (Jul 05 2020 at 09:02):Isn't it just early? the schedule says start in 30min
Andrej Bauer (Jul 05 2020 at 09:12):May I announce it on Twitter? @Bas Spitters if you announce it there, I'll retweet.
Robbert Krebbers (Jul 05 2020 at 09:16):Is the zoom thing already supposed to work? It gives " Please wait. The webinar will begin soon." for me. Is that intended?
Bas Spitters (Jul 05 2020 at 09:16):https://twitter.com/BasspittersBs/status/1279705632933896192
In 15mins. Panel on the design of libraries at the @CoqLang workshop with @andrejbauer Cyril Cohen Robbert Krebbers Guilluame Melquiond Anders Mortberg Karl Palmskog https://coq-workshop.gitlab.io/2020/#program
- Bas Spitters (@BasspittersBs) Christian Doczkal (Jul 05 2020 at 09:17):Will I (and others) be able to join the Panel session (and other Coq Workshop sessions) via browser? For the "Coffee Break" meeting I'm getting: "The meeting requires registration to join and it is not supported to join from the browser." However, this is work equipment where I am not allowed to install the Zoom Deskop client.
Bas Spitters (Jul 05 2020 at 09:19):"The webinar will begin soon..." @Emilio Jesús Gallego Arias @Théo Zimmermann could you let the panelists in?
Théo Zimmermann (Jul 05 2020 at 09:20):You should use the link that you received in an e-mail to panelists.
Emilio Jesús Gallego Arias (Jul 05 2020 at 09:20):@Bas Spitters sorry I may have sent you the wrong link
Robbert Krebbers (Jul 05 2020 at 09:20):I have used that link, but still it says "Please wait. The webinar will begin soon."
Guillaume Melquiond (Jul 05 2020 at 09:21):Same for me. I can't seem to be able to join.
Emilio Jesús Gallego Arias (Jul 05 2020 at 09:22):Try again folks
Ivanov Dmitriy (Jul 05 2020 at 09:28):It works
Théo Zimmermann (Jul 05 2020 at 09:35):Christian Doczkal said:
Will I (and others) be able to join the Panel session (and other Coq Workshop sessions) via browser? For the "Coffee Break" meeting I'm getting: "The meeting requires registration to join and it is not supported to join from the browser." However, this is work equipment where I am not allowed to install the Zoom Deskop client.
You should be able to follow through browser yes.
Christian Doczkal (Jul 05 2020 at 09:36):I am, thanks!
Enrico Tassi (Jul 05 2020 at 10:09):Q: Do we have a place where libraries are put in a searchable catalog, so that you can know where you can find what you need? (a bit rhetorical...)
Cyril Cohen (Jul 05 2020 at 10:10):Enrico Tassi said:
Q: Do we have a place where libraries are put in a searchable catalog, so that you can know where you can find what you need? (a bit rhetorical...)
You mean as Hoogle for haskell?
Enrico Tassi (Jul 05 2020 at 10:12):Yes, to me libraries are hard to build without tooling, and search is the first one that comes to mind.
Enrico Tassi (Jul 05 2020 at 10:15):Q: we organize the Coq Implementors workshop to help people dig into the OCaml code. Are people interested in organizing something similar but for libraries? (we tried once, but was then cancelled)
Arthur Charguéraud (Jul 05 2020 at 10:18):I hear "axiom agnostic library". I am not sure this is possible. In my experience, the way you set up many definitions depends on whether you can assume a strongly classic logic (classicT & epsilon) or not. Question: is there any hope you believe to have a single library that is agnostic to whether these axioms are included or not?
Andrej Dudenhefner (Jul 05 2020 at 10:19):Q: On proof engineering and coding guidelines: is there a tool that just straight tells to the user that "firstorder. eauto. eauto." is bad practice?
Théo Zimmermann (Jul 05 2020 at 10:31):To anser to Andrej, Yves did a series of videos in French.
Théo Zimmermann (Jul 05 2020 at 10:32):http://www-sop.inria.fr/members/Yves.Bertot/videos-coq/
Emilio Jesús Gallego Arias (Jul 05 2020 at 10:32):@Arthur Charguéraud I guess that ideally you should be able to abstract the class of types T that for example have choice, then let you instantiate with both classical and constructive principles; this works to some extent in math-comp [modulo the different choice for type-class resolution] , unfortunately for some cases [such as constructive vs classical analysis] the definitions are just stated differently. But at least on basic things, such as decidable equality, IMHO it should be able to be abstracted.
Enrico Tassi (Jul 05 2020 at 10:32):Tutorials about Mathematical Components: https://team.inria.fr/marelle/en/teaching/
Christian Doczkal (Jul 05 2020 at 10:33):There is the "Intorduction to Computational Logic" course by Gert Smolka at Saarland University: https://courses.ps.uni-saarland.de/icl_19/
Yves Bertot (Jul 05 2020 at 10:34):Agreeing with Robbert. I would like to have a course directed to engineers, more based on numeric computation a la Interval+gappa+Flocq, and possible with a compcert flavor.
I am currently working on some such course and developping examples with A. Appel.
Pierre Corbineau (Jul 05 2020 at 10:35):Here in Grenoble we use Coq with JF Monin to teach basic PL semantics to engineering students
Yves Bertot (Jul 05 2020 at 10:35):Of course there is a book!
Reynald Affeldt (Jul 05 2020 at 10:35):There is a list of MathComp lectures here: https://math-comp.github.io/documentation.html (it includes the lectures Cyril was talking about, I think).
Michael Soegtrop (Jul 05 2020 at 10:36):In my expereince Coq is quite OK to get into for numerical verification
Gaëtan Gilbert (Jul 05 2020 at 10:36):Looks like the course which introduced me to coq is still alive http://perso.ens-lyon.fr/daniel.hirschkoff/ThPr/
Théo Zimmermann (Jul 05 2020 at 10:37):Everyone is welcome to improve this page BTW: https://coq.inria.fr/documentation
Théo Zimmermann (Jul 05 2020 at 10:37):See here for the sources: https://github.com/coq/www/blob/master/pages/documentation.html
Emilio Jesús Gallego Arias (Jul 05 2020 at 10:38):Indeed , related to several comments it seems that all Coq UI's have little to zero support in order to discover and explore libraries; I'm not sure this is the reason we have such a diversity of libraries, but certainly seems like a hard cliff to climb for new users, specially if they want to re-use existing libs.
Yves Bertot (Jul 05 2020 at 10:38):Having good libraries to convince newcomers is crucial. the interface between newcomers and libraries is worth working on.
Andrej Bauer (Jul 05 2020 at 10:40):That was cool. Thanks everyone.
Michael Soegtrop (Jul 05 2020 at 10:40):A technical question: when you join without having a Zoom account you can only listen?
Emilio Jesús Gallego Arias (Jul 05 2020 at 10:41):Thanks everyone
Emilio Jesús Gallego Arias (Jul 05 2020 at 10:41):I think coqdoc improvements are also a strong necessity [hopefully we get some engieering support for that soon]
Michael Soegtrop (Jul 05 2020 at 10:41):I mean for such a large group it is better if only the panel speaks, but I was desparately searching for a mute button ...
Emilio Jesús Gallego Arias (Jul 05 2020 at 10:41):In particular, we should provide a good way for users to see examples
Emilio Jesús Gallego Arias (Jul 05 2020 at 10:41):"how do I use this" is a very recurring question for some libs, for example mathcomp
Bas Spitters (Jul 05 2020 at 10:41):Thanks everyone for the pleasant and interesting conversation.
Cyril Cohen (Jul 05 2020 at 10:43):Michael Soegtrop said:
A technical question: when you join without having a Zoom account you can only listen?
Actually, it is when you join as an attendent, independently of having a zoom account. If you are a panelist, you get a special invite and you can mute/unmute and display or not your video/presentation/etc... It was very confusing to me too.
Anders Mörtberg (Jul 05 2020 at 10:44):Thanks for the nice chat! And thanks to the organizers for this nice event and to the coqdevs for maintaining this great tool with so many different applications
Karl Palmskog (Jul 05 2020 at 10:44):Andrej Dudenhefner said:
Q: On proof engineering and coding guidelines: is there a tool that just straight tells to the user that "firstorder. eauto. eauto." is bad practice?
This is definitely something that would be nice to have, but initial work in this direction is for more basic properties, like whether a theorem name is appropriate. The Lean community has recently begun working on more advanced linters, which may be able to capture "wrong" tactic sequences. However, they are much more centralized than Coq. I think it's hard to find 3-4 Coq developers that could agree fully on these kind of "bad practices".
Karl Palmskog (Jul 05 2020 at 10:51):Thanks for a nice chat. Here is the list with current Coq books/tutorials we tried to compile: https://github.com/coq-community/awesome-coq#books
Christian Doczkal (Jul 05 2020 at 10:58):Karl Palmskog said:
Here is the list with current Coq books/tutorials we tried to compile: https://github.com/coq-community/awesome-coq#books
Maybe this list could be extended with a "course materials" or "lecture notes" section, for lectures that have run through a few iterations and have accumulated substantial material? (The 2019 lecture notes for the lecture I mentioned above have 180 pages.)
Karl Palmskog (Jul 05 2020 at 11:04):Christian Doczkal said:
Maybe this list could be extended with a "course materials" or "lecture notes" section, for lectures that have run through a few iterations and have accumulated substantial material?
Sure, feel free to open a pull request to do this.
Bas Spitters (Jul 05 2020 at 12:47):regarding @robbert 's request on a better specified unification. What is the status of https://github.com/mattam82/Coq-unif ? @Beta Ziliani ? @Matthieu Sozeau ?
Beta Ziliani (Jul 05 2020 at 14:30):Sorry @Bas Spitters for the late response. I forgot the existence of that development, it should be deleted @Matthieu Sozeau ;-)
I don't know what @robbert 's mean, there is such a thing and it's called Unicoq. It is not specified in Coq, but it is specified. This said, I would love to have it specified (and proved correct) in MetaCoq.
There is an on-going effort to merge code from two unification algorithms, Unicoq and Coq's evarconv, but it turns out to be harder that what I initially thought (what a surprise...).
Robbert Krebbers (Jul 05 2020 at 18:05):@Beta Ziliani What I meant is that a number of Coq tactics, including apply are broken because they use the old unification algorithm. Some people keep on telling me, don't use apply (some even said it's obsolete), but that's barely a serious suggestion since type classes and tactics like eauto use apply. AFAIK Unicoq does not fix this, because it does not change the unification algorithm used by apply.
Bas Spitters (Jul 05 2020 at 18:43):@robbert Is there a github issue connected to this, or a CEP?
Also, it would be great to report your gripes with simpl/cbn.
Bas Spitters (Jul 05 2020 at 18:53):@Yves Bertot about numerical computation. Did you look at the recent work by @Vincent Semeria and @Michael Soegtrop to include computable reals into the coq stdlib and coq platform?
Paolo Giarrusso (Jul 05 2020 at 18:59):Since I talked with Robbert recently on cbn, I have found a few links to existing reports.
(EDITED) Mixing cbn and simpl can work sometimes (and I do it), but using SimplIsCbn runs into more trouble. Issues on cbn include https://github.com/coq/coq/issues/4555 (which affected stdpp/Iris recently), https://github.com/coq/coq/issues/7389, https://github.com/coq/coq/issues/3988, https://github.com/coq/coq/issues/3989 and https://github.com/coq/coq/issues/12619.
The HoTT library also struggled with cbn (see https://github.com/HoTT/HoTT/issues/709).
Those issues don't seem easy; while cbn is described as "more principled", it seems fixing those issues might even require further research? Or at least significant resources.
On the other hand, cbn avoids some issues with simpl, such as the need for such non-extensible code: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/tactics.v#L219-266.
Paolo Giarrusso (Jul 05 2020 at 19:02):And IIUC, many of the unification issues can be found by searching for unifall — a project to replace the oldest unification, used by apply, with the less old unification, used by apply: — which isn't yet Unicoq:
https://github.com/coq/coq/issues?q=is%3Aissue+is%3Aopen+unifall
Robbert Krebbers (Jul 05 2020 at 20:05):Thanks Paolo, that's a good summary!
Robbert Krebbers (Jul 05 2020 at 22:20):Also, maybe relevant, here's an issue related to my failed attempt to switch from simpl to cbn in std++ https://gitlab.mpi-sws.org/iris/stdpp/-/issues/74
Maxime Dénès (Jul 06 2020 at 08:32):Regarding porting apply to the "evarconv" unification algorithm, I'm working actively on it, but it's a lot of work due to poorly designed interfaces between the proof engine and the elaborator.
Maxime Dénès (Jul 06 2020 at 08:35):Regarding cbn and simpl, I had investigated the differences a few years ago after @robbert reported some problems. My conclusion back then was that something should be reimplemented from scratch. simpl is hard to predict and its implementation is inefficient, while cbn has many shortcomings and is also hard to predict. For example, some documents describing cbn change the definition of addition on natural numbers to make the refolding heuristic work, whereas it doesn't on the actual stdlib definition.
Robbert Krebbers (Jul 06 2020 at 09:44):Thanks @Maxime Dénès, I'm happy to hear that you are working on the unification algorithm! Really looking forward to a fix. As I have pointed out in the past, I know that it's very hard/impossible to make something that's backwards compatible (and that would already work for the current standard library), so it would be great if there would be at least a flag that makes it possible to switch the unification algorithm locally.
Bas Spitters (Jul 06 2020 at 10:10):@Emilio Jesús Gallego Arias yesterday @Andrej Bauer asked about your effort to make the tactics independent of the stdlib, e.g. to simplify to the design of HoTT. Could you remind us about the current status?
Emilio Jesús Gallego Arias (Jul 06 2020 at 10:17):@Bas Spitters IMHO most of the stuff is there, Ali was trying to finish the remaining bits, we got delayed in the first part of the year but hopefully we can resume soon
Emilio Jesús Gallego Arias (Jul 06 2020 at 10:17):I think there is not fundamental coupling these days
Emilio Jesús Gallego Arias (Jul 06 2020 at 10:18):all that remains are bugs :)
Bas Spitters (Jul 06 2020 at 10:19):Great! ( you mean @Ali Caglayan )
Emilio Jesús Gallego Arias (Jul 06 2020 at 10:20):Yes!
Bas Spitters (Jul 06 2020 at 10:24):I should have mentioned stdlib2 and coq platform more explicitly yesterday. Glad they are discussed in the session with the developers now.
Enrico Tassi (Jul 06 2020 at 18:03):Hi @Anders Mörtberg , after a comment of yours about Unimath, I wanted to show you some code of mine that elaborates a record into nested sigma types. Actually M. Maggesi suggested this example having the Unimath library in mind. Here it is: https://github.com/LPCIC/coq-elpi/blob/master/theories/examples/example_record_to_sigma.v#L54
Bas Spitters (Jul 06 2020 at 18:37):@Enrico Tassi There is a similar tactic (issig) in HoTT:
https://github.com/HoTT/HoTT/blob/51f7c69be6f8dc997e20fe4a08f5f188d02dacd6/theories/Basics/Overture.v
It also proves that they are equivalent.
Hugo Herbelin (Jul 06 2020 at 20:04):a project to replace the oldest unification, used by apply, with the less old unification,
On the historical side, both algorithms are about the same age (the mid 90's, Coq V5.10, as Jean-Christophe explained). The first one was used for tactics, typically apply, rewrite, auto (limited conversion, existential variables not carrying a substitution, hence faster) while the second was used for type inference (more use of conversion, existential variables with substitution). Both grown "organically". The first was a rather standard form of first-order unification and it progressively incorporate other heuristics (such as Miller pattern-unification). The second is inspired from works by Dowek and Muñoz but otherwise mostly heuristical. We had to wait for Sozeau and Ziliani's paper to start having a high-level description of ideas present in the second algorithm.
Théo Zimmermann (Jul 06 2020 at 20:36):@Hugo Herbelin I thought "meta-variables" predated "existential variables"...
Hugo Herbelin (Jul 06 2020 at 21:16):A quick grep in the V5.6 and V5.10 archives show that both w_unify (the tactic algorithm) and evar_conv_x (the type inference algorithm) were first introduced in V5.10. So in terms of legacy code in the current version (since V7 adopted the kernel-centric approach but reused older code), both algorithms come from V5.10.
But indeed, "meta-variables" predated "existential variables". The first tactic engines, e.g. already in versions 4.X, used first-order-unification-like holes (w/o a substitution) (and they were called Meta). So, Evar arrived with V5.10 (roughly at the time of Dowek-Muñoz' work).
Paolo Giarrusso (Jul 06 2020 at 22:14):I see — that origin is why we have Set Debug Tactic Unification and Set Debug Unification. Are those the current names?
Hugo Herbelin (Jul 06 2020 at 22:17):Which names? If you are talking about w_unify (which is traced by Set Debug Tactic Unification and evar_conv_x (which is traced by Set Debug Unification), these are the current names.
Last updated: May 31 2023 at 04:01 UTC