Raspbian Package Auto-Building

Build log for aac-tactics (8.18.0-1) on armhf

aac-tactics → 8.18.0-1 → armhf → 2024-02-21 10:11:01 

sbuild (Debian sbuild) 0.85.0 (04 January 2023) on test2023

+==============================================================================+
| aac-tactics 8.18.0-1 (armhf)                 Wed, 21 Feb 2024 10:08:17 +0000 |
+==============================================================================+

Package: aac-tactics
Version: 8.18.0-1
Source Version: 8.18.0-1
Distribution: trixie-staging
Machine Architecture: arm64
Host Architecture: armhf
Build Architecture: armhf
Build Type: any

I: NOTICE: Log filtering will replace 'var/run/schroot/mount/trixie-staging-armhf-sbuild-f8880213-078e-45b8-80f6-26a44ce5d040' with '<<CHROOT>>'
I: NOTICE: Log filtering will replace 'build/aac-tactics-pAsd2m/resolver-RIe9I2' with '<<RESOLVERDIR>>'

+------------------------------------------------------------------------------+
| Update chroot                                                                |
+------------------------------------------------------------------------------+

Get:1 http://172.17.4.1/private trixie-staging InRelease [11.3 kB]
Get:2 http://172.17.4.1/private trixie-staging/main Sources [14.5 MB]
Get:3 http://172.17.4.1/private trixie-staging/main armhf Packages [15.1 MB]
Fetched 29.6 MB in 5s (5576 kB/s)
Reading package lists...
W: http://172.17.4.1/private/dists/trixie-staging/InRelease: Key is stored in legacy trusted.gpg keyring (/etc/apt/trusted.gpg), see the DEPRECATION section in apt-key(8) for details.

+------------------------------------------------------------------------------+
| Fetch source files                                                           |
+------------------------------------------------------------------------------+


Check APT
---------

Checking available source versions...

Download source files with APT
------------------------------

Reading package lists...
NOTICE: 'aac-tactics' packaging is maintained in the 'Git' version control system at:
https://salsa.debian.org/ocaml-team/aac-tactics.git
Please use:
git clone https://salsa.debian.org/ocaml-team/aac-tactics.git
to retrieve the latest (possibly unreleased) updates to the package.
Need to get 81.4 kB of source archives.
Get:1 http://172.17.4.1/private trixie-staging/main aac-tactics 8.18.0-1 (dsc) [2104 B]
Get:2 http://172.17.4.1/private trixie-staging/main aac-tactics 8.18.0-1 (tar) [75.6 kB]
Get:3 http://172.17.4.1/private trixie-staging/main aac-tactics 8.18.0-1 (diff) [3716 B]
Fetched 81.4 kB in 0s (1084 kB/s)
Download complete and in download only mode
I: NOTICE: Log filtering will replace 'build/aac-tactics-pAsd2m/aac-tactics-8.18.0' with '<<PKGBUILDDIR>>'
I: NOTICE: Log filtering will replace 'build/aac-tactics-pAsd2m' with '<<BUILDDIR>>'

+------------------------------------------------------------------------------+
| Install package build dependencies                                           |
+------------------------------------------------------------------------------+


Setup apt archive
-----------------

Merged Build-Depends: coq (>= 8.17), debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-core-ocaml-dev, libcoq-stdlib, ocaml, build-essential, fakeroot
Filtered Build-Depends: coq (>= 8.17), debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-core-ocaml-dev, libcoq-stdlib, ocaml, build-essential, fakeroot
dpkg-deb: building package 'sbuild-build-depends-main-dummy' in '/<<RESOLVERDIR>>/apt_archive/sbuild-build-depends-main-dummy.deb'.
Ign:1 copy:/<<RESOLVERDIR>>/apt_archive ./ InRelease
Get:2 copy:/<<RESOLVERDIR>>/apt_archive ./ Release [609 B]
Ign:3 copy:/<<RESOLVERDIR>>/apt_archive ./ Release.gpg
Get:4 copy:/<<RESOLVERDIR>>/apt_archive ./ Sources [695 B]
Get:5 copy:/<<RESOLVERDIR>>/apt_archive ./ Packages [727 B]
Fetched 2031 B in 0s (0 B/s)
Reading package lists...
Reading package lists...

Install main build dependencies (apt-based resolver)
----------------------------------------------------

Installing build dependencies
Reading package lists...
Building dependency tree...
Reading state information...
The following additional packages will be installed:
  autoconf automake autopoint autotools-dev bsdextrautils coq debhelper
  dh-autoreconf dh-coq dh-ocaml dh-strip-nondeterminism dwz file gettext
  gettext-base groff-base intltool-debian libarchive-zip-perl
  libcompiler-libs-ocaml-dev libcoq-core-ocaml libcoq-core-ocaml-dev
  libcoq-stdlib libdebhelper-perl libelf1 libexpat1
  libfile-stripnondeterminism-perl libfindlib-ocaml libfindlib-ocaml-dev
  libgmp-dev libgmp3-dev libgmpxx4ldbl libicu72 libmagic-mgc libmagic1
  libncurses-dev libncurses6 libpipeline1 libpython3-stdlib
  libpython3.11-minimal libpython3.11-stdlib libstdlib-ocaml
  libstdlib-ocaml-dev libsub-override-perl libtool libuchardet0 libxml2
  libzarith-ocaml libzarith-ocaml-dev m4 man-db media-types netbase ocaml
  ocaml-base ocaml-findlib ocaml-interp po-debconf python3 python3-minimal
  python3.11 python3.11-minimal sensible-utils
Suggested packages:
  autoconf-archive gnu-standards autoconf-doc coqide | proofgeneral ledit
  | readline-editor why coq-doc dh-make git gettext-doc libasprintf-dev
  libgettextpo-dev groff gmp-doc libgmp10-doc libmpfr-dev ncurses-doc
  libtool-doc gfortran | fortran95-compiler gcj-jdk m4-doc apparmor less
  www-browser ocaml-doc elpa-tuareg camlp4 libmail-box-perl python3-doc
  python3-tk python3-venv python3.11-venv python3.11-doc binfmt-support
Recommended packages:
  curl | wget | lynx libarchive-cpio-perl libgpm2 ocaml-man libltdl-dev ledit
  | readline-editor libmail-sendmail-perl ca-certificates
The following NEW packages will be installed:
  autoconf automake autopoint autotools-dev bsdextrautils coq debhelper
  dh-autoreconf dh-coq dh-ocaml dh-strip-nondeterminism dwz file gettext
  gettext-base groff-base intltool-debian libarchive-zip-perl
  libcompiler-libs-ocaml-dev libcoq-core-ocaml libcoq-core-ocaml-dev
  libcoq-stdlib libdebhelper-perl libelf1 libexpat1
  libfile-stripnondeterminism-perl libfindlib-ocaml libfindlib-ocaml-dev
  libgmp-dev libgmp3-dev libgmpxx4ldbl libicu72 libmagic-mgc libmagic1
  libncurses-dev libncurses6 libpipeline1 libpython3-stdlib
  libpython3.11-minimal libpython3.11-stdlib libstdlib-ocaml
  libstdlib-ocaml-dev libsub-override-perl libtool libuchardet0 libxml2
  libzarith-ocaml libzarith-ocaml-dev m4 man-db media-types netbase ocaml
  ocaml-base ocaml-findlib ocaml-interp po-debconf python3 python3-minimal
  python3.11 python3.11-minimal sbuild-build-depends-main-dummy sensible-utils
