Stream: Coq devs & plugin devs

Topic: side effects are evil


view this post on Zulip Gaëtan Gilbert (Mar 10 2021 at 16:08):

What do we do about https://github.com/coq/coq/issues/13834 ?

view this post on Zulip Gaëtan Gilbert (Mar 10 2021 at 16:08):

cc @Pierre-Marie Pédrot

view this post on Zulip Enrico Tassi (Mar 10 2021 at 19:11):

Can't we move toward having the rewrite principles declared in advance? The lazy creation/declaration of these lemmas brings very little.
I mean Error: you can't rewrite with foo unless you first run Whatever Scheme foo or decorate foo with #[rewrite].

view this post on Zulip Enrico Tassi (Mar 10 2021 at 19:12):

I totally agree side effects are evil, but there are some which are kind of justified, and some others that look like they were added "for sport" like this one.

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2021 at 10:03):

It's even worse than that: since the rewrite side-effects are globally visible inside a Defined proof, this is a source of non-determinism.

view this post on Zulip Gaëtan Gilbert (Mar 11 2021 at 11:42):

how so?

view this post on Zulip Matthieu Sozeau (Mar 12 2021 at 10:01):

It's a terrible side-effect I think. And IIRC in a universe polymorphic proof it does generalize over unnecessary universes.

view this post on Zulip Enrico Tassi (Mar 12 2021 at 13:17):

So, if we agree that we should generated these term ahead of time, maybe we should plan something. Still I have a memory of some cases in which there are many possible terms, and we don't know which ones (I think @Matthieu Sozeau told me this once). In any case we can design commands to generate the ones the user needs and have good error messages about what the user should run.


Last updated: Oct 21 2021 at 22:02 UTC