Stream: Coq devs & plugin devs

Topic: universe inconsistency in coqchk


view this post on Zulip Jason Gross (May 21 2022 at 00:10):

Is there a way to get coqchk to give more information about universe inconsistencies? I see

2022-05-20T23:56:02.2617019Z   checking module: Rupicola.Lib.Arrays.VectorArrayCompiler
2022-05-20T23:56:02.2617488Z   checking module: Rupicola.Lib.Arrays.UnsizedListArrayCompiler
2022-05-20T23:56:02.2617923Z   checking module: Rupicola.Lib.Arrays.SizedListArrayCompiler
2022-05-20T23:56:02.2618401Z   checking module: Rupicola.Lib.Arrays.AccessSizeCompatibilityNotations
2022-05-20T23:56:02.2630214Z Checking library: Crypto.Bedrock.Group.ScalarMult.CSwap
2022-05-20T23:56:02.2639499Z Fatal Error: Error: Universe inconsistency.
2022-05-20T23:56:02.2804896Z Command exited with non-zero status 129
2022-05-20T23:56:02.2815526Z validate-vo (real: 788.25, user: 784.50, sys: 2.80, mem: 2773400 ko)

for https://github.com/mit-plv/fiat-crypto/runs/6528352231?check_suite_focus=true (https://github.com/mit-plv/fiat-crypto/commit/2b5c1c71af53d50fa0e5f697f844afc60c293563)

view this post on Zulip Jason Gross (May 21 2022 at 00:11):

Also, any bets on whether this is a bug in coqc or a bug in coqchk?

view this post on Zulip Gaëtan Gilbert (May 21 2022 at 08:01):

coqc and coqchk should do the same thing with universes
you don't get the error when you Require those files?

view this post on Zulip Paolo Giarrusso (May 21 2022 at 08:08):

Could the problem be that coqchk tries to load the entire development together, even files that are never combined otherwise? So you just need to Require them all (possibly in the same order)

view this post on Zulip Gaëtan Gilbert (May 21 2022 at 08:10):

order shouldn't matter

view this post on Zulip Paolo Giarrusso (May 21 2022 at 08:19):

if you load the offending CSwap first, the inconsistency will be reported on some other file?

view this post on Zulip Gaëtan Gilbert (May 21 2022 at 08:50):

yes

view this post on Zulip Jason Gross (May 22 2022 at 14:13):

Urgh, the issue is that eapply (lem _) is imposing universe constraints which are not imposed by doing eapply (lem TERM) where TERM is the result of copy-pasting from Set Printing All. Show Proof.


Last updated: Feb 01 2023 at 15:04 UTC