The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

How do I build coq on windows?  When I run ./configure and make, I get

$ ./configure -local

You have GNU Make 4.0. Good!

You have Objective-Caml 4.01.0. Good!

No Camlp5 installation found. Looking for Camlp4 instead...

You have native-code compilation. Good!

LablGtk2 not found: CoqIde will not be available.

hevea was not found; documentation will not be available

  Architecture                      : win32

  Operating system                  : Windows_NT

  Coq VM bytecode link flags        : -custom

  Coq tools bytecode link flags     : -custom

  OS dependent libraries            : -cclib -lunix

  Objective-Caml/Camlp4 version     : 4.01.0

  Objective-Caml/Camlp4 binaries in : D:/OCaml/bin

  Objective-Caml library in         : D:\OCaml\lib

  Camlp4 library in                 : +camlp4

  Native dynamic link support       : true

  Documentation                     : None

  CoqIde                            : no

  Web browser                       : start %s

  Coq web site                      : http://coq.inria.fr/

  Local build, no installation...

Access denied - PLUGINS/BTAUTO

Access denied - PLUGINS/CC

Access denied - PLUGINS/DECL_MODE

Access denied - PLUGINS/EXTRACTION

Access denied - PLUGINS/FIRSTORDER

Access denied - PLUGINS/FOURIER

Access denied - PLUGINS/FUNIND

Access denied - PLUGINS/MICROMEGA

Access denied - PLUGINS/NSATZ

Access denied - PLUGINS/OMEGA

Access denied - PLUGINS/QUOTE

Access denied - PLUGINS/ROMEGA

Access denied - PLUGINS/RTAUTO

Access denied - PLUGINS/SETOID_RING

Access denied - PLUGINS/SYNTAX

Access denied - PLUGINS/XML

File not found - (

File not found - -NAME

File not found - .SVN

File not found - -PRUNE

File not found - )

File not found - -O

File not found - (

File not found - -TYPE

File not found - D

File not found - -EXEC

File not found - PRINTF

File not found - \%S\

File not found - {}

File not found - ;

File not found - )

If anything in the above is wrong, please restart './configure'.

*Warning* To compile the system for a new architecture

          don't forget to do a 'make clean' before './configure'.

$ make coqlight

File not found - *.mly

File not found - *.mll

File not found - *.mllib

File not found - *.ml4

File not found - *.c

Access denied - .

File not found - (

File not found - -NAME

File not found - {ARCH}

File not found - -O

File not found - -NAME

File not found - .SVN

File not found - -O

File not found - -NAME

File not found - _DARCS

File not found - -O

File not found - -NAME

File not found - -O

File not found - -NAME

File not found - .BZR

File not found - -O

File not found - -NAME

File not found - DEBIAN

File not found - -O

File not found - -NAME

File not found - -O

File not found - -NAME

File not found - _BUILD

File not found - )

File not found - -PRUNE

File not found - -O

File not found - (

File not found - -NAME

File not found - )

File not found - -PRINT

File not found - *.mli

File not found - .#*v

make --warn-undefined-variable --no-builtin-rules -f Makefile.build "coqlight"

make[1]: Entering directory '/cygdrive/d/Documents/GitHub/HoTT/coq-HoTT'

Makefile.build:842: target '----------' doesn't match the target pattern

Makefile.build:842: target '.GIT' doesn't match the target pattern

Makefile.build:842: target '----------' doesn't match the target pattern

Makefile.build:842: target 'MYOCAMLBUILD.ML' doesn't match the target pattern

Makefile.build:842: target '----------' doesn't match the target pattern

Makefile.build:842: target 'MYOCAMLBUILD_CONFIG.ML' doesn't match the target pat

tern

Makefile.build:844: target '----------' doesn't match the target pattern

Makefile.build:844: target '.GIT' doesn't match the target pattern

Makefile.build:844: target '----------' doesn't match the target pattern

Makefile.build:844: target 'MYOCAMLBUILD.ML' doesn't match the target pattern

Makefile.build:844: target '----------' doesn't match the target pattern

Makefile.build:844: target 'MYOCAMLBUILD_CONFIG.ML' doesn't match the target pat

tern

OCAMLDEP  lib/loc.ml

OCAMLOPT  lib/loc.ml

File "lib/loc.ml", line 71, characters 15-26:

Error: Unbound module Exninfo

Makefile.build:847: recipe for target 'lib/loc.cmx' failed

make[1]: *** [lib/loc.cmx] Error 2

rm lib/loc.ml.d

make[1]: Leaving directory '/cygdrive/d/Documents/GitHub/HoTT/coq-HoTT'

Makefile:138: recipe for target 'coqlight' failed

make: *** [coqlight] Error 2

/cygdrive/d/Documents/GitHub/HoTT /cygdrive/d/Documents/GitHub/HoTT/etc /cygdriv

e/d/Documents/GitHub/HoTT

Thanks,

Jason