Discharge on the fly

[herbelin]

This is a proof of concept for discharge on the fly, that is for being able to access all generalizations of a declaration in a section at the time of declaration.

Example:

Section S.
Context {A B:Type}.
Inductive option := None | Some (a:A).
Definition map (f : A -> B) (o : option) :=
  match o with
  | None => Top.None
  | Some a => Top.Some (f a)
  end.
End S.

The new model is basically the following:

• one declaration in a nested sequence of sections S1, ..., Sn induces n+1 declarations, corresponding to the original declaration and its n generalizations
• at the time of closing Si, we morally just drop the copy of the declaration in Si (even if, technically, we reset and replay the i generalizations from level 0 to i-1)

There is basically one main change of structure:

• kernel names include a section path in their name (encoded using MPdot)

The changes are otherwise dispatched into three parts:

• in the kernel (safe_typing.ml): add all generalizations of a declaration at declaration time
• in library (lib.ml): add all discharges of objects at declaration time
• adapt all discharge functions to take into account that names now include a section segment and that all discharges virtually live together in the section

This raises questions about the levels at which a declaration has to be done:

• most declarations, starting with definitions and inductive types, as well as their attributes (implicit arguments, scopes, etc.) have to be done at all levels, i.e., for the example above, in section S, both option and Top.option have to be defined
• some declarations should be done only in one level, e.g. for Require, or (mono) Universe only the copy living at the toplevel has to be registered
• for some declarations, such as coercions and canonical structures, it is unclear: do we want to have all discharged version available from section i (even if it is somehow redundant) or only the version discharged at level i?

Incidentally, since the discharge functions have to be adapted anyway, that might be a right time to change the type of Libobject functions (e.g. so that they take an environment and a summary as arguments?).

I open the PR as draft to get some first comments.

Current status: PRs #18062 (preliminatory work on discharge) and #18065 (discharge on the fly in the kernel) have been made out of this PR, which now depends on them.

• Added / updated test-suite.
• Added changelog.
• Added / updated documentation.

Related discussion: Future of sections #6254 and coq/ceps#72.

[JasonGross]

This is nice!

for some declarations, such as coercions and canonical structures, it is unclear: do we want to have all discharged version available from section i (even if it is somehow redundant) or only the version discharged at level i?

I think we want all versions (unless it's declared Local). For example, we might have a coercion from option A >-> A + unit. If this coercion is declared in the same section that the option inductive is created, we might still want access to the coercion from Top.option B >-> B + unit. By contrast, it might be the case that the global coercion isn't good enough, for example if we have Context {A : Type} (default : A)., define Inductive option, and then have a coercion in the section option >-> A (which won't work globally without default).

I worry that doing this for instances is going to blow up typeclass resolution, though? In general, it seems like we only want the more global version of a canonical structure/coercion/instance to trigger if the section-local one cannot apply.

[CohenCyril]

@gares

[gares]

I like the feature, I've always thought that this is how sections should work.
But I think you took a very hard path, making the kernel aware of the the two copies (the section one and the discharged one) of the same constant. I think the section one should not exist in the first place, at best emulated via the nametab, as if we could put modules inside sections.

Section S.
Variable A : Type.
Definition f : T :=. .. A ...
Module Aux. Let f := f A. End Aux. Import Aux. (* pseudo code for nametab *)
Check f : T.
Check Top.f : Type -> T.

or said otherwise

Section S.
Variable A : Type.
Definition f : T :=. .. A ...
Let f_aux := f A.
(* nametab making f -> f_aux *)
Check f : T.
Check f_aux. (* error, no nametab entry *)
Check Top.f : Type -> T.
End S.
(* nametab entry for f -> f_aux gone *)

Modifying the kernel is a regression to me, it has been a while since we managed to get rid of section components in kernel names. But maybe your change amounts to implementing the module-in-section thing just for constants, in that case I stand corrected, but you mark it as the main change which seems a bit odd it is amounts to generate a f_aux name.

[gares]

In any case, I think this is a huge change deserving a CEP (like the one about levels in grammar entries, which studies all details and possible angles to tackle it)

[gares]

I worry that doing this for instances is going to blow up typeclass resolution, though? In general, it seems like we only want the more global version of a canonical structure/coercion/instance to trigger if the section-local one cannot apply.

I think that generating the metadata twice would be an error, e.g. the discharged copy should stay naked.
IMO being able to refer to the discharged constant (and manually adding metadata if one wants) is sufficient to improve the current situation.

[SkySkimmer]

The test suite error is a new warning in an output test, seems quite unlike the other CI errors. Therefore
@coqbot ci minimize

[coqbot-app]

I have initiated minimization at commit 3c89247 for the suggested targets ci-equations, ci-fiat_crypto_legacy, ci-flocq, ci-hott, ci-iris, ci-mathcomp, ci-perennial, ci-rewriter as requested.
However, you may want to try again once the pipeline for the head commit (3c89247) finishes.

[SkySkimmer]

also @coqbot bench

[JasonGross]

@JasonGross: Here is a log (https://gitlab.com/coq/coq/-/jobs/4765018144), with a failure on example 008.

I see. The minimization strategy for removing sections indeed becomes more fragile with this change, since there are more cases where removing End section will change the behavior if Section section is not removed at the same time. I guess I should either adapt the test suite file check or add a pass for removing paired section vernaculars.

[JasonGross]

Actually, sorry, I think I misdiagnosed the failure, and in fact the issue is that minimization got stronger / easier, now that absolute names are available inside sections. I guess the test case check should be adapted

[herbelin]

For the record, a comment of Théo reporting about the experience in Lean of simulating sections with implicit arguments.

[JasonGross]

Is this currently blocked on me writing an overlay for coq-tools, or something else?

[herbelin]

Is this currently blocked on me writing an overlay for coq-tools, or something else?

Nothing strictly blocking yet.

We had a discussion at the Coq call today and decided to merge already the internal (kernel) part (#18065).

For the rest, we decided to collect examples of needs so that we understand better what to exactly implement user-side (e.g. whether the discharge is made on demand or systematically, or how to deal with different versions of a hint, or whether we recover the specific versions from the most general ones, etc.)

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.