Check typing flags in private constants.#21880
Check typing flags in private constants.#21880ppedrot wants to merge 1 commit intorocq-prover:masterfrom
Conversation
We are a bit laxer than just requiring the flags to be kept unchanged across environments, as we also allow for "stricter" flags. Fixes rocq-prover#20550: Side effects lose track of typing flags leading to inconsistency.
ppedrot
added
kind: fix
coqbot-app
bot
removed
the
request: full CI
Use |
|
Oh, sorry, I didn't realize that this was exactly testing an issue with abstract |
| sprop_allowed = sprop_allowed1; | ||
| allow_uip = allow_uip1; | ||
| (* The flags below do not change the theory *) | ||
| conv_oracle = _; |
There was a problem hiding this comment.
you need to enable warning 9 if you want to ensure the field list is exhaustive.
There was a problem hiding this comment.
Wasn't it part of the default flags at some point?
The problem seems to be that Fail (or Succeed) Qed runs with the global env of the proof, which contains the private constants, so Line 852 in f2bc100 You can make an output test I guess. |
3 participants
We are a bit laxer than just requiring the flags to be kept unchanged across environments, as we also allow for "stricter" flags.
Fixes #20550: Side effects lose track of typing flags leading to inconsistency.
I do not know how to write a test for this though, the Qed failure is seemingly not caught by the Fail wrapper and propagates to toplevel regardless of it. Any idea?