The Coq mailing list

[CJ Bell <siegebell AT gmail.com>]

The problem has to do with the '-pp' parameter that you are giving
ocaml to use the camlp5o preprocessor; notice that in the command you
posted, camlp5o never even runs. For whatever reason, it fails when
the filename of camlp5o is in quotes.

Broken:
ocaml ... -pp '"D:\CoqSDK-2\bin/camlp5o" ...' ...

Works:
ocaml ... -pp 'D:\CoqSDK-2\bin/camlp5o ...' ...

The '-pp' is automatically added by coq_makefile. You can manually fix
it by replacing

PP?=-pp '"$(CAMLP4BIN)$(CAMLP4)o" -I "$(CAMLLIB)" -I . $(COQSRCLIBS)
$(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'

with

PP?=-pp '$(CAMLP4BIN)$(CAMLP4)o -I "$(CAMLLIB)" -I . $(COQSRCLIBS)
$(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'


-cj

On Fri, Nov 7, 2014 at 6:26 PM, Jason Gross 
<jasongross9 AT gmail.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
>