The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Hi Talia,

Le 13/04/2018 à 00:31, Talia Ringer 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?

This was answered to me by Guillaume Melquiond a few years ago in
  https://sympa.inria.fr/sympa/arc/coq-club/2016-10/msg00007.html

I copy-paste his answer below:

<< Unfortunately, it means type-checking your term twice, which you
precisely wanted to avoid since you are calling exact_no_check. Another
solution is thus not too call Typing.type_of on your new term, but on a
smaller simpler dummy term. If your dummy term (whatever its type)
happens to produce the exact same universe constraints as your new term,
then you are good to go and you can use the produced evarmap instead. >>

I confirm that Guillaume's hack is simple and (still) works well for me...

Best Regards,

Sylvain.


> 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 
> <mailto:e AT x80.org>> wrote:
>
>     Hello Talia,
>
>     Talia Ringer 
> <tringer AT cs.washington.edu
>     
> <mailto: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.