Stream: Coq devs & plugin devs

Topic: Small uniformity of naming and structure in entries.ml?


view this post on Zulip Hugo Herbelin (May 31 2024 at 08:23):

Hi, if I flatten (from entries.ml and safe_typing.ml):

type constant_entry =
  | DefinitionEntry : definition_entry -> constant_entry
  | ParameterEntry : parameter_entry -> constant_entry
  | PrimitiveEntry : primitive_entry -> constant_entry
  | SymbolEntry : symbol_entry -> constant_entry

type global_declaration =
  | ConstantEntry : Entries.constant_entry -> global_declaration
  | OpaqueEntry : unit Entries.opaque_entry -> global_declaration

into only (in entries.ml)

type constant_entry =
  | OpaqueEntry : unit opaque_entry -> constant_entry
  | DefinitionEntry : definition_entry -> constant_entry
  | ParameterEntry : parameter_entry -> constant_entry
  | PrimitiveEntry : primitive_entry -> constant_entry
  | SymbolEntry : symbol_entry -> constant_entry

then draw according structure and naming uniformizations from it, especially in add_constant, do you see objections?

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:24):

I'm pretty sure this is here for static typing reasons in Safe_typing

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:26):

I'd advise against trying to merge types and APIs when there is clear use of static invariants expressed in the types.

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:27):

Some serious time has been passed in making invariants as precise as possible, especially around the kernel API, so please do not disrupt without a clear cut explanation.

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:28):

Code smells include having to introduce assertions here and there.

view this post on Zulip Hugo Herbelin (May 31 2024 at 08:30):

There seems indeed to be a play between constant_typing.ml, which does not set bytecode nor final body, and safe_typing.ml. Are there particular reasons why constant_typing.ml does not set them itself?

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:31):

Constant typing is too low-level, it's only concerned about typing the body

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:31):

plus there are some tricky horrors related to the with Definition clause for bytecode

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:32):

once again I've passed unreasonable amounts of time exposing static invariants in there. The Declare layer maybe broken, but at least the kernel is somewhat more rigid.

view this post on Zulip Hugo Herbelin (May 31 2024 at 08:32):

So, you mean that, somehow, it is rather that the bytecode field should be extracted out of the constant_body record?

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:33):

no ?

view this post on Zulip Hugo Herbelin (May 31 2024 at 08:34):

once again I've passed unreasonable amounts of time exposing static invariants in there

Yes, I'm precisely asking because I see that indeed a lot of care has been taken in ensuring static typing invariants.

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:34):

why do you want to change it then?

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:34):

there has been no changes in the kernel that warrant an API change

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:35):

you should try to bubble up these invariants to Declare, not the other way around

view this post on Zulip Hugo Herbelin (May 31 2024 at 08:35):

It is about the interaction with declare.ml being broken. It is about trying to make the structure and motivations for this structure easier to follow.

view this post on Zulip Hugo Herbelin (May 31 2024 at 08:36):

you should try to bubble up these invariants to Declare, not the other way around

Indeed, I'm trying to make them closer.

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:36):

it's definitely declare that needs fixing, not the kernel

view this post on Zulip Hugo Herbelin (May 31 2024 at 08:37):

When you look at add_constant, the first thing it does it is precisely to split (in two steps) over these 5 entries, with extra ad hoc treatments. Somehow the question is what it would imply to merge the two-step split into one?

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:39):

I don't know which part of the code you're referring to

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:39):

in Constant_typing you mean?

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:42):

As a general rule of thumb, a shorter API is not a better API. There are reason why some signatures take an explicit data rather than an option, this kind of stuff.

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 08:42):

In OCaml, defining algebraic types is cheap. Use them to rule out impossible cases statically.

view this post on Zulip Hugo Herbelin (May 31 2024 at 09:03):

There is a first split in safe_typing.ml and a second in constant_typing.ml.

view this post on Zulip Hugo Herbelin (May 31 2024 at 09:05):

I wonder what it would imply to inline the case split done in infer_constant in constant_typing.ml inside safe_typing.ml. Would it break invariants?

view this post on Zulip Hugo Herbelin (May 31 2024 at 09:07):

