Stream: Coq users

Topic: ✔ Rust Extraction


view this post on Zulip Notification Bot (Aug 09 2022 at 09:17):

walker has marked this topic as resolved.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Meven Lennon-Bertrand (Aug 22 2022 at 13:05):

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

view this post on Zulip 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"

view this post on Zulip Danil Annenkov (Aug 22 2022 at 14:23):

(I've edited the comment)

view this post on Zulip walker (Sep 13 2022 at 10:44):

That is perfect!


Last updated: Jan 29 2023 at 06:02 UTC