Rocq Object Metadata

[CohenCyril]

No description provided.

[andres-erbsen]

I am in favor of this concept; subscribing. Small comments on the sketched details

For docstrings, comments right before the definition are somewhat of a cross-language standard at this point. We should consider adopting it.

Perhaps alias could be called "suggest"? I think the idea of adding additional searches in response to which a definition should be shown is desirable, but I am less sure about convertibility as a central concept there. Sometimes a non-convertible definition is a good search result anyway, and at other times a convertible definition is not applicable because heuristic conversion takes too long. Instead I'd trust the metadata author to choose what searches the definition should be shown for without relating that choice to convertibility.

I'd also be interested in having Search display the already-stored metadata, for example warnings.

[spitters]

Have you considered the lean search tools?
https://leansearch.net/ (https://github.com/leanprover-community/LeanSearchClient)
https://www.leanexplore.com/
https://loogle.lean-lang.org/
https://www.moogle.ai/

It would be nice to have something along these lines for Rocq.
I guess that my be connected to this rfcs...

[CohenCyril]

I am in favor of this concept; subscribing. Small comments on the sketched details

For docstrings, comments right before the definition are somewhat of a cross-language standard at this point. We should consider adopting it.

I agree with you, we should opt for that.

Perhaps alias could be called "suggest"? I think the idea of adding additional searches in response to which a definition should be shown is desirable, but I am less sure about convertibility as a central concept there. Sometimes a non-convertible definition is a good search result anyway, and at other times a convertible definition is not applicable because heuristic conversion takes too long. Instead I'd trust the metadata author to choose what searches the definition should be shown for without relating that choice to convertibility.

Yes, I agree. Or maybe "similar" or "related"... or something drawn from ontology concepts?

I'd also be interested in having Search display the already-stored metadata, for example warnings.

What do you mean "for example warnings" ?

[CohenCyril]

Have you considered the lean search tools? https://leansearch.net/ (https://github.com/leanprover-community/LeanSearchClient) https://www.leanexplore.com/ https://loogle.lean-lang.org/ https://www.moogle.ai/

It would be nice to have something along these lines for Rocq. I guess that my be connected to this rfcs...

Yes of course, I know several people working in this direction, and it is definitely connected to this rfcs since it should provide all the meta-data required by the potential applications.

[CohenCyril]

I did not know about leanexplore, thanks for mentioning it