The Coq mailing list

[CJ Bell <siegebell+coq AT gmail.com>]

It looks like one of your environmental variables, $COQBIN, is set to
a DOS format path instead of a posix path.

Either:
1)
$ export PATH=$PATH:/cygdrive/c/Program\ Files\ \(x86\)/Coq/bin
$ export COQBIN=
or 2)
$ export COQBIN=/cygdrive/c/Program\ Files\ \(x86\)/Coq/bin

-cj

On Thu, Mar 19, 2015 at 12:36 PM, Marcus Ramos
<marcus.ramos AT univasf.edu.br>
 wrote:
> 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
>>
>>
>