The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I believe the problem is that ocaml complains

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.

and fails to create the native code files.  If I run make -k instead of make, subsequent files get that error, as well as warnings about missing cmxs files.  If this doesn't make sense to you (or if you want me to check this again), I can go get a fresh copy and run ./configure again and let you know whether or not I see any cmxs files.  Do you want me to check?

-Jason

On Mon, Nov 11, 2013 at 11:27 PM, Maxime Dénès <mail AT maximedenes.fr> wrote:

Hi Jason,

I saw in your report on the bugtracker that you get some warnings from the dynlinker, like:

"Dynlink error, cannot find file D:\coq\theories\Init\NCoq_Init_Datatypes.cmxs in search path"

Do the corresponding .cmxs files exist on your file system or not? They should have been produced at the same time as the .vo files.

Maxime.

On 11/11/2013 11:19 PM, Jason Gross wrote:

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 <mailto: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

    <mailto: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

        <mailto: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 <mailto: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

            <http://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

            <http://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

            <http://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

            <http://MYOCAMLBUILD_CONFIG.ML>' doesn't match the target
            > pat
            > tern
            > OCAMLDEP  lib/loc.ml <http://loc.ml>
            > OCAMLOPT  lib/loc.ml <http://loc.ml>
            > File "lib/loc.ml <http://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