Stream: Coq users

Topic: Search Blacklist everything but what's imported?


view this post on Zulip Pierre Rousselin (Dec 05 2023 at 06:46):

I want to Import selectively a very small part of Arith.PeanoNat.Nat and then Add Search Blacklist everything else.

  1. Is it possible? I have tried Add Search Blacklist "PeanoNat". but this blacklists the imported lemmas as well.
  2. Is there any way with Search to get only what's imported? (Bonus: And what is added in the file itself?)

view this post on Zulip Cyril Cohen (Dec 05 2023 at 10:39):

During the last 15 years, I never found out how to properly pre-configure the filtering out of search results nor hack a way to do it. There are two things I usually do though:

view this post on Zulip Michael Soegtrop (Dec 05 2023 at 11:26):

I use Elpi for advanced symbol management, but afaik it doesn't have a search blacklist command. If it would have, the things you want to do should be easy with Elpi. @Enrico Tassi : would this be hard to add?

Of course this doesn't help you with current Coq, but what you can do with Elpi as is is to auto generate a Coq file with fine grained blacklist commands and include this in your student work. I can send you example code which I use for managing delta symbol lists. You can use the same frontend and just replace the file output. I also write include files I then use for Ltac2.

view this post on Zulip Michael Soegtrop (Dec 05 2023 at 11:27):

Btw.: another application for symbol set management commands in Coq.

view this post on Zulip Enrico Tassi (Dec 05 2023 at 12:17):

For this use case, I'd add #[blacklist] to both lemmas/definitions and modules.
And yes, the blacklist attribue could be an instance of #[label="search_blacklist"] with a corresponding API for meta programs to get the set of constants with a given label., covering also the use case of @Michael Soegtrop / VST.

view this post on Zulip Paolo Giarrusso (Dec 05 2023 at 12:30):

@Enrico Tassi I think Pierre can't use a (definition-time) attribute (tho it'd be nice elsewhere): he's teaching an intro class, and wants to hide things that normally should be seen.

view this post on Zulip Michael Soegtrop (Dec 05 2023 at 12:46):

@Enrico Tassi : what I more envisioned is some sort of module set operation interface to blacklist search results. I have something like this (very simple) for delta list, which would need only few changes to create include files. What would be convenient is an elpi command to add / remove symbols to the search black list.

view this post on Zulip Pierre Rousselin (Dec 05 2023 at 15:13):

Thank you very much all of you for your answers.

view this post on Zulip Gaëtan Gilbert (Dec 05 2023 at 15:20):

is there anything close to the static (or just static inline) attributes in C?

Can you rephrase for those who don't know C?

view this post on Zulip Karl Palmskog (Dec 05 2023 at 15:22):

I guess "static" is meant in this sense:

A static global variable or a function is "seen" only in the file it's declared in

view this post on Zulip Karl Palmskog (Dec 05 2023 at 15:23):

the other sense of static doesn't make sense in a pure language

view this post on Zulip Pierre Rousselin (Dec 05 2023 at 15:25):

and static inline is the same but asking gently to the compiler to replace the function by its definition if possible, to avoid a function call.

view this post on Zulip Karl Palmskog (Dec 05 2023 at 15:27):

one problem with analogies to C is that Coq has no compile-time/runtime phase distinction

view this post on Zulip Pierre Rousselin (Dec 05 2023 at 15:28):

Karl Palmskog said:

one problem with analogies to C is that Coq has no compile-time/runtime phase distinction

but it could be asked that the proof term is replaced whenever it is used.

view this post on Zulip Karl Palmskog (Dec 05 2023 at 15:29):

"replace when used" seems like an implementation detail (optimization?) and not a semantics/interface thing

view this post on Zulip Pierre Rousselin (Dec 05 2023 at 15:31):

Wouldn't it make it easier to hide say #[static] Lemma A from the rest of the world if it were replaced everywhere by its definition? (I'm starting to feel scared that my huge ignorance will be revealed...)

view this post on Zulip Karl Palmskog (Dec 05 2023 at 15:36):

hmm, I'm not sure I follow the terminology here, here's what I usually use:

"hiding A from the rest of the world" could have several meanings:

view this post on Zulip Kenji Maillard (Dec 05 2023 at 15:41):

Pierre Rousselin said:

but it could be asked that the proof term is replaced whenever it is used.

I think the Let vernacular does this kind of inlining (or rather substitutions). But it's not an attribute on Lemma/Definition.

view this post on Zulip Karl Palmskog (Dec 05 2023 at 15:42):

right, I think Let processing is done before actually creating constants?

view this post on Zulip Pierre Rousselin (Dec 05 2023 at 15:44):

Thank you very much. I will investigate about Letto see if it can be used to tidy things up (instead of the current _subproof or Private).

view this post on Zulip Karl Palmskog (Dec 05 2023 at 15:47):

so, maybe one can say that Let triggers inlining at constant creation time, since to my knowledge there is no event in Coq for a term getting "used" at runtime

view this post on Zulip Gaëtan Gilbert (Dec 05 2023 at 15:49):

Let is only in sections, probably won't be useful for you

view this post on Zulip Paolo Giarrusso (Dec 05 2023 at 15:55):

the closest things to static inline are Notation (easy to use, but has restrictions) and Parameter Inline (only relevant with module linking).

view this post on Zulip Paolo Giarrusso (Dec 06 2023 at 11:11):

Pierre Rousselin said:

Thank you very much. I will investigate about Letto see if it can be used to tidy things up (instead of the current _subproof or Private).

The point of _subproof is to _intentionally_ deinline parts of a term to fix transparency problems.

Definition some_num (n : nat) : { m : nat | n + m < n + 10 }.
exists 0.
(* goal n + 0 < n + 10 *) abstract lia.
Defined.

here, we want 0 to be visible to clients, and the proof produced by lia should be hidden into a separate, Qed'ed _subproof constant — otherwise, Eval compute in some_num ). Program can create similar proof terms. Avoiding abstract` will avoid the extra constant, but normalizing the result will be more expensive


Last updated: Jun 23 2024 at 04:03 UTC