-
Notifications
You must be signed in to change notification settings - Fork 31
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
no delayed opaque proofs in safe_env #40
Conversation
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. |
Maybe we could replace join_safe_env by 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. |
I believe this would solve #8241. |
I agree, a proper implementation of functors/include is a prerequisite for this cep. |
You mean "this CEP" or "this suggestion by Gaetan"? |
The CEP, if implemented properly. |
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.) |
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. |
And yes, the functor/include thing needs to be fixed (but I've no idea where to look :-/) |
We need to implement properly |
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. |
@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. |
text/000-no-proofs-in-kernel.md
Outdated
# Alternatives | ||
|
||
Isabelle does what we do now (via promises), but does not let one | ||
repair a proof (you simply redo it from scratch). Actually it is |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What does "repair" mean?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In CoqIDE you can repair a broken proof without invalidating the rest of the document.
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. |
@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. |
Yup, indeed this kind of intra-document dependencies are better handled by the document manager than the kernel. |
2a3c710
to
1ea8564
Compare
1ea8564
to
42c6886
Compare
Yeah, we can probably consider this CEP has having been implemented. |
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.