search

MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
368 stars 79 forks source link

Remove Int31 #983

Closed Villetaneuse closed 11 months ago

Villetaneuse commented 1 year ago

This is needed for Coq coq/coq#17977 Modified files are

Villetaneuse commented 11 months ago

Sorry to bother you with this @mattam82, but can we move forward? It would be nice to remove these files in 8.19.

yforster commented 11 months ago

Is CI expected to go green on this? I just approved the run, if it goes green we can merge this for sure

Villetaneuse commented 11 months ago 
  File "./theories/TemplateMonadToPCUIC.v", line 185, characters 20-49:
  Error: Error: Universe instance length is 2 but should be 3.

I have no idea what it means and how it can be related to this PR.

JasonGross commented 11 months ago 
File "./theories/TemplateMonadToPCUIC.v", line 185, characters 20-49:
Error: Error: Universe instance length is 2 but should be 3.

I have no idea what it means and how it can be related to this PR.

It means that somehow when building with -quick, Coq has decided that https://github.com/MetaCoq/metacoq/blob/cde7d00c46a724961fe773f98c6c36f008efd2d7/template-pcuic/theories/TemplateMonadToPCUIC.v#L185 is no longer valid and TransLookup_lookup_inductive'@{_ _} needs to be TransLookup_lookup_inductive'@{_ _ _} instead. It is unrelated to this PR. Maybe Coq broke something since the last CI run?