Re: CVS commit: pkgsrc/math/cvc5

Alexander Nasonov <[email protected]> writes:

> Greg Troxel wrote:
>> "Alexander Nasonov" <[email protected]> writes:
>> 
>> Probably we should arrange for MAKE_JOBS to be passed to cmake tests,
>> instead of not having tests hooked in and suggesting it be done
>> manually.

We have resolved that -j is passed properly.

>> I think having tests run with "make tests", even slowly, is preferable
>> to tests that have to be run by hand.
>
> I commented it out because all tests fail unless you install the
> package. Even if you do, about a hundred will still fail because
> they depend on a private .so.

That's a bug in the upstream package then.  Tests should work without
being installed.

Perhaps you could add TEST_ENV to set LD_LIBRARY_PATH, with a comment
linking to an upstream bug report, and similarly a comment in the
Makefile about test failing if not installed.

I realize that people that want to run tests will have to things they
shouldn't have to do, but installing the package and running make test
is vastly preferable to installing the  package and running tests by
hand.  The whole point of make test is to have the "how to run tests"
encapsulated in the makefile instead of humans having to do it by hand!