kpriv/freebsd-ports
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
freebsd-ports/math/why3/Makefile

72 lines
1.9 KiB
Makefile
Raw Normal View History

Add two new math ports: why3 and why3-gpl The primary motivation for adding why3 is to support the upcoming SPARK 2014 port. However, SPARK 2014 requires a custom version. In time the customizations should make it upstream, but currently the stock version cannot be used to build SPARK. They are also licensed differently (LGPL2 for stock, GPLv3 for SPARK version). Rather than force people that find why3 useful on their own to accept a custom version, both are offered although they currently conflict. Why3 has optional dependencies on coq, isabelle, and frama-c, and all three have issus: * coq rebuilds its libraries in $LOCALBASE, could be issue with coq * isabella currently has a broken dependency (sjsml) and only for i386 when it's not. Updating to 2013-2 version failed, as did trying to build it with polyml instead of sjsml * frama-c is fine, but the plugin code in why3 is still experimental and upstream recommends that it not be used. ============================================================== Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by- construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted.
2014-06-04 21:22:33 +02:00
# Created by: John Marino <marino@FreeBSD.org>
# $FreeBSD$
PORTNAME= why3
PORTVERSION= 0.83
- Add LICENSE_FILE - Strip object files - Bump PORTREVISION for package change
2015-11-20 10:17:20 +01:00
PORTREVISION= 2
Add two new math ports: why3 and why3-gpl The primary motivation for adding why3 is to support the upcoming SPARK 2014 port. However, SPARK 2014 requires a custom version. In time the customizations should make it upstream, but currently the stock version cannot be used to build SPARK. They are also licensed differently (LGPL2 for stock, GPLv3 for SPARK version). Rather than force people that find why3 useful on their own to accept a custom version, both are offered although they currently conflict. Why3 has optional dependencies on coq, isabelle, and frama-c, and all three have issus: * coq rebuilds its libraries in $LOCALBASE, could be issue with coq * isabella currently has a broken dependency (sjsml) and only for i386 when it's not. Updating to 2013-2 version failed, as did trying to build it with polyml instead of sjsml * frama-c is fine, but the plugin code in why3 is still experimental and upstream recommends that it not be used. ============================================================== Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by- construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted.
2014-06-04 21:22:33 +02:00
CATEGORIES= math
MASTER_SITES= http://gforge.inria.fr/frs/download.php/33490/ \
http://pkgs.fedoraproject.org/repo/pkgs/why3/${FEDORA}/
math/why3: Release port I only care about math/why3-gpl, which has been decoupled from why3 and has already diverged. Before resetting MAINTAINER, I reintegrated the Makefile.common file (only used by this port) into the main Makefile. In the process, some options placeholders were lost but in all probability these options can't be built without serious work on external ports.
2015-06-28 09:11:24 +02:00
MAINTAINER= ports@FreeBSD.org
Add two new math ports: why3 and why3-gpl The primary motivation for adding why3 is to support the upcoming SPARK 2014 port. However, SPARK 2014 requires a custom version. In time the customizations should make it upstream, but currently the stock version cannot be used to build SPARK. They are also licensed differently (LGPL2 for stock, GPLv3 for SPARK version). Rather than force people that find why3 useful on their own to accept a custom version, both are offered although they currently conflict. Why3 has optional dependencies on coq, isabelle, and frama-c, and all three have issus: * coq rebuilds its libraries in $LOCALBASE, could be issue with coq * isabella currently has a broken dependency (sjsml) and only for i386 when it's not. Updating to 2013-2 version failed, as did trying to build it with polyml instead of sjsml * frama-c is fine, but the plugin code in why3 is still experimental and upstream recommends that it not be used. ============================================================== Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by- construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted.
2014-06-04 21:22:33 +02:00
COMMENT= Deductive program verification platform
LICENSE= LGPL21
- Add LICENSE_FILE - Strip object files - Bump PORTREVISION for package change
2015-11-20 10:17:20 +01:00
LICENSE_FILE= ${WRKSRC}/LICENSE
Add two new math ports: why3 and why3-gpl The primary motivation for adding why3 is to support the upcoming SPARK 2014 port. However, SPARK 2014 requires a custom version. In time the customizations should make it upstream, but currently the stock version cannot be used to build SPARK. They are also licensed differently (LGPL2 for stock, GPLv3 for SPARK version). Rather than force people that find why3 useful on their own to accept a custom version, both are offered although they currently conflict. Why3 has optional dependencies on coq, isabelle, and frama-c, and all three have issus: * coq rebuilds its libraries in $LOCALBASE, could be issue with coq * isabella currently has a broken dependency (sjsml) and only for i386 when it's not. Updating to 2013-2 version failed, as did trying to build it with polyml instead of sjsml * frama-c is fine, but the plugin code in why3 is still experimental and upstream recommends that it not be used. ============================================================== Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by- construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted.
2014-06-04 21:22:33 +02:00
- Fix various typos in CONFLICTS_INSTALL knob Approved by: portmgr blanket
2016-02-10 17:14:34 +01:00
CONFLICTS_INSTALL= why3-gpl-*
Add two new math ports: why3 and why3-gpl The primary motivation for adding why3 is to support the upcoming SPARK 2014 port. However, SPARK 2014 requires a custom version. In time the customizations should make it upstream, but currently the stock version cannot be used to build SPARK. They are also licensed differently (LGPL2 for stock, GPLv3 for SPARK version). Rather than force people that find why3 useful on their own to accept a custom version, both are offered although they currently conflict. Why3 has optional dependencies on coq, isabelle, and frama-c, and all three have issus: * coq rebuilds its libraries in $LOCALBASE, could be issue with coq * isabella currently has a broken dependency (sjsml) and only for i386 when it's not. Updating to 2013-2 version failed, as did trying to build it with polyml instead of sjsml * frama-c is fine, but the plugin code in why3 is still experimental and upstream recommends that it not be used. ============================================================== Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by- construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted.
2014-06-04 21:22:33 +02:00
Remove ${PORTSDIR}/ from dependencies, categories m, n, o, and p. With hat: portmgr Sponsored by: Absolight
2016-04-01 16:16:16 +02:00
BUILD_DEPENDS= ocaml-zarith>1.2:math/ocaml-zarith \
lablgtk2:x11-toolkits/ocaml-lablgtk2 \
ocaml-sqlite3>2:databases/ocaml-sqlite3 \
ocaml-ocamlgraph>1.8:math/ocaml-ocamlgraph \
camlp5o:devel/ocaml-camlp5
math/why3: Release port I only care about math/why3-gpl, which has been decoupled from why3 and has already diverged. Before resetting MAINTAINER, I reintegrated the Makefile.common file (only used by this port) into the main Makefile. In the process, some options placeholders were lost but in all probability these options can't be built without serious work on external ports.
2015-06-28 09:11:24 +02:00
GNU_CONFIGURE= yes
INSTALL_TARGET= install-all
USES= gmake
USE_OCAML= yes
Add two new math ports: why3 and why3-gpl The primary motivation for adding why3 is to support the upcoming SPARK 2014 port. However, SPARK 2014 requires a custom version. In time the customizations should make it upstream, but currently the stock version cannot be used to build SPARK. They are also licensed differently (LGPL2 for stock, GPLv3 for SPARK version). Rather than force people that find why3 useful on their own to accept a custom version, both are offered although they currently conflict. Why3 has optional dependencies on coq, isabelle, and frama-c, and all three have issus: * coq rebuilds its libraries in $LOCALBASE, could be issue with coq * isabella currently has a broken dependency (sjsml) and only for i386 when it's not. Updating to 2013-2 version failed, as did trying to build it with polyml instead of sjsml * frama-c is fine, but the plugin code in why3 is still experimental and upstream recommends that it not be used. ============================================================== Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by- construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted.
2014-06-04 21:22:33 +02:00
FEDORA= ${DISTNAME}${EXTRACT_SUFX}/35f99e5f64939e50ea57f641ba2073ec
ALL_TARGET= all byte
math/why3: Release port I only care about math/why3-gpl, which has been decoupled from why3 and has already diverged. Before resetting MAINTAINER, I reintegrated the Makefile.common file (only used by this port) into the main Makefile. In the process, some options placeholders were lost but in all probability these options can't be built without serious work on external ports.
2015-06-28 09:11:24 +02:00
CONFIGURE_ARGS= --enable-relocation \
--disable-doc \
--disable-pvs-libs \
--disable-profiling \
--disable-coq-tactic \
--disable-coq-libs \
--disable-isabelle-libs
OPTIONS_DEFINE= DOCS
# The pdf is pre-built, but the makefile wants to build it again in order
# to generate manual.bbl which is used to build the html documention.
# Regenerating pdf fails, and the dependencies are heavy. Disable this
# all for now and just manually install the pdf. The "doc" target was
# also removed from ALL_TARGET
#
#DOCS_CONFIGURE_ENABLE= doc
Remove ${PORTSDIR}/ from dependencies, categories m, n, o, and p. With hat: portmgr Sponsored by: Absolight
2016-04-01 16:16:16 +02:00
#DOCS_BUILD_DEPENDS= rubber:textproc/rubber \
# hevea:textproc/hevea
math/why3: Release port I only care about math/why3-gpl, which has been decoupled from why3 and has already diverged. Before resetting MAINTAINER, I reintegrated the Makefile.common file (only used by this port) into the main Makefile. In the process, some options placeholders were lost but in all probability these options can't be built without serious work on external ports.
2015-06-28 09:11:24 +02:00
MAKE_JOBS_UNSAFE= yes
post-patch:
@${REINPLACE_CMD} -e 's|/bin/bash|/bin/sh|g' \
${WRKSRC}/src/util/sysutil.ml \
${WRKSRC}/src/jessie/Makefile.in
post-install:
- Strip binaries
2015-07-29 19:49:12 +02:00
${STRIP_CMD} ${STAGEDIR}${PREFIX}/bin/why3* \
- Add LICENSE_FILE - Strip object files - Bump PORTREVISION for package change
2015-11-20 10:17:20 +01:00
${STAGEDIR}${PREFIX}/${OCAML_SITELIBDIR}/why3/*.o \
- Strip binaries
2015-07-29 19:49:12 +02:00
${STAGEDIR}${PREFIX}/lib/why3/plugins/*.cmxs \
${STAGEDIR}${PREFIX}/lib/why3/why3-cpulimit
- Switch to options helpers - While here, add some NO_ARCHes and couple missing PORT_OPTIONS=DOCS Approved by: portmgr blanket
2015-08-28 15:39:56 +02:00
post-install-DOCS-on:
math/why3: Release port I only care about math/why3-gpl, which has been decoupled from why3 and has already diverged. Before resetting MAINTAINER, I reintegrated the Makefile.common file (only used by this port) into the main Makefile. In the process, some options placeholders were lost but in all probability these options can't be built without serious work on external ports.
2015-06-28 09:11:24 +02:00
${MKDIR} ${STAGEDIR}${DOCSDIR}
${INSTALL_DATA} ${WRKSRC}/doc/manual.pdf ${STAGEDIR}${DOCSDIR}
Add two new math ports: why3 and why3-gpl The primary motivation for adding why3 is to support the upcoming SPARK 2014 port. However, SPARK 2014 requires a custom version. In time the customizations should make it upstream, but currently the stock version cannot be used to build SPARK. They are also licensed differently (LGPL2 for stock, GPLv3 for SPARK version). Rather than force people that find why3 useful on their own to accept a custom version, both are offered although they currently conflict. Why3 has optional dependencies on coq, isabelle, and frama-c, and all three have issus: * coq rebuilds its libraries in $LOCALBASE, could be issue with coq * isabella currently has a broken dependency (sjsml) and only for i386 when it's not. Updating to 2013-2 version failed, as did trying to build it with polyml instead of sjsml * frama-c is fine, but the plugin code in why3 is still experimental and upstream recommends that it not be used. ============================================================== Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by- construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted.
2014-06-04 21:22:33 +02:00
.include <bsd.port.mk>
Reference in a new issue Copy permalink