diff options
author | Xuanrui Qi | 2019-09-18 21:58:55 -0700 |
---|---|---|
committer | Xuanrui Qi | 2019-09-18 21:58:55 -0700 |
commit | 02aa64f46b75130da85ee764c0855a76caef427b (patch) | |
tree | f68b64034de785c579b56aa4e6ae6a99e0630015 | |
parent | 738306712c35dc8550f4e55d9215c395f07cb11e (diff) | |
download | aur-02aa64f46b75130da85ee764c0855a76caef427b.tar.gz |
Release 3.6
-rw-r--r-- | .SRCINFO | 19 | ||||
-rw-r--r-- | Makefile-runtime.patch | 23 | ||||
-rw-r--r-- | Makefile.patch | 37 | ||||
-rw-r--r-- | PKGBUILD | 24 |
4 files changed, 15 insertions, 88 deletions
@@ -1,23 +1,18 @@ pkgbase = compcert pkgdesc = The formally verified C compiler - pkgver = 3.5 - pkgrel = 3 + pkgver = 3.6 + pkgrel = 1 url = http://compcert.inria.fr arch = x86_64 license = custom:INRIA Non-Commercial License Agreement - makedepends = coq>=8.6.1 + checkdepends = parallel + makedepends = coq>=8.7.2 makedepends = ocaml>=4.0.2 - makedepends = ocaml-menhir>=20161201 - makedepends = ocaml-menhir<=20181113 + makedepends = ocaml-menhir>=20190626 makedepends = ocaml-findlib - makedepends = parallel depends = gcc - source = http://compcert.inria.fr/release/compcert-3.5.tgz - source = Makefile.patch - source = Makefile-runtime.patch - sha1sums = 375705b2a02062d3af0906cb53d9a08a25382097 - sha1sums = 12abd465a238501777573391c551deb1637a9384 - sha1sums = 810e5efc65179168764221d4d7fd83b8340f61bb + source = http://compcert.inria.fr/release/compcert-3.6.tgz + sha1sums = 2b0da15587fc1676852d241a5cc11c66e094f483 pkgname = compcert diff --git a/Makefile-runtime.patch b/Makefile-runtime.patch deleted file mode 100644 index 77aa1f4d0bbd..000000000000 --- a/Makefile-runtime.patch +++ /dev/null @@ -1,23 +0,0 @@ ---- 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 deleted file mode 100644 index 0a61b414c764..000000000000 --- a/Makefile.patch +++ /dev/null @@ -1,37 +0,0 @@ ---- 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 - @@ -2,31 +2,23 @@ pkgname=compcert _dirname=CompCert -pkgver=3.5 -pkgrel=3 +pkgver=3.6 +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' +makedepends=('coq>=8.7.2' 'ocaml>=4.0.2' + 'ocaml-menhir>=20190626' 'ocaml-findlib' # See: https://github.com/AbsInt/CompCert/issues/281 - 'parallel') -source=("http://compcert.inria.fr/release/$pkgname-$pkgver.tgz" - "Makefile.patch" - "Makefile-runtime.patch") -sha1sums=('375705b2a02062d3af0906cb53d9a08a25382097' - '12abd465a238501777573391c551deb1637a9384' - '810e5efc65179168764221d4d7fd83b8340f61bb') + ) +checkdepends=('parallel') +source=("http://compcert.inria.fr/release/$pkgname-$pkgver.tgz") +sha1sums=('2b0da15587fc1676852d241a5cc11c66e094f483') prepare() { cd $srcdir/$_dirname-$pkgver - - # 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() { |