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

update to CompCert 3.12; from Volker Schlecht

Browse Source
This commit is contained in:
daniel 2023-01-07 13:11:42 +00:00
parent 4c6b7f4f13
commit 28e912feb8
4 changed files with 17 additions and 60 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lang/compcert/Makefile
View File

@ -2,13 +2,12 @@ ONLY_FOR_ARCHS = aarch64 amd64 i386 powerpc
COMMENT = high assurance C compiler
V = 3.10
V = 3.12
GH_ACCOUNT = AbsInt
GH_PROJECT = CompCert
GH_TAGNAME = v${V}
DISTNAME = ${GH_PROJECT}-${V}
PKGNAME = ${DISTNAME:L}
REVISION = 1
HOMEPAGE = https://compcert.org/
@ -26,6 +25,7 @@ USE_GMAKE = Yes
CONFIGURE_STYLE = simple
CONFIGURE_ARGS = -mandir ${PREFIX}/man \
-libdir ${PREFIX}/lib \
-sharedir ${PREFIX}/share/compcert \
-toolprefix e \
-no-standard-headers \
${MACHINE_ARCH}-bsd

4
lang/compcert/distinfo
View File

@ -1,2 +1,2 @@
SHA256 (CompCert-3.10.tar.gz) = ideImkHZ0pXulZ/53nrtGgp8gT93+ppmi+7avq3pGSc=
SIZE (CompCert-3.10.tar.gz) = 2774118
SHA256 (CompCert-3.12.tar.gz) = 69HR8oGZXth0c2sg8Xg2ESD+HfWd2pv0vkMfq4ZM99Q=
SIZE (CompCert-3.12.tar.gz) = 2797848

4
lang/compcert/patches/patch-Makefile
View File

