diff options
author | Xuanrui Qi | 2019-04-27 01:17:25 -0400 |
---|---|---|
committer | Xuanrui Qi | 2019-04-27 01:17:25 -0400 |
commit | 9cd5b4a53a2b371f1b103f4b4edb321fa60067cb (patch) | |
tree | 227b0a0f9452b238802f85011a2693e3e96660cc | |
download | aur-9cd5b4a53a2b371f1b103f4b4edb321fa60067cb.tar.gz |
Initial commit
-rw-r--r-- | .SRCINFO | 25 | ||||
-rw-r--r-- | Makefile-runtime.patch | 23 | ||||
-rw-r--r-- | Makefile.patch | 37 | ||||
-rw-r--r-- | PKGBUILD | 56 |
4 files changed, 141 insertions, 0 deletions
diff --git a/.SRCINFO b/.SRCINFO new file mode 100644 index 000000000000..835257928d89 --- /dev/null +++ b/.SRCINFO @@ -0,0 +1,25 @@ +pkgbase = compcert-git + pkgdesc = The formally verified C compiler + pkgver = 3.5.r25.g8df51b98 + pkgrel = 1 + url = http://compcert.inria.fr + arch = x86_64 + license = custom:INRIA Non-Commercial License Agreement + makedepends = coq>=8.6.1 + makedepends = ocaml>=4.0.2 + makedepends = ocaml-menhir>=20161201 + makedepends = ocaml-menhir<=20181113 + makedepends = ocaml-findlib + makedepends = git + depends = gcc + provides = compcert=3.5.r25.g8df51b98 + conflicts = compcert + source = git+https://github.com/AbsInt/CompCert.git + source = Makefile.patch + source = Makefile-runtime.patch + sha1sums = SKIP + sha1sums = 12abd465a238501777573391c551deb1637a9384 + sha1sums = 810e5efc65179168764221d4d7fd83b8340f61bb + +pkgname = compcert-git + diff --git a/Makefile-runtime.patch b/Makefile-runtime.patch new file mode 100644 index 000000000000..77aa1f4d0bbd --- /dev/null +++ b/Makefile-runtime.patch @@ -0,0 +1,23 @@ +--- runtime/Makefile 2019-04-27 00:16:12.285242632 -0400 ++++ runtime/Makefile.fixed 2019-04-27 00:17:03.020157520 -0400 +@@ -70,16 +70,16 @@ + + ifeq ($(strip $(HAS_RUNTIME_LIB)),true) + install:: +- install -d $(LIBDIR) +- install -m 0644 $(LIB) $(LIBDIR) ++ install -d $(DESTDIR)/$(LIBDIR) ++ install -m 0644 $(LIB) $(DESTDIR)/$(LIBDIR) + else + install:: + endif + + ifeq ($(strip $(HAS_STANDARD_HEADERS)),true) + install:: +- install -d $(LIBDIR)/include +- install -m 0644 $(INCLUDES) $(LIBDIR)/include ++ install -d $(DESTDIR)/$(LIBDIR)/include ++ install -m 0644 $(INCLUDES) $(DESTDIR)/$(LIBDIR)/include + else + install:: + endif diff --git a/Makefile.patch b/Makefile.patch new file mode 100644 index 000000000000..0a61b414c764 --- /dev/null +++ b/Makefile.patch @@ -0,0 +1,37 @@ +--- Makefile 2019-03-28 19:51:22.546637034 -0400 ++++ Makefile.fixed 2019-04-27 00:14:54.922847839 -0400 +@@ -238,23 +238,23 @@ + @$(COQDEP) $^ > .depend + + install: +- install -d $(BINDIR) +- install -m 0755 ./ccomp $(BINDIR) +- install -d $(SHAREDIR) +- install -m 0644 ./compcert.ini $(SHAREDIR) +- install -d $(MANDIR)/man1 +- install -m 0644 ./doc/ccomp.1 $(MANDIR)/man1 ++ install -d $(DESTDIR)/$(BINDIR) ++ install -m 0755 ./ccomp $(DESTDIR)/$(BINDIR) ++ install -d $(DESTDIR)/$(SHAREDIR) ++ install -m 0644 ./compcert.ini $(DESTDIR)/$(SHAREDIR) ++ install -d $(DESTDIR)/$(MANDIR)/man1 ++ install -m 0644 ./doc/ccomp.1 $(DESTDIR)/$(MANDIR)/man1 + $(MAKE) -C runtime install + ifeq ($(CLIGHTGEN),true) +- install -m 0755 ./clightgen $(BINDIR) ++ install -m 0755 ./clightgen $(DESTDIR)/$(BINDIR) + endif + ifeq ($(INSTALL_COQDEV),true) +- install -d $(COQDEVDIR) ++ install -d $(DESTDIR)/$(COQDEVDIR) + for d in $(DIRS); do \ +- install -d $(COQDEVDIR)/$$d && \ +- install -m 0644 $$d/*.vo $(COQDEVDIR)/$$d/; \ ++ install -d $(DESTDIR)/$(COQDEVDIR)/$$d && \ ++ install -m 0644 $$d/*.vo $(DESTDIR)/$(COQDEVDIR)/$$d/; \ + done +- install -m 0644 ./VERSION $(COQDEVDIR) ++ install -m 0644 ./VERSION $(DESTDIR)/$(COQDEVDIR) + @(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(COQDEVDIR)/README + endif + diff --git a/PKGBUILD b/PKGBUILD new file mode 100644 index 000000000000..702362d5077a --- /dev/null +++ b/PKGBUILD @@ -0,0 +1,56 @@ +# Maintainer: Xuanrui Qi <me@xuanruiqi.com> +pkgname=compcert-git +_basepkgname=${pkgname%-*} +_dirname=CompCert +pkgver=3.5.r25.g8df51b98 +pkgrel=1 +pkgdesc="The formally verified C compiler" +arch=('x86_64') +url="http://compcert.inria.fr" +license=('custom:INRIA Non-Commercial License Agreement') +depends=('gcc') +makedepends=('coq>=8.6.1' 'ocaml>=4.0.2' + 'ocaml-menhir>=20161201' 'ocaml-menhir<=20181113' + 'ocaml-findlib' # See: https://github.com/AbsInt/CompCert/issues/281 + 'git') +provides=($_basepkgname=$pkgver) +conflicts=($_basepkgname) +source=("git+https://github.com/AbsInt/CompCert.git" + "Makefile.patch" + "Makefile-runtime.patch") +sha1sums=('SKIP' + '12abd465a238501777573391c551deb1637a9384' + '810e5efc65179168764221d4d7fd83b8340f61bb') + +pkgver() { + cd $srcdir/$_dirname + git describe --long --tags | sed 's/^v//;s/\([^-]*-g\)/r\1/;s/-/./g' +} + +prepare() { + cd $srcdir/$_dirname + + # Fix missing $DESTDIR references in Makefile + # Until upstream fixes this, we're forced to use this patch + patch -Np0 -i ../Makefile.patch + patch -Np0 -i ../Makefile-runtime.patch +} + +build() { + cd $srcdir/$_dirname + + # Some useful options: + # -clightgen: builds and installs the clightgen tool + # -install-coqdev: also installs the Coq development, implied by -clightgen, useful + # if you will use tools such as Princeton VST) + ./configure -prefix /usr $CARCH-linux + + make all +} + +package() { + cd $srcdir/$_dirname + make DESTDIR=$pkgdir install + + install -Dm644 LICENSE $pkgdir/usr/share/licenses/$pkgname/LICENSE +} |