diff -Nru why-2.34/debian/changelog why-2.34/debian/changelog --- why-2.34/debian/changelog 2015-10-16 23:12:21.000000000 +0000 +++ why-2.34/debian/changelog 2016-07-28 19:40:40.000000000 +0000 @@ -1,3 +1,45 @@ +why (2.34-4+rpi1) stretch-staging; urgency=medium + + * adopt ubuntu changes in raspbian to get package building until Debian + fixes it. + + -- Peter Michael Green Thu, 28 Jul 2016 19:40:12 +0000 + +why (2.34-4ubuntu5) yakkety; urgency=medium + + * No-change rebuild against frama-c 20151002+magnesium+dfsg-1build2 + + -- Steve Langasek Sun, 10 Jul 2016 13:41:00 -0700 + +why (2.34-4ubuntu4) xenial; urgency=medium + + * Disable the why+coq autopkg test. + + -- Matthias Klose Tue, 23 Feb 2016 16:34:34 +0100 + +why (2.34-4ubuntu3) xenial; urgency=medium + + * Drop build dependency on libfloat-coq, not buildable with the + the current coq. + * why still fails to build, so drop the the libwhy-coq binary + and coq build dependency. + + -- Matthias Klose Tue, 23 Feb 2016 15:36:48 +0100 + +why (2.34-4ubuntu2) xenial; urgency=medium + + * Rebuild for new OCaml ABIs. + + -- Matthias Klose Fri, 12 Feb 2016 12:07:26 +0000 + +why (2.34-4ubuntu1) xenial; urgency=medium + + * Rebase on Debian, remaining change: + + debian/tests/control: Disable frama-c+jessie+alt-ergo test, since we + don't have a jessie plugin currently (until we get 'why3') + + -- Iain Lane Wed, 04 Nov 2015 12:12:10 +0000 + why (2.34-4) unstable; urgency=medium [ Ralf Treinen ] diff -Nru why-2.34/debian/control why-2.34/debian/control --- why-2.34/debian/control 2015-10-16 22:19:11.000000000 +0000 +++ why-2.34/debian/control 2016-07-10 20:41:21.000000000 +0000 @@ -1,7 +1,8 @@ Source: why Section: math Priority: optional -Maintainer: Debian OCaml Maintainers +Maintainer: Ubuntu Developers +XSBC-Original-Maintainer: Debian OCaml Maintainers Uploaders: Samuel Mimram , Mehdi Dogguy , Ralf Treinen @@ -14,8 +15,6 @@ ocaml-best-compilers, camlp4, liblablgtk2-ocaml-dev (>= 2.12.0-3~), - coq (>= 8.3~), - libfloat-coq, libocamlgraph-ocaml-dev (>= 1.4~), frama-c-base (>= 20140301+neon+dfsg), libapron-ocaml-dev (>= 0.9.10-4~), @@ -48,7 +47,6 @@ Architecture: all Depends: ${misc:Depends}, - libwhy-coq, why Section: doc Description: Examples of programs certified with Why @@ -60,16 +58,3 @@ decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey. . This package contains examples of programs verified using Why. - -Package: libwhy-coq -Architecture: all -Depends: - ${misc:Depends}, - coq-${F:CoqABI} -Replaces: - why (<< 2.18.dfsg-1) -Section: libdevel -Description: Why library for Coq - This package contains all useful logical definitions, lemmas with their - proofs and axioms used by Why. Users may need this package when proving - some proof obligations in Coq. diff -Nru why-2.34/debian/rules why-2.34/debian/rules --- why-2.34/debian/rules 2015-10-16 22:19:11.000000000 +0000 +++ why-2.34/debian/rules 2016-02-23 15:10:37.000000000 +0000 @@ -4,7 +4,6 @@ export DH_VERBOSE=1 include /usr/share/ocaml/ocamlvars.mk -include /usr/share/coq/coqvars.mk WHYDIR = $(CURDIR)/debian/why FRAMADIR = $(WHYDIR)/$(shell frama-c -print-plugin-path) @@ -12,6 +11,10 @@ VERSION = $(shell cat Version | grep ^VERSION | cut -d= -f 2) export OCAMLINIT_SED += -e 's/@VERSION@/$(VERSION)/g' +override_dh_auto_test: + : # requires coq + true + override_dh_auto_configure: autoconf ./configure \ @@ -41,7 +44,6 @@ -$(RM) -rf $(WHYDIR)/usr/share/jessie/ #Jessie.cma is installed, no need for this extra file -$(RM) -f $(FRAMADIR)/Jessie.cmo - echo 'F:CoqABI=$(COQ_ABI)' >> debian/libwhy-coq.substvars echo 'F:FramaCVersion=$(FRAMAVER)' >> debian/why.substvars override_dh_compress: diff -Nru why-2.34/debian/tests/control why-2.34/debian/tests/control --- why-2.34/debian/tests/control 2015-10-16 22:19:11.000000000 +0000 +++ why-2.34/debian/tests/control 2016-02-23 15:34:32.000000000 +0000 @@ -4,8 +4,8 @@ Tests: why+cvc3 Depends: why, cvc3 -Tests: why+coq -Depends: why, libwhy-coq, coq +#Tests: why+coq +#Depends: why, libwhy-coq, coq -Tests: frama-c+jessie+alt-ergo -Depends: why, frama-c-base, alt-ergo +#Tests: frama-c+jessie+alt-ergo +#Depends: why, frama-c-base, alt-ergo