The Coq mailing list

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

I get these messages:

$ make -f __makefile.coq

/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\coqdep -c -slash -R . Current "useless_examples.v" > "useless_examples.v.d" || ( RV=$?; rm -f "useless_examples.v.d"; exit ${RV} )

/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\coqdep -c -slash -R . Current \useless_examples.v\ > \useless_examples.v.d\ || ( RV=$?; rm -f \useless_examples.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "useless.v" > "useless.v.d" || ( RV=$?; rm -f "useless.v.d"; exit ${RV} )

/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\coqdep -c -slash -R . Current \useless.v\ > \useless.v.d\ || ( RV=$?; rm -f \useless.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "unitrules_examples.v" > "unitrules_examples.v.d" || ( RV=$?; rm -f "unitrules_examples.v.d"; exit ${RV} )

/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\coqdep -c -slash -R . Current \unitrules_examples.v\ > \unitrules_examples.v.d\ || ( RV=$?; rm -f \unitrules_examples.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "unitrules.v" > "unitrules.v.d" || ( RV=$?; rm -f "unitrules.v.d"; exit ${RV} )

/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\coqdep -c -slash -R . Current \unitrules.v\ > \unitrules.v.d\ || ( RV=$?; rm -f \unitrules.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "misc_list.v" > "misc_list.v.d" || ( RV=$?; rm -f "misc_list.v.d"; exit ${RV} )

/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\coqdep -c -slash -R . Current \misc_list.v\ > \misc_list.v.d\ || ( RV=$?; rm -f \misc_list.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "misc_arith.v" > "misc_arith.v.d" || ( RV=$?; rm -f "misc_arith.v.d"; exit ${RV} )

/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\coqdep -c -slash -R . Current \misc_arith.v\ > \misc_arith.v.d\ || ( RV=$?; rm -f \misc_arith.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "inaccessible.v" > "inaccessible.v.d" || ( RV=$?; rm -f "inaccessible.v.d"; exit ${RV} )

/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\coqdep -c -slash -R . Current \inaccessible.v\ > \inaccessible.v.d\ || ( RV=$?; rm -f \inaccessible.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "emptyrules.v" > "emptyrules.v.d" || ( RV=$?; rm -f "emptyrules.v.d"; exit ${RV} )

/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\coqdep -c -slash -R . Current \emptyrules.v\ > \emptyrules.v.d\ || ( RV=$?; rm -f \emptyrules.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "cfg_examples.v" > "cfg_examples.v.d" || ( RV=$?; rm -f "cfg_examples.v.d"; exit ${RV} )

/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\coqdep -c -slash -R . Current \cfg_examples.v\ > \cfg_examples.v.d\ || ( RV=$?; rm -f \cfg_examples.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "cfg.v" > "cfg.v.d" || ( RV=$?; rm -f "cfg.v.d"; exit ${RV} )

/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\coqdep -c -slash -R . Current \cfg.v\ > \cfg.v.d\ || ( RV=$?; rm -f \cfg.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "and_useless_inaccessible.v" > "and_useless_inaccessible.v.d" || ( RV=$?; rm -f "and_useless_inaccessible.v.d"; exit ${RV} )

/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\coqdep -c -slash -R . Current \and_useless_inaccessible.v\ > \and_useless_inaccessible.v.d\ || ( RV=$?; rm -f \and_useless_inaccessible.v.d\; exit ${RV} )'

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

2015-03-19 16:00 GMT+00:00 Ralf Jung <jung AT mpi-sws.org>:

Hi,

> Thanks Ralf. I tried that, however the output is:
>
> $ make -f __makefile.coq clean
> /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' '@'; }'

I cannot completely understand this, but it looks like something doesn't
like the spaces? I have no experience with the CLI on Windows.

It seems to delete your files just fine though. So what's the problem?
Just re-run "make" now.

Kind regards,
Ralf