The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I do not know if ocamlbuild would behave better.

Otherwise, if you have an ocaml module exporting the compiler primitives (or if you compile ocamlc from the source), there might be a way to write a ml program such as:

let _ = ml_compile "a.out" ("D:\coq-8.4pl5/kernel"::"D:\coq-8.4pl5/lib"::"D:\coq-8.4pl5/library"...

I guess it is quite overkill, though, and not very convenient.

2014-11-08 0:26 GMT+01:00 Jason Gross <jasongross9 AT gmail.com>:

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

--

.../Sedrikov\...