[vernac] refine check for unresolved evars #12759
Conversation
gares
added
kind: user messages
|
For your complete information, the job test-suite:4.11+trunk+dune in allow failure mode has failed for commit adb5936: [vernac] refine check for undresolved evars |
|
For your complete information, the job test-suite:base+async in allow failure mode has failed for commit adb5936: [vernac] refine check for undresolved evars |
gares
force-pushed
the
fix-prepare-definition
branch
from
adb5936 to
39b09c4
Compare
gares
force-pushed
the
fix-prepare-definition
branch
from
39b09c4 to
246686b
Compare
There was a problem hiding this comment.
Looks useful.
The error should probably be some new exception with registered handler instead of user_err.
A more clean solution would be to have Evarutil.finalize produce the nice error message in the first place rather than an anomaly, but that change would be more intrusive, and I'd like this patch to be backported. Upon request I can prepare another PR with this change.
I request ;)
| let error_unresolved_evars env sigma t evars = | ||
| let pr_unresolved_evar e = | ||
| hov 2 (str"- " ++ Printer.pr_existential_key sigma e ++ str ": " ++ | ||
| Himsg.explain_pretype_error env sigma |
There was a problem hiding this comment.
You could expose explain_unsolvable_implicit for this. Not sure if that's better.
There was a problem hiding this comment.
Hum, either I stay like this or we craft a new error that take the evar set and the term and that is printed as I do.
I mean, move all of the new code to Himsg.
Exposing more API for this use case seems a bit too ad-hoc to me.
SkySkimmer
added
the
needs: test-suite update
SkySkimmer
force-pushed
the
fix-prepare-definition
branch
from
a3d777e to
a7e54ad
Compare
SkySkimmer
force-pushed
the
fix-prepare-definition
branch
from
a7e54ad to
d269b70
Compare
|
Did a bit of squashing and merged the 2 tests (I originally got confused because I didn't understand that missing record fields are treated as holes). |
SkySkimmer
removed
the
needs: test-suite update
|
For your complete information, the job test-suite:4.11+trunk+dune in allow failure mode has failed for commit d269b70: [vernac] refine check for unresolved evars |
|
OK thanks |
|
all green! |
|
@coqbot: merge now |
@gares Will you have time to do that? |
|
Thanks for merging. I won't have time today, nor the next week :-/ |
Since 8.12
DeclarecallsPretypingcheck for unresolved evars, but this check is both too strict and produces non informative error messages. In particular you get stuff like "could not resolve an implicit of type Type" without even printing the term in which it occurs. Having a larger evar map is just OK and has use cases even if you are not usingProgramand hence you are not preparing an obligation. Since~allow_evarflag has gone there is not way to circumvent this change in the API. Finally, there is no API to restrict an evar map so that the current API is happy with it (at lease, I could not find it).In this PR I refine the check for unresolved evars to be both more informative and precise (only unresolved evars actually occurring in the term generate an error).
I'd really like this patch or a variant of it to be in 8.12.1.
A more clean solution would be to have
Evarutil.finalizeproduce the nice error message in the first place rather than an anomaly, but that change would be more intrusive, and I'd like this patch to be backported. Upon request I can prepare another PR with this change.