search

coq-community / reduction-effects

A Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]
Mozilla Public License 2.0
6 stars 6 forks source link

_UNBOUND_REL_i #23

Open yforster opened 1 month ago

yforster commented 1 month ago

I am trying to debug a large meta-program written in MetaCoq using the printing effect, and I'm running into an issue where print_id prints _UNBOUND_REL_0.

The meta program has the guard checker turned off, but otherwise, apart from being fairly long, doesn't do anything specific.

I am not using the TemplateMonad, so we're looking at a pure Coq program.

Could this be a bug in reduction effects, or a bug in reduction? I could try to minimise, but given the complexity of the program that would take some while, so I'm doing a shot into the dark here, maybe somebody (@JasonGross @herbelin?) has an idea what's going on :)

SkySkimmer commented 1 month ago

Which reduction machine? I think some of them don't have the local env at hand.

yforster commented 1 month ago

I'm using cbv

SkySkimmer commented 1 month ago

Indeed it seems cbv has a delayed substitution instead of a local env

herbelin commented 1 month ago

This suggests a bug somewhere (e.g. the 0 suggests an invalid lift (-1) or something like that), but more details would be needed. What is the context of binders, what subexpressions is being reduced, what should be the expected term being printed instead of _UNBOUND_REL_0?

SkySkimmer commented 1 month ago

I guess around https://github.com/coq/coq/blob/ae57be8165c4d3b475106983c504280cc3e6bc4c/pretyping/cbv.ml#L967 and other cases where cbv goes under binders we would need to push_rel in the info.env