Yannick Forster

> I initially thought of using the opam file hash as suffix of the key and add the largest tested coq version, but that would mean we must watch out...

> Or live with the fact that for every new 8.12.(x+1) bump, opam for users who updated coq does not compile our library until we say it's allowed, although most...

@mrhaandi @DmxLarchey would you be fine with such a change? Lots of files would have to be touched, so I'm not I can finish it today, but if it's possible...

Regarding Change 1: MetaCoq is now following Coq `master`, which means that we can release an opam package immediately for every new Coq version. I have ported the library to...

Regarding Change 2, Andrej started working on bringing some of the most important problems into this shape, which I think is great. > I am not sure how to implement...

These are the directories which do not follow the structure guidelines at the moment: - [ ] `MuRec` - [ ] `TRAKHTENBROT` - [ ] `HOU` That's not so bad!...

This looks good, and the 20% reduction in compilation time is great! I think the best way to merge this is to first let Fabian port the files and results...

Meaning `HOU` makes up for 30% of the whole computation power needed? That's surprising. I knew it was high, but not *that* high.

Oh no, this is probably going to fail until the opam package for MetaCoq is merged (https://github.com/coq/opam-coq-archive/pull/2288#issuecomment-1239201703), which in turn relies on a new release of MetaCoq (https://github.com/MetaCoq/metacoq/pull/748)

https://github.com/coq/opam-coq-archive/pull/2370