递归提取库
生成多个.ml
和.mli
文件。是否可以在提取过程中打印生成的文件列表?
我想到的最好办法是注意生成的文件以大写字母开头,但这不是最佳选择。
最佳答案
通过 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用于命令行标志或设置。
关于coq - 使用递归提取库时获取提取文件列表,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/46545217/