再帰的抽出ライブラリを使用する場合、抽出されたファイルのリストを取得

Question

Recursive Extraction Libraryは、複数のファイルを生成します。.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コマンドラインフラグや設定の必要があります。