[CEP] Proposal for libobject API refactoring

[ejgallego]

trafficstars

Rendered version here

[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 https://github.com/coq/coq/pull/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