如何在Coq提取的OCaml文件中自动添加头尾代码？

我通过Extraction "foo.ml" main.将Coq开发内容提取为OCaml文件，当前使用dune构建项目。由于用到多个原生类型，需要映射到OCaml或第三方库的函数，因此必须在生成的OCaml文件顶部添加若干open语句导入依赖库，同时在文件末尾添加主函数调用以生成可运行程序。

尝试过Coq的Set Extraction File Comment方法，但存在格式问题，还会在.mli文件中触发警告（dune默认将警告视为错误）；此外，传递给Extraction "filename"的常量列表会被任意重排，无法按照预期顺序提取代码。

在dune侧也未找到为生成文件添加前缀/后缀代码的方法，且不想回归使用Makefile。询问是否有办法通过Coq或dune自动添加所需的头尾代码。

解决方案 #

Coq侧：控制提取顺序并映射OCaml顶层逻辑 #

1. 映射OCaml函数并定义包裹逻辑：通过Extract Constant将OCaml的顶层常用函数（如Sys.exit、print_endline）映射到Coq常量，在Coq中定义包裹主逻辑的函数，再指定提取顺序确保该函数最后输出：

   (* 映射OCaml函数到Coq常量 *)
   Extract Constant print_endline => "print_endline".
   Extract Constant sys_exit => "Sys.exit".
   
   (* 定义包裹主逻辑的函数 *)
   Definition main_wrapper :=
     let _ := main in
     let _ := print_endline "执行完成" in
     sys_exit 0.
   
   (* 指定提取顺序，确保main_wrapper最后被提取 *)
   Set Extraction Order main, main_wrapper.
   (* 提取包含包裹函数的代码 *)
   Extraction "foo.ml" main_wrapper.
   

   生成的OCaml代码会包含main_wrapper函数，后续只需添加一行顶层调用即可运行。

2. 自定义提取脚本（进阶）：利用Coq的提取API编写简单脚本，直接在生成OCaml代码时插入前缀的open语句和后缀的主函数调用。这种方式完全控制代码结构，不会触发.mli的警告问题。

Dune侧：通过规则自动处理生成的代码 #

在dune中定义链式规则，用sed工具在提取完成后自动修改OCaml文件，添加头尾内容：

(* 基础规则：从Coq文件提取OCaml代码 *)
(rule
 (targets foo.ml)
 (deps foo.v)
 (action (run coqc -Q . YourNamespace foo.v)))

(* 处理规则：添加前缀open语句和后缀主函数调用 *)
(rule
 (targets foo_run.ml)
 (deps foo.ml)
 (action
  (progn
   (* 在文件开头插入依赖库open语句 *)
   (run sed -i '1i open Lib1\nopen Lib2\nopen Lib3' %{deps})
   (* 在文件末尾追加主函数调用 *)
   (run echo 'let () = main ()' >> %{deps})
   (* 重命名为最终编译文件 *)
   (run mv %{deps} %{targets}))))

(* 定义可执行文件，依赖处理后的ml文件 *)
(executable
 (name foo_run)
 (libraries lib1 lib2 lib3))

该方案无需修改Coq代码，完全通过dune规则链实现自动化处理，避免手动修改文件。

内容的提问来源于stack exchange，提问作者nobody