Diff of the two buildlogs:

--
--- b1/build.log	2023-05-30 11:18:19.954616324 +0000
+++ b2/build.log	2023-05-30 11:38:57.068422669 +0000
@@ -1,6 +1,6 @@
 I: pbuilder: network access will be disabled during build
-I: Current time: Mon May 29 22:04:10 -12 2023
-I: pbuilder-time-stamp: 1685441050
+I: Current time: Wed May 31 01:20:28 +14 2023
+I: pbuilder-time-stamp: 1685445628
 I: Building the build Environment
 I: extracting base tarball [/var/cache/pbuilder/bookworm-reproducible-base.tgz]
 I: copying local configuration
@@ -16,7 +16,7 @@
 I: copying [./coq-hott_8.16.orig.tar.gz]
 I: copying [./coq-hott_8.16-2.debian.tar.xz]
 I: Extracting source
-gpgv: Signature made Tue Jan 24 18:59:50 2023 -12
+gpgv: Signature made Wed Jan 25 20:59:50 2023 +14
 gpgv:                using RSA key 812EEFD8A3FBA4ACE4DF114B04C53BD7FE030551
 gpgv:                issuer "jpuydt@debian.org"
 gpgv: Can't check signature: No public key
@@ -26,135 +26,167 @@
 dpkg-source: info: unpacking coq-hott_8.16-2.debian.tar.xz
 I: Not using root during the build.
 I: Installing the build-deps
-I: user script /srv/workspace/pbuilder/29051/tmp/hooks/D02_print_environment starting
+I: user script /srv/workspace/pbuilder/5929/tmp/hooks/D01_modify_environment starting
+debug: Running on virt64b.
+I: Changing host+domainname to test build reproducibility
+I: Adding a custom variable just for the fun of it...
+I: Changing /bin/sh to bash
+'/bin/sh' -> '/bin/bash'
+lrwxrwxrwx 1 root root 9 May 31 01:21 /bin/sh -> /bin/bash
+I: Setting pbuilder2's login shell to /bin/bash
+I: Setting pbuilder2's GECOS to second user,second room,second work-phone,second home-phone,second other
+I: user script /srv/workspace/pbuilder/5929/tmp/hooks/D01_modify_environment finished
+I: user script /srv/workspace/pbuilder/5929/tmp/hooks/D02_print_environment starting
 I: set
-  BUILDDIR='/build'
-  BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other'
-  BUILDUSERNAME='pbuilder1'
-  BUILD_ARCH='armhf'
-  DEBIAN_FRONTEND='noninteractive'
-  DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=3 '
-  DISTRIBUTION='bookworm'
-  HOME='/root'
-  HOST_ARCH='armhf'
+  BASH=/bin/sh
+  BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath
+  BASH_ALIASES=()
+  BASH_ARGC=()
+  BASH_ARGV=()
+  BASH_CMDS=()
+  BASH_LINENO=([0]="12" [1]="0")
+  BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:.
+  BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment")
+  BASH_VERSINFO=([0]="5" [1]="2" [2]="15" [3]="1" [4]="release" [5]="arm-unknown-linux-gnueabihf")
+  BASH_VERSION='5.2.15(1)-release'
+  BUILDDIR=/build
+  BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other'
+  BUILDUSERNAME=pbuilder2
+  BUILD_ARCH=armhf
+  DEBIAN_FRONTEND=noninteractive
+  DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=4 '
+  DIRSTACK=()
+  DISTRIBUTION=bookworm
+  EUID=0
+  FUNCNAME=([0]="Echo" [1]="main")
+  GROUPS=()
+  HOME=/root
+  HOSTNAME=i-capture-the-hostname
+  HOSTTYPE=arm
+  HOST_ARCH=armhf
   IFS=' 	
   '
-  INVOCATION_ID='6e734cfb06c84f26805f16034249b71b'
-  LANG='C'
-  LANGUAGE='en_US:en'
-  LC_ALL='C'
-  MAIL='/var/mail/root'
-  OPTIND='1'
-  PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games'
-  PBCURRENTCOMMANDLINEOPERATION='build'
-  PBUILDER_OPERATION='build'
-  PBUILDER_PKGDATADIR='/usr/share/pbuilder'
-  PBUILDER_PKGLIBDIR='/usr/lib/pbuilder'
-  PBUILDER_SYSCONFDIR='/etc'
-  PPID='29051'
-  PS1='# '
-  PS2='> '
+  INVOCATION_ID=8605905695cc4463a7a0c2ad70d6be69
+  LANG=C
+  LANGUAGE=it_CH:it
+  LC_ALL=C
+  MACHTYPE=arm-unknown-linux-gnueabihf
+  MAIL=/var/mail/root
+  OPTERR=1
+  OPTIND=1
+  OSTYPE=linux-gnueabihf
+  PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path
+  PBCURRENTCOMMANDLINEOPERATION=build
+  PBUILDER_OPERATION=build
+  PBUILDER_PKGDATADIR=/usr/share/pbuilder
+  PBUILDER_PKGLIBDIR=/usr/lib/pbuilder
+  PBUILDER_SYSCONFDIR=/etc
+  PIPESTATUS=([0]="0")
+  POSIXLY_CORRECT=y
+  PPID=5929
   PS4='+ '
-  PWD='/'
-  SHELL='/bin/bash'
-  SHLVL='2'
-  SUDO_COMMAND='/usr/bin/timeout -k 18.1h 18h /usr/bin/ionice -c 3 /usr/bin/nice /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.ECR7vjhr/pbuilderrc_qTH6 --distribution bookworm --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bookworm-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.ECR7vjhr/b1 --logfile b1/build.log coq-hott_8.16-2.dsc'
-  SUDO_GID='113'
-  SUDO_UID='107'
-  SUDO_USER='jenkins'
-  TERM='unknown'
-  TZ='/usr/share/zoneinfo/Etc/GMT+12'
-  USER='root'
-  _='/usr/bin/systemd-run'
-  http_proxy='http://10.0.0.15:3142/'
+  PWD=/
+  SHELL=/bin/bash
+  SHELLOPTS=braceexpand:errexit:hashall:interactive-comments:posix
+  SHLVL=3
+  SUDO_COMMAND='/usr/bin/timeout -k 24.1h 24h /usr/bin/ionice -c 3 /usr/bin/nice -n 11 /usr/bin/unshare --uts -- /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.ECR7vjhr/pbuilderrc_Ac4R --distribution bookworm --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bookworm-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.ECR7vjhr/b2 --logfile b2/build.log --extrapackages usrmerge coq-hott_8.16-2.dsc'
+  SUDO_GID=113
+  SUDO_UID=107
+  SUDO_USER=jenkins
+  TERM=unknown
+  TZ=/usr/share/zoneinfo/Etc/GMT-14
+  UID=0
+  USER=root
+  _='I: set'
+  http_proxy=http://10.0.0.15:3142/
 I: uname -a
