Ralf Jung (Sep 08 2023 at 09:39): 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.
Ralf Jung (Sep 08 2023 at 09:40):here's the log for what commit range: https://github.com/coq/coq/compare/e0d96f91e2d17e85e3d56387845209d7e2682237...8cec8c968653f8d7efbba7d32313dfd9188f791c
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
Gaëtan Gilbert (Sep 08 2023 at 09:43):you can use 8.18 with Set Warnings "+bad-set-minimization" to find problem inductives
Ralf Jung (Sep 08 2023 at 09:49):yeah we got a bunch of those warnings before
Ralf Jung (Sep 08 2023 at 09:50):I dont really understand what they mean :shrug:
Ralf Jung (Sep 08 2023 at 09:50):let alone how to fix them
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
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)
Ralf Jung (Sep 08 2023 at 09:54):hm., 8.17 shows no warning
Gaëtan Gilbert (Sep 08 2023 at 09:55):the warning is 8.18 only
Ralf Jung (Sep 08 2023 at 09:55):so this is a breaking change that had no warning cycle?
Gaëtan Gilbert (Sep 08 2023 at 09:55):there is a warning in 8.18 and break in 8.19
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.
Théo Zimmermann (Sep 08 2023 at 09:56):There's a rc already, but no announcements have been made yet.
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.
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
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 :/
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 doInductive 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)
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 doInductive 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: Oct 13 2024 at 01:02 UTC