coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Compile failure on Mac OS X

From: Edsko de Vries <edskodevries AT gmail.com>
To: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
Cc: coq-club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Compile failure on Mac OS X
Date: Thu, 9 Jul 2009 15:22:01 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Well, it's not part of the Coq distribution, but it seems to be generated during compilation. I believe the relevant part of Makefile.build is

parsing/grammar.cma: $(GRAMMARCMO)
        $(SHOW)'Testing $@'
        @touch test.ml4
$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $ (CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
        @rm -f test-grammar test.*
        $(SHOW)'OCAMLC -a $@'
        $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@

Edsko

On 9 Jul 2009, at 15:10, Yves Bertot wrote:

I don't understand why you say you have a trouble compiling coq. test.ml4 is not a source file of the coq distribution. Is it?

Yves

[Coq-Club] Compile failure on Mac OS X, Edsko de Vries
- Re: [Coq-Club] Compile failure on Mac OS X, Yves Bertot
  - Re: [Coq-Club] Compile failure on Mac OS X, Edsko de Vries
- Re: [Coq-Club] Compile failure on Mac OS X, Arnaud Spiwack
  - Re: [Coq-Club] Compile failure on Mac OS X, Edsko de Vries
- Message not available
  - Message not available
    - Message not available
      - Message not available
        
        Message not available
        
        Re: [Coq-Club] Compile failure on Mac OS X, Edsko de Vries