@ -3,7 +3,7 @@ Convenience test target
Index: Makefile
--- Makefile.orig
+++ Makefile
@@ -231,7 +231,7 @@ runtime:
@@ -226,7 +226,7 @@ runtime:
FORCE:
@ -12,7 +12,7 @@ Index: Makefile
documentation: $(FILES)
mkdir -p doc/html
@@ -338,6 +338,10 @@ ifeq ($(INSTALL_COQDEV),true)
@@ -333,6 +333,10 @@ ifeq ($(INSTALL_COQDEV),true)
install -m 0644 ./compcert.config $(DESTDIR)$(COQDEVDIR)
@(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(DESTDIR)$(COQDEVDIR)/README
endif

65
lang/compcert/patches/patch-configure
View File

@ -1,18 +1,9 @@
1) Fixup path locations for OpenBSD
2) Add configuration support for macppc and aarch64 on OpenBSD
Add configuration support for macppc and aarch64 on OpenBSD
Index: configure
--- configure.orig
+++ configure
@@ -20,6 +20,7 @@ prefix='/usr/local'
bindir='$(PREFIX)/bin'
libdir='$(PREFIX)/lib/compcert'
mandir='$(PREFIX)/share/man'
+sharedir='$(PREFIX)/share/compcert'
coqdevdir='$(PREFIX)/lib/compcert/coq'
toolprefix=''
target=''
@@ -41,6 +42,7 @@ Supported targets:
@@ -42,6 +42,7 @@ Supported targets:
ppc-eabi (PowerPC, EABI with GNU/Unix tools)
ppc-eabi-diab (PowerPC, EABI with Diab tools)
ppc-linux (PowerPC, Linux)
@ -20,7 +11,7 @@ Index: configure
arm-eabi (ARM, EABI, little endian)
arm-linux (ARM, EABI, little endian)
arm-eabihf (ARM, EABI using hardware FP registers, little endian)
@@ -59,6 +61,7 @@ Supported targets:
@@ -60,6 +61,7 @@ Supported targets:
rv32-linux (RISC-V 32 bits, Linux)
rv64-linux (RISC-V 64 bits, Linux)
aarch64-linux (AArch64, i.e. ARMv8 in 64-bit mode, Linux)
@ -28,33 +19,16 @@ Index: configure
aarch64-macos (AArch64, i.e. Apple silicon, MacOS)
manual (edit configuration file by hand)
@@ -66,7 +69,7 @@ For x86 targets, the "x86_32-" prefix can also be writ
For x86 targets, the "x86_64-" prefix can also be written "amd64-".
@@ -68,7 +70,7 @@ For x86 targets, the "x86_64-" prefix can also be writ
For AArch64 targets, the "aarch64-" prefix can also be written "arm64-".
For RISC-V targets, the "rv32-" or "rv64-" prefix can also be written "riscv32-" or "riscv64-".
-For PowerPC targets, the "ppc-" prefix can be refined into:
+For PowerPC targets, the "ppc-" prefix can also be written "powerpc-" and can be refined into:
ppc64- PowerPC 64 bits
e5500- Freescale e5500 core (PowerPC 64 bit, EREF extensions)
@@ -88,6 +91,7 @@ Options:
-bindir <dir> Install binaries in <dir>
-libdir <dir> Install libraries in <dir>
-mandir <dir> Install man pages in <dir>
+ -sharedir <dir> Install compcert.ini in <dir>
-coqdevdir <dir> Install Coq development (.vo files) in <dir>
-toolprefix <pref> Prefix names of tools ("gcc", etc) with <pref>
-use-external-Flocq Use an already-installed Flocq library
@@ -119,6 +123,8 @@ while : ; do
libdir="$2"; shift;;
-mandir|--mandir)
mandir="$2"; shift;;
+ -sharedir|--sharedir)
+ sharedir="$2"; shift;;
-coqdevdir|--coqdevdir)
coqdevdir="$2"; install_coqdev=true; shift;;
-toolprefix|--toolprefix)
@@ -225,7 +231,7 @@ clinker_options=""
@@ -230,7 +232,7 @@ clinker_options=""
clinker_needs_no_pie=true
cprepro="${toolprefix}gcc"
cprepro_options="-E"
@ -63,7 +37,7 @@ Index: configure
libmath="-lm"
responsefile="gnu"
@@ -258,7 +264,7 @@ fi
@@ -263,7 +265,7 @@ fi
if test "$arch" = "powerpc"; then
case "$target" in
@ -72,7 +46,7 @@ Index: configure
;;
*)
echo "Error: invalid eabi/system '$target' for architecture PowerPC." 1>&2
@@ -290,6 +296,11 @@ if test "$arch" = "powerpc"; then
@@ -295,6 +297,11 @@ if test "$arch" = "powerpc"; then
system="diab"
responsefile="diab"
;;
@ -83,10 +57,10 @@ Index: configure
+ ;;
*)
casmruntime="${toolprefix}gcc -c -Wa,-mregnames"
cprepro_options="-std=c99 -U__GNUC__ -E"
@@ -410,6 +421,11 @@ if test "$arch" = "aarch64"; then
cprepro_options="-U__GNUC__ -E"
@@ -415,6 +422,11 @@ if test "$arch" = "aarch64"; then
abi="standard"
cprepro_options="-std=c99 -U__GNUC__ -E"
cprepro_options="-U__GNUC__ -E"
system="linux";;
+ bsd)
+ abi="standard"
@ -96,20 +70,3 @@ Index: configure
macos|macosx)
abi="apple"
casm="${toolprefix}cc"
@@ -612,8 +628,6 @@ fi
#
# Generate Makefile.config
#
-sharedir="$(dirname "$bindir")"/share
-
rm -f Makefile.config
cat > Makefile.config <<EOF
PREFIX=$prefix
@@ -832,6 +846,7 @@ CompCert configuration:
Runtime library provided...... $has_runtime_lib
Library files installed in.... $(expandprefix $libdir)
Man pages installed in........ $(expandprefix $mandir)
+ compcert.ini installed in..... $(expandprefix $sharedir)
Standard headers provided..... $has_standard_headers
Standard headers installed in. $(expandprefix $libdir)/include
EOF