Stream: Coq users

Topic: ✔ Rust Extraction


view this post on Zulip walker (Jul 28 2022 at 16:19):

I am trying to create some project in rust and Coq, Currently I am literally rewriting code manually, is there a way to automat the process of generating code from coq to rust ?

view this post on Zulip walker (Jul 28 2022 at 16:21):

I see there is an old project from 2014 that claims to do that: https://github.com/pirapira/coq2rust but the project is ocaml an I am worried it is dead (and I don't know ocaml so if it is not working, I won't be able to fix it quickly)

view this post on Zulip Gaëtan Gilbert (Jul 28 2022 at 16:23):

maybe look at https://arxiv.org/abs/2108.02995

view this post on Zulip Gaëtan Gilbert (Jul 28 2022 at 16:23):

I don't know how well it works

view this post on Zulip Karl Palmskog (Jul 28 2022 at 16:23):

https://rust-formal-methods.github.io/tools.html has some Coq-related links

view this post on Zulip Bas Spitters (Jul 30 2022 at 16:16):

More information on rust extraction using ConCert is here: https://github.com/AU-COBRA/ConCert

view this post on Zulip Bas Spitters (Aug 01 2022 at 11:09):

@walker is there anything you need from rust extraction that's not already in concert?

view this post on Zulip walker (Aug 08 2022 at 18:01):

@Bas Spitters I only noticed this message right now so sorry for late reply:

Actually yes the project works only for old Coq, I tried porting to modern coq and it was not trivial. That will be something that I will heavily rely on for my PhD and I am worried that CompCert is just academic project that will die once funding stop.

view this post on Zulip walker (Aug 08 2022 at 18:02):

I actually also believe that it will be hard to write Trustworthy extraction plugin for rust since there are some trickery with MiniML so unfortunately I might move to something with already existing FFI like lean4.

view this post on Zulip walker (Aug 08 2022 at 18:02):

Still I am happy that I learned coq first. It was instructive.

view this post on Zulip Karl Palmskog (Aug 08 2022 at 18:20):

if you're looking at formal verification projects in academia, CompCert is probably one of the most likely to live on for a while. Besides basic connections to Inria which has sustained funding through French government, it also has the commercial side: https://www.absint.com/compcert/index.htm

view this post on Zulip Gaëtan Gilbert (Aug 08 2022 at 18:25):

Actually yes the project works only for old Coq, I tried porting to modern coq and it was not trivial.

getting help for that may work better than getting help for a new extraction backend

view this post on Zulip Paolo Giarrusso (Aug 08 2022 at 18:34):

There might be some confusion between ConCert and CompCert?

view this post on Zulip Karl Palmskog (Aug 08 2022 at 18:51):

ah, ConCert is a more academic framework

view this post on Zulip Karl Palmskog (Aug 08 2022 at 18:51):

yes, the preferred approach around here when we need some code to work with recent Coq is to work with code authors

view this post on Zulip Karl Palmskog (Aug 08 2022 at 18:52):

thanks to Coq's code compatibility policy, it's usually not a big deal to port between versions using the changelog

view this post on Zulip Gaëtan Gilbert (Aug 08 2022 at 18:53):

we're talking about plugins not .v code, the changelog is basically useless for porting plugins

view this post on Zulip Karl Palmskog (Aug 08 2022 at 18:54):

but is ConCert really much of a plugin? Last time I checked, it was mostly Coq code, and then it uses MetaCoq

view this post on Zulip Karl Palmskog (Aug 08 2022 at 18:56):

according to cloc, ConCert repo has no OCaml code at all

view this post on Zulip walker (Aug 08 2022 at 18:57):

you can be right, I could have talked to the authors but I took the easy way out and decided to just use lean

view this post on Zulip walker (Aug 08 2022 at 18:58):

also I wouldn't compare compcert to concert, I would consider compcert an anomaly, it is one of the very few academic project that lived on.

view this post on Zulip Enrico Tassi (Aug 08 2022 at 19:03):

Didn't Ocaml live on? Didn't Coq? Also, you mention your PhD, isn't it going to be an academic project too?

view this post on Zulip Karl Palmskog (Aug 08 2022 at 19:11):

I'd say Bas has a pretty good record of keeping Coq projects alive at this point... CoRN is around 20 years old

