introduce spark2014

3 files changed, 194 insertions, 0 deletions

diff --git a/.SRCINFO b/.SRCINFO
new file mode 100644
index 000000000000..2fc4fe405aec
--- /dev/null
+++ b/.SRCINFO
@@ -0,0 +1,42 @@
+pkgbase = spark2014-git
+	pkgdesc = formally defined programming language based on ada (gnat fsf)
+	pkgver = 0.3.draft.r17301.g094e550af
+	pkgrel = 5
+	url = https://www.spark-2014.org
+	arch = x86_64
+	license = GPL
+	makedepends = git
+	makedepends = coq
+	makedepends = gnatcoll-core
+	makedepends = gprbuild
+	makedepends = ocaml-num
+	makedepends = ocaml-menhir
+	makedepends = ocaml-ocamlgraph
+	makedepends = ocaml-zarith
+	makedepends = ocaml-camlzip
+	makedepends = ocaml-ocplib-simplex
+	makedepends = python-sphinx
+	depends = gprbuild
+	depends = python
+	optdepends = alt-ergo: alternative prover
+	optdepends = z3: alternative prover
+	optdepends = cvc4: alternative prover
+	provides = spark2014
+	conflicts = spark2014
+	conflicts = why3
+	options = !makeflags
+	source = git+https://github.com/AdaCore/spark2014
+	source = why3-adacore::git+https://github.com/AdaCore/why3
+	source = git+https://github.com/gcc-mirror/gcc
+	source = https://github.com/AdaCore/spark2014/files/2261639/sa_messages.ads.txt
+	source = https://github.com/AdaCore/spark2014/files/2261640/sa_messages.adb.txt
+	source = makefile-installdir-fixes.diff
+	sha256sums = SKIP
+	sha256sums = SKIP
+	sha256sums = SKIP
+	sha256sums = 6f3e5269b3d6e2b6c62d77976994056b7d32668ec2837b91e201405da52546a3
+	sha256sums = 9d4d0d228a025c1d723dbf9f18e2bfd1335f1d35a60360ad67f0cc55e2990a06
+	sha256sums = 2820a309db93782af029ba5b8492379e7aa2c58350629def00f748123866f3dd
+
+pkgname = spark2014-git
+
diff --git a/PKGBUILD b/PKGBUILD
new file mode 100644
index 000000000000..83d77810ca2d
--- /dev/null
+++ b/PKGBUILD
@@ -0,0 +1,97 @@
+pkgname=spark2014-git
+pkgver=0.3.draft.r17301.g094e550af
+pkgrel=5
+
+pkgdesc='formally defined programming language based on ada (gnat fsf)'
+url='https://www.spark-2014.org'
+arch=('x86_64')
+license=('GPL')
+
+options=('!makeflags')
+
+depends=('gprbuild' 'python')
+makedepends=('git' 'coq' 'gnatcoll-core' 'gprbuild' 'ocaml-num' 'ocaml-menhir'
+             'ocaml-ocamlgraph' 'ocaml-zarith' 'ocaml-camlzip'
+             'ocaml-ocplib-simplex' 'python-sphinx')
+optdepends=('alt-ergo: alternative prover'
+            'z3: alternative prover'
+            'cvc4: alternative prover')
+
+provides=('spark2014')
+conflicts=('spark2014' 'why3')
+
+source=('git+https://github.com/AdaCore/spark2014'
+        'why3-adacore::git+https://github.com/AdaCore/why3'
+        'git+https://github.com/gcc-mirror/gcc'
+        'https://github.com/AdaCore/spark2014/files/2261639/sa_messages.ads.txt'
+        'https://github.com/AdaCore/spark2014/files/2261640/sa_messages.adb.txt'
+        'makefile-installdir-fixes.diff')
+
+sha256sums=('SKIP'
+            'SKIP'
+            'SKIP'
+            '6f3e5269b3d6e2b6c62d77976994056b7d32668ec2837b91e201405da52546a3'
+            '9d4d0d228a025c1d723dbf9f18e2bfd1335f1d35a60360ad67f0cc55e2990a06'
+            '2820a309db93782af029ba5b8492379e7aa2c58350629def00f748123866f3dd')
+
+prepare() {
+    cd spark2014
+    git submodule init
+    git config submodule.why3.url "$srcdir"/why3-adacore
+    git submodule update why3
+
+    ln -sf "$srcdir"/gcc/gcc/ada gnat2why/gnat_src
+
+    # https://github.com/AdaCore/spark2014/issues/5#issuecomment-410622564
+    ln -sf "$srcdir"/sa_messages.ads.txt gnat2why/gnat_src/sa_messages.ads
+    ln -sf "$srcdir"/sa_messages.adb.txt gnat2why/gnat_src/sa_messages.adb
+
+    # Use install instead of mv to install the various targets while also
+    # houring the INSTALLDIR convention used within this Makefile.
+    patch -Np1 -i "$srcdir"/makefile-installdir-fixes.diff
+
+    # Arch Linux doesn't use libexec, everything lives under lib.
+    sed -i 's/libexec/lib/g' gnatprove/configuration.ads
+}
+
+pkgver() {
+    cd spark2014
+    git describe --long --tags | sed 's/_/-/; s/\([^-]*-g\)/r\1/; s/-/./g'
+}
+
+build() {
+    cd spark2014
+    make setup
+    make
+    make -C docs/lrm man
+    make -C docs/ug man
+}
+
+check() {
+    cd spark2014
+    # XXX ImportError: No module named gnatpython.env
+    # python2 testsuite/gnatprove/run-tests
+    # python2 testsuite/gnatmerge/run-tests
+}
+
+package() {
+    cd spark2014
+    make INSTALLDIR="$pkgdir"/usr install-all install-examples
+
+    install -Dm0755 install/bin/gnat2why "$pkgdir"/usr/bin/gnat2why
+    install -Dm0755 install/bin/gnatprove "$pkgdir"/usr/bin/gnatprove
+    install -Dm0755 install/bin/spark_codepeer_wrapper "$pkgdir"/usr/bin/spark_codepeer_wrapper
+    install -Dm0755 install/bin/spark_memcached_wrapper "$pkgdir"/usr/bin/spark_memcached_wrapper
+    install -Dm0755 install/bin/spark_report "$pkgdir"/usr/bin/spark_report
+
+    # For some reason the spark install why3 drivers and the other bits
+    # gnatprove needs to function.
+    cp -a --no-preserve=ownership install/share/why3 "$pkgdir"/usr/share
+
+    # Needed?
+    # install -Dm0755 install/bin/why3cpulimit "$pkgdir"/usr/lib/spark/bin/why3cpulimit
+    # rm -f -- "$pkgdir"/usr/bin/target.atp
+
+    install -Dm0644 docs/lrm/_build/man/spark2014refman.1 "$pkgdir"/usr/share/man/man7/spark2014_reference.7
+    install -Dm0644 docs/ug/_build/man/spark2014usersguide.1 "$pkgdir"/usr/share/man/man7/spark2014_userguide.7
+}
diff --git a/makefile-installdir-fixes.diff b/makefile-installdir-fixes.diff
new file mode 100644
index 000000000000..080060b71153
--- /dev/null
+++ b/makefile-installdir-fixes.diff
@@ -0,0 +1,55 @@
+diff --git a/Makefile b/Makefile
+index d1f314054..a4d375d24 100644
+--- a/Makefile
++++ b/Makefile
+@@ -36,7 +36,6 @@
+ INSTALLDIR=$(CURDIR)/install
+ SHAREDIR=$(INSTALLDIR)/share
+ INCLUDEDIR=$(INSTALLDIR)/include/spark
+-LIBDIR=$(INSTALLDIR)/lib/gnat
+ EXAMPLESDIR=$(SHAREDIR)/examples/spark
+ DOCDIR=$(SHAREDIR)/doc/spark
+ GNATPROVEDIR=$(SHAREDIR)/spark
+@@ -84,22 +83,21 @@ install-all:
+ 	# does (in anod scripts), as why3 executables expect this relative
+ 	# location to find the Why3 installation files in share. Do this for
+ 	# all internal binaries even if not strictly needed.
+-	mkdir -p install/libexec/spark/bin
+-	$(MV) install/bin/why3server install/libexec/spark/bin
+-	$(MV) install/bin/why3realize install/libexec/spark/bin
+-	$(MV) install/bin/gnatwhy3 install/libexec/spark/bin
+-	$(MV) install/bin/gnat_server install/libexec/spark/bin
+-	$(MV) install/bin/why3config install/libexec/spark/bin
+-	$(MV) install/bin/why3session install/libexec/spark/bin
++	install -Dm0755 install/bin/why3server $(INSTALLDIR)/lib/spark/bin/why3server
++	install -Dm0755 install/bin/why3realize $(INSTALLDIR)/lib/spark/bin/why3realize
++	install -Dm0755 install/bin/gnatwhy3 $(INSTALLDIR)/lib/spark/bin/gnatwhy3
++	install -Dm0755 install/bin/gnat_server $(INSTALLDIR)/lib/spark/bin/gnat_server
++	install -Dm0755 install/bin/why3config $(INSTALLDIR)/lib/spark/bin/why3config
++	install -Dm0755 install/bin/why3session $(INSTALLDIR)/lib/spark/bin/why3session
+ 	# the following line is allowed to fail - why3ide might not be
+ 	# installed
+-	-$(MV) install/bin/why3ide install/libexec/spark/bin
++	-install -Dm0755 install/bin/why3ide $(INSTALLDIR)/lib/spark/bin/why3ide
+ 	# Create the fake prover scripts to help extract benchmarks.
+-	$(CP) benchmark_script/fake_* install/libexec/spark/bin
++	install -Dm0755 -t $(INSTALLDIR)/lib/spark/bin benchmark_script/fake_*
+ 
+ install:
+ 	mkdir -p $(INSTALLDIR)/bin $(CONFIGDIR) $(THEORIESDIR) \
+-	  $(RUNTIMESDIR) $(INCLUDEDIR) $(LIBDIR)
++	  $(RUNTIMESDIR) $(INCLUDEDIR) $(INSTALLDIR)/lib/gnat
+ 	@echo "Generate default target.atp in $(INSTALLDIR)/bin:"
+ 	$(GNATMAKE) -q -c -u -gnats spark2014vsn.ads \
+ 	  -gnatet=$(INSTALLDIR)/bin/target.atp
+@@ -111,8 +109,8 @@ install:
+ 	@echo "Generate Coq files by preprocessing context files:"
+ 	$(MAKE) -C include generate
+ 	$(CP) include/*.ad? $(INCLUDEDIR)
+-	$(CP) include/*.gpr $(LIBDIR)
+-	$(CP) include/proof $(LIBDIR)
++	$(CP) include/*.gpr $(INSTALLDIR)/lib/gnat
++	$(CP) include/proof $(INSTALLDIR)/lib/gnat
+ 
+ doc: $(DOC)
+