The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

For what it's worth, Pierre Letouzey just gave me the solution:

Cd "folder/"
before the Separate Extraction command in the Coq script worked well for me.

Cheers!

2013/11/20 Nuno Gaspar <nmpgaspar AT gmail.com>

Hello.

I have a question regarding the extraction mechanism. By checking [1] I see that I can specify the file (with path) to which I want to extract too. For instance,

Extraction "folder/file.ml" Semantics.operation

works well.

However, I need other types of extraction, namely 

Separate Extraction Semantics.

Extraction Library Semantics.

Which doesn't seem to support the parameter to target file...

In short, I want all my ocaml extracted files to go to one particular subfolder and not to the root of my Coq project from which I call my Makefile.

I can easily do that with the first extraction command shown in this email, but it seems impossible right the remaining? 

Sure, I can include some bash scripting in my Makefile to obtain what I want but I would rather prefer a "pure" Coq solution.

 

[1] http://coq.inria.fr/refman/Reference-Manual025.html

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.