view this post on Zulip walker (Aug 08 2022 at 19:12):

I get your point, maybe I am over paranoid, I never knew the author, I would like nothing more than looking back and realizing that I was wrong.

view this post on Zulip walker (Aug 08 2022 at 19:13):

In any was it was also fun learning Ocaml, I had to learn it in my failing attempt to write the plugin.

view this post on Zulip walker (Aug 08 2022 at 19:13):

also was cool exploring Coq's source code.

view this post on Zulip walker (Aug 08 2022 at 19:18):

Also, you mention your PhD, isn't it going to be an academic?

Good question, So It is industrial PhD and while it is understandable that papers are cool an essential for the Degree, the industrial partner (also the ones who pay for everything) are solely interested in Code that works reliably, an it will be nightmare if anything I use turned into fix it yourself kind of projects.

view this post on Zulip walker (Aug 08 2022 at 19:19):

I worked in some projects like that in the past, But Ocaml and Coq are (same for compcert and any project with commits 5+ years after it it was first published). And those project lived for like 20+ years not just 5 so yes they are reliable. That why I trust that Coq and Ocaml are not going anywhere soon.

view this post on Zulip Théo Zimmermann (Aug 08 2022 at 20:21):

If you are worried about durability, then using Lean4 looks like a strange choice. Lean4 is still alpha (or beta) software and its author has a history of breaking user's code without looking back. On the contrary, the Coq ecosystem has a history of deeply caring about compatibility and upgrading.

view this post on Zulip walker (Aug 08 2022 at 21:01):

mmm, I will have to think about it. my problem is not with coq, it is with coq's support for Rust extraction.

view this post on Zulip Paolo Giarrusso (Aug 08 2022 at 22:54):

see also https://github.com/leanprover/lean4/blob/master/doc/faq.md#should-i-use-lean

view this post on Zulip Huỳnh Trần Khanh (Aug 09 2022 at 02:09):

Could you explain why you think Lean is the easy way out?

view this post on Zulip Enrico Tassi (Aug 09 2022 at 05:02):

Imo the json extraction module is the option giving you the most freedom. I could even imagine Lean or agda producing the same kind of output. Then you use what you want. Of course, not using something already existing, does not seem the quickest option. In particular, software rarely gets written well the first time, and the prototype better be written quickly (not from scratch) since you are going to toss it anyway.

view this post on Zulip Théo Zimmermann (Aug 09 2022 at 07:49):

walker said:

mmm, I will have to think about it. my problem is not with coq, it is with coq's support for Rust extraction.

This is not necessarily the most recommended option (for various reasons that others can ellaborate), but if you were to write a Rust extraction plugin in OCaml, then you could benefit from upgrades from one version to the next by adding it into Coq's CI. See https://github.com/coq/coq/blob/master/CONTRIBUTING.md#support-for-plugin-and-library-authors.

view this post on Zulip Théo Zimmermann (Aug 09 2022 at 07:51):

The comments about plugins quickly bitrotting relate to plugins that are not in Coq's CI (for instance, because their authors have created them for a version of Coq that was already not master and never upgraded them to master which is necessary to get into Coq's CI).

view this post on Zulip walker (Aug 09 2022 at 08:05):

I admit, lean is more cumbersome than I thought, I am back to coq. The problem with writing my own extraction plugin is that it was best-effort, there were many corrner cases with polymorphism that were were not handled.

view this post on Zulip walker (Aug 09 2022 at 08:05):

so the solution I am attempting next is just extracting to OCAML and see if I can use OCaml ffi interface in rust

view this post on Zulip Karl Palmskog (Aug 09 2022 at 08:14):

I'd recommend using the FFI approach given here (go via C FFI): https://github.com/xavierleroy/camljava

view this post on Zulip Bas Spitters (Aug 09 2022 at 08:33):

@walker Aside, since you're doing a PhD, I'd recommend using your real name and affiliation. But that's up to you.
The concert's extraction to rust is build on metacoq, a central and well-supported part of Coq.
If you're serious about contributing to it, we could discuss moving some parts to a more central place.
In fact, we're already working with the metacoq team on tighter integration. They are working on certified extraction to ocaml.

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 now 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: Mar 28 2024 at 11:01 UTC