0 upgraded, 63 newly installed, 0 to remove and 0 not upgraded.
Need to get 304 MB of archives.
After this operation, 1207 MB of additional disk space will be used.
Get:1 copy:/<<RESOLVERDIR>>/apt_archive ./ sbuild-build-depends-main-dummy 0.invalid.0 [912 B]
Get:2 http://172.17.4.1/private trixie-staging/main armhf libpython3.11-minimal armhf 3.11.8-1 [801 kB]
Get:3 http://172.17.4.1/private trixie-staging/main armhf libexpat1 armhf 2.5.0-2 [76.8 kB]
Get:4 http://172.17.4.1/private trixie-staging/main armhf python3.11-minimal armhf 3.11.8-1 [1676 kB]
Get:5 http://172.17.4.1/private trixie-staging/main armhf python3-minimal armhf 3.11.6-1 [26.2 kB]
Get:6 http://172.17.4.1/private trixie-staging/main armhf media-types all 10.1.0 [26.9 kB]
Get:7 http://172.17.4.1/private trixie-staging/main armhf netbase all 6.4 [12.8 kB]
Get:8 http://172.17.4.1/private trixie-staging/main armhf libpython3.11-stdlib armhf 3.11.8-1 [1697 kB]
Get:9 http://172.17.4.1/private trixie-staging/main armhf python3.11 armhf 3.11.8-1 [597 kB]
Get:10 http://172.17.4.1/private trixie-staging/main armhf libpython3-stdlib armhf 3.11.6-1 [9224 B]
Get:11 http://172.17.4.1/private trixie-staging/main armhf python3 armhf 3.11.6-1 [26.2 kB]
Get:12 http://172.17.4.1/private trixie-staging/main armhf libuchardet0 armhf 0.0.8-1 [65.5 kB]
Get:13 http://172.17.4.1/private trixie-staging/main armhf groff-base armhf 1.23.0-3 [1033 kB]
Get:14 http://172.17.4.1/private trixie-staging/main armhf bsdextrautils armhf 2.39.3-6 [81.4 kB]
Get:15 http://172.17.4.1/private trixie-staging/main armhf libpipeline1 armhf 1.5.7-1 [33.4 kB]
Get:16 http://172.17.4.1/private trixie-staging/main armhf man-db armhf 2.12.0-3 [1358 kB]
Get:17 http://172.17.4.1/private trixie-staging/main armhf sensible-utils all 0.0.22 [22.4 kB]
Get:18 http://172.17.4.1/private trixie-staging/main armhf libmagic-mgc armhf 1:5.45-2 [314 kB]
Get:19 http://172.17.4.1/private trixie-staging/main armhf libmagic1 armhf 1:5.45-2 [96.1 kB]
Get:20 http://172.17.4.1/private trixie-staging/main armhf file armhf 1:5.45-2 [41.6 kB]
Get:21 http://172.17.4.1/private trixie-staging/main armhf gettext-base armhf 0.21-14 [157 kB]
Get:22 http://172.17.4.1/private trixie-staging/main armhf m4 armhf 1.4.19-4 [256 kB]
Get:23 http://172.17.4.1/private trixie-staging/main armhf autoconf all 2.71-3 [332 kB]
Get:24 http://172.17.4.1/private trixie-staging/main armhf autotools-dev all 20220109.1 [51.6 kB]
Get:25 http://172.17.4.1/private trixie-staging/main armhf automake all 1:1.16.5-1.3 [823 kB]
Get:26 http://172.17.4.1/private trixie-staging/main armhf autopoint all 0.21-14 [496 kB]
Get:27 http://172.17.4.1/private trixie-staging/main armhf libcoq-stdlib armhf 8.18.0+dfsg-1 [23.2 MB]
Get:28 http://172.17.4.1/private trixie-staging/main armhf libstdlib-ocaml armhf 4.14.1-1+rpi1 [458 kB]
Get:29 http://172.17.4.1/private trixie-staging/main armhf ocaml-base armhf 4.14.1-1+rpi1 [335 kB]
Get:30 http://172.17.4.1/private trixie-staging/main armhf libfindlib-ocaml armhf 1.9.6-1+b2 [167 kB]
Get:31 http://172.17.4.1/private trixie-staging/main armhf libzarith-ocaml armhf 1.13-2+b1 [100 kB]
Get:32 http://172.17.4.1/private trixie-staging/main armhf libcoq-core-ocaml armhf 8.18.0+dfsg-1 [22.8 MB]
Get:33 http://172.17.4.1/private trixie-staging/main armhf libstdlib-ocaml-dev armhf 4.14.1-1+rpi1 [7138 kB]
Get:34 http://172.17.4.1/private trixie-staging/main armhf libcompiler-libs-ocaml-dev armhf 4.14.1-1+rpi1 [32.1 MB]
Get:35 http://172.17.4.1/private trixie-staging/main armhf ocaml-interp armhf 4.14.1-1+rpi1 [6458 kB]
Get:36 http://172.17.4.1/private trixie-staging/main armhf libncurses6 armhf 6.4+20240113-1 [80.9 kB]
Get:37 http://172.17.4.1/private trixie-staging/main armhf libncurses-dev armhf 6.4+20240113-1 [289 kB]
Get:38 http://172.17.4.1/private trixie-staging/main armhf ocaml armhf 4.14.1-1+rpi1 [65.4 MB]
Get:39 http://172.17.4.1/private trixie-staging/main armhf ocaml-findlib armhf 1.9.6-1+b2 [441 kB]
Get:40 http://172.17.4.1/private trixie-staging/main armhf coq armhf 8.18.0+dfsg-1 [76.1 MB]
Get:41 http://172.17.4.1/private trixie-staging/main armhf libdebhelper-perl all 13.13 [85.0 kB]
Get:42 http://172.17.4.1/private trixie-staging/main armhf libtool all 2.4.7-7 [517 kB]
Get:43 http://172.17.4.1/private trixie-staging/main armhf dh-autoreconf all 20 [17.1 kB]
Get:44 http://172.17.4.1/private trixie-staging/main armhf libarchive-zip-perl all 1.68-1 [104 kB]
Get:45 http://172.17.4.1/private trixie-staging/main armhf libsub-override-perl all 0.10-1 [10.6 kB]
Get:46 http://172.17.4.1/private trixie-staging/main armhf libfile-stripnondeterminism-perl all 1.13.1-1 [19.4 kB]
Get:47 http://172.17.4.1/private trixie-staging/main armhf dh-strip-nondeterminism all 1.13.1-1 [8620 B]
Get:48 http://172.17.4.1/private trixie-staging/main armhf libelf1 armhf 0.188-2.1+rpi1 [171 kB]
Get:49 http://172.17.4.1/private trixie-staging/main armhf dwz armhf 0.15-1 [92.4 kB]
Get:50 http://172.17.4.1/private trixie-staging/main armhf libicu72 armhf 72.1-4 [9009 kB]
Get:51 http://172.17.4.1/private trixie-staging/main armhf libxml2 armhf 2.9.14+dfsg-1.3 [571 kB]
Get:52 http://172.17.4.1/private trixie-staging/main armhf gettext armhf 0.21-14 [1203 kB]
Get:53 http://172.17.4.1/private trixie-staging/main armhf intltool-debian all 0.35.0+20060710.6 [22.9 kB]
Get:54 http://172.17.4.1/private trixie-staging/main armhf po-debconf all 1.0.21+nmu1 [248 kB]
Get:55 http://172.17.4.1/private trixie-staging/main armhf debhelper all 13.13 [889 kB]
Get:56 http://172.17.4.1/private trixie-staging/main armhf dh-coq all 0.8 [6676 B]
Get:57 http://172.17.4.1/private trixie-staging/main armhf dh-ocaml all 2.0 [75.1 kB]
Get:58 http://172.17.4.1/private trixie-staging/main armhf libfindlib-ocaml-dev armhf 1.9.6-1+b2 [164 kB]
Get:59 http://172.17.4.1/private trixie-staging/main armhf libgmpxx4ldbl armhf 2:6.3.0+dfsg-2 [328 kB]
Get:60 http://172.17.4.1/private trixie-staging/main armhf libgmp-dev armhf 2:6.3.0+dfsg-2 [577 kB]
Get:61 http://172.17.4.1/private trixie-staging/main armhf libgmp3-dev armhf 2:6.3.0+dfsg-2 [322 kB]
Get:62 http://172.17.4.1/private trixie-staging/main armhf libzarith-ocaml-dev armhf 1.13-2+b1 [101 kB]
Get:63 http://172.17.4.1/private trixie-staging/main armhf libcoq-core-ocaml-dev armhf 8.18.0+dfsg-1 [44.7 MB]
debconf: delaying package configuration, since apt-utils is not installed
Fetched 304 MB in 34s (8838 kB/s)
Selecting previously unselected package libpython3.11-minimal:armhf.
(Reading database ... 12765 files and directories currently installed.)
Preparing to unpack .../libpython3.11-minimal_3.11.8-1_armhf.deb ...
Unpacking libpython3.11-minimal:armhf (3.11.8-1) ...
Selecting previously unselected package libexpat1:armhf.
Preparing to unpack .../libexpat1_2.5.0-2_armhf.deb ...
Unpacking libexpat1:armhf (2.5.0-2) ...
Selecting previously unselected package python3.11-minimal.
Preparing to unpack .../python3.11-minimal_3.11.8-1_armhf.deb ...
Unpacking python3.11-minimal (3.11.8-1) ...
Setting up libpython3.11-minimal:armhf (3.11.8-1) ...
Setting up libexpat1:armhf (2.5.0-2) ...
Setting up python3.11-minimal (3.11.8-1) ...
Selecting previously unselected package python3-minimal.
(Reading database ... 13081 files and directories currently installed.)
Preparing to unpack .../0-python3-minimal_3.11.6-1_armhf.deb ...
Unpacking python3-minimal (3.11.6-1) ...
Selecting previously unselected package media-types.
Preparing to unpack .../1-media-types_10.1.0_all.deb ...
Unpacking media-types (10.1.0) ...
Selecting previously unselected package netbase.
Preparing to unpack .../2-netbase_6.4_all.deb ...
Unpacking netbase (6.4) ...
Selecting previously unselected package libpython3.11-stdlib:armhf.
Preparing to unpack .../3-libpython3.11-stdlib_3.11.8-1_armhf.deb ...
Unpacking libpython3.11-stdlib:armhf (3.11.8-1) ...
Selecting previously unselected package python3.11.
Preparing to unpack .../4-python3.11_3.11.8-1_armhf.deb ...
Unpacking python3.11 (3.11.8-1) ...
Selecting previously unselected package libpython3-stdlib:armhf.
Preparing to unpack .../5-libpython3-stdlib_3.11.6-1_armhf.deb ...
Unpacking libpython3-stdlib:armhf (3.11.6-1) ...
Setting up python3-minimal (3.11.6-1) ...
Selecting previously unselected package python3.
(Reading database ... 13515 files and directories currently installed.)
Preparing to unpack .../00-python3_3.11.6-1_armhf.deb ...
Unpacking python3 (3.11.6-1) ...
Selecting previously unselected package libuchardet0:armhf.
Preparing to unpack .../01-libuchardet0_0.0.8-1_armhf.deb ...
Unpacking libuchardet0:armhf (0.0.8-1) ...
Selecting previously unselected package groff-base.
Preparing to unpack .../02-groff-base_1.23.0-3_armhf.deb ...
Unpacking groff-base (1.23.0-3) ...
Selecting previously unselected package bsdextrautils.
Preparing to unpack .../03-bsdextrautils_2.39.3-6_armhf.deb ...
Unpacking bsdextrautils (2.39.3-6) ...
Selecting previously unselected package libpipeline1:armhf.
Preparing to unpack .../04-libpipeline1_1.5.7-1_armhf.deb ...
Unpacking libpipeline1:armhf (1.5.7-1) ...
Selecting previously unselected package man-db.
Preparing to unpack .../05-man-db_2.12.0-3_armhf.deb ...
Unpacking man-db (2.12.0-3) ...
Selecting previously unselected package sensible-utils.
Preparing to unpack .../06-sensible-utils_0.0.22_all.deb ...
Unpacking sensible-utils (0.0.22) ...
Selecting previously unselected package libmagic-mgc.
Preparing to unpack .../07-libmagic-mgc_1%3a5.45-2_armhf.deb ...
Unpacking libmagic-mgc (1:5.45-2) ...
Selecting previously unselected package libmagic1:armhf.
Preparing to unpack .../08-libmagic1_1%3a5.45-2_armhf.deb ...
Unpacking libmagic1:armhf (1:5.45-2) ...
Selecting previously unselected package file.
Preparing to unpack .../09-file_1%3a5.45-2_armhf.deb ...
Unpacking file (1:5.45-2) ...
Selecting previously unselected package gettext-base.
Preparing to unpack .../10-gettext-base_0.21-14_armhf.deb ...
Unpacking gettext-base (0.21-14) ...
Selecting previously unselected package m4.
Preparing to unpack .../11-m4_1.4.19-4_armhf.deb ...
Unpacking m4 (1.4.19-4) ...
Selecting previously unselected package autoconf.
Preparing to unpack .../12-autoconf_2.71-3_all.deb ...
Unpacking autoconf (2.71-3) ...
Selecting previously unselected package autotools-dev.
Preparing to unpack .../13-autotools-dev_20220109.1_all.deb ...
Unpacking autotools-dev (20220109.1) ...
Selecting previously unselected package automake.
Preparing to unpack .../14-automake_1%3a1.16.5-1.3_all.deb ...
Unpacking automake (1:1.16.5-1.3) ...
Selecting previously unselected package autopoint.
Preparing to unpack .../15-autopoint_0.21-14_all.deb ...
Unpacking autopoint (0.21-14) ...
Selecting previously unselected package libcoq-stdlib.
Preparing to unpack .../16-libcoq-stdlib_8.18.0+dfsg-1_armhf.deb ...
Unpacking libcoq-stdlib (8.18.0+dfsg-1) ...
Selecting previously unselected package libstdlib-ocaml.
Preparing to unpack .../17-libstdlib-ocaml_4.14.1-1+rpi1_armhf.deb ...
Unpacking libstdlib-ocaml (4.14.1-1+rpi1) ...
Selecting previously unselected package ocaml-base.
Preparing to unpack .../18-ocaml-base_4.14.1-1+rpi1_armhf.deb ...
Unpacking ocaml-base (4.14.1-1+rpi1) ...
Selecting previously unselected package libfindlib-ocaml.
Preparing to unpack .../19-libfindlib-ocaml_1.9.6-1+b2_armhf.deb ...
Unpacking libfindlib-ocaml (1.9.6-1+b2) ...
Selecting previously unselected package libzarith-ocaml.
Preparing to unpack .../20-libzarith-ocaml_1.13-2+b1_armhf.deb ...
Unpacking libzarith-ocaml (1.13-2+b1) ...
Selecting previously unselected package libcoq-core-ocaml.
Preparing to unpack .../21-libcoq-core-ocaml_8.18.0+dfsg-1_armhf.deb ...
Unpacking libcoq-core-ocaml (8.18.0+dfsg-1) ...
Selecting previously unselected package libstdlib-ocaml-dev.
Preparing to unpack .../22-libstdlib-ocaml-dev_4.14.1-1+rpi1_armhf.deb ...
Unpacking libstdlib-ocaml-dev (4.14.1-1+rpi1) ...
Selecting previously unselected package libcompiler-libs-ocaml-dev.
Preparing to unpack .../23-libcompiler-libs-ocaml-dev_4.14.1-1+rpi1_armhf.deb ...
Unpacking libcompiler-libs-ocaml-dev (4.14.1-1+rpi1) ...
Selecting previously unselected package ocaml-interp.
Preparing to unpack .../24-ocaml-interp_4.14.1-1+rpi1_armhf.deb ...
Unpacking ocaml-interp (4.14.1-1+rpi1) ...
Selecting previously unselected package libncurses6:armhf.
Preparing to unpack .../25-libncurses6_6.4+20240113-1_armhf.deb ...
Unpacking libncurses6:armhf (6.4+20240113-1) ...
Selecting previously unselected package libncurses-dev:armhf.
Preparing to unpack .../26-libncurses-dev_6.4+20240113-1_armhf.deb ...
Unpacking libncurses-dev:armhf (6.4+20240113-1) ...
Selecting previously unselected package ocaml.
Preparing to unpack .../27-ocaml_4.14.1-1+rpi1_armhf.deb ...
Unpacking ocaml (4.14.1-1+rpi1) ...
Selecting previously unselected package ocaml-findlib.
Preparing to unpack .../28-ocaml-findlib_1.9.6-1+b2_armhf.deb ...
Unpacking ocaml-findlib (1.9.6-1+b2) ...
Selecting previously unselected package coq.
Preparing to unpack .../29-coq_8.18.0+dfsg-1_armhf.deb ...
Unpacking coq (8.18.0+dfsg-1) ...
Selecting previously unselected package libdebhelper-perl.
Preparing to unpack .../30-libdebhelper-perl_13.13_all.deb ...
Unpacking libdebhelper-perl (13.13) ...
Selecting previously unselected package libtool.
Preparing to unpack .../31-libtool_2.4.7-7_all.deb ...
Unpacking libtool (2.4.7-7) ...
Selecting previously unselected package dh-autoreconf.
Preparing to unpack .../32-dh-autoreconf_20_all.deb ...
Unpacking dh-autoreconf (20) ...
Selecting previously unselected package libarchive-zip-perl.
Preparing to unpack .../33-libarchive-zip-perl_1.68-1_all.deb ...
Unpacking libarchive-zip-perl (1.68-1) ...
Selecting previously unselected package libsub-override-perl.
Preparing to unpack .../34-libsub-override-perl_0.10-1_all.deb ...
Unpacking libsub-override-perl (0.10-1) ...
Selecting previously unselected package libfile-stripnondeterminism-perl.
Preparing to unpack .../35-libfile-stripnondeterminism-perl_1.13.1-1_all.deb ...
Unpacking libfile-stripnondeterminism-perl (1.13.1-1) ...
Selecting previously unselected package dh-strip-nondeterminism.
Preparing to unpack .../36-dh-strip-nondeterminism_1.13.1-1_all.deb ...
Unpacking dh-strip-nondeterminism (1.13.1-1) ...
Selecting previously unselected package libelf1:armhf.
Preparing to unpack .../37-libelf1_0.188-2.1+rpi1_armhf.deb ...
Unpacking libelf1:armhf (0.188-2.1+rpi1) ...
Selecting previously unselected package dwz.
Preparing to unpack .../38-dwz_0.15-1_armhf.deb ...
Unpacking dwz (0.15-1) ...
Selecting previously unselected package libicu72:armhf.
Preparing to unpack .../39-libicu72_72.1-4_armhf.deb ...
Unpacking libicu72:armhf (72.1-4) ...
Selecting previously unselected package libxml2:armhf.
Preparing to unpack .../40-libxml2_2.9.14+dfsg-1.3_armhf.deb ...
Unpacking libxml2:armhf (2.9.14+dfsg-1.3) ...
Selecting previously unselected package gettext.
Preparing to unpack .../41-gettext_0.21-14_armhf.deb ...
Unpacking gettext (0.21-14) ...
Selecting previously unselected package intltool-debian.
Preparing to unpack .../42-intltool-debian_0.35.0+20060710.6_all.deb ...
Unpacking intltool-debian (0.35.0+20060710.6) ...
Selecting previously unselected package po-debconf.
Preparing to unpack .../43-po-debconf_1.0.21+nmu1_all.deb ...
Unpacking po-debconf (1.0.21+nmu1) ...
Selecting previously unselected package debhelper.
Preparing to unpack .../44-debhelper_13.13_all.deb ...
Unpacking debhelper (13.13) ...
Selecting previously unselected package dh-coq.
Preparing to unpack .../45-dh-coq_0.8_all.deb ...
Unpacking dh-coq (0.8) ...
Selecting previously unselected package dh-ocaml.
Preparing to unpack .../46-dh-ocaml_2.0_all.deb ...
Unpacking dh-ocaml (2.0) ...
Selecting previously unselected package libfindlib-ocaml-dev.
Preparing to unpack .../47-libfindlib-ocaml-dev_1.9.6-1+b2_armhf.deb ...
Unpacking libfindlib-ocaml-dev (1.9.6-1+b2) ...
Selecting previously unselected package libgmpxx4ldbl:armhf.
Preparing to unpack .../48-libgmpxx4ldbl_2%3a6.3.0+dfsg-2_armhf.deb ...
Unpacking libgmpxx4ldbl:armhf (2:6.3.0+dfsg-2) ...
Selecting previously unselected package libgmp-dev:armhf.
Preparing to unpack .../49-libgmp-dev_2%3a6.3.0+dfsg-2_armhf.deb ...
Unpacking libgmp-dev:armhf (2:6.3.0+dfsg-2) ...
Selecting previously unselected package libgmp3-dev:armhf.
Preparing to unpack .../50-libgmp3-dev_2%3a6.3.0+dfsg-2_armhf.deb ...
Unpacking libgmp3-dev:armhf (2:6.3.0+dfsg-2) ...
Selecting previously unselected package libzarith-ocaml-dev.
Preparing to unpack .../51-libzarith-ocaml-dev_1.13-2+b1_armhf.deb ...
Unpacking libzarith-ocaml-dev (1.13-2+b1) ...
Selecting previously unselected package libcoq-core-ocaml-dev.
Preparing to unpack .../52-libcoq-core-ocaml-dev_8.18.0+dfsg-1_armhf.deb ...
Unpacking libcoq-core-ocaml-dev (8.18.0+dfsg-1) ...
Selecting previously unselected package sbuild-build-depends-main-dummy.
Preparing to unpack .../53-sbuild-build-depends-main-dummy_0.invalid.0_armhf.deb ...
Unpacking sbuild-build-depends-main-dummy (0.invalid.0) ...
Setting up media-types (10.1.0) ...
Setting up libpipeline1:armhf (1.5.7-1) ...
Setting up libicu72:armhf (72.1-4) ...
Setting up bsdextrautils (2.39.3-6) ...
Setting up libmagic-mgc (1:5.45-2) ...
Setting up dh-coq (0.8) ...
Setting up libarchive-zip-perl (1.68-1) ...
Setting up libdebhelper-perl (13.13) ...
Setting up dh-ocaml (2.0) ...
Setting up libmagic1:armhf (1:5.45-2) ...
Setting up gettext-base (0.21-14) ...
Setting up m4 (1.4.19-4) ...
Setting up file (1:5.45-2) ...
Setting up autotools-dev (20220109.1) ...
Setting up libcoq-stdlib (8.18.0+dfsg-1) ...
Setting up libgmpxx4ldbl:armhf (2:6.3.0+dfsg-2) ...
Setting up libncurses6:armhf (6.4+20240113-1) ...
Setting up libstdlib-ocaml (4.14.1-1+rpi1) ...
Setting up autopoint (0.21-14) ...
Setting up ocaml-base (4.14.1-1+rpi1) ...
Setting up autoconf (2.71-3) ...
Setting up sensible-utils (0.0.22) ...
Setting up libuchardet0:armhf (0.0.8-1) ...
Setting up libsub-override-perl (0.10-1) ...
Setting up netbase (6.4) ...
Setting up libelf1:armhf (0.188-2.1+rpi1) ...
Setting up libxml2:armhf (2.9.14+dfsg-1.3) ...
Setting up automake (1:1.16.5-1.3) ...
update-alternatives: using /usr/bin/automake-1.16 to provide /usr/bin/automake (automake) in auto mode
Setting up libfile-stripnondeterminism-perl (1.13.1-1) ...
Setting up libncurses-dev:armhf (6.4+20240113-1) ...
Setting up gettext (0.21-14) ...
Setting up libgmp-dev:armhf (2:6.3.0+dfsg-2) ...
Setting up libtool (2.4.7-7) ...
Setting up libstdlib-ocaml-dev (4.14.1-1+rpi1) ...
Setting up libpython3.11-stdlib:armhf (3.11.8-1) ...
Setting up libfindlib-ocaml (1.9.6-1+b2) ...
Setting up libzarith-ocaml (1.13-2+b1) ...
Setting up intltool-debian (0.35.0+20060710.6) ...
Setting up dh-autoreconf (20) ...
Setting up libcompiler-libs-ocaml-dev (4.14.1-1+rpi1) ...
Setting up ocaml-interp (4.14.1-1+rpi1) ...
Setting up ocaml-findlib (1.9.6-1+b2) ...
Setting up dh-strip-nondeterminism (1.13.1-1) ...
Setting up dwz (0.15-1) ...
Setting up libcoq-core-ocaml (8.18.0+dfsg-1) ...
Setting up groff-base (1.23.0-3) ...
Setting up libgmp3-dev:armhf (2:6.3.0+dfsg-2) ...
Setting up libpython3-stdlib:armhf (3.11.6-1) ...
Setting up python3.11 (3.11.8-1) ...
Setting up po-debconf (1.0.21+nmu1) ...
Setting up python3 (3.11.6-1) ...
Setting up ocaml (4.14.1-1+rpi1) ...
Setting up man-db (2.12.0-3) ...
Not building database; man-db/auto-update is not 'true'.
Setting up libfindlib-ocaml-dev (1.9.6-1+b2) ...
Setting up coq (8.18.0+dfsg-1) ...
Setting up libzarith-ocaml-dev (1.13-2+b1) ...
Setting up debhelper (13.13) ...
Setting up libcoq-core-ocaml-dev (8.18.0+dfsg-1) ...
Setting up sbuild-build-depends-main-dummy (0.invalid.0) ...
Processing triggers for libc-bin (2.37-15~deb13u1+rpi1) ...

