The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

2nd update. Sorry for the noise!

So, forget my previous update.

It works when I run the executable from the downloaded directory
(~/coq-trunk/bin/coqtop.byte), but it does not when I run it from the
installed *exactly the same* executable in /usr/bin/coqtop.byte. I
tried every possible way of saying the latter where to find the files
(nothing, in ~/coq-trunk/, in /usr/lib/coq) and somehow it refuses to
work. With the binary from the downloaded  directory it doesn't matter
what value I export in COQTOP, it always works.

For the moment I will use the binary from the downloaded directory,
but if someone figures out what the heck I'm doing wrong, I will be
very happy.

Thanks for reading, and happy winter break,
Beta


2011/12/28 Beta Ziliani 
<beta AT mpi-sws.org>:
> *UPDATE*
>
> I have a linux desktop and a Macbook. In my Mac I was able to debug
> with no problem using version 8.3pl2. Then, I shifted, both in my mac
> and desktop, to the trunk version of Coq. I never debugged Coq in my
> desktop before, and when I tried I get the mentioned error. Then, I
> tried in my Mac and oh surprise, I get the same result. It works when
> I switch back to 8.3pl2.
>
> At first sight, it seems to be a problem in the trunk version,
> although it's puzzling that no one else acknowledge it.
>
> Best wishes,
> Beta