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)
Also, any bets on whether this is a bug in coqc or a bug in coqchk?
coqc and coqchk should do the same thing with universes
you don't get the error when you Require those files?
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)
order shouldn't matter
if you load the offending
CSwap first, the inconsistency will be reported on some other file?
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: Jun 08 2023 at 04:01 UTC