walker has marked this topic as resolved.

Hi @walker , thank you for your interest in our project! I'm currently porting ConCert to Coq 8.14, the non-trivial bit comes from MetaCoq that has changed quite a bit. Rust extraction is ported already, I'll ping you once I get something you can build. Personally, I would be glad if someone could pick up Rust extraction and improve it. Also, as @Bas Spitters mentioned, we would like to move some general parts to MetaCoq, this would help to make maintenance simpler in the future.

@walker ConCert is not compatible with Coq 8.15 https://github.com/AU-COBRA/ConCert

There is also branches for Coq 8.14 https://github.com/AU-COBRA/ConCert/tree/coq-8.14

and Coq 8.11 https://github.com/AU-COBRA/ConCert/tree/coq-8.11

Do you mean "now" rather than "not"?

Ah, yes, sorry, you're right @Meven Lennon-Bertrand :) "ConCert is **now** compatible with Coq 8.15"

(I've edited the comment)

That is perfect!

Last updated: Jan 29 2023 at 06:02 UTC