Re: Bug#663754: ITP: hol-light -- HOL Light theorem prover
Le 22/03/2012 15:45, David MENTRE a écrit :
> As far as I have understood, those tests are testing internal HOL
> logic. If you haven't modified any line of the original code, I don't
> see why those tests would fail (under assumption: all the relevant
> modules have correctly been installed). The only things that a
> packaging can change is the interface with the environment of the
> package.
Beware, I've already seen tests failing when they "should not" have. For
example, a bug in the compiler, or some external library can produce
very strange bugs and make some tests unexpectedly fail (whereas others
seemingly testing the same thing succeed). Think about a bug in the
compiler itself, for example.
Cheers,
--
Stéphane
Reply to: