coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] universe inconsistency on import

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Cc: Vadim Zaliva <vzaliva AT cmu.edu>
Subject: Re: [Coq-Club] universe inconsistency on import
Date: Fri, 29 Nov 2019 21:15:28 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f46.google.com
Ironport-phdr: 9a23:CzTXbBcl2evP1FPHxpmhhQ7XlGMj4u6mDksu8pMizoh2WeGdxcuyYx7h7PlgxGXEQZ/co6odzbaP6Oa5BjRLvc/JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRu7oR/MusQUnYduJak8xgbUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU063/chNBug61HoRKhvx1/zJDSYIGJL/p1Y6fRccoHSWZdQspdUipMCZ6+YYQSFeoMJelXr4f/qFUOoxWwBhSiCv3zxTJTnHD6wbc33v49HQ3a3gEtGc8FvnTOrNXyMacfSeS7w7PTzTXEafNdxDbz6JLPchA6uvGHQLV9ccjLxkk0EAPFiFqQqZbiPzOOzeQAt3OW7+VlVe21im4nrxt9rSSoxscpk4TEgJ8exF7D9SV82ok1JNu4RVZgYd6+CpdQtz2aOo1rSc0hW2FloDg2xqECtJKhfyUHyI4rywDDZ/GEaYSF7RPuWeCMKjlinn1lYqiwhxOq/Eig1OL8Us603U5PriVfk9nMsmkB2ALO5cSaU/d98Eis1DeV2wDc7eFEJk80la7FJJI73rEwkZ8TvVzCHi/whkr2kLebels49uWs8ejqYbXrqoWCO4NoiQzyKKsjl82nDeQ9KAcOXmyb+eqm1L3k+E30WLdKgectkqnetpDaKt4bpqmiAw9O1osu8Bm/DzK839QZmXkLNk5KeBWCj4TxIVHBPOj4Deujg1SriDpk2/fGPqT4DprRKnjDjazucK1m609czQoz1cpQ64hVCrEHOvLzW1X+uMbWDh8jYESIxLPsD8w43YcDUyrbCaiAdajWrFWg5+Q1IuDKapVD6xjnLP1wxff1inlxtkUaZrLhiZkec3e+Ee5hOF7ISXXpi9YFV2wNu1xtH6TRlFSeXGsLND6JVKUm62R+Udr+VNqRdsWWmLWEmRyDMNhWa2RBUA3eFH7pc8CJV65JZn7MZMBmlTMAWP6qTIpzjUj/5j+/8KJuK6/vwgNdsJvi0NZv4OiKzEM98DV1C4KW1GTfFjgozFNNfCc/2eVEmWI40k2KiPEqjPlRFNgV7PRMAF83

If you `Set Printing Universes` before you do the Require Import, you will get more info, often enough to figure out which file they're in. If you then print the file (with printing universes on), you can figure out which definition the universes come from (figuring out where the constraints come from is much harder, unfortunately).

On Fri, Nov 29, 2019, 20:08 Brett Gilio <brettg AT posteo.net> wrote:

Vadim Zaliva <vzaliva AT cmu.edu> writes:

> I have `Require Import` which fails with the "universe inconsistency" error. There is no more detail besides this message. Any hints on how one can debug this?
>
> Vadim
>
> --
> Vadim Zaliva
> A button for name playback in email signature
>
> CMU ECE Ph.D. candidate
> Mobile/Signal/WhatsApp: +1(510)220-1060
>

Hello Vadim,

Can I see an example of what you are trying to achieve? Sometimes a
universe inconsistency error can point to an error with logic in the import.

--
Brett M. Gilio
https://git.sr.ht/~brettgilio/

[Coq-Club] universe inconsistency on import, Vadim Zaliva, 11/30/2019
- Re: [Coq-Club] universe inconsistency on import, Brett Gilio, 11/30/2019
  - Re: [Coq-Club] universe inconsistency on import, Jason Gross, 11/30/2019
    - Re: [Coq-Club] universe inconsistency on import, Christian Doczkal, 11/30/2019