+------------------------------------------------------------------------------+
| Check architectures                                                          |
+------------------------------------------------------------------------------+

Arch check ok (armhf included in any)

+------------------------------------------------------------------------------+
| Build environment                                                            |
+------------------------------------------------------------------------------+

Kernel: Linux 6.1.47-v8+ #1 SMP PREEMPT Fri Sep  1 07:05:33 BST 2023 arm64 (aarch64)
Toolchain package versions: binutils_2.41-6+rpi1 dpkg-dev_1.22.4+rpi1 g++-12_12.3.0-14+rpi1 g++-13_13.2.0-9+rpi1 gcc-12_12.3.0-14+rpi1 gcc-13_13.2.0-9+rpi1 libc6-dev_2.37-15~deb13u1+rpi1 libstdc++-12-dev_12.3.0-14+rpi1 libstdc++-13-dev_13.2.0-9+rpi1 libstdc++6_13.2.0-9+rpi1 linux-libc-dev_6.5.6-1+rpi1+b1
Package versions: adduser_3.137 apt_2.7.11 autoconf_2.71-3 automake_1:1.16.5-1.3 autopoint_0.21-14 autotools-dev_20220109.1 base-files_13+rpi1 base-passwd_3.6.3 bash_5.2.21-2 binutils_2.41-6+rpi1 binutils-arm-linux-gnueabihf_2.41-6+rpi1 binutils-common_2.41-6+rpi1 bsdextrautils_2.39.3-6 bsdutils_1:2.39.3-6 build-essential_12.10 bzip2_1.0.8-5+b2 coq_8.18.0+dfsg-1 coreutils_9.4-3 cpp_4:13.2.0-1+rpi1 cpp-12_12.3.0-14+rpi1 cpp-13_13.2.0-9+rpi1 dash_0.5.12-6 debconf_1.5.86 debhelper_13.13 debianutils_5.16 dh-autoreconf_20 dh-coq_0.8 dh-ocaml_2.0 dh-strip-nondeterminism_1.13.1-1 diffutils_1:3.10-1 dirmngr_2.2.40-1.1 dpkg_1.22.4+rpi1 dpkg-dev_1.22.4+rpi1 dwz_0.15-1 e2fsprogs_1.47.0-2 fakeroot_1.33-1 file_1:5.45-2 findutils_4.9.0-5 g++_4:13.2.0-1+rpi1 g++-12_12.3.0-14+rpi1 g++-13_13.2.0-9+rpi1 gcc_4:13.2.0-1+rpi1 gcc-10-base_10.4.0-7+rpi1 gcc-12_12.3.0-14+rpi1 gcc-12-base_12.3.0-14+rpi1 gcc-13_13.2.0-9+rpi1 gcc-13-base_13.2.0-9+rpi1 gcc-7-base_7.5.0-6+rpi1+b2 gcc-8-base_8.4.0-7+rpi1 gcc-9-base_9.4.0-2+rpi1 gettext_0.21-14 gettext-base_0.21-14 gnupg_2.2.40-1.1 gnupg-l10n_2.2.40-1.1 gnupg-utils_2.2.40-1.1 gpg_2.2.40-1.1 gpg-agent_2.2.40-1.1 gpg-wks-client_2.2.40-1.1 gpg-wks-server_2.2.40-1.1 gpgconf_2.2.40-1.1 gpgsm_2.2.40-1.1 gpgv_2.2.40-1.1 grep_3.11-4 groff-base_1.23.0-3 gzip_1.12-1 hostname_3.23+nmu2 init-system-helpers_1.66 intltool-debian_0.35.0+20060710.6 libacl1_2.3.2-1 libapt-pkg6.0_2.7.11 libarchive-zip-perl_1.68-1 libasan8_13.2.0-9+rpi1 libassuan0_2.5.6-1 libatomic1_13.2.0-9+rpi1 libattr1_1:2.5.2-1 libaudit-common_1:3.1.2-2 libaudit1_1:3.1.2-2 libbinutils_2.41-6+rpi1 libblkid1_2.39.3-6 libbz2-1.0_1.0.8-5+b2 libc-bin_2.37-15~deb13u1+rpi1 libc-dev-bin_2.37-15~deb13u1+rpi1 libc6_2.37-15~deb13u1+rpi1 libc6-dev_2.37-15~deb13u1+rpi1 libcap-ng0_0.8.4-2 libcap2_1:2.66-5 libcc1-0_13.2.0-9+rpi1 libcom-err2_1.47.0-2 libcompiler-libs-ocaml-dev_4.14.1-1+rpi1 libcoq-core-ocaml_8.18.0+dfsg-1 libcoq-core-ocaml-dev_8.18.0+dfsg-1 libcoq-stdlib_8.18.0+dfsg-1 libcrypt-dev_1:4.4.36-4 libcrypt1_1:4.4.36-4 libctf-nobfd0_2.41-6+rpi1 libctf0_2.41-6+rpi1 libdb5.3_5.3.28+dfsg2-4 libdebconfclient0_0.271 libdebhelper-perl_13.13 libdpkg-perl_1.22.4+rpi1 libelf1_0.188-2.1+rpi1 libexpat1_2.5.0-2 libext2fs2_1.47.0-2 libfakeroot_1.33-1 libffi8_3.4.4-2 libfile-find-rule-perl_0.34-3 libfile-stripnondeterminism-perl_1.13.1-1 libfindlib-ocaml_1.9.6-1+b2 libfindlib-ocaml-dev_1.9.6-1+b2 libgcc-12-dev_12.3.0-14+rpi1 libgcc-13-dev_13.2.0-9+rpi1 libgcc-s1_13.2.0-9+rpi1 libgcrypt20_1.10.3-2 libgdbm-compat4_1.23-5 libgdbm6_1.23-5 libgmp-dev_2:6.3.0+dfsg-2 libgmp10_2:6.3.0+dfsg-2 libgmp3-dev_2:6.3.0+dfsg-2 libgmpxx4ldbl_2:6.3.0+dfsg-2 libgnutls30_3.8.3-1 libgomp1_13.2.0-9+rpi1 libgpg-error0_1.47-3 libgssapi-krb5-2_1.20.1-5 libhogweed6_3.9.1-2 libicu72_72.1-4 libidn2-0_2.3.7-2 libisl23_0.26-3 libjansson4_2.14-2 libk5crypto3_1.20.1-5 libkeyutils1_1.6.3-3 libkrb5-3_1.20.1-5 libkrb5support0_1.20.1-5 libksba8_1.6.5-2 libldap-2.5-0_2.5.13+dfsg-5+rpi1+b1 liblocale-gettext-perl_1.07-6+b1 liblz4-1_1.9.4-1+rpi1+b1 liblzma5_5.4.5-0.3 libmagic-mgc_1:5.45-2 libmagic1_1:5.45-2 libmd0_1.1.0-2 libmount1_2.39.3-6 libmpc3_1.3.1-1 libmpfr6_4.2.1-1 libncurses-dev_6.4+20240113-1 libncurses6_6.4+20240113-1 libncursesw6_6.4+20240113-1 libnettle8_3.9.1-2 libnpth0_1.6-3 libnsl-dev_1.3.0-3 libnsl2_1.3.0-3 libnumber-compare-perl_0.03-3 libp11-kit0_0.25.3-4 libpam-modules_1.5.2-9.1 libpam-modules-bin_1.5.2-9.1 libpam-runtime_1.5.2-9.1 libpam0g_1.5.2-9.1 libpcre2-8-0_10.42-4 libperl5.38_5.38.2-3 libpipeline1_1.5.7-1 libpython3-stdlib_3.11.6-1 libpython3.11-minimal_3.11.8-1 libpython3.11-stdlib_3.11.8-1 libreadline8_8.2-3 libsasl2-2_2.1.28+dfsg1-4 libsasl2-modules-db_2.1.28+dfsg1-4 libseccomp2_2.5.5-1+rpi1 libselinux1_3.5-2 libsemanage-common_3.5-1 libsemanage2_3.5-1 libsepol2_3.5-2 libsframe1_2.41-6+rpi1 libsmartcols1_2.39.3-6 libsqlite3-0_3.45.1-1 libss2_1.47.0-2 libssl3_3.1.5-1 libstdc++-12-dev_12.3.0-14+rpi1 libstdc++-13-dev_13.2.0-9+rpi1 libstdc++6_13.2.0-9+rpi1 libstdlib-ocaml_4.14.1-1+rpi1 libstdlib-ocaml-dev_4.14.1-1+rpi1 libsub-override-perl_0.10-1 libsystemd0_255.3-1+rpi1 libtasn1-6_4.19.0-3 libtext-charwidth-perl_0.04-11+b1 libtext-glob-perl_0.11-3 libtext-iconv-perl_1.7-8+b1 libtinfo6_6.4+20240113-1 libtirpc-common_1.3.4+ds-1 libtirpc-dev_1.3.4+ds-1 libtirpc3_1.3.4+ds-1 libtool_2.4.7-7 libubsan1_13.2.0-9+rpi1 libuchardet0_0.0.8-1 libudev1_255.3-1+rpi1 libunistring5_1.1-2 libuuid1_2.39.3-6 libxml2_2.9.14+dfsg-1.3 libxxhash0_0.8.2-2 libzarith-ocaml_1.13-2+b1 libzarith-ocaml-dev_1.13-2+b1 libzstd1_1.5.5+dfsg2-2 linux-libc-dev_6.5.6-1+rpi1+b1 login_1:4.13+dfsg1-3 logsave_1.47.0-2 lsb-base_11.6+rpi1 m4_1.4.19-4 make_4.3-4.1 man-db_2.12.0-3 mawk_1.3.4.20240123-1 media-types_10.1.0 mount_2.39.3-6 nano_7.2-2 ncurses-base_6.4+20240113-1 ncurses-bin_6.4+20240113-1 netbase_6.4 ocaml_4.14.1-1+rpi1 ocaml-base_4.14.1-1+rpi1 ocaml-findlib_1.9.6-1+b2 ocaml-interp_4.14.1-1+rpi1 passwd_1:4.13+dfsg1-3 patch_2.7.6-7 perl_5.38.2-3 perl-base_5.38.2-3 perl-modules-5.38_5.38.2-3 pinentry-curses_1.2.1-3 po-debconf_1.0.21+nmu1 python3_3.11.6-1 python3-minimal_3.11.6-1 python3.11_3.11.8-1 python3.11-minimal_3.11.8-1 raspbian-archive-keyring_20120528.2 readline-common_8.2-3 rpcsvc-proto_1.4.3-1 sbuild-build-depends-main-dummy_0.invalid.0 sed_4.9-2 sensible-utils_0.0.22 sysvinit-utils_3.08-6 tar_1.35+dfsg-3 tzdata_2024a-1 usr-is-merged_39 usrmerge_39 util-linux_2.39.3-6 xz-utils_5.4.5-0.3 zlib1g_1:1.3.dfsg-3

+------------------------------------------------------------------------------+
| Build                                                                        |
+------------------------------------------------------------------------------+


Unpack source
-------------

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Format: 3.0 (quilt)
Source: aac-tactics
Binary: libcoq-aac-tactics
Architecture: any
Version: 8.18.0-1
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Uploaders: Stéphane Glondu <glondu@debian.org>, Julien Puydt <jpuydt@debian.org>
Homepage: https://github.com/coq-community/aac-tactics
Standards-Version: 4.6.2
Vcs-Browser: https://salsa.debian.org/ocaml-team/aac-tactics
Vcs-Git: https://salsa.debian.org/ocaml-team/aac-tactics.git
Build-Depends: coq (>= 8.17), debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-core-ocaml-dev, libcoq-stdlib, ocaml
Package-List:
 libcoq-aac-tactics deb math optional arch=any
Checksums-Sha1:
 42377897155f135ffc45764eef5c20f9fc896a79 75607 aac-tactics_8.18.0.orig.tar.gz
 e3ebf5d73982c549f398770e8edb0c149917d902 3716 aac-tactics_8.18.0-1.debian.tar.xz
Checksums-Sha256:
 f86eac00fa0e63e67cfbd9a4a1c7485f521ce00c780223f905648c0b86532a8d 75607 aac-tactics_8.18.0.orig.tar.gz
 90a1e66c3cffd5dae2d500eeb464368dcfa74293835dfdb00e7cd058461cad0c 3716 aac-tactics_8.18.0-1.debian.tar.xz
Files:
 28a2247ef3676cb0de64970f14e24fc0 75607 aac-tactics_8.18.0.orig.tar.gz
 28f9cef8bba6cace90878abf8b57e72f 3716 aac-tactics_8.18.0-1.debian.tar.xz

-----BEGIN PGP SIGNATURE-----

iQJGBAEBCgAwFiEEgS7v2KP7pKzk3xFLBMU71/4DBVEFAmWESdISHGpwdXlkdEBk
ZWJpYW4ub3JnAAoJEATFO9f+AwVRrfMP/3AOZ0voMhlXTC0gMmQfZmrok4RqhcJO
BiY1dfakfZlRRHZC9pP48ebf7UUVXzqjAwBlDfeTVvLseQq/qh/FiOQKZBKUPcU0
pXuF+ygcisMN4BAx8YrTWfwIvFcFu/3h3x+luryn6nbE4c2dlaPNttlChVgYTUEi
MvKgug7+mfB9iGMsQnknyQB1MgYia80/IunfxL6H4mCWArk4pMrFItq2dx7h/zT2
dRsOH6xkgMd0S9o0K5iKL/7C9kmVAOCDnwILAWAkwXUXxgqQJje8F32zJJWjyFGS
lm0RAchevMGyldKuo0YlZJTbtEt2jKItBUpllQst8HO6p2+cttpoMNVZhvftQNyC
ObtyO2gSwi54J9lobO/857DnIBfKC2HHtijYPQzr8dDR2gHIlbDrSfDxz6V9H4e3
PsHT5Q9XPGa8qqXeJubv5DusStaKNwOUktHgeo7fLXxafdRYC+coTCtB8RydJnNT
+OugevDH96HE6swfW05rS+fAmS7xqKPrQVUxjZOkkPgmVTbjpeG09S1tVi4cfoil
KFM6Hc3SCntrTrS2QbwXGyLQnzK6jvNOpm4CErmSaSXihVUN/4d/3B8DKB3/iTc5
HLvBhZvilNEwFq9r0ixKOl9ltmoxUgS/DRc0tBDxdvRkgCCb+C2gQwX3Y2QvLwJA
5SELSwV9bWOn
=oxzT
-----END PGP SIGNATURE-----

gpgv: Signature made Thu Dec 21 14:21:06 2023 UTC
gpgv:                using RSA key 812EEFD8A3FBA4ACE4DF114B04C53BD7FE030551
gpgv:                issuer "jpuydt@debian.org"
gpgv: Can't check signature: No public key
dpkg-source: warning: cannot verify inline signature for ./aac-tactics_8.18.0-1.dsc: no acceptable signature found
dpkg-source: info: extracting aac-tactics in /<<PKGBUILDDIR>>
dpkg-source: info: unpacking aac-tactics_8.18.0.orig.tar.gz
dpkg-source: info: unpacking aac-tactics_8.18.0-1.debian.tar.xz

Check disk space
----------------

Sufficient free space for build

User Environment
----------------

APT_CONFIG=/var/lib/sbuild/apt.conf
DEB_BUILD_OPTIONS=parallel=4
HOME=/sbuild-nonexistent
LANG=en_GB.UTF-8
LC_ALL=C.UTF-8
LOGNAME=buildd
PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games
SCHROOT_ALIAS_NAME=trixie-staging-armhf-sbuild
SCHROOT_CHROOT_NAME=trixie-staging-armhf-sbuild
SCHROOT_COMMAND=env
SCHROOT_GID=124
SCHROOT_GROUP=buildd
SCHROOT_SESSION_ID=trixie-staging-armhf-sbuild-f8880213-078e-45b8-80f6-26a44ce5d040
SCHROOT_UID=114
SCHROOT_USER=buildd
SHELL=/bin/sh
USER=buildd

dpkg-buildpackage
-----------------

Command: dpkg-buildpackage --sanitize-env -us -uc -mRaspbian pi5 test autobuilder <root@raspbian.org> -B -rfakeroot
dpkg-buildpackage: info: source package aac-tactics
dpkg-buildpackage: info: source version 8.18.0-1
dpkg-buildpackage: info: source distribution unstable
 dpkg-source --before-build .
dpkg-buildpackage: info: host architecture armhf
 debian/rules clean
dh clean --with coq,ocaml
   debian/rules override_dh_auto_clean
