The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

$ getconf ARG_MAX

32000

$ (cd src/reification/; echo """-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""" > /tmp/foo; ocamlc -c @/tmp/foo reif.ml4)

D:\CoqSDK-2\bin\ocamlc.exe: don't know what to do with @/tmp/foo.

Has this feature been recently removed from OCaml?  I'm using 4.01.0.

I've tried renaming "D:\coq-8.4pl5" to "D:\a", and still got the same error.  I'm not sure that I can make it any shorter.

I am using this particular ocaml because I figured it was a good oppertunity to try out the Coq SDK (see https://sympa.inria.fr/sympa/arc/coqdev/2014-09/msg00133.html), and it seems poor if Coq's official SDK, specifically made for compiling ML plugins compatible with the distributed binary version of Coq on Windows, doesn't support compiling ML plugins.

It does seem very suspicious that I'm hitting this error with such a "short" command line.  Furthermore, if I copy-paste the camlp5o command line that it gives me, it runs fine....

I'll try recompiling Coq with the cygwin version of OCaml, and see if I can make that work.  It'd be nice to know why the SDK is failing, though, and how to make it work.

Any other ideas, or things for me to try?

Thanks,

Jason

On Fri Nov 07 2014 at 7:35:59 PM Kyle Stemen <ncyms8r3x2 AT snkmail.com> wrote:

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