coq - 使用递归提取库时获取提取文件列表

Question

递归提取库 生成多个.ml 和.mli 文件。是否可以在提取过程中打印生成的文件列表？

我想到的最好办法是注意生成的文件以大写字母开头，但这不是最佳选择。

Answer 1

通过 coqtop 而不是通过 coqc 运行代码:

$ echo 'Recursive Extraction Library Specif.' | coqtop
Welcome to Coq 8.6.1 (July 2017)

Coq < The file Logic.ml has been created by extraction.
The file Logic.mli has been created by extraction.
The file Datatypes.ml has been created by extraction.
The file Datatypes.mli has been created by extraction.
The file Specif.ml has been created by extraction.
The file Specif.mli has been created by extraction.

Coq <

如果你希望它在运行 coqc 时打印，你可能应该 submit a feature request用于命令行标志或设置。