make[1]: Entering directory '/<<PKGBUILDDIR>>'
/usr/bin/make clean
make[2]: Entering directory '/<<PKGBUILDDIR>>'
coq_makefile -f _CoqProject -o Makefile.coq
make[3]: Entering directory '/<<PKGBUILDDIR>>'
rm -f src/aac.cmo src/coq.cmo src/helper.cmo src/search_monad.cmo src/matcher.cmo src/theory.cmo src/print.cmo src/aac_rewrite.cmo src/aac_plugin.cmo
rm -f src/aac.cmi src/coq.cmi src/helper.cmi src/search_monad.cmi src/matcher.cmi src/theory.cmi src/print.cmi src/aac_rewrite.cmi src/aac_plugin.cmi src/coq.cmi src/helper.cmi src/search_monad.cmi src/matcher.cmi src/theory.cmi src/print.cmi src/aac_rewrite.cmi
rm -f  src/aac_plugin.cma
rm -f src/aac.cmx src/coq.cmx src/helper.cmx src/search_monad.cmx src/matcher.cmx src/theory.cmx src/print.cmx src/aac_rewrite.cmx src/aac_plugin.cmx
rm -f src/aac_plugin.cmxa
rm -f src/aac_plugin.cmxs src/aac_plugin.cmxs 
rm -f src/aac.o src/coq.o src/helper.o src/search_monad.o src/matcher.o src/theory.o src/print.o src/aac_rewrite.o src/aac_plugin.o
rm -f src/aac_plugin.a
rm -f src/aac.ml
rm -f src/aac.cmt src/coq.cmt src/helper.cmt src/search_monad.cmt src/matcher.cmt src/theory.cmt src/print.cmt src/aac_rewrite.cmt src/aac_plugin.cmt
rm -f src/coq.cmti src/helper.cmti src/search_monad.cmti src/matcher.cmti src/theory.cmti src/print.cmti src/aac_rewrite.cmti
rm -f src/aac.mlg.d src/coq.ml.d src/helper.ml.d src/search_monad.ml.d src/matcher.ml.d src/theory.ml.d src/print.ml.d src/aac_rewrite.ml.d src/aac_plugin.mlpack.d src/coq.mli.d src/helper.mli.d src/search_monad.mli.d src/matcher.mli.d src/theory.mli.d src/print.mli.d src/aac_rewrite.mli.d .Makefile.coq.d
rm -f 
find . -name .coq-native -type d -empty -delete
rm -f theories/Utils.vo theories/Constants.vo theories/AAC.vo theories/Instances.vo theories/Tutorial.vo theories/Caveats.vo
rm -f theories/Utils.vio theories/Constants.vio theories/AAC.vio theories/Instances.vio theories/Tutorial.vio theories/Caveats.vio
rm -f theories/Utils.vos theories/Constants.vos theories/AAC.vos theories/Instances.vos theories/Tutorial.vos theories/Caveats.vos
rm -f theories/Utils.vok theories/Constants.vok theories/AAC.vok theories/Instances.vok theories/Tutorial.vok theories/Caveats.vok
rm -f theories/Utils.v.beautified theories/Constants.v.beautified theories/AAC.v.beautified theories/Instances.v.beautified theories/Tutorial.v.beautified theories/Caveats.v.beautified theories/Utils.v.old theories/Constants.v.old theories/AAC.v.old theories/Instances.v.old theories/Tutorial.v.old theories/Caveats.v.old
rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
rm -f theories/Utils.glob theories/Constants.glob theories/AAC.glob theories/Instances.glob theories/Tutorial.glob theories/Caveats.glob
rm -f theories/Utils.tex theories/Constants.tex theories/AAC.tex theories/Instances.tex theories/Tutorial.tex theories/Caveats.tex
rm -f theories/Utils.g.tex theories/Constants.g.tex theories/AAC.g.tex theories/Instances.g.tex theories/Tutorial.g.tex theories/Caveats.g.tex
rm -f pretty-timed-success.ok
rm -f META
rm -rf html mlihtml
rm -f theories/.Utils.aux theories/.Constants.aux theories/.AAC.aux theories/.Instances.aux theories/.Tutorial.aux theories/.Caveats.aux
rm -f time-of-build.log time-of-build-before.log time-of-build-after.log time-of-build-pretty.log time-of-build-both.log
rm -f theories/Utils.v.timing theories/Constants.v.timing theories/AAC.v.timing theories/Instances.v.timing theories/Tutorial.v.timing theories/Caveats.v.timing
rm -f theories/Utils.v.before-timing theories/Constants.v.before-timing theories/AAC.v.before-timing theories/Instances.v.before-timing theories/Tutorial.v.before-timing theories/Caveats.v.before-timing
rm -f theories/Utils.v.after-timing theories/Constants.v.after-timing theories/AAC.v.after-timing theories/Instances.v.after-timing theories/Tutorial.v.after-timing theories/Caveats.v.after-timing
rm -f theories/Utils.v.timing.diff theories/Constants.v.timing.diff theories/AAC.v.timing.diff theories/Instances.v.timing.diff theories/Tutorial.v.timing.diff theories/Caveats.v.timing.diff
rm -f .lia.cache .nia.cache
make[3]: Leaving directory '/<<PKGBUILDDIR>>'
make[2]: Leaving directory '/<<PKGBUILDDIR>>'
rm src/META.coq-aac-tactics
make[1]: Leaving directory '/<<PKGBUILDDIR>>'
   dh_ocamlclean
   dh_clean
 debian/rules binary-arch
dh binary-arch --with coq,ocaml
   dh_update_autotools_config -a
   dh_autoreconf -a
   dh_ocamlinit -a
   dh_auto_configure -a
   debian/rules override_dh_auto_build
make[1]: Entering directory '/<<PKGBUILDDIR>>'
/usr/bin/make Makefile.coq
make[2]: Entering directory '/<<PKGBUILDDIR>>'
coq_makefile -f _CoqProject -o Makefile.coq
make[2]: Leaving directory '/<<PKGBUILDDIR>>'
/usr/bin/make -f Makefile.coq opt byte html
make[2]: Entering directory '/<<PKGBUILDDIR>>'
"coqdep" -m "src/META.coq-aac-tactics" -vos -dyndep var -f _CoqProject   > ".Makefile.coq.d" || ( RV=$?; rm -f ".Makefile.coq.d"; exit $RV )
"coqpp" src/aac.mlg
"/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/aac_rewrite.mli" > "src/aac_rewrite.mli.d" || ( RV=$?; rm -f "src/aac_rewrite.mli.d"; exit $RV )
"/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/print.mli" > "src/print.mli.d" || ( RV=$?; rm -f "src/print.mli.d"; exit $RV )
"/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/theory.mli" > "src/theory.mli.d" || ( RV=$?; rm -f "src/theory.mli.d"; exit $RV )
"/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/matcher.mli" > "src/matcher.mli.d" || ( RV=$?; rm -f "src/matcher.mli.d"; exit $RV )
"/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/search_monad.mli" > "src/search_monad.mli.d" || ( RV=$?; rm -f "src/search_monad.mli.d"; exit $RV )
"/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/helper.mli" > "src/helper.mli.d" || ( RV=$?; rm -f "src/helper.mli.d"; exit $RV )
"/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/coq.mli" > "src/coq.mli.d" || ( RV=$?; rm -f "src/coq.mli.d"; exit $RV )
"ocamllibdep" -c -I src "src/aac_plugin.mlpack" > "src/aac_plugin.mlpack.d" || ( RV=$?; rm -f "src/aac_plugin.mlpack.d"; exit $RV )
"/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/aac_rewrite.ml" > "src/aac_rewrite.ml.d" || ( RV=$?; rm -f "src/aac_rewrite.ml.d"; exit $RV )
"/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/print.ml" > "src/print.ml.d" || ( RV=$?; rm -f "src/print.ml.d"; exit $RV )
"/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/theory.ml" > "src/theory.ml.d" || ( RV=$?; rm -f "src/theory.ml.d"; exit $RV )
"/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/matcher.ml" > "src/matcher.ml.d" || ( RV=$?; rm -f "src/matcher.ml.d"; exit $RV )
"/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/search_monad.ml" > "src/search_monad.ml.d" || ( RV=$?; rm -f "src/search_monad.ml.d"; exit $RV )
"/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/helper.ml" > "src/helper.ml.d" || ( RV=$?; rm -f "src/helper.ml.d"; exit $RV )
"/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/coq.ml" > "src/coq.ml.d" || ( RV=$?; rm -f "src/coq.ml.d"; exit $RV )
"/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/aac.ml" > "src/aac.mlg.d" || ( RV=$?; rm -f "src/aac.mlg.d"; exit $RV )
/usr/bin/make all "OPT:=-opt" -f "Makefile.coq"
make[3]: Entering directory '/<<PKGBUILDDIR>>'
/usr/bin/make --no-print-directory -f "Makefile.coq" pre-all
if [ "8.18.0" != "8.18.0" ]; then\
  echo "W: This Makefile was generated by Coq 8.18.0";\
  echo "W: while the current Coq version is 8.18.0";\
fi
/usr/bin/make --no-print-directory -f "Makefile.coq" real-all
"coqc"   -q '-w' '+default'  "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I src -Q theories AAC_tactics -Q src AAC_tactics  theories/Utils.v
"coqc"   -q '-w' '+default'  "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I src -Q theories AAC_tactics -Q src AAC_tactics  theories/Constants.v
"/usr/bin/ocamlfind" ocamlc   -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  src/coq.mli
"/usr/bin/ocamlfind" opt      -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  -for-pack Aac_plugin src/coq.ml
"/usr/bin/ocamlfind" ocamlc   -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  src/helper.mli
"/usr/bin/ocamlfind" opt      -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  -for-pack Aac_plugin src/helper.ml
"/usr/bin/ocamlfind" ocamlc   -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  src/search_monad.mli
"/usr/bin/ocamlfind" opt      -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  -for-pack Aac_plugin src/search_monad.ml
"/usr/bin/ocamlfind" ocamlc   -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  src/matcher.mli
"/usr/bin/ocamlfind" opt      -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  -for-pack Aac_plugin src/matcher.ml
"/usr/bin/ocamlfind" ocamlc   -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  src/theory.mli
"/usr/bin/ocamlfind" opt      -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  -for-pack Aac_plugin src/theory.ml
"/usr/bin/ocamlfind" ocamlc   -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  src/print.mli
"/usr/bin/ocamlfind" opt      -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  -for-pack Aac_plugin src/print.ml
"/usr/bin/ocamlfind" ocamlc   -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  src/aac_rewrite.mli
"/usr/bin/ocamlfind" opt      -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  -for-pack Aac_plugin src/aac_rewrite.ml
"/usr/bin/ocamlfind" opt      -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  -for-pack Aac_plugin src/aac.ml
"/usr/bin/ocamlfind" opt      -linkall  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  -pack -o src/aac_plugin.cmx src/coq.cmx src/helper.cmx src/search_monad.cmx src/matcher.cmx src/theory.cmx src/print.cmx src/aac_rewrite.cmx src/aac.cmx
"/usr/bin/ocamlfind" opt      -linkall  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  -a -o src/aac_plugin.cmxa src/aac_plugin.cmx
"/usr/bin/ocamlfind" opt      -linkall  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  \
	-shared -o src/aac_plugin.cmxs src/aac_plugin.cmxa
"coqc"   -q '-w' '+default'  "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I src -Q theories AAC_tactics -Q src AAC_tactics  theories/AAC.v
"coqc"   -q '-w' '+default'  "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I src -Q theories AAC_tactics -Q src AAC_tactics  theories/Instances.v
"coqc"   -q '-w' '+default'  "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I src -Q theories AAC_tactics -Q src AAC_tactics  theories/Tutorial.v
All solutions:
occurrence 0: transitivity through forall x : X, plus x x
1 possible(s) substitution(s)
0:	[x: f (a + a); ]

occurrence 1: transitivity through forall x : X,
                                    plus (f (x + x)) (f (a + a))
1 possible(s) substitution(s)
0:	[x: a; ]


All solutions:
occurrence 0: transitivity through forall x y : X, dot (a * x * y) b
3 possible(s) substitution(s)
0:	[x: c; y: dot (d * c) d; ]
1:	[x: dot c d; y: dot c d; ]
2:	[x: dot (c * d) c; y: d; ]


All solutions:
occurrence 0: transitivity through forall x y : X, dot (a * x * y) b
4 possible(s) substitution(s)
0:	[x: c; y: dot (d * c * d) b; ]
1:	[x: dot c d; y: dot (c * d) b; ]
2:	[x: dot (c * d) c; y: dot d b; ]
3:	[x: dot (c * d * c) d; y: b; ]

occurrence 1: transitivity through forall x y : X, dot (a * x * y * b) b
3 possible(s) substitution(s)
0:	[x: c; y: dot (d * c) d; ]
1:	[x: dot c d; y: dot c d; ]
2:	[x: dot (c * d) c; y: d; ]


All solutions:
occurrence 0: transitivity through forall x y : X, dot (a * x * y) b
1 possible(s) substitution(s)
0:	[x: plus (c * d) (c * d); y: b; ]


All solutions:
occurrence 0: transitivity through forall x : X, dot (a * x) a
1 possible(s) substitution(s)
0:	[x: 1; ]


All solutions:
occurrence 0: transitivity through forall x y z : X,
                                   plus (x * y + x * z) (a * b)
2 possible(s) substitution(s)
0:	[x: a; y: c; z: dot b c; ]
1:	[x: a; y: dot b c; z: c; ]

occurrence 1: transitivity through forall x y z : X,
                                    plus (x * y + x * z) (a * c)
2 possible(s) substitution(s)
0:	[x: a; y: dot b c; z: b; ]
1:	[x: a; y: b; z: dot b c; ]

occurrence 2: transitivity through forall x y z : X,
                                    plus (x * y + x * z) (a * b * c)
2 possible(s) substitution(s)
0:	[x: a; y: c; z: b; ]
1:	[x: a; y: b; z: c; ]


File "./theories/Tutorial.v", line 227, characters 6-24:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through forall x y z : X, plus (x * y) (x * z)
6 possible(s) substitution(s)
0:	[x: 1; y: dot a (b * c + c); z: dot a b; ]
1:	[x: a; y: plus (b * c) c; z: b; ]
2:	[x: 1; y: 0; z: plus (a * (b * c + c)) (a * b); ]
3:	[x: 1; y: plus (a * (b * c + c)) (a * b); z: 0; ]
4:	[x: 1; y: dot a b; z: dot a (b * c + c); ]
5:	[x: a; y: b; z: plus (b * c) c; ]

occurrence 1: transitivity through forall x y z : X,
                                    plus (x * y + x * z) (a * b)
2 possible(s) substitution(s)
0:	[x: 1; y: dot a (b * c + c); z: 0; ]
1:	[x: 1; y: 0; z: dot a (b * c + c); ]

occurrence 2: transitivity through forall x y z : X,
                                    plus (a * (x * y + x * z)) (a * b)
4 possible(s) substitution(s)
0:	[x: 1; y: dot b c; z: c; ]
1:	[x: 1; y: 0; z: plus (b * c) c; ]
2:	[x: 1; y: plus (b * c) c; z: 0; ]
3:	[x: 1; y: c; z: dot b c; ]

occurrence 3: transitivity through forall x y z : X,
                                    plus (a * (x * y + x * z + c)) (a * b)
2 possible(s) substitution(s)
0:	[x: 1; y: dot b c; z: 0; ]
1:	[x: 1; y: 0; z: dot b c; ]

occurrence 4: transitivity through forall x y z : X,
                                    plus (x * y + x * z) (a * (b * c + c))
2 possible(s) substitution(s)
0:	[x: 1; y: dot a b; z: 0; ]
1:	[x: 1; y: 0; z: dot a b; ]

occurrence 5: transitivity through forall x y z : X,
                                    plus (a * (b * (x * y + x * z) + c))
                                      (a * b)
2 possible(s) substitution(s)
0:	[x: 1; y: c; z: 0; ]
1:	[x: 1; y: 0; z: c; ]

occurrence 6: transitivity through forall x y z : X,
                                    plus (a * ((x * y + x * z) * c + c))
                                      (a * b)
2 possible(s) substitution(s)
0:	[x: 1; y: b; z: 0; ]
1:	[x: 1; y: 0; z: b; ]

occurrence 7: transitivity through forall x y z : X,
                                    plus (a * (x * y + x * z + b * c))
                                      (a * b)
2 possible(s) substitution(s)
0:	[x: 1; y: c; z: 0; ]
1:	[x: 1; y: 0; z: c; ]

occurrence 8: transitivity through forall x y z : X,
                                    plus ((x * y + x * z) * (b * c + c))
                                      (a * b)