-  Linux cbxi4pro0 5.10.0-23-armmp #1 SMP Debian 5.10.179-1 (2023-05-12) armv7l GNU/Linux
+  Linux i-capture-the-hostname 5.10.0-23-arm64 #1 SMP Debian 5.10.179-1 (2023-05-12) aarch64 GNU/Linux
 I: ls -l /bin
   total 5072
-  -rwxr-xr-x 1 root root 838488 Apr 23 09:24 bash
-  -rwxr-xr-x 3 root root  67144 Sep 18  2022 bunzip2
-  -rwxr-xr-x 3 root root  67144 Sep 18  2022 bzcat
-  lrwxrwxrwx 1 root root      6 Sep 18  2022 bzcmp -> bzdiff
-  -rwxr-xr-x 1 root root   2225 Sep 18  2022 bzdiff
-  lrwxrwxrwx 1 root root      6 Sep 18  2022 bzegrep -> bzgrep
-  -rwxr-xr-x 1 root root   4893 Nov 27  2021 bzexe
-  lrwxrwxrwx 1 root root      6 Sep 18  2022 bzfgrep -> bzgrep
-  -rwxr-xr-x 1 root root   3775 Sep 18  2022 bzgrep
-  -rwxr-xr-x 3 root root  67144 Sep 18  2022 bzip2
-  -rwxr-xr-x 1 root root  67112 Sep 18  2022 bzip2recover
-  lrwxrwxrwx 1 root root      6 Sep 18  2022 bzless -> bzmore
-  -rwxr-xr-x 1 root root   1297 Sep 18  2022 bzmore
-  -rwxr-xr-x 1 root root  67632 Sep 20  2022 cat
-  -rwxr-xr-x 1 root root  67676 Sep 20  2022 chgrp
-  -rwxr-xr-x 1 root root  67644 Sep 20  2022 chmod
-  -rwxr-xr-x 1 root root  67684 Sep 20  2022 chown
-  -rwxr-xr-x 1 root root 133532 Sep 20  2022 cp
-  -rwxr-xr-x 1 root root 132868 Jan  5 01:20 dash
-  -rwxr-xr-x 1 root root 133220 Sep 20  2022 date
-  -rwxr-xr-x 1 root root  67732 Sep 20  2022 dd
-  -rwxr-xr-x 1 root root  68104 Sep 20  2022 df
-  -rwxr-xr-x 1 root root 133632 Sep 20  2022 dir
-  -rwxr-xr-x 1 root root  59128 Mar 22 21:02 dmesg
-  lrwxrwxrwx 1 root root      8 Dec 19 01:33 dnsdomainname -> hostname
-  lrwxrwxrwx 1 root root      8 Dec 19 01:33 domainname -> hostname
-  -rwxr-xr-x 1 root root  67560 Sep 20  2022 echo
-  -rwxr-xr-x 1 root root     41 Jan 24 02:43 egrep
-  -rwxr-xr-x 1 root root  67548 Sep 20  2022 false
-  -rwxr-xr-x 1 root root     41 Jan 24 02:43 fgrep
-  -rwxr-xr-x 1 root root  55748 Mar 22 21:02 findmnt
-  -rwsr-xr-x 1 root root  26208 Mar 22 20:15 fusermount
-  -rwxr-xr-x 1 root root 128608 Jan 24 02:43 grep
-  -rwxr-xr-x 2 root root   2346 Apr  9  2022 gunzip
-  -rwxr-xr-x 1 root root   6447 Apr  9  2022 gzexe
-  -rwxr-xr-x 1 root root  64220 Apr  9  2022 gzip
-  -rwxr-xr-x 1 root root  67032 Dec 19 01:33 hostname
-  -rwxr-xr-x 1 root root  67720 Sep 20  2022 ln
-  -rwxr-xr-x 1 root root  35132 Mar 22 21:51 login
-  -rwxr-xr-x 1 root root 133632 Sep 20  2022 ls
-  -rwxr-xr-x 1 root root 136808 Mar 22 21:02 lsblk
-  -rwxr-xr-x 1 root root  67800 Sep 20  2022 mkdir
-  -rwxr-xr-x 1 root root  67764 Sep 20  2022 mknod
-  -rwxr-xr-x 1 root root  67596 Sep 20  2022 mktemp
-  -rwxr-xr-x 1 root root  38504 Mar 22 21:02 more
-  -rwsr-xr-x 1 root root  38496 Mar 22 21:02 mount
-  -rwxr-xr-x 1 root root   9824 Mar 22 21:02 mountpoint
-  -rwxr-xr-x 1 root root 133532 Sep 20  2022 mv
-  lrwxrwxrwx 1 root root      8 Dec 19 01:33 nisdomainname -> hostname
-  lrwxrwxrwx 1 root root     14 Apr  2 18:25 pidof -> /sbin/killall5
-  -rwxr-xr-x 1 root root  67608 Sep 20  2022 pwd
-  lrwxrwxrwx 1 root root      4 Apr 23 09:24 rbash -> bash
-  -rwxr-xr-x 1 root root  67600 Sep 20  2022 readlink
-  -rwxr-xr-x 1 root root  67672 Sep 20  2022 rm
-  -rwxr-xr-x 1 root root  67600 Sep 20  2022 rmdir
-  -rwxr-xr-x 1 root root  67400 Nov  2  2022 run-parts
-  -rwxr-xr-x 1 root root 133372 Jan  5 07:55 sed
-  lrwxrwxrwx 1 root root      4 Jan  5 01:20 sh -> dash
-  -rwxr-xr-x 1 root root  67584 Sep 20  2022 sleep
-  -rwxr-xr-x 1 root root  67644 Sep 20  2022 stty
-  -rwsr-xr-x 1 root root  50800 Mar 22 21:02 su
-  -rwxr-xr-x 1 root root  67584 Sep 20  2022 sync
-  -rwxr-xr-x 1 root root 336764 Apr  6 02:25 tar
-  -rwxr-xr-x 1 root root  67144 Nov  2  2022 tempfile
-  -rwxr-xr-x 1 root root 133224 Sep 20  2022 touch
-  -rwxr-xr-x 1 root root  67548 Sep 20  2022 true
-  -rwxr-xr-x 1 root root   9768 Mar 22 20:15 ulockmgr_server
-  -rwsr-xr-x 1 root root  22108 Mar 22 21:02 umount
-  -rwxr-xr-x 1 root root  67572 Sep 20  2022 uname
-  -rwxr-xr-x 2 root root   2346 Apr  9  2022 uncompress
-  -rwxr-xr-x 1 root root 133632 Sep 20  2022 vdir
-  -rwxr-xr-x 1 root root  42608 Mar 22 21:02 wdctl
-  lrwxrwxrwx 1 root root      8 Dec 19 01:33 ypdomainname -> hostname
-  -rwxr-xr-x 1 root root   1984 Apr  9  2022 zcat
-  -rwxr-xr-x 1 root root   1678 Apr  9  2022 zcmp
-  -rwxr-xr-x 1 root root   6460 Apr  9  2022 zdiff
-  -rwxr-xr-x 1 root root     29 Apr  9  2022 zegrep
-  -rwxr-xr-x 1 root root     29 Apr  9  2022 zfgrep
-  -rwxr-xr-x 1 root root   2081 Apr  9  2022 zforce
-  -rwxr-xr-x 1 root root   8103 Apr  9  2022 zgrep
-  -rwxr-xr-x 1 root root   2206 Apr  9  2022 zless
-  -rwxr-xr-x 1 root root   1842 Apr  9  2022 zmore
-  -rwxr-xr-x 1 root root   4577 Apr  9  2022 znew
-I: user script /srv/workspace/pbuilder/29051/tmp/hooks/D02_print_environment finished
+  -rwxr-xr-x 1 root root 838488 Apr 24 11:24 bash
+  -rwxr-xr-x 3 root root  67144 Sep 19  2022 bunzip2
+  -rwxr-xr-x 3 root root  67144 Sep 19  2022 bzcat
+  lrwxrwxrwx 1 root root      6 Sep 19  2022 bzcmp -> bzdiff
+  -rwxr-xr-x 1 root root   2225 Sep 19  2022 bzdiff
+  lrwxrwxrwx 1 root root      6 Sep 19  2022 bzegrep -> bzgrep
+  -rwxr-xr-x 1 root root   4893 Nov 28  2021 bzexe
+  lrwxrwxrwx 1 root root      6 Sep 19  2022 bzfgrep -> bzgrep
+  -rwxr-xr-x 1 root root   3775 Sep 19  2022 bzgrep
+  -rwxr-xr-x 3 root root  67144 Sep 19  2022 bzip2
+  -rwxr-xr-x 1 root root  67112 Sep 19  2022 bzip2recover
+  lrwxrwxrwx 1 root root      6 Sep 19  2022 bzless -> bzmore
+  -rwxr-xr-x 1 root root   1297 Sep 19  2022 bzmore
+  -rwxr-xr-x 1 root root  67632 Sep 21  2022 cat
+  -rwxr-xr-x 1 root root  67676 Sep 21  2022 chgrp
+  -rwxr-xr-x 1 root root  67644 Sep 21  2022 chmod
+  -rwxr-xr-x 1 root root  67684 Sep 21  2022 chown
+  -rwxr-xr-x 1 root root 133532 Sep 21  2022 cp
+  -rwxr-xr-x 1 root root 132868 Jan  6 03:20 dash
+  -rwxr-xr-x 1 root root 133220 Sep 21  2022 date
+  -rwxr-xr-x 1 root root  67732 Sep 21  2022 dd
+  -rwxr-xr-x 1 root root  68104 Sep 21  2022 df
+  -rwxr-xr-x 1 root root 133632 Sep 21  2022 dir
+  -rwxr-xr-x 1 root root  59128 Mar 23 23:02 dmesg
+  lrwxrwxrwx 1 root root      8 Dec 20 03:33 dnsdomainname -> hostname
+  lrwxrwxrwx 1 root root      8 Dec 20 03:33 domainname -> hostname
+  -rwxr-xr-x 1 root root  67560 Sep 21  2022 echo
+  -rwxr-xr-x 1 root root     41 Jan 25 04:43 egrep
+  -rwxr-xr-x 1 root root  67548 Sep 21  2022 false
+  -rwxr-xr-x 1 root root     41 Jan 25 04:43 fgrep
+  -rwxr-xr-x 1 root root  55748 Mar 23 23:02 findmnt
+  -rwsr-xr-x 1 root root  26208 Mar 23 22:15 fusermount
+  -rwxr-xr-x 1 root root 128608 Jan 25 04:43 grep
+  -rwxr-xr-x 2 root root   2346 Apr 10  2022 gunzip
+  -rwxr-xr-x 1 root root   6447 Apr 10  2022 gzexe
+  -rwxr-xr-x 1 root root  64220 Apr 10  2022 gzip
+  -rwxr-xr-x 1 root root  67032 Dec 20 03:33 hostname
+  -rwxr-xr-x 1 root root  67720 Sep 21  2022 ln
+  -rwxr-xr-x 1 root root  35132 Mar 23 23:51 login
+  -rwxr-xr-x 1 root root 133632 Sep 21  2022 ls
+  -rwxr-xr-x 1 root root 136808 Mar 23 23:02 lsblk
+  -rwxr-xr-x 1 root root  67800 Sep 21  2022 mkdir
+  -rwxr-xr-x 1 root root  67764 Sep 21  2022 mknod
+  -rwxr-xr-x 1 root root  67596 Sep 21  2022 mktemp
+  -rwxr-xr-x 1 root root  38504 Mar 23 23:02 more
+  -rwsr-xr-x 1 root root  38496 Mar 23 23:02 mount
+  -rwxr-xr-x 1 root root   9824 Mar 23 23:02 mountpoint
+  -rwxr-xr-x 1 root root 133532 Sep 21  2022 mv
+  lrwxrwxrwx 1 root root      8 Dec 20 03:33 nisdomainname -> hostname
+  lrwxrwxrwx 1 root root     14 Apr  3 20:25 pidof -> /sbin/killall5
+  -rwxr-xr-x 1 root root  67608 Sep 21  2022 pwd
+  lrwxrwxrwx 1 root root      4 Apr 24 11:24 rbash -> bash
+  -rwxr-xr-x 1 root root  67600 Sep 21  2022 readlink
+  -rwxr-xr-x 1 root root  67672 Sep 21  2022 rm
+  -rwxr-xr-x 1 root root  67600 Sep 21  2022 rmdir
+  -rwxr-xr-x 1 root root  67400 Nov  3  2022 run-parts
+  -rwxr-xr-x 1 root root 133372 Jan  6 09:55 sed
+  lrwxrwxrwx 1 root root      9 May 31 01:21 sh -> /bin/bash
+  -rwxr-xr-x 1 root root  67584 Sep 21  2022 sleep
+  -rwxr-xr-x 1 root root  67644 Sep 21  2022 stty
+  -rwsr-xr-x 1 root root  50800 Mar 23 23:02 su
+  -rwxr-xr-x 1 root root  67584 Sep 21  2022 sync
+  -rwxr-xr-x 1 root root 336764 Apr  7 04:25 tar
+  -rwxr-xr-x 1 root root  67144 Nov  3  2022 tempfile
+  -rwxr-xr-x 1 root root 133224 Sep 21  2022 touch
+  -rwxr-xr-x 1 root root  67548 Sep 21  2022 true
+  -rwxr-xr-x 1 root root   9768 Mar 23 22:15 ulockmgr_server
+  -rwsr-xr-x 1 root root  22108 Mar 23 23:02 umount
+  -rwxr-xr-x 1 root root  67572 Sep 21  2022 uname
+  -rwxr-xr-x 2 root root   2346 Apr 10  2022 uncompress
+  -rwxr-xr-x 1 root root 133632 Sep 21  2022 vdir
+  -rwxr-xr-x 1 root root  42608 Mar 23 23:02 wdctl
+  lrwxrwxrwx 1 root root      8 Dec 20 03:33 ypdomainname -> hostname
+  -rwxr-xr-x 1 root root   1984 Apr 10  2022 zcat
+  -rwxr-xr-x 1 root root   1678 Apr 10  2022 zcmp
+  -rwxr-xr-x 1 root root   6460 Apr 10  2022 zdiff
+  -rwxr-xr-x 1 root root     29 Apr 10  2022 zegrep
+  -rwxr-xr-x 1 root root     29 Apr 10  2022 zfgrep
+  -rwxr-xr-x 1 root root   2081 Apr 10  2022 zforce
+  -rwxr-xr-x 1 root root   8103 Apr 10  2022 zgrep
+  -rwxr-xr-x 1 root root   2206 Apr 10  2022 zless
+  -rwxr-xr-x 1 root root   1842 Apr 10  2022 zmore
+  -rwxr-xr-x 1 root root   4577 Apr 10  2022 znew
+I: user script /srv/workspace/pbuilder/5929/tmp/hooks/D02_print_environment finished
  -> Attempting to satisfy build-dependencies
  -> Creating pbuilder-satisfydepends-dummy package
 Package: pbuilder-satisfydepends-dummy
