search

MetaCoq / metacoq

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

Compatibility with HoTT #139

Open annenkov opened 5 years ago

annenkov commented 5 years ago

It would be nice to make MetaCoq compatible with the HoTT library (https://github.com/HoTT/HoTT). I know that @andreaslyn would be interested in this kind of compatibility. I guess, making translations to work with HoTT would be already nice, the rest (like CIC meta-theory and extraction) is probably not needed to be compatible. Of course, this requires at least to resolve #138 first.

gmalecha commented 5 years ago

What incompatibilities are there? Is this an issue with the translations or with the core meta-coq infrastructure?

annenkov commented 5 years ago

I guess, the first thing is that HoTT library builds with the dev version of Coq and MetaCoq is not compatible with the dev version of Coq currently.

andreaslyn commented 5 years ago

The HoTT library relies on Coq version >= 8.10. So at least issue https://github.com/MetaCoq/metacoq/issues/138 is standing in the way of making metacoq compatible with HoTT.

spitters commented 5 years ago

Doesn't #138 just mean that we cannot reflect SProp. Is there anything standing in the way of making this more limited version of metacoq compile with HoTT? Currently SProp is not used in HoTT.

spitters commented 5 years ago

@mattam82 @SkySkimmer would this be a viable approach?