The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi Talia,

Your proposal to curate a list of confusing things is definitely welcome. When you have it, please submit it as a new issue on the Coq repository.

But what do you mean by "the new API which is a start"?

Théo

Le jeu. 12 avr. 2018 à 23:32, Talia Ringer <tringer AT cs.washington.edu> a écrit :

Thanks all; calling type inference worked well. Is there any performance overhead to using this over the kernel? If so, do you have an idea of how significant it is?

Also, it would be useful I think to have documentation of best practices for plugin developers, beyond the new API which is a start. It can still be difficult as a plugin developer to know which of my many options are better for which situations. I can help by curating things I've been confused about in the past, so you know what questions a plugin developer might have.

Talia

On Wed, Apr 11, 2018, 8:18 AM Emilio Jesús Gallego Arias <e AT x80.org> wrote:

Hello Talia,

Talia Ringer <tringer AT cs.washington.edu> writes:

> 1. A way to tell type-checking from within a plugin about the universe
> constraints so that it knows to solve them correctly, or
>
> 2. a way to tell type-checking from within a plugin to just assume all
> universe constraints go through, because this will always be true for me,
> and if it isn't, then the plugin will just fail later anyways
>
> I'm assuming #1 is the proper way to call type-checking from within a
> plugin, but I'm not sure how to do it.

So indeed as others have pointed out, the kernel won't infer constraints
for you anymore so you'll have to manually infer them [very cumbersome]
or call the type inference mechanism.

Coq devs are aware the universe-handling API could certainly take some
usability improvements, please, as an API user don't hesitate to share
thoughts or suggestions about it.

I think that the preferred interface these is to open an issue on
GitHub, but of course mailing list discussion is welcome too [however it
has the downside that, contrary to GH issues, it tends to be harder to
translate to concrete actionable plans].

Best,
E.