Secondarily to the question of one-step vs two-steps case split, is it important that the final const_body for opaque is set in safe_typing.ml and not directly in infer_opaque in constant_typing.ml?

view this post on Zulip Pierre-Marie Pédrot (May 31 2024 at 09:09):

For the second point, I think it is indeed relatively important. This separates type-checking per se from other computations about the constant.

view this post on Zulip Hugo Herbelin (May 31 2024 at 09:51):

OK, I see. So, the idea is really to separate the pure CCI part (in constant_typing.ml) and the non purely CCI part (bytecode and opacity tricks, in safe_typing.ml), right?

view this post on Zulip Hugo Herbelin (May 31 2024 at 09:52):

Then, flattening the two case splits into one is compatible with this distinction.

view this post on Zulip Hugo Herbelin (Jun 09 2024 at 07:53):

Could the handle for opaque entries be the kernel name itself, rather than an object of some abstract type? Any Opaqueproof.opaque is associated to a unique kernel name, right?

For instance, could Safe_typing.check_opaque could instead take a kernel name as input?

Such change woud provide a more "logically-minded" model.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2024 at 12:58):

IMHO @Hugo Herbelin any change here is moot without a proof of concept of the upper layers taking advantage of it.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2024 at 12:58):

Which we don't have at the moment IMO.

view this post on Zulip Hugo Herbelin (Jun 09 2024 at 14:04):

What do "upper layers" need? For instance, supporting concurrent constructions of safe environments and, eventually, safe merge of such concurrently-built safe environments be enough?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2024 at 14:16):

It is not clear @Hugo Herbelin

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2024 at 14:16):

I mean, it is hard to know before a fully prototype is assembled

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2024 at 14:17):

as there are several possible design approaches.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2024 at 14:22):

What are you trying to do here?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2024 at 14:22):

How do you envision the API being used?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2024 at 14:23):

Hugo Herbelin said:

What do "upper layers" need? For instance, supporting concurrent constructions of safe environments and, eventually, safe merge of such concurrently-built safe environments be enough?

That looks pretty complicated to me, what would be such an scenario?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2024 at 14:33):

But maybe we can discuss in the call if thing would be easier, or at IRIF

view this post on Zulip Hugo Herbelin (Jun 09 2024 at 14:36):

What are you trying to do here?

If you are asking about me, I'm mostly guided these days by simplifying, clarifying, documenting the current code in declare.ml, with the idea that not only CEP #42 will be easier to implement but the technical debt will diminish, the maintenance will be easier, and the generality of the code will increase.

I did not have in mind "upper layers" a priori and I actually don't know what you are exactly referring to by the words "upper layers" (though I suspect you mean "document managers").

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2024 at 14:39):

By upper layers indeed I mean whoever is calling that API.

view this post on Zulip Hugo Herbelin (Jun 09 2024 at 14:39):

For instance, supporting concurrent constructions of safe environments and, eventually, safe merge of such concurrently-built safe environments be enough?

Isn't it basically what we already provide for the logical part? (But building concurrently the non-logical part might be much more complex.)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2024 at 14:39):

Usually the document managers fit this role, but who knows, there are other parts. (For example state handling is both used by the document managers and section mechanism, a design that makes things very complex sometimes)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2024 at 14:39):

Regarding the cleanups, I would try to keep the API changes to a minimum, just for a matter of efficiency

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2024 at 14:40):

My view on this is that changes should be driven by real needs of the users, otherwise they tend to be mostly churn.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2024 at 14:40):

But of course it depends.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2024 at 14:41):

In the case how of to handle opaque proofs, I think we have no agreed upon plan or satisfying proposal yet, so it makes sense to discuss that first.

view this post on Zulip Hugo Herbelin (Jun 09 2024 at 14:42):

In the case how of to handle opaque proofs, I think we have no agreed upon plan or satisfying proposal yet, so it makes sense to discuss that first.

Looks good.

view this post on Zulip Hugo Herbelin (Jun 09 2024 at 14:43):

we have no agreed upon plan or satisfying proposal

If we have proposals, we can already compare them!

view this post on Zulip Hugo Herbelin (Jun 09 2024 at 14:44):

And we actually already have the current implementation...


Last updated: Oct 13 2024 at 01:02 UTC