Stream: Coq devs & plugin devs

Topic: deprecation for definitions


view this post on Zulip Ali Caglayan (Mar 16 2022 at 18:16):

I think if we wanted to implement deprecated for gallina terms we would do it when tackling CEP 42 https://github.com/coq/ceps/pull/42

view this post on Zulip Ali Caglayan (Mar 16 2022 at 18:16):

I had a look a while back, and extending all the warnings etc. to gallina terms will take some work

view this post on Zulip Pierre-Marie Pédrot (Mar 16 2022 at 18:20):

I don't think this has much to do with that CEP though.

view this post on Zulip Pierre-Marie Pédrot (Mar 16 2022 at 18:21):

it's just a matter of adding a warning in the pretyper, this should cover 90% of the use-cases

view this post on Zulip Pierre-Marie Pédrot (Mar 16 2022 at 18:21):

(to whomever wants to implement that: just tweak Pretyping.pretype_ref)

view this post on Zulip Pierre-Marie Pédrot (Mar 16 2022 at 18:23):

actually, maybe the intern phase would be a better place otherwise this will get spammy with tactics using internally glob constrs

view this post on Zulip Ali Caglayan (Mar 16 2022 at 18:23):

What would happen if you deprecated an instance? Would typeclass search spam it every time it was checked?

view this post on Zulip Pierre-Marie Pédrot (Mar 16 2022 at 18:24):

no, this is already resolved by then

view this post on Zulip Pierre-Marie Pédrot (Mar 16 2022 at 18:24):

you'd see it for uconstr:() and the like

view this post on Zulip Gaëtan Gilbert (Mar 16 2022 at 18:24):

if you put the warning in intern it should only impact uses directly in the code

view this post on Zulip Pierre-Marie Pédrot (Mar 16 2022 at 18:24):

yep, this looks like the desired behaviour

view this post on Zulip Pierre-Marie Pédrot (Mar 16 2022 at 18:25):

(there will be a few misses like e.g. commands that take a globref as argument but this can be done in a second time)

view this post on Zulip Notification Bot (Mar 16 2022 at 18:25):

12 messages were moved here from #Coq users > Compilation error in coq-json with coq-dev GitHub action by Ali Caglayan.

view this post on Zulip Ali Caglayan (Mar 16 2022 at 18:26):

constrintern?

view this post on Zulip Pierre-Marie Pédrot (Mar 16 2022 at 18:26):

somewhere around Constrintern.intern_reference

view this post on Zulip Ali Caglayan (Mar 16 2022 at 18:27):

Cool I'll see what I can do later

view this post on Zulip Pierre-Marie Pédrot (Mar 16 2022 at 18:27):

or intern_qualid rather

view this post on Zulip Emilio Jesús Gallego Arias (Mar 16 2022 at 18:34):

You could even put it in vernac not?

view this post on Zulip Ali Caglayan (Mar 16 2022 at 18:34):

But if you deprecate an expression how will you throw a warning without interpreting it?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 16 2022 at 18:34):

ah never mind

view this post on Zulip Emilio Jesús Gallego Arias (Mar 16 2022 at 18:35):

indeed the registration should go there

view this post on Zulip Emilio Jesús Gallego Arias (Mar 16 2022 at 18:35):

of course you need to put in the name resolution in interp

view this post on Zulip Emilio Jesús Gallego Arias (Mar 16 2022 at 18:35):

I'm a bit tired I guess


Last updated: Feb 05 2023 at 22:03 UTC