Stream: Coq devs & plugin devs

Topic: deprecation for definitions

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

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

Pierre-Marie Pédrot (Mar 16 2022 at 18:20):

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

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

Pierre-Marie Pédrot (Mar 16 2022 at 18:21):

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

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

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?

Pierre-Marie Pédrot (Mar 16 2022 at 18:24):

no, this is already resolved by then

Pierre-Marie Pédrot (Mar 16 2022 at 18:24):

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

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

Pierre-Marie Pédrot (Mar 16 2022 at 18:24):

yep, this looks like the desired behaviour

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)

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.

Ali Caglayan (Mar 16 2022 at 18:26):

constrintern?

Pierre-Marie Pédrot (Mar 16 2022 at 18:26):

somewhere around Constrintern.intern_reference

Ali Caglayan (Mar 16 2022 at 18:27):

Cool I'll see what I can do later

Pierre-Marie Pédrot (Mar 16 2022 at 18:27):

or intern_qualid rather

Emilio Jesús Gallego Arias (Mar 16 2022 at 18:34):

You could even put it in vernac not?

Ali Caglayan (Mar 16 2022 at 18:34):

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

Emilio Jesús Gallego Arias (Mar 16 2022 at 18:34):

ah never mind

Emilio Jesús Gallego Arias (Mar 16 2022 at 18:35):

indeed the registration should go there

Emilio Jesús Gallego Arias (Mar 16 2022 at 18:35):

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

Emilio Jesús Gallego Arias (Mar 16 2022 at 18:35):

I'm a bit tired I guess

Last updated: Dec 05 2023 at 04:01 UTC