Jason Gross (May 21 2022 at 00:10): 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)
Jason Gross (May 21 2022 at 00:11):Also, any bets on whether this is a bug in coqc or a bug in coqchk?
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?
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)
Gaëtan Gilbert (May 21 2022 at 08:10):order shouldn't matter
Paolo Giarrusso (May 21 2022 at 08:19):if you load the offending CSwap first, the inconsistency will be reported on some other file?
Gaëtan Gilbert (May 21 2022 at 08:50):yes
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: Oct 08 2024 at 15:02 UTC