coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Commands/Tools for Debugging Universe Inconsistency?

From: Yao Li <liyao AT seas.upenn.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Commands/Tools for Debugging Universe Inconsistency?
Date: Thu, 9 Apr 2020 18:14:27 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=liyao AT seas.upenn.edu; spf=Pass smtp.mailfrom=liyao AT seas.upenn.edu; spf=None smtp.helo=postmaster AT mail-qv1-f51.google.com
Ironport-phdr: 9a23:rkWYJBbX9laL6xKNAhoCOuH/LSx+4OfEezUN459isYplN5qZr8y9bnLW6fgltlLVR4KTs6sC17OL9fq5EjVeqdbZ6TZeKcAKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrsxxxfTvHdEZutayX5pKFmOmxrw+tq88IRs/ihNtP8t7dJMXbn/c68lUbFWETMqPnw668HsqRTNVxaE6GEGUmURnBpIAgzF4w//U5zsrCb0tfdz1TeDM8HuQr86RTqt76FwSB/1kygHLCI28HvWisNrkq1Wpg+qqgFlzI7VZIGVM+d+fr/YcNgHS2dNQtpdWipcCY66coABDfcOPfxAoof9u1QAohSxCxSvCu3h1DFGgWT73bEj0+QkDQ3G3BAsEtAIvX/JrNv1LqASUeWtwabK1zrDaO5d1zH86IPVdR0hpfCMXLJqfsrW0kQvDB3KgU+LqYD/IjOVzvoCs26d7+Z6S+2glnMnphh3rzOyxckskpHEipwJxl3A7yl0w4Y4KcemREJmZdOoCptduzyCO4doQ84uX3xktSMkxrAJpZK2eSsHxZs7yxLDbvGLbpSE7x3iWeuULjp1gHJod666ihuy9UWtyvfzW8yw3VtIsCZKj9zBuW0J2hHX6MWKTOZ28F271jaVzQ/T7/lJIUAqmqrfLJ4s2rswmYASsUTHByP2gVv2gLKPekUq+uWk9v7rYrrhpp+bOI90jh/xPr4ylcy4BOQ0KgkOX26F9uSgzLDv41H1TbFQgvA1kqTVqo7WKdkfq6KjAwJZz54v6xOlADen1NQYk2MHLFVAeB+fi4jpOlHPL+r/DfqkmFSjji1kx+vcMr38GpXCMH7DkLH7cblj9kFc1RI/zcpD6JJMFrEBPPXzV1ftu9zfFx81KhC7w+L6CNpmzY4eQmKOAqqBMKzIq1OI5+QvI/ONZIAPojr9JeIltLbSiioynkZYdq2017MWbmq5F7JoORa3e33p1+YIFi8uv0JqSO37gVqqSjNafDCvR6864Hc2BJ/wXtSLfZyknLHUhHTzJZZRfG0TUgndQ0etTJ2NXrI3UAzXJ8ZgljIeUr34Fd062Bi18hLixrxhaOfY539B7M6x5J1O/+TW0CoK23lsFc3EjTOWQmhv2H4QSjkwmq1zvB4lkwrR4e1Dm/VdUOdrybZJXwM9b8OOyuV7D5XrRFuEcIrQDlmhRdqiDHc6Sddjm9I=

Dear All,

I am having some recurring universe inconsistency problems lately and I would
like to know if there are any commands/tools for helping me debugging what
happened.

For example, a recurring pattern is that Coq complains to me that it cannot
unify two universe levels (assuming they are u1 and u4) because “u1 <= u2 <
u3 <= u4” or “u1 <= u2 < u3 = u4”. I would like to know where the constraints
concerning u3 and u4 (and perhaps other relevant constraints as well) are
generated—or better yet, why. However, I haven’t found a tool for doing that.

I have tried “Set Printing Universes”. Unfortunately, the constraints
concerning u3 and u4 cannot be found at any relevant definitions. I have also
tried “Print Universes”, but I cannot find what I’m looking for in the sea of
constraints that Coq shows me.

Best,
Yao

[Coq-Club] Commands/Tools for Debugging Universe Inconsistency?, Yao Li, 04/10/2020
- Re: [Coq-Club] Commands/Tools for Debugging Universe Inconsistency?, Christian Doczkal, 04/10/2020
  - Re: [Coq-Club] Commands/Tools for Debugging Universe Inconsistency?, Yao Li, 04/10/2020
    - Re: [Coq-Club] Commands/Tools for Debugging Universe Inconsistency?, Gaëtan Gilbert, 04/10/2020
      - Re: [Coq-Club] Commands/Tools for Debugging Universe Inconsistency?, Yao Li, 04/10/2020
        
        Re: [Coq-Club] Commands/Tools for Debugging Universe Inconsistency?, Yao Li, 04/10/2020