why3 (1.8.2-3) unstable; urgency=medium

  * Team upload
  * Actually b-d on graphviz-tools, some tools are now split into that
    package.

 -- Gianfranco Costamagna <locutusofborg@debian.org>  Tue, 06 Jan 2026 10:11:53 +0100

why3 (1.8.2-2) unstable; urgency=medium

  * Team upload
  * Add b-d on graphviz to fix missing ccomps during build (Closes: #1122492)

 -- Gianfranco Costamagna <locutusofborg@debian.org>  Sun, 04 Jan 2026 10:00:25 +0100

why3 (1.8.2-1) unstable; urgency=medium

  * New upstream release

 -- Ralf Treinen <treinen@debian.org>  Tue, 23 Sep 2025 22:40:18 +0200

why3 (1.8.1-1) unstable; urgency=medium

  * Team upload
  * New upstream release (Closes: #1098092)

 -- Stéphane Glondu <glondu@debian.org>  Fri, 12 Sep 2025 14:59:57 +0200

why3 (1.8.0-3) experimental; urgency=medium

  * Update home page.
  * Build again the documentation packages.
  * Standards-Version 4.7.2 (no change)

 -- Ralf Treinen <treinen@debian.org>  Sun, 20 Apr 2025 14:13:02 +0200

why3 (1.8.0-2) unstable; urgency=medium

  * Team upload
  * Add Breaks+Replaces to avoid file conflict (Closes: #1093827)

 -- Stéphane Glondu <glondu@debian.org>  Sun, 02 Feb 2025 07:37:18 +0100

why3 (1.8.0-1) unstable; urgency=medium

  * New upstream release.
  * Stop building the documentation packages:
    - debian/control: disable why3-doc-* packages
    - debian/rules: disable override_dh_auto_build-arch
    - debian-rules: disable Build-Depends-Indep
  * Create a symlink from /usr/lib/ocaml/why3 to the why3 library in order
    to work around a bug in why3, which does not properly take into account
    the --libdir option to ./configure.
  * Dependency and Test-Dependency on provers:
    - bump z3 to version << 4.14
    - add cvc5 << 1.3
  * Add an as-installed test with cvc5

 -- Ralf Treinen <treinen@debian.org>  Wed, 22 Jan 2025 21:27:21 +0100

why3 (1.7.2-2) unstable; urgency=medium

  * Team upload
  * Do not hardcode /usr/lib/ocaml
  * Depend on ocaml-native-compilers in tests for now

 -- Stéphane Glondu <glondu@debian.org>  Tue, 13 Aug 2024 01:43:15 +0200

why3 (1.7.2-1) unstable; urgency=medium

  * New upstream release.
  * debian/clean: add doc/.doctrees (closes: #1046969), remove cruft
  * debian/watch: use release tags of INRIA's gitlab
  * debian/rules: update url of external mathjax resources, which are
    replaced by locally installed mathjax.
  * The alt-ergo package is no longer in debian: drop it from Recommends,
    and drop the corresponding as-installed test.
  * Standards-Version 4.7.0 (no change)

 -- Ralf Treinen <treinen@debian.org>  Mon, 12 Aug 2024 11:54:59 +0200

why3 (1.6.0-1) unstable; urgency=medium

  * Team upload
  * New upstream release
  * Depend on ocaml instead of transitional ocaml-nox
  * Bump Standards-Version to 4.6.2

 -- Stéphane Glondu <glondu@debian.org>  Fri, 08 Sep 2023 07:09:51 +0200

why3 (1.5.1-1) unstable; urgency=medium

  * New upstream release.
  * Supports z3 until 4.11.0
  * Standards-Version 4.6.1 (no change)
  * Add lintian override for test file with national character encoding

 -- Ralf Treinen <treinen@debian.org>  Wed, 19 Oct 2022 03:37:35 +0200

why3 (1.5.0-1) unstable; urgency=medium

  * New upstream version.
  * Refresh patch hardening-flags.
  * Drop patch ocamlgraph-cma, issue has been fixed upstream.
  * debian/rules: configure with option --disable-coq-libs, so that
    we are sure that coq stuff is not build.
  * Bump dependency on z3 to (<< 4.8.16).
  * Simplify test why3+z3: drop preliminary testing of z3.

 -- Ralf Treinen <treinen@debian.org>  Tue, 03 May 2022 08:00:48 +0200

why3 (1.4.1-2) unstable; urgency=medium

  * Fix compilation on bytecode architectures, on these architectures we
    have to look for exported units in why3ide.cma.

 -- Ralf Treinen <treinen@debian.org>  Sat, 19 Mar 2022 15:01:40 +0100

why3 (1.4.1-1) unstable; urgency=medium

  * New upstream release.
  * New patch ocamlgraph-cma to cope with the fact that ocamlgraph does no
    longer produce graph.cmo (closes: #1003801)
  * Drop building of the why3-coq package.

 -- Ralf Treinen <treinen@debian.org>  Sat, 19 Mar 2022 12:16:02 +0100

why3 (1.4.0-3) unstable; urgency=medium

  * Update Recommends and test-dependencies of why3: cvc4 up to 1.8, z3 up
    to 4.8.10
  * Build-dependency on ocamlgraph and coq: add version constraints
    according to upstream opam file
  * Use a debian/control.in to fill in automatically the native architectures
    on which coq is available
  * Update why3 manpage to document the new syntax of "why3 config"
  * Add debian/upstream/metadata

 -- Ralf Treinen <treinen@debian.org>  Sat, 11 Dec 2021 11:37:13 +0100

why3 (1.4.0-2) unstable; urgency=medium

  * Team upload
  * Fix autopkgtests

 -- Stéphane Glondu <glondu@debian.org>  Wed, 24 Nov 2021 08:49:42 +0100

why3 (1.4.0-1) unstable; urgency=medium

  * Team upload
  * New upstream release
    - Backport Coq 8.14 support from upstream git
  * Bump Standards-Version to 4.6.0
  * Update debian/watch

 -- Stéphane Glondu <glondu@debian.org>  Tue, 23 Nov 2021 14:26:23 +0100

why3 (1.3.3-3) unstable; urgency=medium

  * Add new tex-gyre dependency, useful to fix a build failure on
    pdflatex doc generation, Thanks <bunk> for the hint and patch!

 -- Gianfranco Costamagna <locutusofborg@debian.org>  Tue, 26 Oct 2021 15:17:59 +0200

why3 (1.3.3-2) unstable; urgency=medium

  [ Gianfranco Costamagna ]
  * Cherry-pick two upstream fixes for new sphinx-bibtex version:
    - d/p/99377bc169d86f86b167150624d248f01d9025f9.patch:
    - d/p/50f39bb6164bd40ed580a12452f83853f885c344.patch:
      (Closes: #995603)
  [ Ralf Treinen ]
  * debian/watch: format version 4

 -- Gianfranco Costamagna <locutusofborg@debian.org>  Tue, 26 Oct 2021 09:47:54 +0200

why3 (1.3.3-1) unstable; urgency=medium

  * New upstream release:
    - drop patch why8.12, issue is solved by upstream
  * Alternative dependency of why3, and test dependency on cvc4: add a
    version constraint << 1.8 since cvc4 is supported only up to upstream
    version 1.7 (closes: #970510)

 -- Ralf Treinen <treinen@debian.org>  Wed, 23 Sep 2020 21:23:15 +0200

why3 (1.3.2-1) unstable; urgency=medium

  * New upstream release.
  * Add patch coq8.12: support coq versions 8.11.* and 8.12.*
    (thanks to Guillaume Melquiond)
  * Test why3+coq: send warning to stderr
  * Replace embedded sphinx javascript libraries by symlinks,
    and add dependency on libjs-sphinxdoc to package why3-doc-html.
  * debian/control: update architecture of the why3-coq package, and
    architecture strings in build-dependencies on coq stuff.

 -- Ralf Treinen <treinen@debian.org>  Thu, 10 Sep 2020 23:09:31 +0200

why3 (1.3.1-3) unstable; urgency=medium

  * Team upload
  * Include ocamlvars.mk to prevent FTBFS in dh_dwz
  * Bump debhelper compat level to 13
  * Add Rules-Requires-Root: no

 -- Stéphane Glondu <glondu@debian.org>  Sun, 16 Aug 2020 01:08:26 +0200

why3 (1.3.1-2) unstable; urgency=medium

  * Add Build-Depends-Indep: graphviz

 -- Ralf Treinen <treinen@debian.org>  Tue, 07 Apr 2020 19:11:39 +0200

why3 (1.3.1-1) unstable; urgency=medium

  * New upstream version.
    This version contains the micro-C plugin (closes: #950605)
  * Drop patches fixed by this upstream version:
    - coq-8.10+11
    - 0002-Move-menhirLib-from-EXTOBJS-to-EXTLIBS
  * Refresh patch hardening-flags
  * Upstream switched the building of the documentation to sphinx:
    - added build-dependencies python3-sphinx, python3-sphinxcontrib.bibtex
    - dropped build-dependencies rubber, hevea, lmodern
    - why3-doc-pdf.docs: update path of manual.pdf
  * configuration: explicitly set --libdir
  * debian/rules: simplify by using override_dh_auto_build-{arch,indep}
  * Test why+coq: use /tmp when $ADT_ARTIFACTS is not set
  * why3-doc-html:
    - depend on libjs-{jquery,underscore}
    - use why3-doc-html.links to symlink these libraries, replacing the
      embedded copies
    - remove calls to the mathjax library from generated html code

 -- Ralf Treinen <treinen@debian.org>  Mon, 06 Apr 2020 09:35:10 +0200

why3 (1.2.1-6) unstable; urgency=medium

  * Add build-dependency libnum-ocaml-dev (used to be pulled in by coq)
  * Bump build-dependency on ocaml, as indicated by opam file

 -- Ralf Treinen <treinen@debian.org>  Sun, 08 Mar 2020 20:36:59 +0100

why3 (1.2.1-5) unstable; urgency=medium

  * debian/rules: include coqvars.mk, and set F:CoqABI substvar, only where
    that file exists.

 -- Ralf Treinen <treinen@debian.org>  Sun, 08 Mar 2020 17:34:13 +0100

why3 (1.2.1-4) unstable; urgency=medium

  * Support new coq versions:
    - add patch coq-8.10+11:
    - invoke autoconf in debian/rules, add it to build-depends
  * Since coq does no longer build on all release architectures:
    - Mark the test why3+coq as skip-not-installable
    - Restrict build-dependencies on coq to amd64 arm64 ppc64 ppc64el sh4
    - Restrict recommendation of why3-coq to amd64 arm64 ppc64 ppc64el sh4
    - Build why3-coq only on amd64 arm64 ppc64 ppc64el sh4
  * Standards-Version 4.5.0 (no change)
  * Drop override of dh_dwz which is no longer needed.

 -- Ralf Treinen <treinen@debian.org>  Sun, 08 Mar 2020 16:35:43 +0100

why3 (1.2.1-3) unstable; urgency=medium

  [ Stéphane Glondu ]
  * Team upload
  * Fix FTBFS with menhir 20200123 (Closes: #951052)

  [ Ralf Treinen ]
  * drop cvc3 from Recommends and debian/tests as the cvc3 package has
    been removed from sid.

 -- Stéphane Glondu <glondu@debian.org>  Mon, 10 Feb 2020 13:57:51 +0100

why3 (1.2.1-2) unstable; urgency=medium

  * patch hardening-flags: use hardening flags when compiling the
    why3 server.

 -- Ralf Treinen <treinen@debian.org>  Sun, 03 Nov 2019 22:02:08 +0100

why3 (1.2.1-1) unstable; urgency=medium

  * New upstream version.
  * Drop patch lablgtk3-beta6 which is now applied by upstream.
  * Bumped dependency on z3 to << 4.8.7 (d/control and d/tests/control)

 -- Ralf Treinen <treinen@debian.org>  Mon, 28 Oct 2019 18:48:39 +0100

why3 (1.2.0-3) unstable; urgency=medium

  * why3 1.2.0 supports z3 up to version 4.8.4 only (closes: #942344)
    - add a version constraint to Recommends
    - add a version constraint to the dependencies of test why3+z3
    - flag test why3+z3 as skip-not-installable
  * Standards-Version 4.4.1 (no change)

 -- Ralf Treinen <treinen@debian.org>  Tue, 15 Oct 2019 20:42:34 +0200

why3 (1.2.0-2) unstable; urgency=medium

  * debian/rules: add build target
  * Standards-Version 4.4.0 (no change)
  * Patch lablgtk3-beta6: Port to version beta6 of lablgtk3. Patch picked
    from upstream git. This fixes an issue with why3 not detecting
    lablgtk3-sourceview and hence not building the graphical interface.

 -- Ralf Treinen <treinen@debian.org>  Thu, 29 Aug 2019 21:23:49 +0200

why3 (1.2.0-1) unstable; urgency=medium

  * New upstream version
  * Also build the library in bytecode
  * libwhy3-ocaml-dev: add Suggests:ocaml-findlib
  * Re-activate building of the ide, now using lablgtk3

 -- Ralf Treinen <treinen@debian.org>  Fri, 15 Feb 2019 08:19:55 +0100

why3 (1.1.1-4) unstable; urgency=medium

  * Add build-dependency ocaml-findlib (closes: #921465)
  * Replace dependency on debhelper by debhelper-compat
  * Enable coq support

 -- Ralf Treinen <treinen@debian.org>  Wed, 06 Feb 2019 20:57:54 +0100

why3 (1.1.1-3) unstable; urgency=medium

  * disable coq support.

 -- Ralf Treinen <treinen@debian.org>  Sun, 03 Feb 2019 23:01:38 +0100

why3 (1.1.1-2) unstable; urgency=medium

  * why3-coq: depend on the virtual package provided by coq and indicating
    the version of the coq ABI (closes: #918633).
  * Standards-Version 4.3.0 (no change)
  * Debhelper compatibility level 12
    - override dh_dwz to use --no-dwz-multifile

 -- Ralf Treinen <treinen@debian.org>  Thu, 10 Jan 2019 20:12:24 +0100

why3 (1.1.1-1) unstable; urgency=medium

  * New upstream version.
  * Fix whitespace in debian/{control/changelog}

 -- Ralf Treinen <treinen@debian.org>  Tue, 18 Dec 2018 04:50:38 +0100

why3 (1.1.0-1) unstable; urgency=medium

  * New upstream version. Works with cvc4 version 1.6 (closes: #906001)
  * Since lablgtk2 does no longer build liblablgtksourceview2-ocaml-dev:
    - drop build-dependencies liblablgtk2-ocaml-dev and
      liblablgtksourceview2-ocaml-dev
    - d/rules: configure with --disable-ide
    - note in NEWS that the IDE is dropped.
    - drop mention of IDE from why3.1 manpage.
  * Dependencies on provers : enforce version >= 2.0.0. for alt-ergo since
    upstream has dropped support for older versions. Add an
    "skip-not-installable" on the test why3+alt-ergo
  * Test why3+cvc4: fix selection of solver cvc4
  * d/copyright: update full text of CC license.
  * d/rules: remove empty why3shapes.gz files
  * Standards-Version 4.2.1 (no change)

 -- Ralf Treinen <treinen@debian.org>  Mon, 05 Nov 2018 19:23:56 +0100

why3 (1.0.0-2) unstable; urgency=medium

  * as-installed test why3+cvc4:
    - dropped erroneous version constraint on cvc4.
    - invoke prover simply as CVC4
    - marked test as skip-not-installable, instead of flaky, as cvc4 does not
      build on all architectures (architecture restriction set in src:cvc4),
      and since cvc4 is only an alternative dependency of why3.
  * as-installed test why3+cvc3:
    - marked test as skip-not-installable, instead of flaky, since cvc3
      recently has FTBFS, and since cvc3 is only an alternative dependency
      of why3.
  * as-installed-test why3+spass:
    - marked test as skip-not-installable since spass recently has FTBFS
      issues and was dropped from testing, and since spass is only an
      alternative dependency of why3.

 -- Ralf Treinen <treinen@debian.org>  Sun, 12 Aug 2018 23:29:44 +0200

why3 (1.0.0-1) unstable; urgency=medium

  * New upstream version
    - drop patch getopt_long-return-value which has been applied upstream
  * Upstream does no longer build coq-tactic:
    - drop these from why3-coq.install
    - drop mention of these from the long description of why3-coq
  * libwhy3-ocaml-dep: add dependency ${shlibs:Depends}
  * As-installed-tests:
    - adapt the why3 files in d/tests/why to the new syntax of WhyML
    - mark tests with cvc3 and cvc4 as flaky  (closes: #902308)
    - test why3+cvc4: specify 'CVC4 1.5' in the invocation of why3,
      constrain the dependency of the test on cvc4 accordingly.
  * NEWS.Debian: new syntax of WhyML, new location of standard lib

 -- Ralf Treinen <treinen@debian.org>  Wed, 27 Jun 2018 22:19:33 +0200

why3 (0.88.3-3) unstable; urgency=medium

  * d/control: update Vcs-* fields to salsa
  * Add build-dependendency texlive-plain-generic to fix FTBFS with
    texlive 2018.20180505-1 (closes: #899084)
  * test why3+cvc4: skip when cvc4 is not available (closes: #895104)

 -- Ralf Treinen <treinen@debian.org>  Sun, 27 May 2018 13:37:54 +0200

why3 (0.88.3-2) unstable; urgency=medium

  * Standards-version 4.1.4 (no change).
  * d/copyright: https in format specification
  * Add patch getopt_long-return-value which fixes a portability issue
    (closes: #895103). Thanks a lot to Steve Langasek for the patch!

 -- Ralf Treinen <treinen@debian.org>  Sat, 07 Apr 2018 11:54:01 +0200

why3 (0.88.3-1) unstable; urgency=medium

  * New upstream version.
    - drop creation of empty directories in debian/rules, this has been
      fixed by upstream.
  * Standards-Version 4.1.3 (no change)
  * debian/rules:
    - fix configure stamps
    - drop build stamps, we do not need them.
    - dh-install: exclude extra LICENSE file
    - drop override_dh_auto_build
  * debhelper compatibility level 11

 -- Ralf Treinen <treinen@debian.org>  Sun, 14 Jan 2018 14:52:54 +0100

why3 (0.88.2-1) unstable; urgency=medium

  * New upstream version.
  * Standards-Version 4.1.2 (no change)
  * d/rules:
    - recreate in target configure the empty directories that are
      in the orig tarball.
    - invoke dh_missing with --fail-missing
  * fix why3.install, add missing files from usr/lib
  * Added build-dep-indep texlive-bibtex-extra
  * debhelper compat level 10
  * New SMT solver cvc4:
    - add as an alternative Recommends
    - add autopkgtest test case

 -- Ralf Treinen <treinen@debian.org>  Tue, 12 Dec 2017 22:22:24 +0100

why3 (0.87.3-2) unstable; urgency=medium

  * upload to unstable
  * as-installed test why3+z3: do not fail when z3 segfaults.

 -- Ralf Treinen <treinen@debian.org>  Sat, 21 Jan 2017 21:02:08 +0100

why3 (0.87.3-1) experimental; urgency=medium

  * New upstream version:
    - drop patch coq8.6 which is now integrated by upstream.
  * Fix path of ocaml libdir in debian/libwhy3-ocaml-dev.install
  * Capitalization in short description of libwhy3-ocaml-dev
  * Drop build-dependency on autoconf

 -- Ralf Treinen <treinen@debian.org>  Thu, 12 Jan 2017 16:56:47 +0100

why3 (0.87.2-3) unstable; urgency=medium

  * adapt to coq version 8.6:
    - patch coq8.6: compile coq plugin with coq8.6. Thanks to Guillaume
      Melquiond for the patch!
    - add autoconf to build-dependency (needed since configure.in is patched)
    - fix path of ocaml libdir in debian/libwhy3-ocaml-dev.install

 -- Ralf Treinen <treinen@debian.org>  Tue, 03 Jan 2017 20:56:05 +0100

why3 (0.87.2-2) sid; urgency=medium

  * install why3lang.sty:
    - add to why3.install
    - add target directory to why3.dirs
    - invoke dh --with tex
    - add build-dependency on tex-common

 -- Ralf Treinen <treinen@debian.org>  Wed, 21 Sep 2016 21:15:04 +0200

why3 (0.87.2-1) unstable; urgency=medium

  * new upstream release.
    - d/rules: replace EMACS=no by --disable-emacs-compilation
    - drop patch typos, applied by upstream
    - drop patch drop-timestamp, applied by upstream. As a consequence,
      we drop autoconf from d/rules and from build-dependencies
  * add debian/tests/why3+coq

 -- Ralf Treinen <treinen@debian.org>  Thu, 01 Sep 2016 19:21:22 +0200

why3 (0.87.1-2) unstable; urgency=medium

  * amended patch drop-timestamp: drop setting of BUILDDATE from configure.in
    (closes: #831664). Invoke autoconf, and build-depend on autoconf,
    since we patch configure.in

 -- Ralf Treinen <treinen@debian.org>  Tue, 19 Jul 2016 19:05:11 +0200

why3 (0.87.1-1) unstable; urgency=medium

  * new upstream version
    -dropped patch makefile-for-bytecode, since integrated by upstream
  * added z3 prover:
    - alternative dependency z3
    - add package test with z3
  * new patch drop-timestamp: do not include the build-timestamp in the
    produced binaries.

 -- Ralf Treinen <treinen@debian.org>  Wed, 08 Jun 2016 20:42:36 +0200

why3 (0.87.0-3) unstable; urgency=medium

  * debian/tests/*: run "why3 config --detect-provers" to make tests
    work in a clean environment.

 -- Ralf Treinen <treinen@debian.org>  Thu, 14 Apr 2016 19:00:49 +0200

why3 (0.87.0-2) unstable; urgency=medium

  * added a new binary package libwhy3-ocaml-dev
    - install libraries in install-arch target of d/rules
    - add d/*.install and d/*.dir files for this package
    - call dh_ocaml with --nodefined-map=why3-coq:Why3 since this unit is
      also exported by the library package
  * d/rules: split into -arch and -indep rules
  * d/control: split off Build-Depends-Indep
  * build and install why tactic for coq:
    - add build-dependency on libcoq-ocaml-dev
    - add coq-tactic to d/why3-coq.install
    - why3-coq: add dependencies ${ocaml:Depends} ${shlibs:Depends}
  * build with menhirlib:
    - add build-dependency on libmenhir-ocaml-dev
    - call dh_ocaml with --nodefined-map=why3-coq:MenhirLib
  * build with ocamlgraph:
    - turn build-conflict with libocamlgraph-ocaml-dev into build-dependency
    - call dh_ocaml with --nodefined-map=why3:Graph since this unit is
      also exported by libocamlgraph-ocaml-dev.
  * build with compression library:
    - added build-dependency on libzip-ocaml-dev
    - call dh_ocaml with --nodefined-map=why3-coq:Gzip,Zlib since these units
      are also exported by libzip-ocaml
  * build-dependency ocaml-nox: needs version >=3.11.2, according to
    upstream instructions.
  * added build-dependency libzarith-ocaml-dev
  * added recommendation (alternative): spass
  * added as-installed package tests:
    - why3+alt-ergo
    - why3+cvc3
    - why3+spass
  * update Vcs-* fields
  * standards-version 3.9.8 (no change)
  * patch typos: various typos found by lintian

 -- Ralf Treinen <treinen@debian.org>  Wed, 13 Apr 2016 20:48:54 +0200

why3 (0.87.0-1) unstable; urgency=low

  * Initial Release (closes: #797696)

 -- Ralf Treinen <treinen@debian.org>  Sun, 20 Mar 2016 18:44:54 +0100