Stream: Coq users

Topic: Recent change in coq dev leading to universe inconsistency?


view this post on Zulip Ralf Jung (Sep 08 2023 at 09:39):

We are seeing a universe inconsistency error in Perennial when building against coq dev, but not with Coq 8.17:

  File "./src/goose_lang/ffi/jrnl_ffi_spec.v", line 87, characters 23-29:
  Error:
  The term "JrnlOp" has type "Type" while it is expected to have type
  "Set" (universe inconsistency: Cannot enforce JrnlOp.u0 <= Set).

This started fairly recently, and when we rebuild old commits that used to work, the error also shows up there -- so it looks like this is caused by a change in Coq, not a change in Perennial. Any idea what this might be?

The first log where we see the error is https://github.com/mit-pdos/perennial/actions/runs/6097280358/job/16544594398; that was coq version 8cec8c968653f8d7efbba7d32313dfd9188f791c. things definitely still worked with e0d96f91e2d17e85e3d56387845209d7e2682237.

view this post on Zulip Ralf Jung (Sep 08 2023 at 09:40):

here's the log for what commit range: https://github.com/coq/coq/compare/e0d96f91e2d17e85e3d56387845209d7e2682237...8cec8c968653f8d7efbba7d32313dfd9188f791c

view this post on Zulip Gaëtan Gilbert (Sep 08 2023 at 09:42):

probably https://github.com/mit-pdos/perennial/pull/52 wasn't complete since we don't build all perennial in CI

view this post on Zulip Gaëtan Gilbert (Sep 08 2023 at 09:43):

you can use 8.18 with Set Warnings "+bad-set-minimization" to find problem inductives

view this post on Zulip Ralf Jung (Sep 08 2023 at 09:49):

yeah we got a bunch of those warnings before

view this post on Zulip Ralf Jung (Sep 08 2023 at 09:50):

I dont really understand what they mean :shrug:

view this post on Zulip Ralf Jung (Sep 08 2023 at 09:50):

let alone how to fix them

view this post on Zulip Gaëtan Gilbert (Sep 08 2023 at 09:52):

it means if you do

Unset Universe Minimization ToSet. (* this is global in perennial AFAICT *)

Inductive DiskOp := ReadOp | WriteOp | SizeOp.

in <=8.18 DiskOp : Set but in 8.19 DiskOp : Type@{DiskOp.u0} with DiskOp.u0 > Set

view this post on Zulip Gaëtan Gilbert (Sep 08 2023 at 09:54):

so to fix you (backwards-compatibly) change to explicitly Inductive DiskOp : Set := ...
or if you decide that actually you don't want it in set you do Inductive DiskOp@{u0} : Type@{u0} := ... (but this requires adapting the rest of your code, since you'll get the univ inconsistency)

view this post on Zulip Ralf Jung (Sep 08 2023 at 09:54):

hm., 8.17 shows no warning

view this post on Zulip Gaëtan Gilbert (Sep 08 2023 at 09:55):

the warning is 8.18 only

view this post on Zulip Ralf Jung (Sep 08 2023 at 09:55):

so this is a breaking change that had no warning cycle?

view this post on Zulip Gaëtan Gilbert (Sep 08 2023 at 09:55):

there is a warning in 8.18 and break in 8.19

view this post on Zulip Ralf Jung (Sep 08 2023 at 09:55):

oh I didnt realize dev is 8.19 already. there was no 8.18 release yet so I dont think anyone can expect us to have noticed these 8.18-only warnings.

view this post on Zulip Théo Zimmermann (Sep 08 2023 at 09:56):

There's a rc already, but no announcements have been made yet.

view this post on Zulip Théo Zimmermann (Sep 08 2023 at 09:56):

But you can already add 8.18 testing to your project, using opam and or the Docker image.

view this post on Zulip Karl Palmskog (Sep 08 2023 at 09:57):

8.18+rc1 has been out for more than a month now in core-dev opam, Docker images have been around for maybe 2-3 weeks

view this post on Zulip Ralf Jung (Sep 08 2023 at 09:58):

yeah but I only see warnings when they appear in my local builds, so... this came out of nowhere :/

view this post on Zulip Gaëtan Gilbert (Sep 08 2023 at 09:58):

Gaëtan Gilbert said:

so to fix you (backwards-compatibly) change to explicitly Inductive DiskOp : Set := ...
or if you decide that actually you don't want it in set you do Inductive DiskOp@{u0} : Type@{u0} := ... (but this requires adapting the rest of your code, since you'll get the univ inconsistency)

(or even re-enable minim to set around the inductive's declaration)

view this post on Zulip Ralf Jung (Sep 08 2023 at 09:58):

Gaëtan Gilbert said:

so to fix you (backwards-compatibly) change to explicitly Inductive DiskOp : Set := ...
or if you decide that actually you don't want it in set you do Inductive DiskOp@{u0} : Type@{u0} := ... (but this requires adapting the rest of your code, since you'll get the univ inconsistency)

that's helpful, thanks. would have been even more helpful if the warning already explained that I should add an explicit : Set to maintain backcompat. :)


Last updated: Jun 13 2024 at 19:02 UTC