Soft Question: How to setup a dev environment for reading?

[BlastWind]

I'm intrigued by the solid work here! But as someone who never used MetaCoq and ocaml before, reading it is a bit difficult. I feel that the entry point of the core logic is really in the Rust Extract keyword extension in g_rust_extraction.ml, from which the pipeline runs.

It would be of great help if someone can teach me how to 1) Setup the proper linting for the files in plugin/src. Although make succeeds, there are Unbound module errors everywhere in the .ml files. Claude tried setting up dune for me to no avail. 2) Setup a debugger for the pipeline to see the input/output data shape at each step. Where would this debugger start at? Presumably it can't start from the .v files that use Rust Extract. But if it starts in g_rust_extraction.ml, then I would need to somehow inject coq for the pipeline to run from.

[4ever2]

I wouldn't recommend reading the OCaml code, g_rust_extraction.mlg is just a small wrapper that registers the Rust Extract command in Coq. Most of the code is written in Coq.

The Rust Extract command is one of two entrypoints that you can use, it is also possible to use the extraction directly in Coq without the OCaml plugin. You can see here how this is done. It is probably easier to understand and debug that code.

Please note that this repository only contains the code for printing extracted code to Rust, the main extraction logic was merged into MetaCoq https://github.com/MetaCoq/metacoq/tree/coq-8.19/erasure/theories/Typed