formal-land / coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦
GNU Affero General Public License v3.0
418 stars 14 forks source link

Draft: add links generation from JSON and Python #608

Open clarus opened 1 month ago

clarus commented 1 month ago

The goal of this PR is to automate as much as possible the generation of links files, generating the Coq code in Python from the JSON of the AST used in coq-of-rust.