[CEP] Proposal for libobject API refactoring

[ejgallego]

Rendered version here

[SkySkimmer]

Does this refer to a branch somewhere or is more like "for now we propose to start with a reverse map for names"?

[ejgallego]

This is implemented in the prototype branch, cleaning it up to submit as we speak.

[ejgallego]

PR done, you can use (hack hack) Print Graph to print the reverse map

[SkySkimmer]

Note that currently I believe the only part of libobject which modifies the safe_env is the Require replay after closing section/module (in_require in library.ml).

[ejgallego]

Yup, that's correct. Tho the trait is meant to capture objects that call the diverse Global.* functions, so at some point the env can be owned by declaremods.

[ejgallego]

I've clarified this a bit in an update.

[SkySkimmer]

My understanding is that currently nametab itself is not uniform (there are separate tables for globref, modules, ltacs, some other stuff) so this may require a nametab redesign first.

[ppedrot]

FTR I think that unifying the various nametabs is gong the wrong way. It's a feature that each plugin can define its own set of names, so the design critically needs to account for this.

[ejgallego]

Yes, the idea is that when an object declares a nametab trait, it does so with their own nametab. Refactoring is indeed needed, you can see current progress here, but need to advance more https://github.com/ejgallego/coq/blob/f059e5a57e95c5c80a3c9026e91ba91936d90db5/library/nametab.mli

Ideally, if we think this is a good idea we would do such a change in two steps:

• we would first define the trait, which takes a module as a parameter and performs the imperative state
• we would then push the trait to be functional, and have Declaremods own the nametab.

[ejgallego]

Clarified a bit.

[gares]

Can you explain how the proposed approach solves/improves-on the downsides of the current approach, in particular:

• there is no possibility to systematically explore the list of objects currently in scope (other than hoping the ad-hoc internal structures are somehow exposed)

• in some cases (such as printing), we need to perform a costly (and messy) global imperative state update as to simulate that a module has been opened, due to the imperative nature of the module system implementation

[ejgallego]

• there is no possibility to systematically explore the list of objects currently in scope (other than hoping the ad-hoc internal structures are somehow exposed)

For this see for example coq/coq#16261 , and how the API with the reverse map introduced here is used in Search and Locate. If we move Category.t in that PR to the data, one could have a reverse map on categories too. What metadata to add is a bit open, for now I was thinking of documentation as sketched in the proposal for liberabaci.

• in some cases (such as printing), we need to perform a costly (and messy) global imperative state update as to simulate that a module has been opened, due to the imperative nature of the module system implementation

Hopefully the Named trait could be used to avoid the global state update for the Nametab in printmod.ml

[maximedenes]

Is there a description of the Behavior API?

[ejgallego]

I don't have a too precise view on how to implement it, there are several options so here we can use some feedback.

I guess for the first prototype I'd try to have a list of traits, indeed due to the existential nature of traits that would mean turning the declaration of objects into a module, but I think I'm fine with that (as in the case for the proposal about errors in coq/coq#12602)