The Coq mailing list

["Kyle Stemen" <ncyms8r3x2 AT snkmail.com>]

Your command line looks relatively small for exceeding a limit. With some googling, it appears the cygwin command line limit should be 32,000 characters (http://www.in-ulm.de/~mascheck/various/argmax/). What does 'getconf ARG_MAX' return?

It looks like camlp5o is a native windows application and you are calling it through cygwin. If you can use cygwin's ocaml package instead, it may support a longer command line.

On Fri, Nov 7, 2014 at 3:26 PM, Jason Gross jasongross9-at-gmail.com |coq-club/Example Allow| <ballsejvgt AT sneakemail.com> 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