The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I'm using a clone of coq from github, and the most recent commit I have is

commit abe2f0cd9e529fb25c85cb9c93c8c4c09e28ee02

Author: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>

Date:   Tue Aug 7 22:49:04 2012 +0000

    Typo in r15654

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15700 85f007b7-540e-

I get

OCAMLC    tactics/eqdecide.ml

OCAMLOPT  tactics/eqdecide.ml

OCAMLOPT -a -o tactics/hightactics.cmxa

COQMKTOP -o bin/coqtop.opt.exe

The system cannot find the path specified.

Makefile.build:205: recipe for target `bin/coqtop.opt.exe' failed

make[1]: *** [bin/coqtop.opt.exe] Error 1

make[1]: Leaving directory `/cygdrive/d/Documents/Dropbox/MIT/2012 Summer/Catego

rical Informatics UROP/coq'

Makefile:139: recipe for target `world' failed

make: *** [world] Error 2

Thanks for the help with ocaml native-code; it worked.

-Jason

On Tue, Aug 7, 2012 at 2:26 PM, Pierre Letouzey <pierre.letouzey AT inria.fr> wrote:

----- Mail original -----

> After commenting out the -mno-cygwin flag, I get
>
> OCAMLC    kernel/byterun/coq_interp.c
> cd kernel/byterun/ && \
> "ocamlmklib" -oc coqrun coq_fix_code.o coq_memory.o coq_values.o
> coq_interp.o
> "ranlib" kernel/byterun/libcoqrun.a
> COQMKTOP -o bin/coqtop.byte.exe
> The system cannot find the path specified.

Which version of Coq are you using ? A few of my recent commits (e.g. 15687)
might help concerning this kind of path-related issues. Could you please
try with today's svn version (either trunk or v8.4 branch) ?

> Tangentially, I'm still trying to get native code compilation working with
> ocaml.  Do you know the right invocation of make && make install for camlp5
> to get it to install the .cmxa files (which seem to be what Coq's configure
> looks for)?
>

Normally, it's make world.opt && make install. But I haven't tried it myself
on windows. Alternatively, you can now use camlp4 (the one coming along with
ocaml) instead of camlp5, it should work as well. Simply add the -usecamlp4
option to coq's configure, or remove your partial camlp5 installation and
let coq's configure pick the available camlpX (only in recent svn version).

Best regards
Pierre