This is the topic to ask questions to the panelists on libraries.

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.

Provocative statement by Andrej Bauer, do we want to build Yahoo or Google?

https://github.com/formalabstracts/formalabstracts/issues/44

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

Thanks, but I will not have another way to reach Robbert here then?

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

I just pinged Robbert privately

Here I am.

It would be nice if the other panelists could also join zulip...

@Bas Spitters do you intend to invite them too?

Cyril Cohen said:

It would be nice if the other panelists could also join zulip...

Hi Cyril and everyone else, I'm also here :-)

Done!

Hi.

Hi @Andrej Bauer !

Only 39 people here. Should the stream be announced more widely?

Isn't it just early? the schedule says start in 30min

May I announce it on Twitter? @Bas Spitters if you announce it there, I'll retweet.

Is the zoom thing already supposed to work? It gives " Please wait. The webinar will begin soon." for me. Is that intended?

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)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.

"The webinar will begin soon..." @Emilio Jesús Gallego Arias @Théo Zimmermann could you let the panelists in?

You should use the link that you received in an e-mail to panelists.

@Bas Spitters sorry I may have sent you the wrong link

I have used that link, but still it says "Please wait. The webinar will begin soon."

Same for me. I can't seem to be able to join.

Try again folks

It works

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.

I am, thanks!

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...)

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?

Yes, to me libraries are hard to build without tooling, and search is the first one that comes to mind.

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)

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?

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?

To anser to Andrej, Yves did a series of videos in French.

http://www-sop.inria.fr/members/Yves.Bertot/videos-coq/

@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.

Tutorials about Mathematical Components: https://team.inria.fr/marelle/en/teaching/

There is the "Intorduction to Computational Logic" course by Gert Smolka at Saarland University: https://courses.ps.uni-saarland.de/icl_19/

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.

Here in Grenoble we use Coq with JF Monin to teach basic PL semantics to engineering students

Of course there is a book!

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).

In my expereince Coq is quite OK to get into for numerical verification

Looks like the course which introduced me to coq is still alive http://perso.ens-lyon.fr/daniel.hirschkoff/ThPr/

Everyone is welcome to improve this page BTW: https://coq.inria.fr/documentation

See here for the sources: https://github.com/coq/www/blob/master/pages/documentation.html

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.

Having good libraries to convince newcomers is crucial. the interface between newcomers and libraries is worth working on.

That was cool. Thanks everyone.

A technical question: when you join without having a Zoom account you can only listen?

Thanks everyone

I think coqdoc improvements are also a strong necessity [hopefully we get some engieering support for that soon]

I mean for such a large group it is better if only the panel speaks, but I was desparately searching for a mute button ...

In particular, we should provide a good way for users to see examples

"how do I use this" is a very recurring question for some libs, for example mathcomp

Thanks everyone for the pleasant and interesting conversation.

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.

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

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".

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

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.)

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.

regarding @robbert 's request on a better specified unification. What is the status of https://github.com/mattam82/Coq-unif ? @Beta Ziliani ? @Matthieu Sozeau ?

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...).

@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`

.

@robbert Is there a github issue connected to this, or a CEP?

Also, it would be great to report your gripes with simpl/cbn.

@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?

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.

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

Thanks Paolo, that's a good summary!

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

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.

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.

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.

@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?

@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

I think there is not fundamental coupling these days

all that remains are bugs :)

Great! ( you mean @Ali Caglayan )

Yes!

I should have mentioned stdlib2 and coq platform more explicitly yesterday. Glad they are discussed in the session with the developers now.

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

@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.

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.

@Hugo Herbelin I thought "meta-variables" predated "existential variables"...

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).

I see — that origin is why we have `Set Debug Tactic Unification`

and `Set Debug Unification`

. Are those the current names?

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