Michael Lindgren

Possible downside: Universe checking would be disabled for all packages importing Foundations.Init. If this is the case then this has the complete opposite effect of the intended goal to incrementally...

Right, I just tested the change and it will definitely disable universe checking for any project using UniMath that today have universe checking enabled, and it will do so in...

> whereas with `Unset Universe Checking` you have more control over which ones precisely rely on an unsafe hierarchy. I think that is an advantage of `Unset Universe Checking`. I...

> #[local] Unset Universe Checking. > Defining hprop_resizing@{i j} (T : Type@{i}) (_ : is_hprop T) : Type@{j} := T. Using something similar to this I got `Foundations` to build...

I prefer option (1) or (2) because as Peter points out it's very helpful to find where things breaks. My plan is to use something like (3) later on, once...

> Does this mean the only way to use unimath now is to use coq's master branch ? No, there's also the option to use [dune](https://dune.build/) to build UniMath. `dune...

There's also the option of still generating the `All.v`-files but having them under version control, like what is done currently for `CONTENTS.md`. I don't know what I prefer. I wouldn't...

I have a solution almost done, but I need to test it more to ensure it works when branch protection is activated, and also see that it doesn't fail in...

I've been experimenting with using dune cache in CI, and I think UniMath can benefit from it. I'll see If I can build the satellites with it as well.

In #1590 the satellites finish in 15-25 minutes, and in my own tests they finish in about 5min if their dependencies are not changed, i.e. if they have everything cached.