Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Building coq on Windows under cygwin

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Building coq on Windows under cygwin


Chronological Thread 
  • From: Maxime Dénès <mail AT maximedenes.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Building coq on Windows under cygwin
  • Date: Mon, 11 Nov 2013 23:27:18 -0500
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






Archive powered by MHonArc 2.6.18.

Top of Page