2 possible(s) substitution(s)
0:	[x: 1; y: a; z: 0; ]
1:	[x: 1; y: 0; z: a; ]

occurrence 9: transitivity through forall x y z : X,
                                    plus (a * (x * y + x * z))
                                      (a * (b * c + c))
2 possible(s) substitution(s)
0:	[x: 1; y: b; z: 0; ]
1:	[x: 1; y: 0; z: b; ]

occurrence 10: transitivity through forall x y z : X,
                                     plus ((x * y + x * z) * b)
                                       (a * (b * c + c))
2 possible(s) substitution(s)
0:	[x: 1; y: a; z: 0; ]
1:	[x: 1; y: 0; z: a; ]

occurrence 11: transitivity through plus (a * (b * c + c))
                                       ((1 * 1 + 1 * 0) * (a * b))

occurrence 12: transitivity through 
plus (a * (b * c + c)) (a * b * (1 * 1 + 1 * 0))

occurrence 13: transitivity through 
plus (a * (b * c + c)) (a * ((1 * 1 + 1 * 0) * b))

occurrence 14: transitivity through 
plus (a * b) ((1 * 1 + 1 * 0) * (a * (b * c + c)))

occurrence 15: transitivity through 
plus (a * b) (a * (b * c + c) * (1 * 1 + 1 * 0))

occurrence 16: transitivity through 
plus (a * b) (a * (b * c + (1 * 1 + 1 * 0) * c))

occurrence 17: transitivity through 
plus (a * b) (a * (b * c + c * (1 * 1 + 1 * 0)))

occurrence 18: transitivity through 
plus (a * b) (a * (c + (1 * 1 + 1 * 0) * (b * c)))

occurrence 19: transitivity through 
plus (a * b) (a * (c + b * c * (1 * 1 + 1 * 0)))

occurrence 20: transitivity through 
plus (a * b) (a * (c + b * ((1 * 1 + 1 * 0) * c)))

occurrence 21: transitivity through 
plus (a * b) (a * ((1 * 1 + 1 * 0) * (b * c + c)))

occurrence 22: transitivity through 
dot (a * (b * c + c) + a * b) (1 * 1 + 1 * 0)

occurrence 23: transitivity through 
dot (1 * 1 + 1 * 0) (a * (b * c + c) + a * b)

occurrence 24: transitivity through 
plus (a * (b * c + c)) ((1 * 0 + 1 * 1) * (a * b))

occurrence 25: transitivity through 
plus (a * (b * c + c)) (a * b * (1 * 0 + 1 * 1))

occurrence 26: transitivity through 
plus (a * (b * c + c)) (a * ((1 * 0 + 1 * 1) * b))

occurrence 27: transitivity through 
plus (a * b) ((1 * 0 + 1 * 1) * (a * (b * c + c)))

occurrence 28: transitivity through 
plus (a * b) (a * (b * c + c) * (1 * 0 + 1 * 1))

occurrence 29: transitivity through 
plus (a * b) (a * (b * c + (1 * 0 + 1 * 1) * c))

occurrence 30: transitivity through 
plus (a * b) (a * (b * c + c * (1 * 0 + 1 * 1)))

occurrence 31: transitivity through 
plus (a * b) (a * (c + (1 * 0 + 1 * 1) * (b * c)))

occurrence 32: transitivity through 
plus (a * b) (a * (c + b * c * (1 * 0 + 1 * 1)))

occurrence 33: transitivity through 
plus (a * b) (a * (c + b * ((1 * 0 + 1 * 1) * c)))

occurrence 34: transitivity through 
plus (a * b) (a * ((1 * 0 + 1 * 1) * (b * c + c)))

occurrence 35: transitivity through 
dot (a * (b * c + c) + a * b) (1 * 0 + 1 * 1)

occurrence 36: transitivity through 
dot (1 * 0 + 1 * 1) (a * (b * c + c) + a * b)

occurrence 37: transitivity through 
plus (a * (b * c + c) + a * b) (1 * 0 + 1 * 0)

occurrence 38: transitivity through 
plus (a * (b * c + c)) (a * (b + (1 * 0 + 1 * 0)))

occurrence 39: transitivity through 
plus (a * (b * c + c)) ((a + (1 * 0 + 1 * 0)) * b)

occurrence 40: transitivity through 
plus (a * b) (a * (b * c + c + (1 * 0 + 1 * 0)))

occurrence 41: transitivity through 
plus (a * b) (a * (c + b * (c + (1 * 0 + 1 * 0))))

occurrence 42: transitivity through 
plus (a * b) (a * (c + (b + (1 * 0 + 1 * 0)) * c))

occurrence 43: transitivity through 
plus (a * b) ((a + (1 * 0 + 1 * 0)) * (b * c + c))

occurrence 44: transitivity through 
plus (a * (b * c + c) + a * b) (0 * 1 + 0 * 1)

occurrence 45: transitivity through 
plus (a * (b * c + c)) (a * (b + (0 * 1 + 0 * 1)))

occurrence 46: transitivity through 
plus (a * (b * c + c)) ((a + (0 * 1 + 0 * 1)) * b)

occurrence 47: transitivity through 
plus (a * b) (a * (b * c + c + (0 * 1 + 0 * 1)))

occurrence 48: transitivity through 
plus (a * b) (a * (c + b * (c + (0 * 1 + 0 * 1))))

occurrence 49: transitivity through 
plus (a * b) (a * (c + (b + (0 * 1 + 0 * 1)) * c))

occurrence 50: transitivity through 
plus (a * b) ((a + (0 * 1 + 0 * 1)) * (b * c + c))

occurrence 51: transitivity through 
plus (a * (b * c + c)) (a * b * (1 + (1 * 0 + 1 * 0)))

occurrence 52: transitivity through 
plus (a * (b * c + c)) (a * ((1 + (1 * 0 + 1 * 0)) * b))

occurrence 53: transitivity through 
plus (a * (b * c + c)) ((1 + (1 * 0 + 1 * 0)) * (a * b))

occurrence 54: transitivity through 
plus (a * b) (a * (b * c + c) * (1 + (1 * 0 + 1 * 0)))

occurrence 55: transitivity through 
plus (a * b) (a * (c + b * c * (1 + (1 * 0 + 1 * 0))))

occurrence 56: transitivity through 
plus (a * b) (a * (c + b * ((1 + (1 * 0 + 1 * 0)) * c)))

occurrence 57: transitivity through 
plus (a * b) (a * (c + (1 + (1 * 0 + 1 * 0)) * (b * c)))

occurrence 58: transitivity through 
plus (a * b) (a * ((1 + (1 * 0 + 1 * 0)) * (b * c + c)))

occurrence 59: transitivity through 
plus (a * b) ((1 + (1 * 0 + 1 * 0)) * (a * (b * c + c)))

occurrence 60: transitivity through 
plus (a * (b * c + c)) (a * b * (1 + (0 * 1 + 0 * 1)))

occurrence 61: transitivity through 
plus (a * (b * c + c)) (a * ((1 + (0 * 1 + 0 * 1)) * b))

occurrence 62: transitivity through 
plus (a * (b * c + c)) ((1 + (0 * 1 + 0 * 1)) * (a * b))

occurrence 63: transitivity through 
plus (a * b) (a * (b * c + c) * (1 + (0 * 1 + 0 * 1)))

occurrence 64: transitivity through 
plus (a * b) (a * (c + b * c * (1 + (0 * 1 + 0 * 1))))

occurrence 65: transitivity through 
plus (a * b) (a * (c + b * ((1 + (0 * 1 + 0 * 1)) * c)))

occurrence 66: transitivity through 
plus (a * b) (a * (c + (1 + (0 * 1 + 0 * 1)) * (b * c)))

occurrence 67: transitivity through 
plus (a * b) (a * ((1 + (0 * 1 + 0 * 1)) * (b * c + c)))

occurrence 68: transitivity through 
plus (a * b) ((1 + (0 * 1 + 0 * 1)) * (a * (b * c + c)))


All solutions:
occurrence 0: transitivity through forall x y z : nat,
                                   Nat.max (x + y) (x + z)
2 possible(s) substitution(s)
0:	[x: a; y: b; z: c; ]
1:	[x: a; y: c; z: b; ]


All solutions:
occurrence 0: transitivity through forall x y z : nat,
                                   Nat.max (x + y) (x + z)
2 possible(s) substitution(s)
0:	[x: a; y: b; z: c; ]
1:	[x: a; y: c; z: b; ]


(lift_reflexivity
   (let env_sym :=
      sigma_get
        {|
          Internal.Sym.ar := 0;
          Internal.Sym.value := b;
          Internal.Sym.morph := proper_eq b
        |}
        (sigma_add 1%positive
           {|
             Internal.Sym.ar := 0;
             Internal.Sym.value := a;
             Internal.Sym.morph := proper_eq a
           |} (sigma_empty Internal.Sym.pack)) in
    let env_bin :=
      sigma_get
        {|
          Internal.Bin.value := Z.max;
          Internal.Bin.compat := Z.max_compat;
          Internal.Bin.assoc := aac_Z_max_Assoc;
          Internal.Bin.comm := Some aac_Z_max_Comm;
          Internal.Bin.idem := Some aac_Z_max_Idem
        |}
        (sigma_add 2%positive
           {|
             Internal.Bin.value := Z.add;
             Internal.Bin.compat := reflexive_proper Z.add;
             Internal.Bin.assoc := aac_Z_add_Assoc;
             Internal.Bin.comm := Some aac_Z_add_Comm;
             Internal.Bin.idem := None
           |} (sigma_empty Internal.Bin.pack)) in
    let env_units :=
      sigma_get
        {|
          Internal.u_value := 0;
          Internal.u_desc :=
            {| Internal.uf_idx := 2; Internal.uf_desc := aac_Z_add_0_Unit |}
            :: nil
        |} (sigma_empty (Internal.unit_pack env_bin)) in
    let tty := Internal.T env_sym in
    let rsum := Internal.sum (e_sym:=env_sym) in
    let rprd := Internal.prd (e_sym:=env_sym) in
    let rsym := Internal.sym (e_sym:=env_sym) in
    let vnil := Internal.vnil env_sym in
    let vcons := Internal.vcons (e_sym:=env_sym) in
    let eval := Internal.eval (e_sym:=env_sym) env_units in
    let left :=
      rsum 1%positive
        (Utils.cons
           (rsum 2%positive
              (Utils.cons (rsym 1%positive vnil, 1%positive)
                 (Utils.nil (rsym 2%positive vnil, 1%positive))), 1%positive)
           (Utils.nil
              (rsum 2%positive
                 (Utils.cons (rsym 2%positive vnil, 1%positive)
                    (Utils.nil (rsym 1%positive vnil, 1%positive))),
               1%positive))) in
    let right :=
      rsum 2%positive
        (Utils.cons (rsym 1%positive vnil, 1%positive)
           (Utils.nil (rsym 2%positive vnil, 1%positive))) in
    Internal.decide env_units left right
      (eq_refl
       :
       Internal.compare (Internal.norm env_units left)
         (Internal.norm env_units right) = Eq)
    <:
    Z.max (a + b) (b + a) = a + b))
File "./theories/Tutorial.v", line 399, characters 4-36:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through (Z.abs a + - Z.abs b + 0)%Z

occurrence 1: transitivity through 
(Z.abs a + - (Z.abs b + 0))%Z

occurrence 2: transitivity through 
(Z.abs a + - Z.abs (b + 0))%Z

occurrence 3: transitivity through 
(- Z.abs b + Z.abs (a + 0))%Z


File "./theories/Tutorial.v", line 400, characters 4-39:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
"coqc"   -q '-w' '+default'  "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I src -Q theories AAC_tactics -Q src AAC_tactics  theories/Caveats.v
All solutions:
occurrence 0: transitivity through forall x : Z, (- (x + x) + (b + b + c))%Z
1 possible(s) substitution(s)
0:	[x: a; ]

occurrence 1: transitivity through forall x : Z, (x + x + (- (a + a) + c))%Z
1 possible(s) substitution(s)
0:	[x: b; ]


File "./theories/Caveats.v", line 294, characters 4-32:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through dot y 1

occurrence 1: transitivity through 
dot 1 y


File "./theories/Caveats.v", line 295, characters 4-35:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
File "./theories/Caveats.v", line 315, characters 4-18:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
File "./theories/Caveats.v", line 320, characters 4-23:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
File "./theories/Caveats.v", line 347, characters 4-21:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through (c * b + a + 0)%nat

occurrence 1: transitivity through 
(a + b * (c + 0))%nat

occurrence 2: transitivity through 
(a + c * (b + 0))%nat


File "./theories/Caveats.v", line 364, characters 4-28:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through (c + b + a + 0)%nat


File "./theories/Caveats.v", line 366, characters 4-28:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through ((c + b + a) * 1)%nat

occurrence 1: transitivity through 
(c + a + b * 1)%nat

occurrence 2: transitivity through 
(a + (c + b) * 1)%nat

occurrence 3: transitivity through 
(b + a + c * 1)%nat

occurrence 4: transitivity through 
(c + (b + a) * 1)%nat

occurrence 5: transitivity through 
(c + b + a * 1)%nat

occurrence 6: transitivity through 
(b + (c + a) * 1)%nat


All solutions:
occurrence 0: transitivity through forall x y : nat, (x * x + y * x + c)%nat
1 possible(s) substitution(s)
0:	[x: a; y: b; ]


File "./theories/Caveats.v", line 384, characters 4-24:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through forall x y : nat, (x * x + y * x + c)%nat
1 possible(s) substitution(s)
0:	[x: a; y: b; ]

occurrence 1: transitivity through ((a * b + a * a + c) * (1 * 1 + 0 * 1))%nat

occurrence 2: transitivity through 
(a * b + c + a * a * (1 * 1 + 0 * 1))%nat

occurrence 3: transitivity through 
(c + (a * b + a * a) * (1 * 1 + 0 * 1))%nat

occurrence 4: transitivity through 
(a * a + c + a * b * (1 * 1 + 0 * 1))%nat

occurrence 5: transitivity through 
(a * b + (a * a + c) * (1 * 1 + 0 * 1))%nat

occurrence 6: transitivity through 
(a * b + a * a + c * (1 * 1 + 0 * 1))%nat

occurrence 7: transitivity through 
(a * a + (a * b + c) * (1 * 1 + 0 * 1))%nat


File "./theories/Caveats.v", line 386, characters 4-22:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through ((a * b + a * a + c) * 1)%nat

occurrence 1: transitivity through 
(a * b + c + a * a * 1)%nat

occurrence 2: transitivity through 
(c + (a * b + a * a) * 1)%nat

occurrence 3: transitivity through 
(a * a + c + a * b * 1)%nat

occurrence 4: transitivity through 
(a * b + (a * a + c) * 1)%nat

occurrence 5: transitivity through 
(a * b + a * a + c * 1)%nat

occurrence 6: transitivity through 
(a * a + (a * b + c) * 1)%nat


/usr/bin/make --no-print-directory -f "Makefile.coq" post-all
make[3]: Leaving directory '/<<PKGBUILDDIR>>'
/usr/bin/make all "OPT:=-byte" -f "Makefile.coq"
make[3]: Entering directory '/<<PKGBUILDDIR>>'
/usr/bin/make --no-print-directory -f "Makefile.coq" pre-all
if [ "8.18.0" != "8.18.0" ]; then\
  echo "W: This Makefile was generated by Coq 8.18.0";\
  echo "W: while the current Coq version is 8.18.0";\
fi
/usr/bin/make --no-print-directory -f "Makefile.coq" real-all
"/usr/bin/ocamlfind" ocamlc   -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  src/coq.ml
"/usr/bin/ocamlfind" ocamlc   -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  src/helper.ml
"/usr/bin/ocamlfind" ocamlc   -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  src/search_monad.ml
"/usr/bin/ocamlfind" ocamlc   -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  src/matcher.ml
"/usr/bin/ocamlfind" ocamlc   -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  src/theory.ml
"/usr/bin/ocamlfind" ocamlc   -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  src/print.ml
"/usr/bin/ocamlfind" ocamlc   -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  src/aac_rewrite.ml
"/usr/bin/ocamlfind" ocamlc   -c  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  src/aac.ml
"/usr/bin/ocamlfind" ocamlc   -linkall  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  -pack -o src/aac_plugin.cmo src/coq.cmo src/helper.cmo src/search_monad.cmo src/matcher.cmo src/theory.cmo src/print.cmo src/aac_rewrite.cmo src/aac.cmo
"/usr/bin/ocamlfind" ocamlc   -linkall  -thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -I src  -warn-error +a-3 -package coq-core.plugins.ltac  -a -o src/aac_plugin.cma src/aac_plugin.cmo
"coqc"   -q '-w' '+default'  "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I src -Q theories AAC_tactics -Q src AAC_tactics  theories/AAC.v
"coqc"   -q '-w' '+default'  "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I src -Q theories AAC_tactics -Q src AAC_tactics  theories/Instances.v
"coqc"   -q '-w' '+default'  "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I src -Q theories AAC_tactics -Q src AAC_tactics  theories/Tutorial.v
All solutions:
occurrence 0: transitivity through forall x : X, plus x x
1 possible(s) substitution(s)
0:	[x: f (a + a); ]

