gistfile1.txt

diff --git a/.SRCINFO b/.SRCINFO
index 8b08ee2..3650db6 100644
--- a/.SRCINFO
+++ b/.SRCINFO
@@ -1,6 +1,6 @@
 pkgbase = spark2014-git
 	pkgdesc = formally defined programming language based on ada (gnat fsf)
-	pkgver = 0.3.draft.r17853.g7a0a54649
+	pkgver = 0.3.draft.r19318.g3559419bef
 	pkgrel = 1
 	url = https://www.spark-2014.org
 	arch = x86_64
@@ -17,7 +17,7 @@ pkgbase = spark2014-git
 	makedepends = ocaml-ocplib-simplex
 	makedepends = python-sphinx
 	depends = gprbuild
-	depends = python
+	depends = python2
 	optdepends = alt-ergo: alternative prover
 	optdepends = z3: alternative prover
 	optdepends = cvc4: alternative prover
@@ -32,7 +32,7 @@ pkgbase = spark2014-git
 	sha256sums = SKIP
 	sha256sums = SKIP
 	sha256sums = SKIP
-	sha256sums = 2820a309db93782af029ba5b8492379e7aa2c58350629def00f748123866f3dd
+	sha256sums = ed0c29406e5e2728aa7202b22a3df95922ae5a6ba82ce71da6e432f0f1cbf6d4
 
 pkgname = spark2014-git
 
diff --git a/PKGBUILD b/PKGBUILD
index 0b9d35d..19a657c 100644
--- a/PKGBUILD
+++ b/PKGBUILD
@@ -1,5 +1,5 @@
 pkgname=spark2014-git
-pkgver=0.3.draft.r17853.g7a0a54649
+pkgver=0.3.draft.r19318.g3559419bef
 pkgrel=1
 
 pkgdesc='formally defined programming language based on ada (gnat fsf)'
@@ -9,7 +9,7 @@ license=('GPL')
 
 options=('!makeflags')
 
-depends=('gprbuild' 'python')
+depends=('gprbuild' 'python2')
 makedepends=('git' 'coq' 'gnatcoll-core' 'gprbuild' 'ocaml-num' 'ocaml-menhir'
              'ocaml-ocamlgraph' 'ocaml-zarith' 'ocaml-camlzip'
              'ocaml-ocplib-simplex' 'python-sphinx')
@@ -27,17 +27,20 @@ conflicts=('spark2014' 'why3')
 source=('git+https://github.com/AdaCore/spark2014#branch=fsf'
         'why3-adacore::git+https://github.com/AdaCore/why3'
         'git+https://github.com/gcc-mirror/gcc'
-        'makefile-installdir-fixes.diff')
+        'makefile-installdir-fixes.diff'
+        'why3-menhirLib-fix.diff')
 
 
 sha256sums=('SKIP' 'SKIP' 'SKIP'
-            '2820a309db93782af029ba5b8492379e7aa2c58350629def00f748123866f3dd')
+            'fa399eab4d3acaf73158ebb5774c8b5d4421ef8a86a31bc8232bc0f16af8cf2f'
+            '8bcf62beb5773a6da910a512d8384343774aa3561d6d5b5c1891e545aef635aa')
 
 prepare() {
     cd spark2014
     git submodule init
     git config submodule.why3.url "$srcdir"/why3-adacore
     git submodule update why3
+    cd why3 && git reset --hard && cd ..
 
     ln -sf "$srcdir"/gcc/gcc/ada gnat2why/gnat_src
 
@@ -45,6 +48,8 @@ prepare() {
     # houring the INSTALLDIR convention used within this Makefile.
     patch -Np1 -i "$srcdir"/makefile-installdir-fixes.diff
 
+    patch -Np1 -i "$srcdir"/why3-menhirLib-fix.diff
+
     # Arch Linux doesn't use libexec, everything lives under lib.
     sed -i 's/libexec/lib/g' gnatprove/configuration.ads
 }
@@ -56,7 +61,7 @@ pkgver() {
 
 build() {
     cd spark2014
-    make setup
+    make setup INSTALLDIR="$pkgdir"/usr
     make
     make -C docs/lrm man
     make -C docs/ug man
@@ -81,7 +86,7 @@ package() {
 
     # For some reason the spark install doesn't include the why3 drivers and
     # the other bits which gnatprove needs to function.
-    cp -a --no-preserve=ownership install/share/why3 "$pkgdir"/usr/share
+    # cp -a --no-preserve=ownership install/share/why3 "$pkgdir"/usr/share
 
     # Needed?
     # install -Dm0755 install/bin/why3cpulimit "$pkgdir"/usr/lib/spark/bin/why3cpulimit
diff --git a/makefile-installdir-fixes.diff b/makefile-installdir-fixes.diff
index 080060b..20673ba 100644
--- a/makefile-installdir-fixes.diff
+++ b/makefile-installdir-fixes.diff
@@ -1,55 +1,33 @@
 diff --git a/Makefile b/Makefile
-index d1f314054..a4d375d24 100644
+index fe788de34e..4d298e247e 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
+@@ -76,8 +76,8 @@ coverage-nightly: coverage gnatprove-nightly install install-coverage install-ex
+ #   install-all  install of gnatprove and why3
+ 
+ setup:
+-	cd why3 && ./configure --prefix=$(INSTALLDIR)/libexec/spark \
+-		--enable-relocation --disable-js-of-ocaml
++	cd why3 && ./configure --prefix=$(INSTALLDIR)/lib/spark \
++		--enable-relocation --disable-js-of-ocaml --disable-emacs-compilation
+ 
+ why3:
+ 	$(MAKE) -C why3
+@@ -86,7 +86,7 @@ install-all:
+ 	$(MAKE) install
+ 	$(MAKE) -C why3 install_spark2014_dev
  	# 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_*
++	$(CP) benchmark_script/fake_* install/lib/spark/bin
  
  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)
+@@ -126,7 +126,7 @@ gnat2why:
+ 	# Produce Ada code that stores the reserved keywords of Why3
+ 	# This script should be run *ONLY* in developper build not in prod
+ 	# (gnat2why-nightly)
+-	python scripts/why3keywords.py why3/src/parser/lexer.mll gnat2why/why/why-keywords.adb
++	python2 scripts/why3keywords.py why3/src/parser/lexer.mll gnat2why/why/why-keywords.adb
+ 	$(MAKE) -C gnat2why
  
+ coverage:
diff --git a/why3-menhirLib-fix.diff b/why3-menhirLib-fix.diff
new file mode 100644
index 0000000..ca2e964
--- /dev/null
+++ b/why3-menhirLib-fix.diff
@@ -0,0 +1,15 @@
+diff --git a/why3/Makefile.in b/why3/Makefile.in
+index f630aad5f..9976366f4 100644
+--- a/why3/Makefile.in
++++ b/why3/Makefile.in
+@@ -126,7 +126,7 @@ CMIHACK = -intf-suffix .cmi
+
+ # external libraries common to all binaries
+
+-EXTOBJS = menhirLib
+-EXTLIBS = str unix nums dynlink @ZIPLIB@ @MLMPFR@ @WHY3LIB@
++EXTOBJS =
++EXTLIBS = menhirLib str unix nums dynlink @ZIPLIB@ @MLMPFR@ @WHY3LIB@
+
+ EXTCMA	= $(addsuffix .cmo,$(EXTOBJS)) $(addsuffix .cma,$(EXTLIBS))
+ EXTCMXA = $(addsuffix .cmx,$(EXTOBJS)) $(addsuffix .cmxa,$(EXTLIBS))