Stream: Coq devs & plugin devs

Topic: Excluding constants from Search


view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Jun 10 2020 at 13:22):

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

view this post on Zulip Théo Zimmermann (Jun 10 2020 at 13:22):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Jun 10 2020 at 13:23):

abstract: _subproof
transparent_abstract: _subterm

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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: Oct 21 2021 at 21:03 UTC