walker (Jul 28 2022 at 16:19): 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 ?
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)
Gaëtan Gilbert (Jul 28 2022 at 16:23):maybe look at https://arxiv.org/abs/2108.02995
Gaëtan Gilbert (Jul 28 2022 at 16:23):I don't know how well it works
Karl Palmskog (Jul 28 2022 at 16:23):https://rust-formal-methods.github.io/tools.html has some Coq-related links
Bas Spitters (Jul 30 2022 at 16:16):More information on rust extraction using ConCert is here: https://github.com/AU-COBRA/ConCert
Bas Spitters (Aug 01 2022 at 11:09):@walker is there anything you need from rust extraction that's not already in concert?
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.
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.
walker (Aug 08 2022 at 18:02):Still I am happy that I learned coq first. It was instructive.
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
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
Paolo Giarrusso (Aug 08 2022 at 18:34):There might be some confusion between ConCert and CompCert?
Karl Palmskog (Aug 08 2022 at 18:51):ah, ConCert is a more academic framework
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
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
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
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
Karl Palmskog (Aug 08 2022 at 18:56):according to cloc, ConCert repo has no OCaml code at all
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
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.
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?
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
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.
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.
walker (Aug 08 2022 at 19:13):also was cool exploring Coq's source code.
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.
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.
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.
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.
Paolo Giarrusso (Aug 08 2022 at 22:54):see also https://github.com/leanprover/lean4/blob/master/doc/faq.md#should-i-use-lean
Huỳnh Trần Khanh (Aug 09 2022 at 02:09):Could you explain why you think Lean is the easy way out?
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.
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.
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).
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.
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
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
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.
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 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
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: Oct 01 2023 at 19:01 UTC