Get the list of extracted files when using Recursive Extraction Library

Viewed 54

Recursive Extraction Library generates multiple .ml and .mli files. Is it possible to print the list of generated files during the extraction ?

The best I have come up with is to note that generated files begin with a capital letter, but it is not optimal.

1 Answers

Run your code through coqtop rather than through 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 <

If you want it to print when you run coqc, you should probably submit a feature request for a command line flag or a setting.

Related