no delayed opaque proofs in safe_env

[gares]

Rendered https://github.com/gares/ceps/blob/no-proofs-in-kernel/text/000-no-proofs-in-kernel.md

The idea is to be brave and do what I should have done when STM was added. At that time I did opt for the most conservative changes.

[SkySkimmer]

I think we have to keep the bodies in the safe_env for extraction until we have some solution to accessing non kernel objects for functors.
See eg coq/coq#9136, there should be some related issues around too and there was a mention when FakeRecord was introduced in coq/coq#7750 but I think it was on gitter as it doesn't appear in the PR.

[SkySkimmer]

Maybe we could replace join_safe_env by add_opaque_bodies : safe_env -> constr constant.map -> safe_env (assuming that works out for the callers)

We also need to keep in mind the need to use the right environment when typechecking the bodies, including possible functor issues:

Lemma foo := bar. Lemma bar := foo. (* this should fail because we should check the body of foo in an env where bar doesn't exist *)

Module F(X:Bla). Lemma boz := X.x. End F.
(* we need to use an env where X is available when checking the body even if we do the check after closing F *)

Not sure how difficult this is.

[ppedrot]

I believe this would solve #8241.

[gares]

I agree, a proper implementation of functors/include is a prerequisite for this cep.

[gares]

I believe this

You mean "this CEP" or "this suggestion by Gaetan"?

[ppedrot]

The CEP, if implemented properly.

[ppedrot]

For the record (no pun intended) I did face issues when trying to remove the non-primitive record flag from the kernel because it broke extraction of functors.

But in the particular case discussed in this CEP, I think we could be even stricter and turn the warning when extracting a Qed-proof into a real error. Why should we special-case extraction regarding unopacifying? Let's boldly deprecate this misfeature instead of trying to reimplement it.

(That doesn't prevent us trying to fix the functor mess though, but this would be orthogonal.)

[gares]

With this CEP the (opaque) proofs can't be asked to the kernel simply because they are not there.

They are going to be stored somewhere else, in the STM during document checking and eventually on disk by Library. If the code of Extraction or Dpdgraph wants to access these terms, it should load them from disk (API in Library I suppose) or ask the STM (for the ones in the current document).

Then, one could also say that Extraction should not look at these, full stop.
But that choice is orthogonal to this CEP, IMHO. I just want to make this clear.

[gares]

And yes, the functor/include thing needs to be fixed (but I've no idea where to look :-/)

[ppedrot]

but I've no idea where to look

We need to implement properly Declaremods.process_module_binding. Currently it only registers libobjects from the domain, while it should also do so for the codomain. Problem is, in general we don't have the right information regarding the type of the codomain

[ejgallego]

This makes a lot of sense; given the way OCaml works it is much more convenient for the kernel to be notified from the upper layers. The current approach is a bit messy as forcing a future may not always return a proof, however using an option type here allows us to have better static guarantees.

[ppedrot]

I agree, a proper implementation of functors/include is a prerequisite for this cep.

@gares Also, not wanting to be defeatist, but if this is really required, it is likely that this will never happen before the thermodynamical end of the universe. A more reasonable strategy would be to first list the places that are broken and see what we can do about them, like e.g. for notations.

[SkySkimmer]

What does "repair" mean?

[gares]

In CoqIDE you can repair a broken proof without invalidating the rest of the document.

[ejgallego]

I an wondering, why this cannot go ahead just directly?

In the current implementation, there is no guarantee either that a body will be available, because you could get an exception from a future; so you would just need to tweak the current failure mode to be less catastrophic; and the upper level layer should be careful to provide bodies for all the tricky constructions.

[gares]

@ppedrot the truth is that I don't know why functors/include need to access opaque proofs. So I can't possible propose a fix. Your messages here are not understandable to me. I'll try to look at the code you mentioned and see.

@ejgallego note that if you extract an opaque proof while it is being computed, then the Future.force/join is blocking. So you wait until it is ready. This very same code can still be used, it is just that the blocking future will live in STM and not in kernel. Nothing changes wrt the status quo.

[ejgallego]

So you wait until it is ready. This very same code can still be used, it is just that the blocking future will live in STM and not in kernel. Nothing changes wrt the status quo.

Yup, indeed this kind of intra-document dependencies are better handled by the document manager than the kernel.

[gares]

I remove the stale label, since recent PRs by @ppedrot have moved delayed-opaque proofs out of the kernel.
I think this CEP is "kind of done", do you agree @ppedrot ?

[ppedrot]

Yeah, we can probably consider this CEP has having been implemented.