@@ -262,7 +294,7 @@
 Get: 60 http://deb.debian.org/debian bookworm/main armhf libgmp3-dev armhf 2:6.2.1+dfsg1-1.1 [331 kB]
 Get: 61 http://deb.debian.org/debian bookworm/main armhf libzarith-ocaml-dev armhf 1.12-1+b1 [90.2 kB]
 Get: 62 http://deb.debian.org/debian bookworm/main armhf libcoq-core-ocaml-dev armhf 8.16.1+dfsg-1+b2 [43.1 MB]
-Fetched 310 MB in 35s (8861 kB/s)
+Fetched 310 MB in 34s (9021 kB/s)
 debconf: delaying package configuration, since apt-utils is not installed
 Selecting previously unselected package libpython3.11-minimal:armhf.
 (Reading database ... 
(Reading database ... 5%
(Reading database ... 10%
(Reading database ... 15%
(Reading database ... 20%
(Reading database ... 25%
(Reading database ... 30%
(Reading database ... 35%
(Reading database ... 40%
(Reading database ... 45%
(Reading database ... 50%
(Reading database ... 55%
(Reading database ... 60%
(Reading database ... 65%
(Reading database ... 70%
(Reading database ... 75%
(Reading database ... 80%
(Reading database ... 85%
(Reading database ... 90%
(Reading database ... 95%
(Reading database ... 100%
(Reading database ... 19324 files and directories currently installed.)
@@ -526,8 +558,19 @@
 Writing extended state information...
 Building tag database...
  -> Finished parsing the build-deps
+Reading package lists...
+Building dependency tree...
+Reading state information...
+usrmerge is already the newest version (35).
+0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded.
 I: Building the package
-I: Running cd /build/coq-hott-8.16/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S  > ../coq-hott_8.16-2_source.changes
+I: user script /srv/workspace/pbuilder/5929/tmp/hooks/A99_set_merged_usr starting
+Re-configuring usrmerge...
+removed '/etc/unsupported-skip-usrmerge-conversion'
+The system has been successfully converted.
+I: user script /srv/workspace/pbuilder/5929/tmp/hooks/A99_set_merged_usr finished
+hostname: Name or service not known
+I: Running cd /build/coq-hott-8.16/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-genchanges -S  > ../coq-hott_8.16-2_source.changes
 dpkg-buildpackage: info: source package coq-hott
 dpkg-buildpackage: info: source version 8.16-2
 dpkg-buildpackage: info: source distribution unstable
@@ -547,7 +590,7 @@
    dh_autoreconf
    dh_auto_configure
    dh_auto_build
-	make -j3 "INSTALL=install --strip-program=true"
+	make -j4 "INSTALL=install --strip-program=true"
 make[1]: Entering directory '/build/coq-hott-8.16'
 bash etc/generate_coqproject.sh
 Warning: Not a git clone, using find instead
@@ -565,16 +608,16 @@
 COQC theories/Tactics/Nameless.v
 COQC theories/Categories/Category/Core.v
 COQC theories/Axioms/Funext.v
+COQC theories/Basics/Hexadecimal.v
 COQC theories/Categories/Functor/Core.v
 COQC theories/Categories/Category/Strict.v
 COQC theories/Categories/Category/Sum.v
-COQC theories/Basics/Hexadecimal.v
 COQC theories/Categories/Functor/Composition/Core.v
 COQC theories/Categories/Functor/Identity.v
 COQC theories/Categories/NaturalTransformation/Core.v
 COQC theories/Basics/Numeral.v
-COQC theories/Categories/NaturalTransformation/Composition/Core.v
 COQC theories/Basics/Nat.v
+COQC theories/Categories/NaturalTransformation/Composition/Core.v
 COQC theories/Basics/Tactics.v
 COQC theories/Basics/PathGroupoids.v
 COQC theories/Basics/UniverseLevel.v
@@ -587,16 +630,18 @@
 COQC theories/Basics/Decidable.v
 COQC theories/Basics.v
 COQC theories/Types/Unit.v
-COQC theories/Types/Paths.v
 COQC theories/Types/Empty.v
+COQC theories/Types/Paths.v
 COQC theories/WildCat/Core.v
 COQC theories/Diagrams/CommutativeSquares.v
 COQC theories/Colimits/GraphQuotient.v
 COQC theories/Spaces/Pos/Core.v
 COQC theories/Types/Prod.v
-COQC theories/Types/Forall.v
 COQC theories/Spaces/Pos/Spec.v
-COQC theories/Types/Arrow.v
+COQC theories/Types/Forall.v
+COQC theories/Spaces/Pos.v
+COQC theories/Spaces/Int/Core.v
+COQC theories/Spaces/Int/Spec.v
 COQC theories/WildCat/Equiv.v
 COQC theories/WildCat/Sigma.v
 COQC theories/WildCat/Paths.v
@@ -604,49 +649,47 @@
 COQC theories/WildCat/EmptyCat.v
 COQC theories/WildCat/Sum.v
 COQC theories/WildCat/Forall.v
-COQC theories/Spaces/Pos.v
 COQC theories/Tactics.v
 COQC theories/Categories/Category/Pi.v
 COQC theories/Categories/Category/Prod.v
-COQC theories/Types/Sigma.v
+COQC theories/Types/Arrow.v
+COQC theories/Spaces/Int/Equiv.v
 COQC theories/WildCat/Square.v
 COQC theories/WildCat/Prod.v
 COQC theories/WildCat/Induced.v
 COQC theories/WildCat/Universe.v
 COQC theories/WildCat/PointedCat.v
+COQC theories/Types/Sigma.v
+COQC theories/WildCat/NatTrans.v
+COQC theories/WildCat/EquivGpd.v
+COQC theories/WildCat/TwoOneCat.v
+COQC theories/Types/Equiv.v
+COQC theories/Types/WType.v
+COQC theories/WildCat/FunctorCat.v
 COQC theories/NullHomotopy.v
 COQC theories/HIT/Interval.v
-COQC theories/Spaces/Int/Core.v
 COQC theories/Limits/Equalizer.v
 COQC theories/Categories/Category/Sigma/Core.v
-COQC theories/Types/Equiv.v
-COQC theories/Types/WType.v
-COQC theories/WildCat/NatTrans.v
-COQC theories/Spaces/Int/Spec.v
 COQC theories/Types/Bool.v
 COQC theories/Types/IWType.v
 COQC theories/EquivGroupoids.v
-COQC theories/Spaces/Int/Equiv.v
 COQC theories/Types/Universe.v
 COQC theories/Types/Sum.v
-COQC theories/WildCat/FunctorCat.v
-COQC theories/WildCat/EquivGpd.v
-COQC theories/WildCat/TwoOneCat.v
+COQC theories/WildCat/Opposite.v
 COQC theories/Spaces/Int/LoopExp.v
 COQC theories/Axioms/Univalence.v
+COQC theories/WildCat/Yoneda.v
+COQC theories/Spaces/Int.v
 COQC theories/Types.v
-COQC theories/WildCat/Opposite.v
 COQC theories/Cubical/DPath.v
 COQC theories/PathAny.v
 COQC theories/HProp.v
 COQC theories/Equiv/PathSplit.v
-COQC theories/TruncType.v
 COQC theories/Equiv/BiInv.v
 COQC theories/Equiv/Relational.v
 COQC theories/Misc.v
 COQC theories/ExcludedMiddle.v
 COQC theories/PropResizing/PropResizing.v
-COQC theories/Spaces/Int.v
 COQC theories/Diagrams/Graph.v
 COQC theories/Spaces/List.v
 COQC theories/Spaces/Cantor.v
@@ -655,46 +698,54 @@
 COQC theories/Metatheory/Core.v
 COQC theories/Categories/Category/Morphisms.v
 COQC theories/Categories/Functor/Paths.v
-COQC theories/Categories/Category/Univalent.v
 COQC theories/Categories/Category/Paths.v
 COQC theories/Categories/NaturalTransformation/Paths.v
 COQC theories/Categories/GroupoidCategory/Core.v
-COQC theories/Categories/IndiscreteCategory.v
 COQC theories/Categories/Functor/Prod/Core.v
 COQC theories/Categories/Functor/Composition/Laws.v
 COQC theories/Categories/Functor/Sum.v
-COQC theories/Categories/GroupoidCategory/Morphisms.v
 COQC theories/Categories/ExponentialLaws/Tactics.v
 COQC theories/PropResizing/ImpredicativeTruncation.v
-COQC theories/WildCat/Yoneda.v
+COQC theories/WildCat/Adjoint.v
 COQC theories/Cubical/PathSquare.v
 COQC theories/HSet.v
 COQC theories/Colimits/Coeq.v
-COQC theories/Functorish.v
+COQC theories/TruncType.v
 COQC theories/Diagrams/Diagram.v
 COQC theories/Spaces/TwoSphere.v
 COQC theories/Metatheory/FunextVarieties.v
 COQC theories/Categories/Category/Objects.v
 COQC theories/Categories/Category/Sigma/OnMorphisms.v
 COQC theories/Categories/Category/Sigma/OnObjects.v
+COQC theories/Categories/Category/Univalent.v
 COQC theories/Categories/Category/Subcategory/Wide.v
 COQC theories/Categories/NaturalTransformation/Identity.v
 COQC theories/Categories/DiscreteCategory.v
+COQC theories/Categories/IndiscreteCategory.v
 COQC theories/Categories/Functor/Prod/Universal.v
 COQC theories/Categories/SetCategory/Core.v
 COQC theories/Categories/NaturalTransformation/Sum.v
+COQC theories/Categories/GroupoidCategory/Morphisms.v
+COQC theories/Categories/SetCategory/Morphisms.v
+COQC theories/Categories/SetCategory/Functors/SetProp.v
+COQC theories/Categories/Grothendieck/ToSet/Core.v
 COQC theories/Categories/CategoryOfSections/Core.v
 COQC theories/Categories/Structure/Core.v
 COQC theories/PropResizing/Nat.v
-COQC theories/WildCat/Adjoint.v
+COQC theories/WildCat.v
 COQC theories/Cubical/DPathSquare.v
+COQC theories/Pointed/Core.v
 COQC theories/HFiber.v
+COQC theories/Colimits/Pushout.v
+COQC theories/Limits/Pullback.v
+COQC theories/Functorish.v
 COQC theories/HIT/Flattening.v
 COQC theories/Diagrams/Cone.v
 COQC theories/Diagrams/Cocone.v
 COQC theories/Diagrams/DDiagram.v
 COQC theories/Diagrams/Sequence.v
 COQC theories/Diagrams/Span.v
+COQC theories/Homotopy/Wedge.v
 COQC theories/Metatheory/IntervalImpliesFunext.v
 COQC theories/Metatheory/UnivalenceImpliesFunext.v
 COQC theories/Categories/Category/Dual.v
@@ -705,39 +756,38 @@
 COQC theories/Categories/HomFunctor.v
 COQC theories/Categories/Functor/Dual.v
 COQC theories/Categories/GroupoidCategory/Dual.v
-COQC theories/Categories/SetCategory/Morphisms.v
-COQC theories/Categories/SetCategory/Functors/SetProp.v
+COQC theories/Categories/SetCategory/Functors.v
 COQC theories/Categories/Profunctor/Core.v
-COQC theories/Categories/Grothendieck/ToSet/Core.v
+COQC theories/Categories/Grothendieck/ToSet/Morphisms.v
 COQC theories/Categories/CategoryOfSections.v
 COQC theories/Categories/Structure/Notations.v
 COQC theories/Categories/Structure/IdentityPrinciple.v
 COQC theories/Categories/Structure/Utf8.v
-COQC theories/WildCat.v
 COQC theories/Cubical/PathCube.v
-COQC theories/Pointed/Core.v
-COQC theories/Colimits/Pushout.v
-COQC theories/Limits/Pullback.v
+COQC theories/Colimits/MappingCylinder.v
+COQC theories/Pointed/pHomotopy.v
 COQC theories/Colimits/SpanPushout.v
 COQC theories/Diagrams/ConstantDiagram.v
 COQC theories/Diagrams/ParallelPair.v
-COQC theories/Homotopy/Wedge.v
-COQC theories/Categories/Category/Sigma.v
+COQC theories/Limits/Limit.v
+COQC theories/Colimits/Colimit.v
 COQC theories/Categories/Category/Subcategory.v
 COQC theories/Categories/FunctorCategory/Core.v
 COQC theories/Categories/InitialTerminalCategory/Core.v
 COQC theories/Categories/NaturalTransformation/Dual.v
 COQC theories/Categories/GroupoidCategory.v
-COQC theories/Categories/SetCategory/Functors.v
+COQC theories/Categories/SetCategory.v
 COQC theories/Categories/Profunctor/Identity.v
 COQC theories/Categories/Adjoint/UnitCounit.v
-COQC theories/Categories/Grothendieck/ToSet/Morphisms.v
+COQC theories/Categories/Grothendieck/ToSet/Univalent.v
 COQC theories/Categories/Structure.v
-COQC theories/Colimits/MappingCylinder.v
-COQC theories/Pointed/pHomotopy.v
-COQC theories/Limits/Limit.v
-COQC theories/Colimits/Colimit.v
-COQC theories/Categories/Category/Notations.v
+COQC theories/Extensions.v
+COQC theories/Pointed/pMap.v
+COQC theories/Colimits/Colimit_Pushout.v
+COQC theories/Colimits/Colimit_Coequalizer.v
+COQC theories/Colimits/Colimit_Flattening.v
+COQC theories/Colimits/Colimit_Sigma.v
+COQC theories/Categories/Category/Sigma.v
 COQC theories/Categories/NaturalTransformation/Composition/Functorial.v
 COQC theories/Categories/ExponentialLaws/Law4/Functors.v
 COQC theories/Categories/InitialTerminalCategory/Functors.v
@@ -749,8 +799,8 @@
 COQC theories/Categories/FunctorCategory/Notations.v
 COQC theories/Categories/Cat/Core.v
 COQC theories/Categories/FunctorCategory/Dual.v
+COQC theories/Categories/CategoryOfGroupoids.v
 COQC theories/Categories/InitialTerminalCategory/NaturalTransformations.v
-COQC theories/Categories/SetCategory.v
 COQC theories/Categories/Profunctor/Notations.v
 COQC theories/Categories/Profunctor/Representable.v
 COQC theories/Categories/Cat/Morphisms.v
@@ -761,23 +811,19 @@
 COQC theories/Categories/Comma/Core.v
 COQC theories/Categories/Adjoint/Core.v
 COQC theories/Categories/DualFunctor.v
-COQC theories/Categories/Grothendieck/ToSet/Univalent.v
-COQC theories/Categories/Category/Utf8.v
+COQC theories/Categories/Grothendieck/ToSet.v
 COQC theories/Categories/Profunctor/Utf8.v
 COQC theories/Cubical/DPathCube.v
-COQC theories/Extensions.v
-COQC theories/Pointed/pMap.v
-COQC theories/Colimits/Colimit_Pushout.v
-COQC theories/Colimits/Colimit_Coequalizer.v
-COQC theories/Colimits/Colimit_Flattening.v
-COQC theories/Colimits/Colimit_Sigma.v
-COQC theories/Categories/Category.v
+COQC theories/Factorization.v
+COQC theories/Modalities/ReflectiveSubuniverse.v
+COQC theories/Pointed/pEquiv.v
+COQC theories/Colimits/Colimit_Prod.v
+COQC theories/Categories/Category/Notations.v
 COQC theories/Categories/Functor/Prod/Functorial.v
 COQC theories/Categories/NaturalTransformation/Isomorphisms.v
 COQC theories/Categories/Functor/Pointwise/Properties.v
 COQC theories/Categories/NaturalTransformation/Notations.v
 COQC theories/Categories/FunctorCategory/Functorial.v
-COQC theories/Categories/CategoryOfGroupoids.v
 COQC theories/Categories/Pseudofunctor/Core.v
 COQC theories/Categories/Profunctor.v
 COQC theories/Categories/Cat.v
@@ -799,15 +845,13 @@
 COQC theories/Categories/Pseudofunctor/Identity.v
 COQC theories/Categories/PseudonaturalTransformation/Core.v
 COQC theories/Categories/LaxComma/CoreParts.v
-COQC theories/Categories/Grothendieck/ToSet.v
 COQC theories/Categories/Grothendieck/PseudofunctorToCat.v
+COQC theories/Categories/Category/Utf8.v
 COQC theories/Categories/Comma/Utf8.v
 COQC theories/Cubical.v
-COQC theories/Factorization.v
-COQC theories/Modalities/ReflectiveSubuniverse.v
-COQC theories/Pointed/pEquiv.v
-COQC theories/Colimits/Colimit_Prod.v
+COQC theories/Modalities/Modality.v
 COQC theories/Homotopy/Smash.v
+COQC theories/Categories/Category.v
 COQC theories/Categories/Functor/Prod.v
 COQC theories/Categories/Functor/Pointwise.v
 COQC theories/Categories/NaturalTransformation.v
@@ -820,56 +864,53 @@
 COQC theories/Categories/Adjoint/UnitCounitCoercions.v
 COQC theories/Categories/Adjoint/Composition/AssociativityLaw.v
 COQC theories/Categories/Adjoint/Composition/IdentityLaws.v
-COQC theories/Categories/Adjoint/Pointwise.v
-COQC theories/Categories/Adjoint/Functorial/Parts.v
 COQC theories/Categories/Pseudofunctor.v
 COQC theories/Categories/PseudonaturalTransformation.v
 COQC theories/Categories/LaxComma/CoreLaws.v
 COQC theories/Categories/Grothendieck/ToCat.v
-COQC theories/Modalities/Modality.v
-COQC theories/Colimits/Colimit_Pushout_Flattening.v
+COQC theories/Modalities/Accessible.v
 COQC theories/Modalities/Notnot.v
 COQC theories/Categories/ProductLaws.v
 COQC theories/Categories/InitialTerminalCategory/Notations.v
 COQC theories/Categories/ExponentialLaws/Law3/Law.v
-COQC theories/Categories/Comma/ProjectionFunctors.v
 COQC theories/Categories/Adjoint/UniversalMorphisms/Core.v
 COQC theories/Categories/Adjoint/HomCoercions.v
 COQC theories/Categories/Adjoint/Composition.v
-COQC theories/Categories/Adjoint/Functorial/Laws.v
+COQC theories/Categories/Adjoint/Pointwise.v
+COQC theories/Categories/Adjoint/Functorial/Parts.v
 COQC theories/Categories/Adjoint/Notations.v
 COQC theories/Categories/LaxComma/Core.v
 COQC theories/Categories/Grothendieck.v
 COQC theories/Categories/DependentProduct.v
 COQC theories/Categories/Adjoint/Utf8.v
-COQC theories/Modalities/Accessible.v
+COQC theories/Modalities/Localization.v
+COQC theories/Modalities/Identity.v
+COQC theories/Colimits/Colimit_Pushout_Flattening.v
 COQC theories/Categories/Functor/Composition/Functorial/Core.v
 COQC theories/Categories/InitialTerminalCategory.v
-COQC theories/Categories/ExponentialLaws/Law3.v
+COQC theories/Categories/Comma/ProjectionFunctors.v
 COQC theories/Categories/Comma/Functorial.v
 COQC theories/Categories/KanExtensions/Core.v
 COQC theories/Categories/Adjoint/UniversalMorphisms.v
+COQC theories/Categories/Adjoint/Functorial/Laws.v
 COQC theories/Categories/Limits/Core.v
 COQC theories/Categories/LaxComma/Notations.v
-COQC theories/Modalities/Localization.v
-COQC theories/Modalities/Identity.v
-COQC theories/Categories/ExponentialLaws.v
+COQC theories/Modalities/Descent.v
+COQC theories/Categories/ExponentialLaws/Law3.v
 COQC theories/Categories/Comma.v
 COQC theories/Categories/KanExtensions/Functors.v
 COQC theories/Categories/LaxComma.v
 COQC theories/Categories/LaxComma/Utf8.v
-COQC theories/Modalities/Descent.v
+COQC theories/Categories/ExponentialLaws.v
 COQC theories/Categories/KanExtensions.v
 COQC theories/Categories/Limits/Functors.v
-COQC theories/Categories/Limits.v
 COQC theories/Truncations/Core.v
-COQC theories/Categories/Adjoint/Functorial/Core.v
+COQC theories/Categories/Limits.v
 COQC theories/Homotopy/Suspension.v
-COQC theories/Categories/Adjoint/Functorial.v
-COQC theories/Categories/Adjoint.v
 COQC theories/Modalities/Separated.v
 COQC theories/Modalities/Nullification.v
 COQC theories/Truncations/Connectedness.v
+COQC theories/Categories/Adjoint/Functorial/Core.v
 COQC theories/Truncations.v
 COQC theories/Pointed/Loops.v
 COQC theories/Homotopy/Join.v
@@ -883,42 +924,41 @@
 COQC theories/Classes/interfaces/canonical_names.v
 COQC theories/Spaces/No/Core.v
 COQC theories/Spaces/Torus/Torus.v
+COQC theories/Categories/Adjoint/Functorial.v
 COQC theories/Categories/FundamentalPreGroupoidCategory.v
 COQC theories/Categories/HomotopyPreCategory.v
 COQC theories/Utf8.v
 COQC theories/Classes/interfaces/monad.v
 COQC theories/Metatheory/TruncImpliesFunext.v
-COQC theories/Pointed/pFiber.v
-COQC theories/Pointed/pTrunc.v
 COQC theories/Homotopy/BlakersMassey.v
 COQC theories/Idempotents.v
 COQC theories/Spaces/Nat.v
 COQC theories/HIT/FreeIntQuotient.v
 COQC theories/HIT/epi.v
 COQC theories/HIT/surjective_factor.v
-COQC theories/Colimits/Quotient.v
 COQC theories/Colimits/Sequential.v
 COQC theories/Modalities/Topological.v
 COQC theories/Modalities/Open.v
-COQC theories/Modalities/Closed.v
 COQC theories/Modalities/Meet.v
-COQC theories/Modalities/CoreflectiveSubuniverse.v
 COQC theories/Spaces/Finite/Fin.v
 COQC theories/Classes/interfaces/abstract_algebra.v
 COQC theories/Spaces/No/Negation.v
 COQC theories/Spaces/Torus/TorusEquivCircles.v
 COQC theories/Categories/ChainCategory.v
+COQC theories/Categories/Adjoint.v
 COQC theories/Classes/implementations/bool.v
 COQC theories/Classes/implementations/hprop_lattice.v
 COQC theories/Classes/implementations/pointwise.v
 COQC theories/Metatheory/UnivalenceVarieties.v
+COQC theories/Pointed/pFiber.v
+COQC theories/Pointed/pTrunc.v
 COQC theories/Homotopy/Freudenthal.v
 COQC theories/BoundedSearch.v
 COQC theories/HIT/iso.v
 COQC theories/HIT/quotient.v
-COQC theories/HIT/V.v
-COQC theories/Colimits/Quotient/Choice.v
-COQC theories/Modalities/Fracture.v
+COQC theories/Colimits/Quotient.v
+COQC theories/Modalities/Closed.v
+COQC theories/Modalities/CoreflectiveSubuniverse.v
 COQC theories/Spaces/Finite/FinNat.v
 COQC theories/Spaces/Finite/Finite.v
 COQC theories/Spaces/Finite/Tactics.v
@@ -942,15 +982,15 @@
 COQC theories/Classes/implementations/family_prod.v
 COQC theories/Metatheory/PropTrunc.v
 COQC theories/Pointed/pSusp.v
+COQC theories/HIT/V.v
+COQC theories/Colimits/Quotient/Choice.v
+COQC theories/Modalities/Fracture.v
 COQC theories/Spaces/Finite/FinInduction.v
 COQC theories/Spaces/No.v
 COQC theories/Algebra/Groups/Group.v
 COQC theories/Classes/theory/rings.v
 COQC theories/Classes/interfaces/naturals.v
 COQC theories/Classes/orders/orders.v
-COQC theories/Classes/isomorphisms/rings.v
-COQC theories/Classes/tactics/ring_quote.v
-COQC theories/Classes/theory/fields.v
 COQC theories/Sets/AC.v
 COQC theories/Sets/Hartogs.v
 COQC theories/Categories/Functor/Composition/Functorial/Attributes.v
@@ -964,30 +1004,32 @@
 COQC theories/Algebra/Groups/FreeGroup.v
 COQC theories/Classes/interfaces/integers.v
 COQC theories/Classes/orders/maps.v
-COQC theories/Classes/tactics/ring_pol.v
-COQC theories/Classes/theory/dec_fields.v
+COQC theories/Classes/isomorphisms/rings.v
+COQC theories/Classes/tactics/ring_quote.v
+COQC theories/Classes/theory/fields.v
 COQC theories/Homotopy/CayleyDickson.v
 COQC theories/Homotopy/EncodeDecode.v
 COQC theories/Spectra/Spectrum.v
-COQC theories/Sets/GCHtoAC.v
 COQC theories/Categories/Functor/Composition/Functorial.v
 COQC theories/Classes/interfaces/ua_setalgebra.v
-COQC theories/Classes/implementations/field_of_fractions.v
 COQC theories/Classes/interfaces/ua_congruence.v
 COQC theories/ObjectClassifier.v
 COQC theories/Spaces/Spheres.v
 COQC theories/Spaces/Finite.v
 COQC theories/Algebra/Groups/Image.v
 COQC theories/Algebra/Groups/Kernel.v
-COQC theories/Algebra/Groups/GroupCoeq.v
 COQC theories/Algebra/Universal/Algebra.v
 COQC theories/Classes/orders/semirings.v
+COQC theories/Classes/tactics/ring_pol.v
+COQC theories/Classes/theory/dec_fields.v
+COQC theories/Sets/GCHtoAC.v
 COQC theories/Categories/Functor/Composition.v
 COQC theories/Categories/Yoneda.v
 COQC theories/Classes/theory/ua_homomorphism.v
+COQC theories/Classes/implementations/field_of_fractions.v
 COQC theories/Homotopy/SuccessorStructure.v
 COQC theories/Algebra/Groups/QuotientGroup.v
-COQC theories/Algebra/Groups/Presentation.v
+COQC theories/Algebra/Groups/GroupCoeq.v
 COQC theories/Algebra/Universal/Homomorphism.v
 COQC theories/Algebra/Universal/Operation.v
 COQC theories/Classes/implementations/peano_naturals.v
@@ -1001,12 +1043,12 @@
 COQC theories/Classes/theory/ua_quotient_algebra.v
 COQC theories/Classes/theory/ua_prod_algebra.v
 COQC theories/Homotopy/ExactSequence.v
+COQC theories/Algebra/Groups/Presentation.v
 COQC theories/Algebra/Groups/Lagrange.v
 COQC theories/Algebra/Universal/Congruence.v
 COQC theories/Classes/theory/naturals.v
 COQC theories/Classes/tactics/ring_tac.v
 COQC theories/Classes/orders/fields.v
-COQC theories/Classes/orders/dec_fields.v
 COQC theories/Classes/interfaces/round.v
 COQC theories/Categories/Functor.v
 COQC theories/Categories/Notations.v
@@ -1015,30 +1057,31 @@
 COQC theories/Classes/tests/ring_tac.v
 COQC theories/Classes/theory/ua_first_isomorphism.v
 COQC theories/Classes/theory/ua_second_isomorphism.v
-COQC theories/Spaces/BAut.v
-COQC theories/Algebra/Groups/ShortExactSequence.v
 COQC theories/Algebra/Universal/TermAlgebra.v
 COQC theories/Classes/orders/nat_int.v
 COQC theories/Classes/implementations/natpair_integers.v
+COQC theories/Classes/orders/dec_fields.v
 COQC theories/Categories.v
 COQC theories/Categories/NaturalTransformation/Utf8.v
 COQC theories/Categories/Monoidal/MonoidalCategory.v
 COQC theories/Classes/theory/ua_third_isomorphism.v
-COQC theories/Spaces/BAut/Cantor.v
-COQC theories/Spaces/BAut/Bool.v
-COQC theories/Spaces/BAut/Rigid.v
-COQC theories/Algebra/Groups.v
+COQC theories/Spaces/BAut.v
+COQC theories/Algebra/Groups/ShortExactSequence.v
 COQC theories/Classes/orders/naturals.v
 COQC theories/Categories/FunctorCategory/Utf8.v
-COQC theories/Spaces/Universe.v
-COQC theories/Algebra/AbGroups/AbelianGroup.v
+COQC theories/Algebra/Groups.v
 COQC theories/Classes/theory/nat_distance.v
 COQC theories/Categories/Utf8.v
-COQC theories/Spaces/BAut/Bool/IncoherentIdempotent.v
+COQC theories/Spaces/BAut/Cantor.v
+COQC theories/Spaces/BAut/Bool.v
+COQC theories/Spaces/BAut/Rigid.v
+COQC theories/Algebra/AbGroups/AbelianGroup.v
+COQC theories/Spaces/Universe.v
 COQC theories/Algebra/AbGroups/Abelianization.v
 COQC theories/Algebra/AbGroups/AbPullback.v
 COQC theories/Algebra/AbGroups/AbSES/Core.v
 COQC theories/Algebra/AbGroups/Z.v
+COQC theories/Spaces/BAut/Bool/IncoherentIdempotent.v
 COQC theories/Algebra/AbGroups/AbPushout.v
 COQC theories/Algebra/AbGroups/AbSES/Ext.v
 COQC theories/Algebra/AbGroups/AbSES/Pullback.v
@@ -2684,12 +2727,14 @@
 dpkg-buildpackage: info: binary-only upload (no source included)
 dpkg-genchanges: info: not including original source code in upload
 I: copying local configuration
+I: user script /srv/workspace/pbuilder/5929/tmp/hooks/B01_cleanup starting
+I: user script /srv/workspace/pbuilder/5929/tmp/hooks/B01_cleanup finished
 I: unmounting dev/ptmx filesystem
 I: unmounting dev/pts filesystem
 I: unmounting dev/shm filesystem
 I: unmounting proc filesystem
 I: unmounting sys filesystem
 I: cleaning the build env 
-I: removing directory /srv/workspace/pbuilder/29051 and its subdirectories
-I: Current time: Mon May 29 23:18:07 -12 2023
-I: pbuilder-time-stamp: 1685445487
+I: removing directory /srv/workspace/pbuilder/5929 and its subdirectories
+I: Current time: Wed May 31 01:38:44 +14 2023
+I: pbuilder-time-stamp: 1685446724