occurrence 1: transitivity through forall x : X,
                                    plus (f (x + x)) (f (a + a))
1 possible(s) substitution(s)
0:	[x: a; ]


All solutions:
occurrence 0: transitivity through forall x y : X, dot (a * x * y) b
3 possible(s) substitution(s)
0:	[x: c; y: dot (d * c) d; ]
1:	[x: dot c d; y: dot c d; ]
2:	[x: dot (c * d) c; y: d; ]


All solutions:
occurrence 0: transitivity through forall x y : X, dot (a * x * y) b
4 possible(s) substitution(s)
0:	[x: c; y: dot (d * c * d) b; ]
1:	[x: dot c d; y: dot (c * d) b; ]
2:	[x: dot (c * d) c; y: dot d b; ]
3:	[x: dot (c * d * c) d; y: b; ]

occurrence 1: transitivity through forall x y : X, dot (a * x * y * b) b
3 possible(s) substitution(s)
0:	[x: c; y: dot (d * c) d; ]
1:	[x: dot c d; y: dot c d; ]
2:	[x: dot (c * d) c; y: d; ]


All solutions:
occurrence 0: transitivity through forall x y : X, dot (a * x * y) b
1 possible(s) substitution(s)
0:	[x: plus (c * d) (c * d); y: b; ]


All solutions:
occurrence 0: transitivity through forall x : X, dot (a * x) a
1 possible(s) substitution(s)
0:	[x: 1; ]


All solutions:
occurrence 0: transitivity through forall x y z : X,
                                   plus (x * y + x * z) (a * b)
2 possible(s) substitution(s)
0:	[x: a; y: c; z: dot b c; ]
1:	[x: a; y: dot b c; z: c; ]

occurrence 1: transitivity through forall x y z : X,
                                    plus (x * y + x * z) (a * c)
2 possible(s) substitution(s)
0:	[x: a; y: dot b c; z: b; ]
1:	[x: a; y: b; z: dot b c; ]

occurrence 2: transitivity through forall x y z : X,
                                    plus (x * y + x * z) (a * b * c)
2 possible(s) substitution(s)
0:	[x: a; y: c; z: b; ]
1:	[x: a; y: b; z: c; ]


File "./theories/Tutorial.v", line 227, characters 6-24:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through forall x y z : X, plus (x * y) (x * z)
6 possible(s) substitution(s)
0:	[x: 1; y: dot a (b * c + c); z: dot a b; ]
1:	[x: a; y: plus (b * c) c; z: b; ]
2:	[x: 1; y: 0; z: plus (a * (b * c + c)) (a * b); ]
3:	[x: 1; y: plus (a * (b * c + c)) (a * b); z: 0; ]
4:	[x: 1; y: dot a b; z: dot a (b * c + c); ]
5:	[x: a; y: b; z: plus (b * c) c; ]

occurrence 1: transitivity through forall x y z : X,
                                    plus (x * y + x * z) (a * b)
2 possible(s) substitution(s)
0:	[x: 1; y: dot a (b * c + c); z: 0; ]
1:	[x: 1; y: 0; z: dot a (b * c + c); ]

occurrence 2: transitivity through forall x y z : X,
                                    plus (a * (x * y + x * z)) (a * b)
4 possible(s) substitution(s)
0:	[x: 1; y: dot b c; z: c; ]
1:	[x: 1; y: 0; z: plus (b * c) c; ]
2:	[x: 1; y: plus (b * c) c; z: 0; ]
3:	[x: 1; y: c; z: dot b c; ]

occurrence 3: transitivity through forall x y z : X,
                                    plus (a * (x * y + x * z + c)) (a * b)
2 possible(s) substitution(s)
0:	[x: 1; y: dot b c; z: 0; ]
1:	[x: 1; y: 0; z: dot b c; ]

occurrence 4: transitivity through forall x y z : X,
                                    plus (x * y + x * z) (a * (b * c + c))
2 possible(s) substitution(s)
0:	[x: 1; y: dot a b; z: 0; ]
1:	[x: 1; y: 0; z: dot a b; ]

occurrence 5: transitivity through forall x y z : X,
                                    plus (a * (b * (x * y + x * z) + c))
                                      (a * b)
2 possible(s) substitution(s)
0:	[x: 1; y: c; z: 0; ]
1:	[x: 1; y: 0; z: c; ]

occurrence 6: transitivity through forall x y z : X,
                                    plus (a * ((x * y + x * z) * c + c))
                                      (a * b)
2 possible(s) substitution(s)
0:	[x: 1; y: b; z: 0; ]
1:	[x: 1; y: 0; z: b; ]

occurrence 7: transitivity through forall x y z : X,
                                    plus (a * (x * y + x * z + b * c))
                                      (a * b)
2 possible(s) substitution(s)
0:	[x: 1; y: c; z: 0; ]
1:	[x: 1; y: 0; z: c; ]

occurrence 8: transitivity through forall x y z : X,
                                    plus ((x * y + x * z) * (b * c + c))
                                      (a * b)
2 possible(s) substitution(s)
0:	[x: 1; y: a; z: 0; ]
1:	[x: 1; y: 0; z: a; ]

occurrence 9: transitivity through forall x y z : X,
                                    plus (a * (x * y + x * z))
                                      (a * (b * c + c))
2 possible(s) substitution(s)
0:	[x: 1; y: b; z: 0; ]
1:	[x: 1; y: 0; z: b; ]

occurrence 10: transitivity through forall x y z : X,
                                     plus ((x * y + x * z) * b)
                                       (a * (b * c + c))
2 possible(s) substitution(s)
0:	[x: 1; y: a; z: 0; ]
1:	[x: 1; y: 0; z: a; ]

occurrence 11: transitivity through plus (a * (b * c + c))
                                       ((1 * 1 + 1 * 0) * (a * b))

occurrence 12: transitivity through 
plus (a * (b * c + c)) (a * b * (1 * 1 + 1 * 0))

occurrence 13: transitivity through 
plus (a * (b * c + c)) (a * ((1 * 1 + 1 * 0) * b))

occurrence 14: transitivity through 
plus (a * b) ((1 * 1 + 1 * 0) * (a * (b * c + c)))

occurrence 15: transitivity through 
plus (a * b) (a * (b * c + c) * (1 * 1 + 1 * 0))

occurrence 16: transitivity through 
plus (a * b) (a * (b * c + (1 * 1 + 1 * 0) * c))

occurrence 17: transitivity through 
plus (a * b) (a * (b * c + c * (1 * 1 + 1 * 0)))

occurrence 18: transitivity through 
plus (a * b) (a * (c + (1 * 1 + 1 * 0) * (b * c)))

occurrence 19: transitivity through 
plus (a * b) (a * (c + b * c * (1 * 1 + 1 * 0)))

occurrence 20: transitivity through 
plus (a * b) (a * (c + b * ((1 * 1 + 1 * 0) * c)))

occurrence 21: transitivity through 
plus (a * b) (a * ((1 * 1 + 1 * 0) * (b * c + c)))

occurrence 22: transitivity through 
dot (a * (b * c + c) + a * b) (1 * 1 + 1 * 0)

occurrence 23: transitivity through 
dot (1 * 1 + 1 * 0) (a * (b * c + c) + a * b)

occurrence 24: transitivity through 
plus (a * (b * c + c)) ((1 * 0 + 1 * 1) * (a * b))

occurrence 25: transitivity through 
plus (a * (b * c + c)) (a * b * (1 * 0 + 1 * 1))

occurrence 26: transitivity through 
plus (a * (b * c + c)) (a * ((1 * 0 + 1 * 1) * b))

occurrence 27: transitivity through 
plus (a * b) ((1 * 0 + 1 * 1) * (a * (b * c + c)))

occurrence 28: transitivity through 
plus (a * b) (a * (b * c + c) * (1 * 0 + 1 * 1))

occurrence 29: transitivity through 
plus (a * b) (a * (b * c + (1 * 0 + 1 * 1) * c))

occurrence 30: transitivity through 
plus (a * b) (a * (b * c + c * (1 * 0 + 1 * 1)))

occurrence 31: transitivity through 
plus (a * b) (a * (c + (1 * 0 + 1 * 1) * (b * c)))

occurrence 32: transitivity through 
plus (a * b) (a * (c + b * c * (1 * 0 + 1 * 1)))

occurrence 33: transitivity through 
plus (a * b) (a * (c + b * ((1 * 0 + 1 * 1) * c)))

occurrence 34: transitivity through 
plus (a * b) (a * ((1 * 0 + 1 * 1) * (b * c + c)))

occurrence 35: transitivity through 
dot (a * (b * c + c) + a * b) (1 * 0 + 1 * 1)

occurrence 36: transitivity through 
dot (1 * 0 + 1 * 1) (a * (b * c + c) + a * b)

occurrence 37: transitivity through 
plus (a * (b * c + c) + a * b) (1 * 0 + 1 * 0)

occurrence 38: transitivity through 
plus (a * (b * c + c)) (a * (b + (1 * 0 + 1 * 0)))

occurrence 39: transitivity through 
plus (a * (b * c + c)) ((a + (1 * 0 + 1 * 0)) * b)

occurrence 40: transitivity through 
plus (a * b) (a * (b * c + c + (1 * 0 + 1 * 0)))

occurrence 41: transitivity through 
plus (a * b) (a * (c + b * (c + (1 * 0 + 1 * 0))))

occurrence 42: transitivity through 
plus (a * b) (a * (c + (b + (1 * 0 + 1 * 0)) * c))

occurrence 43: transitivity through 
plus (a * b) ((a + (1 * 0 + 1 * 0)) * (b * c + c))

occurrence 44: transitivity through 
plus (a * (b * c + c) + a * b) (0 * 1 + 0 * 1)

occurrence 45: transitivity through 
plus (a * (b * c + c)) (a * (b + (0 * 1 + 0 * 1)))

occurrence 46: transitivity through 
plus (a * (b * c + c)) ((a + (0 * 1 + 0 * 1)) * b)

occurrence 47: transitivity through 
plus (a * b) (a * (b * c + c + (0 * 1 + 0 * 1)))

occurrence 48: transitivity through 
plus (a * b) (a * (c + b * (c + (0 * 1 + 0 * 1))))

occurrence 49: transitivity through 
plus (a * b) (a * (c + (b + (0 * 1 + 0 * 1)) * c))

occurrence 50: transitivity through 
plus (a * b) ((a + (0 * 1 + 0 * 1)) * (b * c + c))

occurrence 51: transitivity through 
plus (a * (b * c + c)) (a * b * (1 + (1 * 0 + 1 * 0)))

occurrence 52: transitivity through 
plus (a * (b * c + c)) (a * ((1 + (1 * 0 + 1 * 0)) * b))

occurrence 53: transitivity through 
plus (a * (b * c + c)) ((1 + (1 * 0 + 1 * 0)) * (a * b))

occurrence 54: transitivity through 
plus (a * b) (a * (b * c + c) * (1 + (1 * 0 + 1 * 0)))

occurrence 55: transitivity through 
plus (a * b) (a * (c + b * c * (1 + (1 * 0 + 1 * 0))))

occurrence 56: transitivity through 
plus (a * b) (a * (c + b * ((1 + (1 * 0 + 1 * 0)) * c)))

occurrence 57: transitivity through 
plus (a * b) (a * (c + (1 + (1 * 0 + 1 * 0)) * (b * c)))

occurrence 58: transitivity through 
plus (a * b) (a * ((1 + (1 * 0 + 1 * 0)) * (b * c + c)))

occurrence 59: transitivity through 
plus (a * b) ((1 + (1 * 0 + 1 * 0)) * (a * (b * c + c)))

occurrence 60: transitivity through 
plus (a * (b * c + c)) (a * b * (1 + (0 * 1 + 0 * 1)))

occurrence 61: transitivity through 
plus (a * (b * c + c)) (a * ((1 + (0 * 1 + 0 * 1)) * b))

occurrence 62: transitivity through 
plus (a * (b * c + c)) ((1 + (0 * 1 + 0 * 1)) * (a * b))

occurrence 63: transitivity through 
plus (a * b) (a * (b * c + c) * (1 + (0 * 1 + 0 * 1)))

occurrence 64: transitivity through 
plus (a * b) (a * (c + b * c * (1 + (0 * 1 + 0 * 1))))

occurrence 65: transitivity through 
plus (a * b) (a * (c + b * ((1 + (0 * 1 + 0 * 1)) * c)))

occurrence 66: transitivity through 
plus (a * b) (a * (c + (1 + (0 * 1 + 0 * 1)) * (b * c)))

occurrence 67: transitivity through 
plus (a * b) (a * ((1 + (0 * 1 + 0 * 1)) * (b * c + c)))

occurrence 68: transitivity through 
plus (a * b) ((1 + (0 * 1 + 0 * 1)) * (a * (b * c + c)))


All solutions:
occurrence 0: transitivity through forall x y z : nat,
                                   Nat.max (x + y) (x + z)
2 possible(s) substitution(s)
0:	[x: a; y: b; z: c; ]
1:	[x: a; y: c; z: b; ]


All solutions:
occurrence 0: transitivity through forall x y z : nat,
                                   Nat.max (x + y) (x + z)
2 possible(s) substitution(s)
0:	[x: a; y: b; z: c; ]
1:	[x: a; y: c; z: b; ]


(lift_reflexivity
   (let env_sym :=
      sigma_get
        {|
          Internal.Sym.ar := 0;
          Internal.Sym.value := b;
          Internal.Sym.morph := proper_eq b
        |}
        (sigma_add 1%positive
           {|
             Internal.Sym.ar := 0;
             Internal.Sym.value := a;
             Internal.Sym.morph := proper_eq a
           |} (sigma_empty Internal.Sym.pack)) in
    let env_bin :=
      sigma_get
        {|
          Internal.Bin.value := Z.max;
          Internal.Bin.compat := Z.max_compat;
          Internal.Bin.assoc := aac_Z_max_Assoc;
          Internal.Bin.comm := Some aac_Z_max_Comm;
          Internal.Bin.idem := Some aac_Z_max_Idem
        |}
        (sigma_add 2%positive
           {|
             Internal.Bin.value := Z.add;
             Internal.Bin.compat := reflexive_proper Z.add;
             Internal.Bin.assoc := aac_Z_add_Assoc;
             Internal.Bin.comm := Some aac_Z_add_Comm;
             Internal.Bin.idem := None
           |} (sigma_empty Internal.Bin.pack)) in
    let env_units :=
      sigma_get
        {|
          Internal.u_value := 0;
          Internal.u_desc :=
            {| Internal.uf_idx := 2; Internal.uf_desc := aac_Z_add_0_Unit |}
            :: nil
        |} (sigma_empty (Internal.unit_pack env_bin)) in
    let tty := Internal.T env_sym in
    let rsum := Internal.sum (e_sym:=env_sym) in
    let rprd := Internal.prd (e_sym:=env_sym) in
    let rsym := Internal.sym (e_sym:=env_sym) in
    let vnil := Internal.vnil env_sym in
    let vcons := Internal.vcons (e_sym:=env_sym) in
    let eval := Internal.eval (e_sym:=env_sym) env_units in
    let left :=
      rsum 1%positive
        (Utils.cons
           (rsum 2%positive
              (Utils.cons (rsym 1%positive vnil, 1%positive)
                 (Utils.nil (rsym 2%positive vnil, 1%positive))), 1%positive)
           (Utils.nil
              (rsum 2%positive
                 (Utils.cons (rsym 2%positive vnil, 1%positive)
                    (Utils.nil (rsym 1%positive vnil, 1%positive))),
               1%positive))) in
    let right :=
      rsum 2%positive
        (Utils.cons (rsym 1%positive vnil, 1%positive)
           (Utils.nil (rsym 2%positive vnil, 1%positive))) in
    Internal.decide env_units left right
      (eq_refl
       :
       Internal.compare (Internal.norm env_units left)
         (Internal.norm env_units right) = Eq)
    <:
    Z.max (a + b) (b + a) = a + b))
