Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Is flag -type-in-type required for this repository? #3

Closed
benediktahrens opened this issue Mar 7, 2022 · 3 comments
Closed

Is flag -type-in-type required for this repository? #3

benediktahrens opened this issue Mar 7, 2022 · 3 comments

Comments

@benediktahrens
Copy link
Member

Until now, this flag has not been required, but starting with UniMath/UniMath#1467, this might be necessary. I am not sure which change exactly triggers the build error:

Cloning into 'SetHITs'...
~/work/UniMath/UniMath/SetHITs ~/work/UniMath/UniMath
COQDEP VFILES
COQC prelude/imports.v
File "./prelude/imports.v", line 2, characters 0-39:
Warning: Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./prelude/imports.v", line 2, characters 0-39:
Warning: Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./prelude/imports.v", line 2, characters 0-39:
Warning: Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./prelude/imports.v", line 2, characters 0-39:
Warning: Notation "_ = _" was already used in scope type_scope.
[notation-overridden,parsing]
File "./prelude/imports.v", line 2, characters 0-39:
Warning: Notation "_ <-> _" was already used in scope type_scope.
[notation-overridden,parsing]
File "./prelude/imports.v", line 2, characters 0-39:
Warning: Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./prelude/imports.v", line 2, characters 0-39:
Warning: Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./prelude/imports.v", line 2, characters 0-39:
Warning: Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./prelude/imports.v", line 2, characters 0-39:
Warning: Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./prelude/imports.v", line 3, characters 0-43:
Warning: Notation "_ ≠ _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./prelude/imports.v", line 3, characters 0-43:
Warning: Notation "_ <-> _" was already used in scope type_scope.
[notation-overridden,parsing]
File "./prelude/imports.v", line 3, characters 0-43:
Warning: Notation "_ = _" was already used in scope type_scope.
[notation-overridden,parsing]
File "./prelude/imports.v", line 3, characters 0-43:
Warning: Notation "_ = _" was already used in scope type_scope.
[notation-overridden,parsing]
File "./prelude/imports.v", line 3, characters 0-43:
Warning: Notation "_ <-> _" was already used in scope type_scope.
[notation-overridden,parsing]
File "./prelude/imports.v", line 3, characters 0-43:
Warning: Notation "_ ≠ _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./prelude/imports.v", line 12, characters 0-57:
Error: Universe inconsistency. Cannot enforce UU.u0 = Set because Set
< UU.u0.

make[1]: *** [Makefile:716: prelude/imports.vo] Error 1
make: *** [Makefile:339: all] Error 2
Error: Process completed with exit code 2.

(Complete CI run at https://github.com/UniMath/UniMath/runs/5442353189?check_suite_focus=true.)
@m-lindgren
Copy link
Member

The problem is that the PR calls bool_rec : ∏ (P : bool → Set), P true → P false → ∏ b : bool, P b and coprod_rec, which also use the Set-eliminator. I suggested some changes to the PR that I tried successfully compiling SetHIT with, so no need -type-in-type.

@m-lindgren
Copy link
Member

So I was wrong, -type-in-type is currently needed, but for a completely different reason:

        coqc SetHITs/code/examples/groups.{glob,vo} (exit 1)
File "./SetHITs/code/examples/groups.v", line 118, characters 12-20:
Error:
The term "group_ax" has type "UU" while it is expected to have type
"Type" (universe inconsistency: Cannot enforce UU.u0 <=
hit_signature.u0 because hit_signature.u0 < UU.u0).

        coqc SetHITs/code/examples/rings.{glob,vo} (exit 1)
File "./SetHITs/code/examples/rings.v", line 192, characters 12-19:
Error:
The term "ring_ax" has type "UU" while it is expected to have type
"Type" (universe inconsistency: Cannot enforce UU.u0 <=
hit_signature.u0 because hit_signature.u0 < UU.u0).

...

I believe these comes from this recent commit with innocent looking changes like:

  (** Labels of group axioms *)
-Inductive group_ax :=
+Inductive group_ax : UU :=
 | assoc : group_ax

I assume this is because UniMath has Definition UU := Type. instead of having UU be a Notation (or just using Type).

@m-lindgren m-lindgren mentioned this issue Nov 7, 2022
Merged
@m-lindgren
Copy link
Member

Closing this following #14. -type-in-type is not needed for this repository. The original issue was that the PR UniMath/UniMath#1467 inadvertently used Set-valued eliminators which caused a universe inconsistency when building this satellite.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@benediktahrens @m-lindgren