Skip to content
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

Sensitivity to universe ordering #112

Open
JasonGross opened this issue Feb 8, 2022 · 0 comments
Open

Sensitivity to universe ordering #112

JasonGross opened this issue Feb 8, 2022 · 0 comments
Labels

Comments

@JasonGross
Copy link
Owner

JasonGross commented Feb 8, 2022

The minimizer should consider the following messages equivalent:

File "/tmp/tmprl1zib8j/bug_01.v", line 2308, characters 58-63:
Error:
In environment
it : ident * type
The term "mpred" has type "Type@{max(Set+1, bug_01.45)}"
while it is expected to have type "Type@{bug_01.833}"
(universe inconsistency).

and

File "./bug_01.v", line 1067, characters 58-63:
Error:
In environment
it : ident * type
The term "mpred" has type "Type@{max(VST.msl.predicates_hered.3, Set+1)}"
while it is expected to have type "Type@{Top.bug_01.323}"
(universe inconsistency).

See coq-community/run-coq-bug-minimizer#2 (comment)

@JasonGross JasonGross added the bug label Feb 8, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant