Extraction: adding file prefix (`open …`) & suffix (e.g. function call), from Coq or dune?

Using Coq
1

After asking a question on stackoverflow and then re-reading the documentation a couple more times, I’m pretty sure that it’s currently not possible to

  • insert stuff at the top of an extracted file (like library imports), or
  • insert stuff at the end of an extracted file (like a call to the main function),

either on the Coq or the dune side. Duplicating the example I included over there, the code

From Coq.extraction Require Import Extraction ExtrOcamlBasic.
From Coq.Lists Require Import List.
Import ListNotations.
Parameter eqb_list : forall {a}, list a -> list a -> bool.
Extract Inlined Constant eqb_list => "(=)".
Extract Inlined Constant map => "map".
Extract Inlined Constant negb => "not".
Definition values := [true; false].
Definition xs := map negb values.
Definition ys := Eval compute in xs.
Definition sanity_test := eqb_list xs ys.
(* FIXME: prefix [open List] ; but expect this to potentially be several definitions *)
(* FIXME: suffix [;;print_endline (if sanity_test then "ok" else "not ok")] *)
Extraction "mce.ml" sanity_test.

together with the dune files (see SO question) will result in (prettified)…

let values = true :: (false :: [])
let xs = map not values
let ys = false :: (true :: [])
let sanity_test = (=) xs ys

…which doesn’t do anything and doesn’t even compile (for lack of open List at the top.)

What I’d like to have instead is…

open List
let values = true :: (false :: [])
let xs = map not values
let ys = false :: (true :: [])
let sanity_test = (=) xs ys
;;print_endline (if sanity_test then "ok" else "not ok")

…which actually compiles and also runs a sanity check (or calls a main function for a fully functioning standalone program).

I can write a Makefile that will cat multiple files together to add the open statement(s, and possibly more definitions) at the top, as well as the final call to main (and/or other sanity checks) at the end, but I’d really like to avoid falling back to Makefiles…

  • Did I miss a way to do this with Coq and/or dune?
  • If it’s currently not possible, is this already on the radar / coming soon? Or should I open a ticket somewhere?
2

Hi,

It is possible to do some “post-processing” of ml files using Dune. In your case we can extract your file to say mce_raw.ml and in your library stanza make sure to disallow this file using the (modules :standard \ mce_raw) field. Now we can add a rule stanza which will take mce_raw.ml and produce the corrected mce.ml. It will look something like this:

(rule
 (deps mce_raw.ml)
 (targets mce.ml)
 (action ...))

Now we need to fill in the action field, which you can read more about here: User Actions — Dune documentation

You can in this case use progn to first (echo) the text open List and then (cat) the mce_raw.ml file. This action will be ok for single line additions but might get a bit more tedious when trying to create a bigger patch. In that case I would suggest creating a patch file with a diff and then using patch with the (run ) action to fix the file.

There is no first-class support for patching extracted code in Dune, mostly because it is difficult to determine what kinds of actions are in scope. It is however possible to do so with manual rules.

What really needs to happen, to make this situation better, is for Coq extraction to produce correct code. We don’t have a lot of maintainers for extraction, so if you think something can be improved, contributions are always welcome.

Let me know if you need any more information on what I’ve said above.

1 Like