File "./theories/Tutorial.v", line 399, characters 4-36:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through (Z.abs a + - Z.abs b + 0)%Z

occurrence 1: transitivity through 
(Z.abs a + - (Z.abs b + 0))%Z

occurrence 2: transitivity through 
(Z.abs a + - Z.abs (b + 0))%Z

occurrence 3: transitivity through 
(- Z.abs b + Z.abs (a + 0))%Z


File "./theories/Tutorial.v", line 400, characters 4-39:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
"coqc"   -q '-w' '+default'  "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I src -Q theories AAC_tactics -Q src AAC_tactics  theories/Caveats.v
All solutions:
occurrence 0: transitivity through forall x : Z, (- (x + x) + (b + b + c))%Z
1 possible(s) substitution(s)
0:	[x: a; ]

occurrence 1: transitivity through forall x : Z, (x + x + (- (a + a) + c))%Z
1 possible(s) substitution(s)
0:	[x: b; ]


File "./theories/Caveats.v", line 294, characters 4-32:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through dot y 1

occurrence 1: transitivity through 
dot 1 y


File "./theories/Caveats.v", line 295, characters 4-35:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
File "./theories/Caveats.v", line 315, characters 4-18:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
File "./theories/Caveats.v", line 320, characters 4-23:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
File "./theories/Caveats.v", line 347, characters 4-21:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through (c * b + a + 0)%nat

occurrence 1: transitivity through 
(a + b * (c + 0))%nat

occurrence 2: transitivity through 
(a + c * (b + 0))%nat


File "./theories/Caveats.v", line 364, characters 4-28:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through (c + b + a + 0)%nat


File "./theories/Caveats.v", line 366, characters 4-28:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through ((c + b + a) * 1)%nat

occurrence 1: transitivity through 
(c + a + b * 1)%nat

occurrence 2: transitivity through 
(a + (c + b) * 1)%nat

occurrence 3: transitivity through 
(b + a + c * 1)%nat

occurrence 4: transitivity through 
(c + (b + a) * 1)%nat

occurrence 5: transitivity through 
(c + b + a * 1)%nat

occurrence 6: transitivity through 
(b + (c + a) * 1)%nat


All solutions:
occurrence 0: transitivity through forall x y : nat, (x * x + y * x + c)%nat
1 possible(s) substitution(s)
0:	[x: a; y: b; ]


File "./theories/Caveats.v", line 384, characters 4-24:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through forall x y : nat, (x * x + y * x + c)%nat
1 possible(s) substitution(s)
0:	[x: a; y: b; ]

occurrence 1: transitivity through ((a * b + a * a + c) * (1 * 1 + 0 * 1))%nat

occurrence 2: transitivity through 
(a * b + c + a * a * (1 * 1 + 0 * 1))%nat

occurrence 3: transitivity through 
(c + (a * b + a * a) * (1 * 1 + 0 * 1))%nat

occurrence 4: transitivity through 
(a * a + c + a * b * (1 * 1 + 0 * 1))%nat

occurrence 5: transitivity through 
(a * b + (a * a + c) * (1 * 1 + 0 * 1))%nat

occurrence 6: transitivity through 
(a * b + a * a + c * (1 * 1 + 0 * 1))%nat

occurrence 7: transitivity through 
(a * a + (a * b + c) * (1 * 1 + 0 * 1))%nat


