summarylogtreecommitdiffstats
diff options
context:
space:
mode:
authorXuanrui Qi2019-05-18 02:16:03 -0400
committerXuanrui Qi2019-05-18 02:16:03 -0400
commit4503d294b3ce2733faf318eb71047c84de8f229c (patch)
tree1644f46f9e8506ca36b8c91064fe25e3b30fcdbf
parent9cd5b4a53a2b371f1b103f4b4edb321fa60067cb (diff)
downloadaur-4503d294b3ce2733faf318eb71047c84de8f229c.tar.gz
Patch no longer needed due to upstream fix
-rw-r--r--.SRCINFO10
-rw-r--r--Makefile-runtime.patch23
-rw-r--r--Makefile.patch37
-rw-r--r--PKGBUILD19
4 files changed, 8 insertions, 81 deletions
diff --git a/.SRCINFO b/.SRCINFO
index 835257928d89..c0b124646e00 100644
--- a/.SRCINFO
+++ b/.SRCINFO
@@ -1,7 +1,7 @@
pkgbase = compcert-git
pkgdesc = The formally verified C compiler
- pkgver = 3.5.r25.g8df51b98
- pkgrel = 1
+ pkgver = 3.5.r36.g5b7fc96a
+ pkgrel = 3
url = http://compcert.inria.fr
arch = x86_64
license = custom:INRIA Non-Commercial License Agreement
@@ -12,14 +12,10 @@ pkgbase = compcert-git
makedepends = ocaml-findlib
makedepends = git
depends = gcc
- provides = compcert=3.5.r25.g8df51b98
+ provides = compcert=3.5.r36.g5b7fc96a
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
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
-
diff --git a/PKGBUILD b/PKGBUILD
index 702362d5077a..3e3f8efdcac3 100644
--- a/PKGBUILD
+++ b/PKGBUILD
@@ -2,8 +2,8 @@
pkgname=compcert-git
_basepkgname=${pkgname%-*}
_dirname=CompCert
-pkgver=3.5.r25.g8df51b98
-pkgrel=1
+pkgver=3.5.r36.g5b7fc96a
+pkgrel=3
pkgdesc="The formally verified C compiler"
arch=('x86_64')
url="http://compcert.inria.fr"
@@ -15,12 +15,8 @@ makedepends=('coq>=8.6.1' 'ocaml>=4.0.2'
'git')
provides=($_basepkgname=$pkgver)
conflicts=($_basepkgname)
-source=("git+https://github.com/AbsInt/CompCert.git"
- "Makefile.patch"
- "Makefile-runtime.patch")
-sha1sums=('SKIP'
- '12abd465a238501777573391c551deb1637a9384'
- '810e5efc65179168764221d4d7fd83b8340f61bb')
+source=("git+https://github.com/AbsInt/CompCert.git")
+sha1sums=('SKIP')
pkgver() {
cd $srcdir/$_dirname
@@ -29,11 +25,6 @@ pkgver() {
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() {
@@ -42,7 +33,7 @@ build() {
# 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)
+ # if you want to use tools such as Princeton VST)
./configure -prefix /usr $CARCH-linux
make all