cpet/openbsd-ports
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
openbsd-ports/lang/compcert/Makefile

48 lines
1023 B
Makefile
Raw Normal View History

Update to commit 0132b8aa for improved builtin support.
2020-07-28 08:35:31 +00:00
# $OpenBSD: Makefile,v 1.23 2020/07/28 08:35:31 daniel Exp $
Update to CompCert 3.3 as requested by danj@ but mark BROKEN until we get coq updated. Biggest improvement in this update is support for amd64. CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.
2018-09-12 04:58:49 +00:00
Update to commit 9af28924 so bytecode-only platforms can be supported.
2020-07-07 23:03:10 +00:00
ONLY_FOR_ARCHS = aarch64 amd64 i386 powerpc
import lang/compcert. ok sthen@ The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM and x86 processors. The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code. CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.
2015-09-05 00:20:08 +00:00
COMMENT = high assurance C compiler
Update to commit 0132b8aa for improved builtin support.
2020-07-28 08:35:31 +00:00
V = 3.7.20200727
import lang/compcert. ok sthen@ The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM and x86 processors. The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code. CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.
2015-09-05 00:20:08 +00:00
GH_ACCOUNT = AbsInt
GH_PROJECT = CompCert
Update to commit 08491de0 for coq 8.11.1 support.
2020-06-02 12:58:22 +00:00
#GH_TAGNAME = v${V}
Update to commit 0132b8aa for improved builtin support.
2020-07-28 08:35:31 +00:00
GH_COMMIT = 0132b8aa669adc10e6ca953d10d5c0b861f304b1
Update to commit d3eba507 for ocaml 4.08.1 support.
2019-09-07 17:24:37 +00:00
DISTNAME = ${GH_PROJECT}-${V}
import lang/compcert. ok sthen@ The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM and x86 processors. The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code. CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.
2015-09-05 00:20:08 +00:00
PKGNAME = ${DISTNAME:L}
HOMEPAGE = http://compcert.inria.fr/
CATEGORIES = lang
# INRIA Non-Commercial License Agreement.
Switch to PERMIT_PACKAGE. CDROM restrictions are no longer applicable.
2019-07-14 00:39:34 +00:00
PERMIT_PACKAGE = Yes
import lang/compcert. ok sthen@ The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM and x86 processors. The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code. CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.
2015-09-05 00:20:08 +00:00
WANTLIB += c m
Drop dependency on base gcc and switch to ports gcc instead.
2019-04-20 22:12:41 +00:00
COMPILER = ports-gcc
import lang/compcert. ok sthen@ The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM and x86 processors. The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code. CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.
2015-09-05 00:20:08 +00:00
USE_GMAKE = Yes
CONFIGURE_STYLE = simple
Update to latest git commit to add support for ocaml 4.08 and coq 8.10. This should allow chrisz@ to move forward with updates of those ports.
2019-08-18 01:15:12 +00:00
CONFIGURE_ARGS = -no-standard-headers \
Update to CompCert 3.3 as requested by danj@ but mark BROKEN until we get coq updated. Biggest improvement in this update is support for amd64. CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.
2018-09-12 04:58:49 +00:00
${MACHINE_ARCH}-bsd
import lang/compcert. ok sthen@ The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM and x86 processors. The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code. CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.
2015-09-05 00:20:08 +00:00
Update to commit 9b881b79 for coq 8.11.0 and ocaml 4.10 support.
2020-02-16 04:34:23 +00:00
BUILD_DEPENDS = lang/ocaml>=4.05 \
math/coq>=8.8.0 \
Update to commit 9af28924 so bytecode-only platforms can be supported.
2020-07-07 23:03:10 +00:00
sysutils/findlib \
Update to latest git commit to add support for ocaml 4.08 and coq 8.10. This should allow chrisz@ to move forward with updates of those ports.
2019-08-18 01:15:12 +00:00
devel/ocaml-menhir>=20190626
import lang/compcert. ok sthen@ The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM and x86 processors. The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code. CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.
2015-09-05 00:20:08 +00:00
Drop dependency on base gcc and switch to ports gcc instead.
2019-04-20 22:12:41 +00:00
RUN_DEPENDS = lang/gcc/${MODGCC4_VERSION}
post-extract:
sed -i -e 's/gcc/egcc/g' ${WRKSRC}/configure
import lang/compcert. ok sthen@ The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM and x86 processors. The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code. CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.
2015-09-05 00:20:08 +00:00
post-install:
${INSTALL_DATA} ${WRKSRC}/LICENSE ${PREFIX}/share/compcert
Update to CompCert 3.3 as requested by danj@ but mark BROKEN until we get coq updated. Biggest improvement in this update is support for amd64. CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.
2018-09-12 04:58:49 +00:00
sed -i -e "s,^stdlib_path=.*,stdlib_path=${TRUEPREFIX}/lib," \
import lang/compcert. ok sthen@ The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM and x86 processors. The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code. CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.
2015-09-05 00:20:08 +00:00
${PREFIX}/share/compcert/compcert.ini
.include <bsd.port.mk>
Reference in New Issue Copy Permalink