Notification Bot (Aug 09 2022 at 09:17): Notification Bot (Aug 09 2022 at 09:17):walker has marked this topic as resolved.
Danil Annenkov (Aug 09 2022 at 09:25):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.
Danil Annenkov (Aug 22 2022 at 11:32):@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
Meven Lennon-Bertrand (Aug 22 2022 at 13:05):Do you mean "now" rather than "not"?
Danil Annenkov (Aug 22 2022 at 14:22):Ah, yes, sorry, you're right @Meven Lennon-Bertrand :) "ConCert is now compatible with Coq 8.15"
Danil Annenkov (Aug 22 2022 at 14:23):(I've edited the comment)
walker (Sep 13 2022 at 10:44):That is perfect!
Last updated: Jan 29 2023 at 06:02 UTC