does not compile with Coq 8.20 release candidate 1

[rmatthes]

In CI, it was visible that Coq dev (an alpha version of Coq 8.21) does not compile this satellite, but it is even worse.

[nmvdw]

What is the error for Coq 8.20?

[rmatthes]

The first error message is:

coqc SetHITs/code/prelude/imports.{glob,vo} (exit 1) File "./SetHITs/code/prelude/imports.v", line 3, characters 0-43: Error: Universe inconsistency. Cannot enforce UU.u0 <= PartA.cast.u1 because PartA.cast.u1 <= PartA.cast.u0 < UU.u0.

[nmvdw]

So, UniMath (and most satellites) are compiled using type-in-type, but SetHITs and Type Theory are not. The error happens in the import file: the only thing that happens here, is that files from UniMath are imported. As such, there are only 2 solutions:

• make SetHITs and TypeTheory depend on type-in-type
• remove type-in-type from UniMath

[rmatthes]

So, this means that, previously, a development that did not by itself require type-in-type, could import libraries that needed it but that the extra compilation could be marked as harmless - by not requiring type-in-type.

Why did this work for nearly all the time when 8.20 was still under development? And why no longer?

[nmvdw]

I don't know.

[rmatthes]

I just made a test compilation with Coq 8.20rc1 where I added -type-in-type as first argument to flags in the file SetHITs/code/dune. It compiles with PR 1900. There is quite a number of warnings, mostly about notation, but also

Warning: Automatically putting mod2_ax in Prop even though it was declared
with Type.
Unset Automatic Proposition Inductives to prevent this (it will become the
default in a future version).
If you instead put mod2_ax explicitly in Prop, set Dependent Proposition
Eliminators around the declaration for full backwards compatibility.
[automatic-prop-lowering,deprecated-since-8.20,deprecated,default]

and analogously with File "./SetHITs/code/examples/truncation.v", line 28, characters 2-66