Re: Bug#663754: ITP: hol-light -- HOL Light theorem prover

[Hendrik Tews <tews@os.inf.tu-dresden.de>]

David MENTRE <dmentre@linux-france.org> writes:

   As far as I have understood, those tests are testing internal HOL
   logic. 

I would say that each of these tests proves certain example
theorems in HOL Light. So each test compiles the HOL Light
deduction machine and validates a number of proofs with it.

   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.

Apparently, the package and upstream use different camlp5
versions. It could be that some minor camlp5 change, changes a
corner case of the HOL Light syntax extension, which is only used
in one of the examples ... or maybe even in none of the examples.

Bye,

Hendrik