search

AU-COBRA / coq-rust-extraction

Coq plugin for extracting Rust code
MIT License
10 stars 3 forks source link

Opam file #4

Closed 4ever2 closed 1 year ago

4ever2 commented 1 year ago

Add opam file and remove the typed-extraction submodule. Also renames the package from ConCert.RustExtract to RustExtraction.

sethahrenbach commented 1 year ago

Let's merge this bad boy!

4ever2 commented 1 year ago

This PR is not ready to be merged yet. It currently depends on an unstable commit of MetaCoq and the CI also needs a bit more work.

sethahrenbach commented 1 year ago

yes I see. I am getting:

  * Missing dependency:
    - ocaml-variants > 5.1.1~
    no matching version

No solution found, exiting

I was hoping I could use this in my project, rather than the larger ConCert code chunks. I think my Fixpoint Coq functions are choking the Rust extraction methods I found in extraction/tests/RustExtractTests.v. I tried to include the plugin in my code, but keep getting META errors relate to the OCaml stuff.