-
Notifications
You must be signed in to change notification settings - Fork 667
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
Kernel/checker reduction cleanups around projection unfolding #6686
Conversation
- use Redflags.red_projection - share unfold_projection between CClosure and Reduction
This just shares the unfold_projection between Closure and Reduction.
kernel/cClosure.ml
Outdated
Some (Zproj (pb.proj_npars, pb.proj_arg, Projection.constant p)) | ||
with Not_found -> | ||
(* This is possible because sometimes for beta reduction we use a dummy env *) | ||
None |
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.
This is messed up. The issue can be witnessed by running some of the test suite files without this exception catching, eg 5761.v (spoilers: we get an uncaught Not_found).
The issue is at
Lines 1244 to 1246 in 76aff3c
let nf_beta = clos_norm_flags CClosure.beta (Global.env ()) | |
let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ()) | |
let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta (Global.env ()) |
These lines get run at module initialisation time so the environment is always empty.
Instead of catching the exception should we either:
- eta-expand so that the environment is somewhat up to date
- or change the interface so that the caller is in charge of passing the right environment?
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.
Second solution (which implies first :) I had a patch to do that but probably before we moved to PRs :/
We can do this after the parent commit (Reductionops.nf_* don't use empty env)
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.
LGTM. Thanks !
Breaks equations. |
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/305/console
|
@SkySkimmer Would you mind opening a PR against Equations? I'll merge then notify them. |
Done (mattam82/Coq-Equations#48). |
Fixes for coq/coq#6686 (nf_beta takes an env).
Essentially: