Including header / footer in a file generated by extraction

I'm using Extraction "foo.ml" main. to extract the relevant parts of my development into an OCaml file, and I'm currently using dune to build everything.

For practical reasons, I'm using several native types, and map many functions to library functions of OCaml or other libraries. That means that (as far as I understand) I'll have to add a bunch of open statements at the top of the file to import the relevant libraries. I also need to add a call to the main function at the very end, to actually get a runnable program.

With the things I found in Coq, so far, neither appears cleanly possible. (Ab)using Set Extraction File Comment "*) import List (*". allows inserting a single line with bad formatting (newlines are removed from the string), but it will be included in both .ml and .mli files, which will generate a warning for an unused import (in the .mli file) that dune treats as an error by default. The list of constants passed to Extraction "filename" is arbitrarily reordered, so I can't go Extraction "foo.ml" init main fini. and expect init to actually extract before main (let alone all the dependencies of main.)

On the dune side, I also can't see any way to prefix/suffix code to the generated file. I'd strongly prefer not to return to Makefiles.

MCE for playing around with:

mce.v:

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.

dune-project:

(lang dune 3.8)
(using coq 0.8)
(name mce)
(package
 (name mce)
 (depends ocaml dune coq))

dune:

(coq.extraction
 (prelude mce)
 (extracted_modules mce))

(executable
 (name mce)
 (public_name mce))

Resulting file and what's missing:

+open List

 (** val values : bool list **)

 let values =
   true :: (false :: [])

 (** val xs' : bool list **)

 let xs' =
   map not values

 (** val ys' : bool list **)

 let ys' =
   false :: (true :: [])

 (** val sanity_test : bool **)

 let sanity_test =
   (=) xs' ys'
+
+;;print_endline (if sanity_test then "ok" else "not ok")

Any way to have either of Coq or dune add those parts automatically?

Solution

dune does have a way to do this, there's a DSL for "user actions" that can be used to do a sequence of echo and cat steps for generating a completed file, and by defining a bunch of custom rules those will be run at the right point in the build process.

Adjusting the MCE as follows:

mce.v:

14c14
< Extraction "mce.ml" sanity_test.
---
> Extraction "mce.raw.ml" sanity_test.

the raw output goes elsewhere now, since rules can't overwrite existing files (or technically they can but it's a bad idea and an error by default)

At the end of dune:

(rule (with-stdout-to mce.ml
 (progn
  (echo "open List")
  (cat mce.raw.ml)
  (echo ";;print_endline (if sanity_test then \"ok\" else \"not ok\")"))))

(rule (copy mce.raw.mli mce.mli))

both the .ml and the .mli file are needed, but the second one can just be copied over since it's already ok
dune can infer deps/target from copy, cat, with-stdout-to, etc., so the full form of (rule (target …) (deps …) (action …)) isn't needed here; for more complex ones you might have to switch

Now a dune exec mce will go through and print ok.