The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

For any others who face this problem, the solution was to pass the -no-native-compiler option to ./configure.

On Wed, Nov 6, 2013 at 4:18 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

However, now I get

cd kernel/byterun/ && \

"ocamlmklib" -oc coqrun coq_fix_code.o coq_memory.o coq_values.o coq_interp.o

COQMKTOP -o bin/coqtop.exe

strip bin/coqtop.exe

COQC -noinit theories/Init/Notations.v

The input line is too long.

Warning:

Removed file D:\Documents\GitHub\HoTT\coq-HoTT\theories/Init/Notations.vo

Anomaly: Library compilation failure. Please report.

Makefile.build:479: recipe for target 'theories/Init/Notations.vo' failed

make[1]: *** [theories/Init/Notations.vo] Error 1

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

Any ideas?

-Jason

On Wed, Nov 6, 2013 at 4:12 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

Thanks.  I tried using 8.4 instead of HoTT/coq (and also switching to using administrator) and got told that I was passing the wrong arguments to FIND.  Turns out the problem was that `find` was Window's FIND, rather than cygwin's.

-Jason

On Wed, Nov 6, 2013 at 1:34 AM, CJ Bell <siegebell AT gmail.com> wrote:

I seem to be able to compile coq just fine with windows 8.1, Cygwin
32bit (setup version 2.830), and coq 8.4pl2. One difference between us
is that my ocaml compiler was installed by Cygwin -- if your ocaml
compiler was compiled for windows, perhaps it expects DOS format
pathnames while configure is giving it posix pathnames.

To get it to work, I only had to fix line 338 of configure (because
checking for version 3.81 or greater of 'make' was rejecting version
4.00). Here is what I changed it to:

if [ "$MAKEVERSIONMAJOR" -ge 4 -o \( "$MAKEVERSIONMAJOR" -eq 3 -a
"$MAKEVERSIONMINOR" -ge 81 \) ]; then



Hope this helps,
-cj


And here are my results:

$ ./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

  Coq top directory                 : C:/Users/cj/Downloads/coq-8.4pl2

  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 : C:/cygwin/bin
  Objective-Caml library in         : /usr/lib/ocaml

  Camlp4 library in                 : +camlp4
  Native dynamic link support       : true
  Documentation                     : None
  CoqIde                            : no
  Web browser                       : start %s
  Coq web site                      : http://coq.inria.fr/

  Paths for true installation:
    binaries      will be copied in C:/Users/cj/Downloads/coq-8.4pl2/bin
    library       will be copied in C:/Users/cj/Downloads/coq-8.4pl2
    config files  will be copied in C:/Users/cj/Downloads/coq-8.4pl2/ide
    data files    will be copied in C:/Users/cj/Downloads/coq-8.4pl2/ide
    man pages     will be copied in C:/Users/cj/Downloads/coq-8.4pl2/man
    documentation will be copied in C:/Users/cj/Downloads/coq-8.4pl2/doc
    emacs mode    will be copied in C:/Users/cj/Downloads/coq-8.4pl2/tools/emacs

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 archclean' before './configure'.

On Tue, Nov 5, 2013 at 9:47 PM, Jason Gross <jasongross9 AT gmail.com> wrote:
> 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