summarylogtreecommitdiffstats
diff options
context:
space:
mode:
authorXuanrui Qi2019-09-18 21:58:55 -0700
committerXuanrui Qi2019-09-18 21:58:55 -0700
commit02aa64f46b75130da85ee764c0855a76caef427b (patch)
treef68b64034de785c579b56aa4e6ae6a99e0630015
parent738306712c35dc8550f4e55d9215c395f07cb11e (diff)
downloadaur-02aa64f46b75130da85ee764c0855a76caef427b.tar.gz
Release 3.6
-rw-r--r--.SRCINFO19
-rw-r--r--Makefile-runtime.patch23
-rw-r--r--Makefile.patch37
-rw-r--r--PKGBUILD24
4 files changed, 15 insertions, 88 deletions
diff --git a/.SRCINFO b/.SRCINFO
index aa9b5778d1eb..d44b7d3ac6db 100644
--- a/.SRCINFO
+++ b/.SRCINFO
@@ -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
-
diff --git a/PKGBUILD b/PKGBUILD
index e19adc7b63d7..3fce54051626 100644
--- a/PKGBUILD
+++ b/PKGBUILD
@@ -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() {