File "./theories/Caveats.v", line 386, characters 4-22:
Warning:
[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing
All solutions:
occurrence 0: transitivity through ((a * b + a * a + c) * 1)%nat

occurrence 1: transitivity through 
(a * b + c + a * a * 1)%nat

occurrence 2: transitivity through 
(c + (a * b + a * a) * 1)%nat

occurrence 3: transitivity through 
(a * a + c + a * b * 1)%nat

occurrence 4: transitivity through 
(a * b + (a * a + c) * 1)%nat

occurrence 5: transitivity through 
(a * b + a * a + c * 1)%nat

occurrence 6: transitivity through 
(a * a + (a * b + c) * 1)%nat


/usr/bin/make --no-print-directory -f "Makefile.coq" post-all
make[3]: Leaving directory '/<<PKGBUILDDIR>>'
mkdir -p html
"coqdoc" \
	-toc -interpolate -utf8  -html  -Q theories AAC_tactics -Q src AAC_tactics  -d html theories/Utils.v theories/Constants.v theories/AAC.v theories/Instances.v theories/Tutorial.v theories/Caveats.v
make[2]: Leaving directory '/<<PKGBUILDDIR>>'
make[1]: Leaving directory '/<<PKGBUILDDIR>>'
   dh_auto_test -a
   create-stamp debian/debhelper-build-stamp
   dh_prep -a
   debian/rules override_dh_auto_install
make[1]: Entering directory '/<<PKGBUILDDIR>>'
/usr/bin/make -f Makefile.coq install install-byte DSTROOT=/<<PKGBUILDDIR>>/debian/tmp
make[2]: Entering directory '/<<PKGBUILDDIR>>'
if [ "src/META.coq-aac-tactics" ]; then \
	cat "src/META.coq-aac-tactics" | grep -v 'directory.*=.*' > META; \
fi
code=0; for f in $(cat .filestoinstall); do\
 if ! [ -f "$f" ]; then >&2 echo $f does not exist; code=1; fi \
done; exit $code
for f in $(cat .filestoinstall); do\
 df="`"coq_makefile" -destination-of "$f" -I src -Q theories AAC_tactics -Q src AAC_tactics `";\
 if [ "$?" != "0" -o -z "$df" ]; then\
   echo SKIP "$f" since it has no logical path;\
 else\
   install -d "/<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/$df" &&\
   install -m 0644 "$f" "/<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/$df" &&\
   echo INSTALL "$f" "/<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/$df";\
 fi;\
done
INSTALL theories/Utils.vo /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/Constants.vo /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/AAC.vo /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/Instances.vo /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/Tutorial.vo /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/Caveats.vo /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/Utils.v /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/Constants.v /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/AAC.v /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/Instances.v /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/Tutorial.v /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/Caveats.v /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/Utils.glob /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/Constants.glob /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/AAC.glob /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/Instances.glob /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/Tutorial.glob /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL theories/Caveats.glob /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL src/aac_plugin.cmxs /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
INSTALL src/aac_plugin.cmxs /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/
if [ ! -z "src/META.coq-aac-tactics" ]; then "/usr/bin/ocamlfind" remove -destdir "/<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq/../coq-core//../" coq-aac-tactics; fi
ocamlfind: [WARNING] No such file: /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-aac-tactics/META
if [ "src/META.coq-aac-tactics" ]; then mkdir -p "/<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq/../coq-core//../" && mv "src/META.coq-aac-tactics" "src/META.coq-aac-tactics.skip" ; "/usr/bin/ocamlfind" install  -destdir "/<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq/../coq-core//../" coq-aac-tactics  META src/aac_plugin.cmi src/aac_plugin.cmxs src/aac_plugin.cmxs  src/aac_plugin.cmxa src/aac_plugin.cmx; rc=$?; mv "src/META.coq-aac-tactics.skip" "src/META.coq-aac-tactics"; exit $rc; fi
Installed /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-aac-tactics/aac_plugin.cmx
Installed /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-aac-tactics/aac_plugin.cmxa
Installed /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-aac-tactics/aac_plugin.cmxs
ocamlfind: [WARNING] Overwriting file /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-aac-tactics/aac_plugin.cmxs
Installed /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-aac-tactics/aac_plugin.cmxs
Installed /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-aac-tactics/aac_plugin.cmi
Installed /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-aac-tactics/META
/usr/bin/make install-extra -f "Makefile.coq"
make[3]: Entering directory '/<<PKGBUILDDIR>>'
make[3]: Leaving directory '/<<PKGBUILDDIR>>'
if [ "src/META.coq-aac-tactics" ]; then mkdir -p "/<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq/../coq-core//../" && mv "src/META.coq-aac-tactics" "src/META.coq-aac-tactics.skip" ; "/usr/bin/ocamlfind" install  -add -destdir "/<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq/../coq-core//../" coq-aac-tactics   src/aac_plugin.cma src/aac_plugin.cmo; rc=$?; mv "src/META.coq-aac-tactics.skip" "src/META.coq-aac-tactics"; exit $rc; fi
Installed /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-aac-tactics/aac_plugin.cmo
Installed /<<PKGBUILDDIR>>/debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-aac-tactics/aac_plugin.cma
make[2]: Leaving directory '/<<PKGBUILDDIR>>'
make[1]: Leaving directory '/<<PKGBUILDDIR>>'
   dh_install -a
   dh_ocamldoc -a
   dh_installdocs -a
   dh_installchangelogs -a
   dh_lintian -a
   dh_perl -a
   dh_link -a
   dh_strip_nondeterminism -a
   dh_compress -a
   dh_fixperms -a
   debian/rules override_dh_missing
make[1]: Entering directory '/<<PKGBUILDDIR>>'
dh_missing --fail-missing
make[1]: Leaving directory '/<<PKGBUILDDIR>>'
   dh_dwz -a
dwz: debian/libcoq-aac-tactics/usr/lib/ocaml/coq-aac-tactics/aac_plugin.cmxs: .debug_info section not present
dwz: debian/libcoq-aac-tactics/usr/lib/ocaml/coq/user-contrib/AAC_tactics/aac_plugin.cmxs: .debug_info section not present
dwz: Too few files for multifile optimization
dh_dwz: warning: No dwz multifile created, but not explicitly requested either so ignoring it.
dh_dwz: warning: Common issues include no debug information at all (missing -g) and
dh_dwz: warning: compressed debug information (#931891).
   dh_strip -a
   dh_makeshlibs -a
   dh_shlibdeps -a
   dh_installdeb -a
   dh_coq -a
   dh_ocaml -a
   dh_gencontrol -a
   dh_md5sums -a
   dh_builddeb -a
dpkg-deb: building package 'libcoq-aac-tactics-dbgsym' in '../libcoq-aac-tactics-dbgsym_8.18.0-1_armhf.deb'.
dpkg-deb: building package 'libcoq-aac-tactics' in '../libcoq-aac-tactics_8.18.0-1_armhf.deb'.
 dpkg-genbuildinfo --build=any -O../aac-tactics_8.18.0-1_armhf.buildinfo
 dpkg-genchanges --build=any -mRaspbian pi5 test autobuilder <root@raspbian.org> -O../aac-tactics_8.18.0-1_armhf.changes
dpkg-genchanges: info: binary-only arch-specific upload (source code and arch-indep packages not included)
 dpkg-source --after-build .
dpkg-buildpackage: info: binary-only upload (no source included)
--------------------------------------------------------------------------------
Build finished at 2024-02-21T10:10:58Z

Finished
--------

I: Built successfully

+------------------------------------------------------------------------------+
| Changes                                                                      |
+------------------------------------------------------------------------------+


aac-tactics_8.18.0-1_armhf.changes:
-----------------------------------

Format: 1.8
Date: Thu, 21 Dec 2023 15:20:11 +0100
Source: aac-tactics
Binary: libcoq-aac-tactics libcoq-aac-tactics-dbgsym
Architecture: armhf
Version: 8.18.0-1
Distribution: trixie-staging
Urgency: medium
Maintainer: Raspbian pi5 test autobuilder <root@raspbian.org>
Changed-By: Julien Puydt <jpuydt@debian.org>
Description:
 libcoq-aac-tactics - Coq tactics for reasoning modulo AC (theories)
Changes:
 aac-tactics (8.18.0-1) unstable; urgency=medium
 .
   * New upstream release.
Checksums-Sha1:
 b1a99028463d7ce022e655ebd38631ef7e4a27a9 6516 aac-tactics_8.18.0-1_armhf.buildinfo
 1a9532b926b47b006b1580c8f6248ed5d1565a6b 14676 libcoq-aac-tactics-dbgsym_8.18.0-1_armhf.deb
 2856e078544b278eccb7813092f87adc0bf28089 379772 libcoq-aac-tactics_8.18.0-1_armhf.deb
Checksums-Sha256:
 e4e32b2a46dc4389e4f86bab6777929735bc79c146235fdfcf64c9d1c5f89b1d 6516 aac-tactics_8.18.0-1_armhf.buildinfo
 e671b3463cfc839021cd3939b5130fef26fb41cb42ab447919134dd0776a1122 14676 libcoq-aac-tactics-dbgsym_8.18.0-1_armhf.deb
 eb68ee1069b5e927a6d2de83f3330ed592c2bccc02f2c6d315952e18a7d946d5 379772 libcoq-aac-tactics_8.18.0-1_armhf.deb
Files:
 4fea2b1bfb7628cfc01c942812a253f4 6516 math optional aac-tactics_8.18.0-1_armhf.buildinfo
 8999f562b278b3d684f6938acd6a9984 14676 debug optional libcoq-aac-tactics-dbgsym_8.18.0-1_armhf.deb
 356adfbfdce9d4cbfdef13fd5cf9da34 379772 math optional libcoq-aac-tactics_8.18.0-1_armhf.deb

+------------------------------------------------------------------------------+
| Buildinfo                                                                    |
+------------------------------------------------------------------------------+

Format: 1.0
Source: aac-tactics
Binary: libcoq-aac-tactics libcoq-aac-tactics-dbgsym
Architecture: armhf
Version: 8.18.0-1
Checksums-Md5:
 8999f562b278b3d684f6938acd6a9984 14676 libcoq-aac-tactics-dbgsym_8.18.0-1_armhf.deb
 356adfbfdce9d4cbfdef13fd5cf9da34 379772 libcoq-aac-tactics_8.18.0-1_armhf.deb
Checksums-Sha1:
 1a9532b926b47b006b1580c8f6248ed5d1565a6b 14676 libcoq-aac-tactics-dbgsym_8.18.0-1_armhf.deb
 2856e078544b278eccb7813092f87adc0bf28089 379772 libcoq-aac-tactics_8.18.0-1_armhf.deb
Checksums-Sha256:
 e671b3463cfc839021cd3939b5130fef26fb41cb42ab447919134dd0776a1122 14676 libcoq-aac-tactics-dbgsym_8.18.0-1_armhf.deb
 eb68ee1069b5e927a6d2de83f3330ed592c2bccc02f2c6d315952e18a7d946d5 379772 libcoq-aac-tactics_8.18.0-1_armhf.deb
Build-Origin: Raspbian
Build-Architecture: armhf
Build-Date: Wed, 21 Feb 2024 10:10:58 +0000
Build-Path: /<<PKGBUILDDIR>>
Build-Tainted-By:
 merged-usr-via-aliased-dirs
Installed-Build-Depends:
 autoconf (= 2.71-3),
 automake (= 1:1.16.5-1.3),
 autopoint (= 0.21-14),
 autotools-dev (= 20220109.1),
 base-files (= 13+rpi1),
 base-passwd (= 3.6.3),
 bash (= 5.2.21-2),
 binutils (= 2.41-6+rpi1),
 binutils-arm-linux-gnueabihf (= 2.41-6+rpi1),
 binutils-common (= 2.41-6+rpi1),
 bsdextrautils (= 2.39.3-6),
 bsdutils (= 1:2.39.3-6),
 build-essential (= 12.10),
 bzip2 (= 1.0.8-5+b2),
 coq (= 8.18.0+dfsg-1),
 coreutils (= 9.4-3),
 cpp (= 4:13.2.0-1+rpi1),
 cpp-12 (= 12.3.0-14+rpi1),
 cpp-13 (= 13.2.0-9+rpi1),
 dash (= 0.5.12-6),
 debconf (= 1.5.86),
 debhelper (= 13.13),
 debianutils (= 5.16),
 dh-autoreconf (= 20),
 dh-coq (= 0.8),
 dh-ocaml (= 2.0),
 dh-strip-nondeterminism (= 1.13.1-1),
 diffutils (= 1:3.10-1),
 dpkg (= 1.22.4+rpi1),
 dpkg-dev (= 1.22.4+rpi1),
 dwz (= 0.15-1),
 file (= 1:5.45-2),
 findutils (= 4.9.0-5),
 g++ (= 4:13.2.0-1+rpi1),
 g++-13 (= 13.2.0-9+rpi1),
 gcc (= 4:13.2.0-1+rpi1),
 gcc-12 (= 12.3.0-14+rpi1),
 gcc-12-base (= 12.3.0-14+rpi1),
 gcc-13 (= 13.2.0-9+rpi1),
 gcc-13-base (= 13.2.0-9+rpi1),
 gettext (= 0.21-14),
 gettext-base (= 0.21-14),
 grep (= 3.11-4),
 groff-base (= 1.23.0-3),
 gzip (= 1.12-1),
 hostname (= 3.23+nmu2),
 init-system-helpers (= 1.66),
 intltool-debian (= 0.35.0+20060710.6),
 libacl1 (= 2.3.2-1),
 libarchive-zip-perl (= 1.68-1),
 libasan8 (= 13.2.0-9+rpi1),
 libatomic1 (= 13.2.0-9+rpi1),
 libattr1 (= 1:2.5.2-1),
 libaudit-common (= 1:3.1.2-2),
 libaudit1 (= 1:3.1.2-2),
 libbinutils (= 2.41-6+rpi1),
 libblkid1 (= 2.39.3-6),
 libbz2-1.0 (= 1.0.8-5+b2),
 libc-bin (= 2.37-15~deb13u1+rpi1),
 libc-dev-bin (= 2.37-15~deb13u1+rpi1),
 libc6 (= 2.37-15~deb13u1+rpi1),
 libc6-dev (= 2.37-15~deb13u1+rpi1),
 libcap-ng0 (= 0.8.4-2),
 libcap2 (= 1:2.66-5),
 libcc1-0 (= 13.2.0-9+rpi1),
 libcom-err2 (= 1.47.0-2),
 libcompiler-libs-ocaml-dev (= 4.14.1-1+rpi1),
 libcoq-core-ocaml (= 8.18.0+dfsg-1),
 libcoq-core-ocaml-dev (= 8.18.0+dfsg-1),
 libcoq-stdlib (= 8.18.0+dfsg-1),
 libcrypt-dev (= 1:4.4.36-4),
 libcrypt1 (= 1:4.4.36-4),
 libctf-nobfd0 (= 2.41-6+rpi1),
 libctf0 (= 2.41-6+rpi1),
 libdb5.3 (= 5.3.28+dfsg2-4),
 libdebconfclient0 (= 0.271),
 libdebhelper-perl (= 13.13),
 libdpkg-perl (= 1.22.4+rpi1),
 libelf1 (= 0.188-2.1+rpi1),
 libexpat1 (= 2.5.0-2),
 libffi8 (= 3.4.4-2),
 libfile-find-rule-perl (= 0.34-3),
 libfile-stripnondeterminism-perl (= 1.13.1-1),
 libfindlib-ocaml (= 1.9.6-1+b2),
 libfindlib-ocaml-dev (= 1.9.6-1+b2),
 libgcc-12-dev (= 12.3.0-14+rpi1),
 libgcc-13-dev (= 13.2.0-9+rpi1),
 libgcc-s1 (= 13.2.0-9+rpi1),
 libgcrypt20 (= 1.10.3-2),
 libgdbm-compat4 (= 1.23-5),
 libgdbm6 (= 1.23-5),
 libgmp-dev (= 2:6.3.0+dfsg-2),
 libgmp10 (= 2:6.3.0+dfsg-2),
 libgmp3-dev (= 2:6.3.0+dfsg-2),
 libgmpxx4ldbl (= 2:6.3.0+dfsg-2),
 libgomp1 (= 13.2.0-9+rpi1),
 libgpg-error0 (= 1.47-3),
 libgssapi-krb5-2 (= 1.20.1-5),
 libicu72 (= 72.1-4),
 libisl23 (= 0.26-3),
 libjansson4 (= 2.14-2),
 libk5crypto3 (= 1.20.1-5),
 libkeyutils1 (= 1.6.3-3),
 libkrb5-3 (= 1.20.1-5),
 libkrb5support0 (= 1.20.1-5),
 liblz4-1 (= 1.9.4-1+rpi1+b1),
 liblzma5 (= 5.4.5-0.3),
 libmagic-mgc (= 1:5.45-2),
 libmagic1 (= 1:5.45-2),
 libmd0 (= 1.1.0-2),
 libmount1 (= 2.39.3-6),
 libmpc3 (= 1.3.1-1),
 libmpfr6 (= 4.2.1-1),
 libncurses-dev (= 6.4+20240113-1),
 libncurses6 (= 6.4+20240113-1),
 libncursesw6 (= 6.4+20240113-1),
 libnsl-dev (= 1.3.0-3),
 libnsl2 (= 1.3.0-3),
 libnumber-compare-perl (= 0.03-3),
 libpam-modules (= 1.5.2-9.1),
 libpam-modules-bin (= 1.5.2-9.1),
 libpam-runtime (= 1.5.2-9.1),
 libpam0g (= 1.5.2-9.1),
 libpcre2-8-0 (= 10.42-4),
 libperl5.38 (= 5.38.2-3),
 libpipeline1 (= 1.5.7-1),
 libpython3-stdlib (= 3.11.6-1),
 libpython3.11-minimal (= 3.11.8-1),
 libpython3.11-stdlib (= 3.11.8-1),
 libreadline8 (= 8.2-3),
 libseccomp2 (= 2.5.5-1+rpi1),
 libselinux1 (= 3.5-2),
 libsframe1 (= 2.41-6+rpi1),
 libsmartcols1 (= 2.39.3-6),
 libsqlite3-0 (= 3.45.1-1),
 libssl3 (= 3.1.5-1),
 libstdc++-13-dev (= 13.2.0-9+rpi1),
 libstdc++6 (= 13.2.0-9+rpi1),
 libstdlib-ocaml (= 4.14.1-1+rpi1),
 libstdlib-ocaml-dev (= 4.14.1-1+rpi1),
 libsub-override-perl (= 0.10-1),
 libsystemd0 (= 255.3-1+rpi1),
 libtext-glob-perl (= 0.11-3),
 libtinfo6 (= 6.4+20240113-1),
 libtirpc-common (= 1.3.4+ds-1),
 libtirpc-dev (= 1.3.4+ds-1),
 libtirpc3 (= 1.3.4+ds-1),
 libtool (= 2.4.7-7),
 libubsan1 (= 13.2.0-9+rpi1),
 libuchardet0 (= 0.0.8-1),
 libudev1 (= 255.3-1+rpi1),
 libunistring5 (= 1.1-2),
 libuuid1 (= 2.39.3-6),
 libxml2 (= 2.9.14+dfsg-1.3),
 libzarith-ocaml (= 1.13-2+b1),
 libzarith-ocaml-dev (= 1.13-2+b1),
 libzstd1 (= 1.5.5+dfsg2-2),
 linux-libc-dev (= 6.5.6-1+rpi1+b1),
 login (= 1:4.13+dfsg1-3),
 m4 (= 1.4.19-4),
 make (= 4.3-4.1),
 man-db (= 2.12.0-3),
 mawk (= 1.3.4.20240123-1),
 media-types (= 10.1.0),
 ncurses-base (= 6.4+20240113-1),
 ncurses-bin (= 6.4+20240113-1),
 netbase (= 6.4),
 ocaml (= 4.14.1-1+rpi1),
 ocaml-base (= 4.14.1-1+rpi1),
 ocaml-findlib (= 1.9.6-1+b2),
 ocaml-interp (= 4.14.1-1+rpi1),
 patch (= 2.7.6-7),
 perl (= 5.38.2-3),
 perl-base (= 5.38.2-3),
 perl-modules-5.38 (= 5.38.2-3),
 po-debconf (= 1.0.21+nmu1),
 python3 (= 3.11.6-1),
 python3-minimal (= 3.11.6-1),
 python3.11 (= 3.11.8-1),
 python3.11-minimal (= 3.11.8-1),
 readline-common (= 8.2-3),
 rpcsvc-proto (= 1.4.3-1),
 sed (= 4.9-2),
 sensible-utils (= 0.0.22),
 sysvinit-utils (= 3.08-6),
 tar (= 1.35+dfsg-3),
 tzdata (= 2024a-1),
 usr-is-merged (= 39),
 usrmerge (= 39),
 util-linux (= 2.39.3-6),
 xz-utils (= 5.4.5-0.3),
 zlib1g (= 1:1.3.dfsg-3)
Environment:
 DEB_BUILD_OPTIONS="parallel=4"
 LANG="en_GB.UTF-8"
 LC_ALL="C.UTF-8"
 LC_COLLATE="C.UTF-8"
 SOURCE_DATE_EPOCH="1703168411"


+------------------------------------------------------------------------------+
| Package contents                                                             |
+------------------------------------------------------------------------------+


libcoq-aac-tactics-dbgsym_8.18.0-1_armhf.deb
--------------------------------------------

 new Debian package, version 2.0.
 size 14676 bytes: control archive=536 bytes.
     398 bytes,    12 lines      control
     106 bytes,     1 lines      md5sums
 Package: libcoq-aac-tactics-dbgsym
 Source: aac-tactics
 Version: 8.18.0-1
 Auto-Built-Package: debug-symbols
 Architecture: armhf
 Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
 Installed-Size: 85
 Depends: libcoq-aac-tactics (= 8.18.0-1)
 Section: debug
 Priority: optional
 Description: debug symbols for libcoq-aac-tactics
 Build-Ids: 14f75661dfd0d4fee657589ad518c56cd721f548

drwxr-xr-x root/root         0 2023-12-21 14:20 ./
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/lib/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/lib/debug/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/lib/debug/.build-id/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/lib/debug/.build-id/14/
-rw-r--r-- root/root     76368 2023-12-21 14:20 ./usr/lib/debug/.build-id/14/f75661dfd0d4fee657589ad518c56cd721f548.debug
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/share/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/share/doc/
lrwxrwxrwx root/root         0 2023-12-21 14:20 ./usr/share/doc/libcoq-aac-tactics-dbgsym -> libcoq-aac-tactics


libcoq-aac-tactics_8.18.0-1_armhf.deb
-------------------------------------

 new Debian package, version 2.0.
 size 379772 bytes: control archive=1772 bytes.
     773 bytes,    18 lines      control
    3589 bytes,    41 lines      md5sums
 Package: libcoq-aac-tactics
 Source: aac-tactics
 Version: 8.18.0-1
 Architecture: armhf
 Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
 Installed-Size: 2784
 Depends: libcoq-stdlib-qs4q4, libcoq-core-ocaml-htc80, libstdlib-ocaml-pq5l6, libzarith-ocaml-wx6x8
 Breaks: libaac-tactics-coq
 Replaces: libaac-tactics-coq, libaac-tactics-ocaml, libaac-tactics-ocaml-dev
 Provides: aac-tactics, libcoq-aac-tactics-of2u8
 Section: math
 Priority: optional
 Homepage: https://github.com/coq-community/aac-tactics
 Description: Coq tactics for reasoning modulo AC (theories)
  This Coq plugin provides tactics for rewriting universally quantified
  equations, modulo associative (and possibly commutative) operators.
  .
  This package provides the Coq support library.

drwxr-xr-x root/root         0 2023-12-21 14:20 ./
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/lib/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/lib/ocaml/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/lib/ocaml/coq-aac-tactics/
-rw-r--r-- root/root       203 2023-12-21 14:20 ./usr/lib/ocaml/coq-aac-tactics/META
-rw-r--r-- root/root    112351 2023-12-21 14:20 ./usr/lib/ocaml/coq-aac-tactics/aac_plugin.cma
-rw-r--r-- root/root     27660 2023-12-21 14:20 ./usr/lib/ocaml/coq-aac-tactics/aac_plugin.cmi
-rw-r--r-- root/root    112344 2023-12-21 14:20 ./usr/lib/ocaml/coq-aac-tactics/aac_plugin.cmo
-rw-r--r-- root/root     28339 2023-12-21 14:20 ./usr/lib/ocaml/coq-aac-tactics/aac_plugin.cmx
-rw-r--r-- root/root      7029 2023-12-21 14:20 ./usr/lib/ocaml/coq-aac-tactics/aac_plugin.cmxa
-rw-r--r-- root/root    290456 2023-12-21 14:20 ./usr/lib/ocaml/coq-aac-tactics/aac_plugin.cmxs
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/lib/ocaml/coq/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/
-rw-r--r-- root/root    121857 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/AAC.glob
-rw-r--r-- root/root     33432 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/AAC.v
-rw-r--r-- root/root    221893 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/AAC.vo
-rw-r--r-- root/root     27054 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/Caveats.glob
-rw-r--r-- root/root     12021 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/Caveats.v
-rw-r--r-- root/root     38076 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/Caveats.vo
-rw-r--r-- root/root       196 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/Constants.glob
-rw-r--r-- root/root      1749 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/Constants.v
-rw-r--r-- root/root      3305 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/Constants.vo
-rw-r--r-- root/root     38862 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/Instances.glob
-rw-r--r-- root/root     15287 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/Instances.v
-rw-r--r-- root/root     73561 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/Instances.vo
-rw-r--r-- root/root     52291 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/Tutorial.glob
-rw-r--r-- root/root     14011 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/Tutorial.v
-rw-r--r-- root/root     78805 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/Tutorial.vo
-rw-r--r-- root/root     31368 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/Utils.glob
-rw-r--r-- root/root      8428 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/Utils.v
-rw-r--r-- root/root     53227 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/Utils.vo
-rw-r--r-- root/root    290456 2023-12-21 14:20 ./usr/lib/ocaml/coq/user-contrib/AAC_tactics/aac_plugin.cmxs
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/share/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/share/doc-base/
-rw-r--r-- root/root       289 2023-12-21 14:20 ./usr/share/doc-base/libcoq-aac-tactics.aac-tactics-theories
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/share/doc/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/share/doc/libcoq-aac-tactics/
-rw-r--r-- root/root      2164 2023-08-03 22:03 ./usr/share/doc/libcoq-aac-tactics/README.md.gz
-rw-r--r-- root/root      1044 2023-12-21 14:20 ./usr/share/doc/libcoq-aac-tactics/changelog.Debian.gz
-rw-r--r-- root/root       990 2023-12-21 14:20 ./usr/share/doc/libcoq-aac-tactics/copyright
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/share/doc/libcoq-aac-tactics/theories/
-rw-r--r-- root/root    373583 2023-12-21 14:20 ./usr/share/doc/libcoq-aac-tactics/theories/AAC_tactics.AAC.html
-rw-r--r-- root/root     99167 2023-12-21 14:20 ./usr/share/doc/libcoq-aac-tactics/theories/AAC_tactics.Caveats.html
-rw-r--r-- root/root      5674 2023-12-21 14:20 ./usr/share/doc/libcoq-aac-tactics/theories/AAC_tactics.Constants.html
-rw-r--r-- root/root    152588 2023-12-21 14:20 ./usr/share/doc/libcoq-aac-tactics/theories/AAC_tactics.Instances.html
-rw-r--r-- root/root    157290 2023-12-21 14:20 ./usr/share/doc/libcoq-aac-tactics/theories/AAC_tactics.Tutorial.html
-rw-r--r-- root/root    110136 2023-12-21 14:20 ./usr/share/doc/libcoq-aac-tactics/theories/AAC_tactics.Utils.html
-rw-r--r-- root/root      6139 2023-12-21 14:20 ./usr/share/doc/libcoq-aac-tactics/theories/coqdoc.css
-rw-r--r-- root/root    200746 2023-12-21 14:20 ./usr/share/doc/libcoq-aac-tactics/theories/index.html
-rw-r--r-- root/root      6137 2023-12-21 14:20 ./usr/share/doc/libcoq-aac-tactics/theories/toc.html
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/share/lintian/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./usr/share/lintian/overrides/
-rw-r--r-- root/root       286 2023-12-21 14:20 ./usr/share/lintian/overrides/libcoq-aac-tactics
drwxr-xr-x root/root         0 2023-12-21 14:20 ./var/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./var/lib/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./var/lib/coq/
drwxr-xr-x root/root         0 2023-12-21 14:20 ./var/lib/coq/md5sums/
-rw-r--r-- root/root         5 2023-12-21 14:20 ./var/lib/coq/md5sums/libcoq-aac-tactics.checksum


+------------------------------------------------------------------------------+
| Post Build                                                                   |
+------------------------------------------------------------------------------+


+------------------------------------------------------------------------------+
| Cleanup                                                                      |
+------------------------------------------------------------------------------+

Purging /<<BUILDDIR>>
Not cleaning session: cloned chroot in use

+------------------------------------------------------------------------------+
| Summary                                                                      |
+------------------------------------------------------------------------------+

Build Architecture: armhf
Build Type: any
Build-Space: 11256
Build-Time: 26
Distribution: trixie-staging
Host Architecture: armhf
Install-Time: 127
Job: aac-tactics_8.18.0-1
Machine Architecture: arm64
Package: aac-tactics
Package-Time: 161
Source-Version: 8.18.0-1
Space: 11256
Status: successful
Version: 8.18.0-1
--------------------------------------------------------------------------------
Finished at 2024-02-21T10:10:58Z
Build needed 00:02:41, 11256k disk space