The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

My suggestion to Jason was to stop trying to use Coq in Windows, but I can see that there could be some benefit to finding a way to stay Windows-compatible. ;)

On 11/07/2014 06:26 PM, Jason Gross wrote:

Hi,

I am trying to compile a Coq project with ml plugins (bedrock, in particular), and when I run `make`, I get:

make[3]: Entering directory '/cygdrive/d/Documents/GitHub/bedrock/src/reification'

ocamlc -c -rectypes  -I . -I "D:\coq-8.4pl5/kernel" -I "D:\coq-8.4pl5/lib" -I "D:\coq-8.4pl5/library" -I "D:\coq-8.4pl5/parsing" -I "D:\coq-8.4pl5/pretyping" -I "D:\coq-8.4pl5/interp" -I "D:\coq-8.4pl5/proofs" -I "D:\coq-8.4pl5/tactics" -I "D:\coq-8.4pl5/tools" -I "D:\coq-8.4pl5/toplevel" -I "D:\coq-8.4pl5/plugins/"cc -I "D:\coq-8.4pl5/plugins/"decl_mode -I "D:\coq-8.4pl5/plugins/"extraction -I "D:\coq-8.4pl5/plugins/"field -I "D:\coq-8.4pl5/plugins/"firstorder -I "D:\coq-8.4pl5/plugins/"fourier -I "D:\coq-8.4pl5/plugins/"funind -I "D:\coq-8.4pl5/plugins/"micromega -I "D:\coq-8.4pl5/plugins/"nsatz -I "D:\coq-8.4pl5/plugins/"omega -I "D:\coq-8.4pl5/plugins/"quote -I "D:\coq-8.4pl5/plugins/"ring -I "D:\coq-8.4pl5/plugins/"romega -I "D:\coq-8.4pl5/plugins/"rtauto -I "D:\coq-8.4pl5/plugins/"setoid_ring -I "D:\coq-8.4pl5/plugins/"subtac -I "D:\coq-8.4pl5/plugins/"subtac/test -I "D:\coq-8.4pl5/plugins/"syntax -I "D:\coq-8.4pl5/plugins/"xml -I D:/CoqSDK-2/lib/camlp5 -pp '"D:\CoqSDK-2\bin/camlp5o" -I "D:/CoqSDK-2/lib/" -I . -I "D:\coq-8.4pl5/kernel" -I "D:\coq-8.4pl5/lib" -I "D:\coq-8.4pl5/library" -I "D:\coq-8.4pl5/parsing" -I "D:\coq-8.4pl5/pretyping" -I "D:\coq-8.4pl5/interp" -I "D:\coq-8.4pl5/proofs" -I "D:\coq-8.4pl5/tactics" -I "D:\coq-8.4pl5/tools" -I "D:\coq-8.4pl5/toplevel" -I "D:\coq-8.4pl5/plugins/"cc -I "D:\coq-8.4pl5/plugins/"decl_mode -I "D:\coq-8.4pl5/plugins/"extraction -I "D:\coq-8.4pl5/plugins/"field -I "D:\coq-8.4pl5/plugins/"firstorder -I "D:\coq-8.4pl5/plugins/"fourier -I "D:\coq-8.4pl5/plugins/"funind -I "D:\coq-8.4pl5/plugins/"micromega -I "D:\coq-8.4pl5/plugins/"nsatz -I "D:\coq-8.4pl5/plugins/"omega -I "D:\coq-8.4pl5/plugins/"quote -I "D:\coq-8.4pl5/plugins/"ring -I "D:\coq-8.4pl5/plugins/"romega -I "D:\coq-8.4pl5/plugins/"rtauto -I "D:\coq-8.4pl5/plugins/"setoid_ring -I "D:\coq-8.4pl5/plugins/"subtac -I "D:\coq-8.4pl5/plugins/"subtac/test -I "D:\coq-8.4pl5/plugins/"syntax -I "D:\coq-8.4pl5/plugins/"xml pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl' -impl reif.ml4

The input line is too long.

Error while running external preprocessor

Command line: "D:\CoqSDK-2\bin/camlp5o" -I "D:/CoqSDK-2/lib/" -I . -I "D:\coq-8.4pl5/kernel" -I "D:\coq-8.4pl5/lib" -I "D:\coq-8.4pl5/library" -I "D:\coq-8.4pl5/parsing" -I "D:\coq-8.4pl5/pretyping" -I "D:\coq-8.4pl5/interp" -I "D:\coq-8.4pl5/proofs" -I "D:\coq-8.4pl5/tactics" -I "D:\coq-8.4pl5/tools" -I "D:\coq-8.4pl5/toplevel" -I "D:\coq-8.4pl5/plugins/"cc -I "D:\coq-8.4pl5/plugins/"decl_mode -I "D:\coq-8.4pl5/plugins/"extraction -I "D:\coq-8.4pl5/plugins/"field -I "D:\coq-8.4pl5/plugins/"firstorder -I "D:\coq-8.4pl5/plugins/"fourier -I "D:\coq-8.4pl5/plugins/"funind -I "D:\coq-8.4pl5/plugins/"micromega -I "D:\coq-8.4pl5/plugins/"nsatz -I "D:\coq-8.4pl5/plugins/"omega -I "D:\coq-8.4pl5/plugins/"quote -I "D:\coq-8.4pl5/plugins/"ring -I "D:\coq-8.4pl5/plugins/"romega -I "D:\coq-8.4pl5/plugins/"rtauto -I "D:\coq-8.4pl5/plugins/"setoid_ring -I "D:\coq-8.4pl5/plugins/"subtac -I "D:\coq-8.4pl5/plugins/"subtac/test -I "D:\coq-8.4pl5/plugins/"syntax -I "D:\coq-8.4pl5/plugins/"xml pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl "reif.ml4" > C:\Users\Jason\AppData\Local\Temp\ocamlpp23f633

The makefile was generated with "coq_makefile -R ../../src Bedrock extlib.mli extlib.ml reif.ml4 example.v -o Makefile.coq", and the target was extlib.cmi.

How to I fix or work around this?

Thanks,

Jason