The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

Hi,

Thanks for the replies. I am now executing (in DOS shell):

coq_makefile *.v -R . Current > __makefile.coq

and it seems to work fine, as it returns silently, without any messages or warnings. However, when I execute (also in DOS):

make -f __makefile.coq

I still get error messages, as shown below (sorry some are in portuguese):

'{' não é reconhecido como um comando interno ou externo, um programa operável ou um arquivo em lotes.

C:\Program Files (x86)\Coq\bin\coqc  -q  -R . Current   and_useless_inaccessible

File "C:\Users\Marcus Ramos\Documents\Formalization\splitfiles/and_useless_inaccessible.v", line 9, characters 0-26:

Error: The file C:\Users\Marcus Ramos\Documents\Formalization\splitfiles/misc_arith.vo contains library misc_arith and not library Current.misc_arith

make: *** [and_useless_inaccessible.vo] Error 1

When I execute the same commands in cygwin, coq_makefile runs silently as well, and make returns:

/usr/bin/sh: -c: line 0: erro de sintaxe próximo do `token' não esperado `('

/usr/bin/sh: -c: line 0: `{ C:\Program Files (x86)\Coq\bin\coqtop -config | tr -d '\r' | tr '\n' '@'; }'

C:\Program Files (x86)\Coq\bin\coqc  -q  -R . Current   and_useless_inaccessible

/usr/bin/sh: -c: line 0: erro de sintaxe próximo do `token' não esperado `('

/usr/bin/sh: -c: line 0: `C:\Program Files (x86)\Coq\bin\coqc  -q  -R . Current   and_useless_inaccessible'

make: *** [and_useless_inaccessible.vo] Error 1

Hope this can help.

Best Regards,

Marcus.

2015-03-19 2:27 GMT+00:00 CJ Bell <siegebell+coq AT gmail.com>:

On Wed, Mar 18, 2015 at 5:49 PM, Marcus Ramos
<marcus.ramos AT univasf.edu.br> wrote:
> I run coq_makefile ("coq_makefile *.v -R . > __makefile.coq") to generate

The -R option expects two arguments:
...
-R dir -as coqdir recursively map physical dir to logical coqdir
-R dir coqdir (idem)
...


-cj