Stream: Coq devs & plugin devs

Topic: Excluding constants from Search

Cyril Cohen (Jun 10 2020 at 13:07):

Cyril Cohen said:

Maxime Dénès said:

I see, thanks. I guess we should figure out a way to properly generate constants on the fly, then.

If so they must be automatically tagged in a way to exclude them from Search

Théo Zimmermann said:

It's easy and we're already doing this for abstract lemmas.

Oh, really? how is it done?

Théo Zimmermann (Jun 10 2020 at 13:22):

https://github.com/coq/coq/blob/95be052f60b1b6b4cc0b12e92b3d1b86b5bd7ca9/theories/Init/Prelude.v#L59

Théo Zimmermann (Jun 10 2020 at 13:22):

Add Search Blacklist "_subproof" "_subterm" "Private_".

Théo Zimmermann (Jun 10 2020 at 13:22):

I know it's not a perfect solutions and nobody likes it, but it has the serious advantage of being already available and it works.

Cyril Cohen (Jun 10 2020 at 13:23):

Théo Zimmermann said:

Add Search Blacklist "_subproof" "_subterm" "Private_".

Oh :sad: ok, concretely which suffix/prefix do you use for abstract?

Théo Zimmermann (Jun 10 2020 at 13:23):

abstract: _subproof
transparent_abstract: _subterm

Théo Zimmermann (Jun 10 2020 at 13:24):

See https://coq.github.io/doc/master/refman/proof-engine/ltac.html#proving-a-subgoal-as-a-separate-lemma-abstract

Cyril Cohen (Jun 10 2020 at 13:24):

Maxime Dénès said:

Search blacklisting should be done by an attribute, not hacking a prefix IMHO

I had hoped there was already some support for this :up:

Théo Zimmermann (Jun 10 2020 at 13:33):

Precisely not. I'd be easy to implement but there is no support today. My point was that this is not the issue at stake here.

Théo Zimmermann (Jun 10 2020 at 13:36):

Anyway, I'd like to get an answer regarding whether we backtrack on the deprecation in 8.12 from @Pierre-Marie Pédrot / @Maxime Dénès / @Matthieu Sozeau before we tag the beta.

Last updated: Apr 19 2024 at 00:02 UTC