Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Release candidate of Coq 8.4

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Release candidate of Coq 8.4


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: Karn Kallio <tierpluspluslists AT gmail.com>, coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Release candidate of Coq 8.4
  • Date: Thu, 9 Aug 2012 02:59:51 -0400

I have the same problems with building the RC version of Coq on windows that I do with the current trunk version.  With camlp4, I get

COQMKTOP -o bin/coqtop.opt.exe
The system cannot find the path specified.

and with camlp5, I get

OCAMLOPT -o bin/coqmktop.opt.exe
** Fatal error: Cannot find file "D:\\OCaml\\lib\\camlp5\\gramlib.a"
File "caml_startup", line 1:
Error: Error during linking

My build logs are available at
https://dl.dropbox.com/u/11313181/Temp/coq-build-logs/make-world-camlp5.log (make clean && ./configure -usecamlp5 && make world)
https://dl.dropbox.com/u/11313181/Temp/coq-build-logs/make-world-k-camlp5.log (make clean && ./configure -usecamlp5 && make world -k)
https://dl.dropbox.com/u/11313181/Temp/coq-build-logs/make-world-k-2-camlp5.log (((make clean && ./configure -usecamlp5 && make world -k) &> /dev/null) && make world -k)

https://dl.dropbox.com/u/11313181/Temp/coq-build-logs/make-world-camlp4.log (make clean && ./configure -usecamlp4 && make world)
https://dl.dropbox.com/u/11313181/Temp/coq-build-logs/make-world-k-camlp4.log (make clean && ./configure -usecamlp4 && make world -k)
https://dl.dropbox.com/u/11313181/Temp/coq-build-logs/make-world-k-2-camlp4.log (((make clean && ./configure -usecamlp4 && make world -k) &> /dev/null) && make world -k)

-Jason

On Wed, Aug 8, 2012 at 3:49 PM, Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:
Indeed. Thanks.

Hugo

On Wed, Aug 08, 2012 at 03:15:36PM -0430, Karn Kallio wrote:
>
> I think it is this:
>
> http://coq.inria.fr/coq-84
>
> > http://coq.inria.fr/coq-8.4
> > Page not found
> >
> > 08.08.2012, 22:33, "Hugo Herbelin" <Hugo.Herbelin AT inria.fr>:
> > > Dear all,
> > >
> > > We plan to release version 8.4 of Coq for the Coq workshop, next
> > > Sunday. In the meantime, we have prepared a release candidate for
> > > testing purpose. Please tell us if you have any problem to
> > > compile/install Coq 8.4 from its source package.
> > >
> > > The source package is downloadable from "http://coq.inria.fr/coq-8.4".
> > >
> > > The Coq development team




Archive powered by MHonArc 2.6.18.

Top of Page