New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Backport of the new universe checking algorithm to V8.5 #178

wants to merge 5 commits into
base: v8.5


None yet
5 participants
Copy link

ejgallego commented May 30, 2016

This is a backport of Jacques-Henri Jourdan universe unification algorithm to 8.5.

I'm not sure this is ready to merge for pl2, but it looks quite stable after a couple of weeks of testing.

There seems to be a problem with universe polymorphism, in particular, different number of universes are inferred, breaking some developments. This also seems to happen in trunk.

I was able to fix such developments (HoTT and mirror-core) and they seem to run fine, however more research may be needed. See

jhjourdan and others added some commits Jul 10, 2015

Splitting kernel universe code in two modules.
1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.
Backport f7030a3
Thanks a lot to PMP. Original commit message:

> Remove unneeded fixpoint in normalize_context_set. Note that it is no
> longer stable w.r.t. equality constraints as the universe graph will
> choose different canonical levels depending on the equalities given to
> it (l = r vs r = l).

@ejgallego ejgallego force-pushed the ejgallego:v8.5-new-universes branch from 10aa16c to ddeb1b2 Jun 1, 2016

Univs: fix bug #4443.
Do not substitute rigid variables during minimization, keeping
their equality constraints instead.

@gares gares added the rejected label Jun 22, 2016


This comment has been minimized.

Copy link

gares commented Jun 22, 2016

Dunno if I should close it. The decision was: it is in 8.6 that will be released soon, 8.5 accepts only minor fixes and the new universe algorithms reveals a couple of bugs (hence it would cause regressions).


This comment has been minimized.

Copy link

ejgallego commented Jun 22, 2016

Yeah let's close.

@ejgallego ejgallego closed this Jun 22, 2016


This comment has been minimized.

Copy link

ejgallego commented Jun 22, 2016

People interested in the speed up can find the patch in my branch; I've moved myself everything to 8.6 so I am not using this tree anymore.

@ejgallego ejgallego deleted the ejgallego:v8.5-new-universes branch Feb 26, 2017

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment