David MENTRE <[email protected]> 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 -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected] Archive: http://lists.debian.org/[email protected]
