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 · 2015-09-05 00:20:08 +00:00 · 3c4bfcc3d7
commit 3c4bfcc3d7
parent 06e407b972
7 changed files with 143 additions and 0 deletions
--- a/lang/compcert/Makefile
+++ b/lang/compcert/Makefile
@ -0,0 +1,42 @@
+# $OpenBSD: Makefile,v 1.1.1.1 2015/09/05 00:20:08 daniel Exp $
+
+ONLY_FOR_ARCHS =	i386
+
+COMMENT =		high assurance C compiler
+
+V=			2.5
+GH_ACCOUNT =		AbsInt
+GH_PROJECT =		CompCert
+GH_TAGNAME =		v${V}
+DISTNAME =              ${GH_PROJECT}-${V}
+PKGNAME =		${DISTNAME:L}
+
+HOMEPAGE =		http://compcert.inria.fr/
+
+CATEGORIES =		lang
+
+MAINTAINER = Daniel Dickman <daniel@openbsd.org>
+
+# INRIA Non-Commercial License Agreement.
+PERMIT_PACKAGE_CDROM =	no commercial use
+PERMIT_PACKAGE_FTP =	Yes
+
+WANTLIB	+= c m
+
+USE_GMAKE	= Yes
+
+CONFIGURE_STYLE = simple
+CONFIGURE_ARGS  = -prefix ${WRKINST}${PREFIX} \
+		  -no-standard-headers \
+		  ${MACHINE_ARCH:S/i386/ia32/}-bsd
+
+BUILD_DEPENDS =	lang/ocaml \
+		math/coq \
+		devel/ocaml-menhir
+
+post-install:
+	${INSTALL_DATA} ${WRKSRC}/LICENSE ${PREFIX}/share/compcert
+	sed -i -e "s,^stdlib_path=.*,stdlib_path=${TRUEPREFIX}/lib/compcert," \
+		${PREFIX}/share/compcert/compcert.ini
+
+.include <bsd.port.mk>
--- a/lang/compcert/distinfo
+++ b/lang/compcert/distinfo
@ -0,0 +1,2 @@
+SHA256 (CompCert-2.5.tar.gz) = NoR7APpUNqyOBSSJtyit7yvGgGT+ItvcGL8iJWhW/ZU=
+SIZE (CompCert-2.5.tar.gz) = 2340145
--- a/lang/compcert/patches/patch-Makefile
+++ b/lang/compcert/patches/patch-Makefile
@ -0,0 +1,26 @@
+$OpenBSD: patch-Makefile,v 1.1.1.1 2015/09/05 00:20:08 daniel Exp $
+
+Convenience test target
+
+--- Makefile.orig	Tue Sep  1 01:54:46 2015
+++ Makefile	Tue Sep  1 01:59:48 2015
+@@ -158,7 +158,7 @@ runtime:
+ 
+ FORCE:
+ 
+-.PHONY: proof extraction runtime FORCE
+.PHONY: proof extraction runtime test FORCE
+ 
+ documentation: doc/coq2html $(FILES)
+ 	mkdir -p doc/html
+@@ -228,6 +228,10 @@ ifeq ($(CCHECKLINK),true)
+ 	install -m 0755 ./cchecklink $(BINDIR)
+ endif
+ 	$(MAKE) -C runtime install
+
+test:
+	$(MAKE) -C test
+	$(MAKE) -C test test
+ 
+ clean:
+ 	rm -f $(patsubst %, %/*.vo, $(DIRS))
--- a/lang/compcert/patches/patch-configure
+++ b/lang/compcert/patches/patch-configure
@ -0,0 +1,15 @@
+$OpenBSD: patch-configure,v 1.1.1.1 2015/09/05 00:20:08 daniel Exp $
+
+compcert.ini should go in share/compcert not share.
+
+--- configure.orig	Tue Sep  1 02:15:46 2015
+++ configure	Tue Sep  1 02:16:53 2015
+@@ -335,7 +335,7 @@ fi
+ 
+ # Generate Makefile.config
+ 
+-sharedir="$(dirname "$bindir")"/share
+sharedir="$(dirname "$bindir")"/share/compcert
+ 
+ rm -f Makefile.config
+ cat > Makefile.config <<EOF
--- a/lang/compcert/patches/patch-driver_Configuration_ml
+++ b/lang/compcert/patches/patch-driver_Configuration_ml
@ -0,0 +1,37 @@
+$OpenBSD: patch-driver_Configuration_ml,v 1.1.1.1 2015/09/05 00:20:08 daniel Exp $
+
+compcert.ini should go in share/compcert not share.
+(Backport of commit c879cd)
+
+--- driver/Configuration.ml.orig	Fri Jun 12 04:10:12 2015
+++ driver/Configuration.ml	Wed Aug 26 23:51:04 2015
+@@ -20,17 +20,20 @@ let ini_file_name =
+     Sys.getenv "COMPCERT_CONFIG"
+   with Not_found ->
+     let exe_dir = Filename.dirname Sys.executable_name in
+-    let exe_ini = Filename.concat exe_dir "compcert.ini" in
+     let share_dir =
+       Filename.concat (Filename.concat exe_dir Filename.parent_dir_name)
+-                      "share" in
+-    let share_ini = Filename.concat share_dir "compcert.ini" in
+-    if Sys.file_exists exe_ini then exe_ini
+-    else if Sys.file_exists share_ini then share_ini
+-    else begin 
+-      eprintf "Cannot find compcert.ini configuration file.\n";
+-      exit 2
+-    end
+        "share" in
+    let share_compcert_dir =
+      Filename.concat share_dir "compcert" in
+    let search_path = [exe_dir;share_dir;share_compcert_dir] in
+    let files = List.map (fun s -> Filename.concat s "compcert.ini") search_path in
+    try
+      List.find  Sys.file_exists files
+    with Not_found ->
+      begin 
+        eprintf "Cannot find compcert.ini configuration file.\n";
+        exit 2
+      end
+ 
+ (* Read in the .ini file *)
+ 
--- a/lang/compcert/pkg/DESCR
+++ b/lang/compcert/pkg/DESCR
@ -0,0 +1,14 @@
+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.
+A commercial version of CompCert, without this restriction and with
+professional support, can be purchased from AbsInt. See the file
+LICENSE for more information.
--- a/lang/compcert/pkg/PLIST
+++ b/lang/compcert/pkg/PLIST
@ -0,0 +1,7 @@
+@comment $OpenBSD: PLIST,v 1.1.1.1 2015/09/05 00:20:08 daniel Exp $
+@bin bin/ccomp
+lib/compcert/
+lib/compcert/libcompcert.a
+share/compcert/
+share/compcert/LICENSE
+share/compcert/compcert.ini