head	1.5;
access;
symbols;
locks; strict;
comment	@# @;


1.5
date	2026.07.25.18.58.36;	author alnsn;	state Exp;
branches;
next	1.4;
commitid	ANoo1rAJXNbif4PG;

1.4
date	2026.07.03.22.03.50;	author alnsn;	state Exp;
branches;
next	1.3;
commitid	uhy8aJBs1lwGYfMG;

1.3
date	2026.07.03.20.36.34;	author alnsn;	state Exp;
branches;
next	1.2;
commitid	UCcOTNnplQZJufMG;

1.2
date	2026.07.02.23.52.13;	author alnsn;	state Exp;
branches;
next	1.1;
commitid	vfywKXYOh215y8MG;

1.1
date	2026.07.02.23.20.47;	author alnsn;	state Exp;
branches;
next	;
commitid	LgXNqbK6t0xIq8MG;


desc
@@


1.5
log
@math/cadical is build-only dep, bump pkgrev.
@
text
@# $NetBSD: Makefile,v 1.4 2026/07/03 22:03:50 alnsn Exp $

DISTNAME=	cvc5-1.3.4
PKGREVISION=	1
CATEGORIES=	math
MASTER_SITES=	${MASTER_SITE_GITHUB:=cvc5/}
GITHUB_TAG=	cvc5-${PKGVERSION_NOREV}

MAINTAINER=	pkgsrc-users@@NetBSD.org
HOMEPAGE=	https://cvc5.github.io/
COMMENT=	Automatic theorem prover for SMT (Satisfiability Modulo Theories)
LICENSE=	modified-bsd

USE_TOOLS+=	git
USE_LANGUAGES=	c c++

CMAKE_CONFIGURE_ARGS+=	-DCMAKE_BUILD_TYPE=Production
CMAKE_CONFIGURE_ARGS+=	-DCMAKE_PREFIX_PATH=${PREFIX}
CMAKE_CONFIGURE_ARGS+=	-DBUILD_SHARED_LIBS=ON
CMAKE_CONFIGURE_ARGS+=	-DUSE_PYTHON_VENV=OFF
CMAKE_CONFIGURE_ARGS+=	-DUSE_POLY=ON

DEPENDS+=	${PYPKGPREFIX}-pyparsing>=3.0.9:../../devel/py-pyparsing

BUILDLINK_DEPMETHOD.cadical=	build

TEST_TARGET=	check
CVC5_BUILD_SRC=	${WRKSRC}/${CMAKE_BUILD_DIR}/src
TEST_ENV+=	LD_LIBRARY_PATH=${CVC5_BUILD_SRC}:${CVC5_BUILD_SRC}/parser:${CVC5_BUILD_SRC}/main

.include "../../devel/cmake/build.mk"
.include "../../lang/python/tool.mk"
.include "../../devel/gmp/buildlink3.mk"
.include "../../math/cadical/buildlink3.mk"
.include "../../math/libpoly/buildlink3.mk"
.include "../../math/symfpu/buildlink3.mk"
.include "../../mk/bsd.pkg.mk"
@


1.4
log
@TEST_TARGET=check is better.
@
text
@d1 1
a1 1
# $NetBSD: Makefile,v 1.3 2026/07/03 20:36:34 alnsn Exp $
d4 1
d25 2
@


1.3
log
@Pass LD_LIBRARY_PATH to TEST_ENV.
@
text
@d1 1
a1 1
# $NetBSD: Makefile,v 1.2 2026/07/02 23:52:13 alnsn Exp $
d24 1
a24 1
TEST_TARGET=	test
@


1.2
log
@Add LD_LIBRARY_PATH to testing instruction.

This improves success rate to 99%.

$ export LD_LIBRARY_PATH=$(pwd)/src:$(pwd)/src/parser:$(pwd)/src/main
$ ctest -j32
...
99% tests passed, 1 tests failed out of 4291

Label Time Summary:
api capi      =   0.18 sec*proc (7 tests)
api cppapi    =   4.69 sec*proc (70 tests)
regress0      = 815.38 sec*proc (2540 tests)
regress1      = 709.94 sec*proc (1468 tests)
regress2      = 211.87 sec*proc (145 tests)
regress3      = 1082.17 sec*proc (51 tests)
regress4      = 663.37 sec*proc (10 tests)

Total Test time (real) = 347.30 sec

The following tests did not run:
        ... 52 skipped regress0 tests ...

The following tests FAILED:
	4157 - regress3/bags/reduce_constants_dup.smt2 (Failed)  regress3
@
text
@d1 1
a1 1
# $NetBSD: Makefile,v 1.1 2026/07/02 23:20:47 alnsn Exp $
d24 3
a26 8
# Tests take a long time to finish, you can instead
# run them inside a sandboxed shell and pass -j N:
# make build-env
# cd cmake-pkgsrc-build
# export LD_LIBRARY_PATH=$(pwd)/src:$(pwd)/src/parser:$(pwd)/src/main
# ctest -j 32
# ^D
#TEST_TARGET=	test
@


1.1
log
@Initial import of math/cvc5 version 1.3.4.

An efficient open-source automatic theorem prover for Satisfiability
Modulo Theories (SMT) problems. It can be used to prove the
satisfiability (or, dually, the validity) of first-order formulas
with respect to (combinations of) a variety of useful background
theories.
@
text
@d1 1
a1 1
# $NetBSD$
a25 1
# make install
d27 3
a29 1
# cd cmake-pkgsrc-build && ctest -j 32
@