Diff of the two buildlogs: -- --- b1/build.log 2024-04-21 23:24:51.975809688 +0000 +++ b2/build.log 2024-04-21 23:32:17.828824148 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Sun Apr 21 11:21:43 -12 2024 -I: pbuilder-time-stamp: 1713741703 +I: Current time: Mon Apr 22 13:25:11 +14 2024 +I: pbuilder-time-stamp: 1713741911 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/trixie-reproducible-base.tgz] I: copying local configuration @@ -26,52 +26,84 @@ dpkg-source: info: unpacking coq-hierarchy-builder_1.6.0-1.debian.tar.xz I: Not using root during the build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/14889/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/14391/tmp/hooks/D01_modify_environment starting +debug: Running on virt32a. +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 Apr 21 23:26 /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/14391/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/14391/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build/reproducible-path' - 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='trixie' - 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]="21" [3]="1" [4]="release" [5]="arm-unknown-linux-gnueabihf") + BASH_VERSION='5.2.21(1)-release' + BUILDDIR=/build/reproducible-path + 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=trixie + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=arm + HOST_ARCH=armhf IFS=' ' - INVOCATION_ID='3c055f066d394c16b853cd7b8d467a32' - 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='14889' - PS1='# ' - PS2='> ' + INVOCATION_ID=167b14e2f2d84cda94db0533e9722990 + 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=14391 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.RaIOf6Je/pbuilderrc_w4u9 --distribution trixie --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.RaIOf6Je/b1 --logfile b1/build.log coq-hierarchy-builder_1.6.0-1.dsc' - SUDO_GID='110' - SUDO_UID='103' - 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.RaIOf6Je/pbuilderrc_OACP --distribution trixie --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.RaIOf6Je/b2 --logfile b2/build.log coq-hierarchy-builder_1.6.0-1.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 virt64z 6.1.0-20-arm64 #1 SMP Debian 6.1.85-1 (2024-04-11) aarch64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-20-armmp-lpae #1 SMP Debian 6.1.85-1 (2024-04-11) armv7l GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Apr 21 07:12 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/14889/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Apr 21 07:14 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/14391/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -161,6 +193,7 @@ Get: 40 http://deb.debian.org/debian trixie/main armhf ocaml armhf 4.14.1-1 [66.5 MB] Get: 41 http://deb.debian.org/debian trixie/main armhf ocaml-findlib armhf 1.9.6-1+b2 [468 kB] Get: 42 http://deb.debian.org/debian trixie/main armhf coq armhf 8.18.0+dfsg-1 [78.4 MB] +Ign http://deb.debian.org/debian trixie/main armhf coq armhf 8.18.0+dfsg-1 Get: 43 http://deb.debian.org/debian trixie/main armhf libdebhelper-perl all 13.15.3 [88.0 kB] Get: 44 http://deb.debian.org/debian trixie/main armhf libtool all 2.4.7-7 [517 kB] Get: 45 http://deb.debian.org/debian trixie/main armhf dh-autoreconf all 20 [17.1 kB] @@ -199,7 +232,8 @@ Get: 78 http://deb.debian.org/debian trixie/main armhf libelpi-ocaml-dev armhf 1.17.4-3+b1 [9262 kB] Get: 79 http://deb.debian.org/debian trixie/main armhf libcoq-elpi armhf 1.19.3-2+b1 [2563 kB] Get: 80 http://deb.debian.org/debian trixie/main armhf wdiff armhf 1.2.2-6 [118 kB] -Fetched 347 MB in 12s (28.2 MB/s) +Get: 81 http://deb.debian.org/debian trixie/main armhf coq armhf 8.18.0+dfsg-1 [78.4 MB] +Fetched 345 MB in 1min 4s (5369 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 ... 19635 files and directories currently installed.) @@ -465,8 +499,8 @@ Setting up tzdata (2024a-1) ... Current default time zone: 'Etc/UTC' -Local time is now: Sun Apr 21 23:22:49 UTC 2024. -Universal Time is now: Sun Apr 21 23:22:49 UTC 2024. +Local time is now: Sun Apr 21 23:28:47 UTC 2024. +Universal Time is now: Sun Apr 21 23:28:47 UTC 2024. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up autotools-dev (20220109.1) ... @@ -542,7 +576,11 @@ Building tag database... -> Finished parsing the build-deps I: Building the package -I: Running cd /build/reproducible-path/coq-hierarchy-builder-1.6.0/ && 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-hierarchy-builder_1.6.0-1_source.changes +I: user script /srv/workspace/pbuilder/14391/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for trixie +I: user script /srv/workspace/pbuilder/14391/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/coq-hierarchy-builder-1.6.0/ && 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-hierarchy-builder_1.6.0-1_source.changes dpkg-buildpackage: info: source package coq-hierarchy-builder dpkg-buildpackage: info: source version 1.6.0-1 dpkg-buildpackage: info: source distribution unstable @@ -572,7 +610,7 @@ dh_ocamlinit 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/reproducible-path/coq-hierarchy-builder-1.6.0' make config make[2]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.6.0' @@ -590,8 +628,8 @@ make test-suite make[2]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.6.0' make -f Makefile.coq -/usr/bin/coq_makefile -f _CoqProject.test-suite -o Makefile.test-suite.coq make[3]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.6.0' +/usr/bin/coq_makefile -f _CoqProject.test-suite -o Makefile.test-suite.coq Warning: . and tests overlap (used in -R or -Q) Warning: . and examples overlap (used in -R or -Q) @@ -604,8 +642,30 @@ COQC examples/readme.v COQC examples/hulk.v COQC examples/demo1/hierarchy_0.v -[1713741800.667112] HB: start module and section AddComoid_of_Type -[1713741800.667936] HB: converting arguments +COQC examples/demo1/hierarchy_1.v +COQC examples/demo1/hierarchy_2.v +[1713742200.642911] HB: begin module for builders +[1713742200.643860] HB: postulating factories +[1713742200.644373] HB: processing key context-item +[1713742200.645164] HB: processing mixin parameter a +[1713742200.646175] HB: declaring parameters and key as section variables +Here is the list of mixins to declare (the order matters): [] +COQC examples/demo1/hierarchy_3.v +File "./examples/hulk.v", line 143, characters 0-63: +Warning: +pulling in dependencies: [Feather_HasEqDec] + +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB,elpi,default] +File "./examples/demo1/hierarchy_2.v", line 57, characters 0-57: +Warning: +pulling in dependencies: +[hierarchy_2_AddComoid_of_TYPE, hierarchy_2_AddAG_of_AddComoid] + +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB,elpi,default] +[1713742203.253873] HB: start module and section AddComoid_of_Type +[1713742203.254813] HB: converting arguments indt-decl (parameter A explicit X0 c0 \ record AddComoid_of_Type (sort (typ X1)) Build_AddComoid_of_Type @@ -631,20 +691,24 @@ app [global (indt «eq»), X10 c0 c1 c2 c3 c4 c5, app [c2, c1, c5], c5]) c5 \ end-record)) to factories -[1713741800.668882] HB: processing key parameter -[1713741800.669805] HB: converting factories +[1713742203.255962] HB: processing key parameter +[1713742203.257120] HB: converting factories w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] to mixins -[1713741800.670197] HB: declaring context +[1713742203.257371] HB: declaring context w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] -[1713741800.670610] HB: declaring parameters and key as section variables +[1713742203.257691] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1713741800.682026] HB: declare mixin or factory -[1713741800.682367] HB: declare record axioms_ -[1713741800.723532] HB: declare notation Build -[1713741800.744170] HB: declare notation axioms -[1713741800.775069] HB: start module Exports -COQC examples/demo1/hierarchy_1.v -[1713741800.907912] HB: end modules and sections; export +[1713742203.271717] HB: declare mixin or factory +[1713742203.272140] HB: declare record axioms_ +[1713742203.322966] HB: declare notation Build +[1713742203.391913] HB: declare notation axioms +[1713742203.477769] HB: start module Exports +HB: A is canonically equipped with structures: + - Equality + Singleton + (from "./examples/hulk.v", line 216) + +[1713742203.884422] HB: end modules and sections; export «HB.examples.readme.AddComoid_of_Type.Exports» (* @@ -701,45 +765,45 @@ Notation AddComoid_of_Type X1 := ( AddComoid_of_Type.phant_axioms X1). *) -[1713741800.950366] HB: start module AddComoid -[1713741800.951011] HB: declare axioms record +[1713742204.044357] HB: start module AddComoid +[1713742204.045005] HB: declare axioms record w-params.nil A (sort (typ «HB.examples.readme.25»)) c0 \ [triple (indt «AddComoid_of_Type.axioms_») [] c0] -[1713741800.951557] HB: typing class field +[1713742204.051386] HB: typing class field indt «AddComoid_of_Type.axioms_» -[1713741800.966744] HB: declare type record -[1713741800.983781] HB: structure: new mixins +[1713742204.091877] HB: declare type record +[1713742204.136982] HB: structure: new mixins [indt «AddComoid_of_Type.axioms_»] -[1713741800.984257] HB: structure: mixin first class +[1713742204.137343] HB: structure: mixin first class [mixin-first-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»)] -[1713741800.984559] HB: declaring clone abbreviation -[1713741801.002375] HB: declaring pack_ constant -[1713741801.004279] HB: declaring pack_ constant = +[1713742204.137587] HB: declaring clone abbreviation +[1713742204.186197] HB: declaring pack_ constant +[1713742204.188774] HB: declaring pack_ constant = fun `A` (sort (typ «axioms_.u0»)) c0 \ fun `m` (app [global (indt «AddComoid_of_Type.axioms_»), c0]) c1 \ app [global (indc «Pack»), c0, app [global (indc «Class»), c0, c1]] -[1713741801.008188] HB: start module Exports -[1713741801.008872] HB: making coercion from type to target -[1713741801.009179] HB: declare sort coercion -[1713741801.009930] HB: exporting unification hints -[1713741801.010501] HB: exporting coercions from class to mixins -[1713741801.011245] HB: export class to mixin coercion for mixin +[1713742204.193815] HB: start module Exports +[1713742204.194744] HB: making coercion from type to target +[1713742204.195104] HB: declare sort coercion +[1713742204.196093] HB: exporting unification hints +[1713742204.196764] HB: exporting coercions from class to mixins +[1713742204.197607] HB: export class to mixin coercion for mixin readme_AddComoid_of_Type -[1713741801.012134] HB: accumulating various props -[1713741801.026777] HB: stop module Exports -[1713741801.036601] HB: declaring on_ abbreviation -[1713741801.051529] HB: declaring `copy` abbreviation -[1713741801.053535] HB: declaring on abbreviation -[1713741801.065096] HB: end modules; export +[1713742204.198751] HB: accumulating various props +[1713742204.216274] HB: stop module Exports +[1713742204.228362] HB: declaring on_ abbreviation +[1713742204.247519] HB: declaring `copy` abbreviation +[1713742204.250264] HB: declaring on abbreviation +[1713742204.264948] HB: end modules; export «HB.examples.readme.AddComoid.Exports» -[1713741801.067691] HB: exporting operations -[1713741801.069668] HB: export operation zero -[1713741801.076116] HB: export operation add -[1713741801.083308] HB: export operation addrA -[1713741801.091236] HB: export operation addrC -[1713741801.098857] HB: export operation add0r -[1713741801.104620] HB: operations meta-data module: ElpiOperations -[1713741801.125545] HB: abbreviation factory-by-classname +[1713742204.268231] HB: exporting operations +[1713742204.271229] HB: export operation zero +[1713742204.279924] HB: export operation add +[1713742204.289600] HB: export operation addrA +[1713742204.300285] HB: export operation addrC +[1713742204.310900] HB: export operation add0r +[1713742204.318677] HB: operations meta-data module: ElpiOperations +[1713742204.344987] HB: abbreviation factory-by-classname (* Module AddComoid. @@ -833,6 +897,11 @@ *) forall (M : AddComoid.type) (x : M), x + x = 0 : Prop +[1713742204.507533] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_AddAG_of_AddComoid +[1713742204.508215] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_Ring_of_AddAG +COQC examples/demo1/hierarchy_4.v AbelianGrp.phant_on_ BinNums_Z__canonical__readme_AbelianGrp (Phant BinNums_Z__canonical__readme_AbelianGrp) : AbelianGrp.axioms_ Z @@ -843,37 +912,6 @@ - AddComoid (from "./examples/readme.v", line 31) -COQC examples/demo1/hierarchy_2.v -[1713741802.293125] HB: begin module for builders -[1713741802.293661] HB: postulating factories -[1713741802.293852] HB: processing key context-item -[1713741802.294327] HB: processing mixin parameter a -[1713741802.294925] HB: declaring parameters and key as section variables -Here is the list of mixins to declare (the order matters): [] -File "./examples/hulk.v", line 143, characters 0-63: -Warning: -pulling in dependencies: [Feather_HasEqDec] - -Please list them or end the declaration with '&' -[HB.implicit-structure-dependency,HB,elpi,default] -COQC examples/demo1/hierarchy_3.v -HB: A is canonically equipped with structures: - - Equality - Singleton - (from "./examples/hulk.v", line 216) - -File "./examples/demo1/hierarchy_2.v", line 57, characters 0-57: -Warning: -pulling in dependencies: -[hierarchy_2_AddComoid_of_TYPE, hierarchy_2_AddAG_of_AddComoid] - -Please list them or end the declaration with '&' -[HB.implicit-structure-dependency,HB,elpi,default] -[1713741804.506363] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_AddAG_of_AddComoid -[1713741804.506966] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_Ring_of_AddAG -COQC examples/demo1/hierarchy_4.v COQC examples/demo1/hierarchy_5.v COQC examples/demo1/test_0_0.v COQC examples/demo1/test_1_0.v @@ -896,16 +934,14 @@ COQC examples/demo3/hierarchy_1.v COQC examples/demo3/hierarchy_2.v COQC examples/demo3/test_0_0.v -Finished transaction in 18.294 secs (17.773u,0.194s) (successful) -Finished transaction in 0.001 secs (0.001u,0.s) (successful) -COQC examples/demo3/test_1_0.v COQC examples/demo4/hierarchy_0.v +COQC examples/demo5/hierarchy_0.v +COQC examples/FSCD2020_material/V1.v inhab : ?s where ?T : [ |- Type] ?s : [ |- s1.type ?T] -COQC examples/demo5/hierarchy_0.v eq_refl : inhab = 7 : inhab = 7 eq_refl : inhab = (7 :: nil)%list @@ -917,7 +953,7 @@ fun X : s2.type nat => inj : nat -> X : forall X : s2.type nat, nat -> X s2_to_s1 not a defined object. -COQC examples/FSCD2020_material/V1.v +COQC examples/FSCD2020_material/V2.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -925,17 +961,7 @@ : forall s : Monoid.type, s -> s -> s @addNr : forall s : Ring.type, left_inverse 0 opp add -COQC examples/FSCD2020_material/V2.v COQC examples/FSCD2020_material/V3.v -Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. - -Arguments Monoid.Pack sort%type_scope class -@add - : forall s : Monoid.type, s -> s -> s -@addNr - : forall s : AbelianGroup.type, left_inverse 0 opp add -@addrC - : forall s : AbelianGroup.type, commutative add COQC examples/FSCD2020_material/V4.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. @@ -947,7 +973,6 @@ @addrC : forall s : AbelianGroup.type, commutative add COQC examples/FSCD2020_talk/V1.v -COQC examples/FSCD2020_talk/V2.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -957,6 +982,9 @@ : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add +COQC examples/FSCD2020_talk/V2.v +Finished transaction in 37.394 secs (32.751u,0.457s) (successful) +Finished transaction in 0.001 secs (0.001u,0.s) (successful) COQC examples/FSCD2020_talk/V3.v File "./examples/FSCD2020_talk/V2.v", line 17, characters 0-66: Warning: @@ -980,18 +1008,28 @@ Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] +Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. + +Arguments Monoid.Pack sort%type_scope class +@add + : forall s : Monoid.type, s -> s -> s +@addNr + : forall s : AbelianGroup.type, left_inverse 0 opp add +@addrC + : forall s : AbelianGroup.type, commutative add forall x y : ?t, x - (y + 0) = x : Prop where ?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) -forall x y : ?t, 1 + x = y * x - : Prop -where -?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) +COQC examples/Coq2020_material/CoqWS_expansion/withHB.v addrC : commutative add where ?s : [ |- CMonoid.type] +forall x y : ?t, 1 + x = y * x + : Prop +where +?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) File "./examples/Coq2020_material/CoqWS_abstract.v", line 23, characters 0-71: Warning: pulling in dependencies: [CoqWS_abstract_CMonoid_of_Type] @@ -1012,9 +1050,6 @@ : Prop add : A -> A -> A -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop -COQC examples/Coq2020_material/CoqWS_expansion/withHB.v forall (G : AbelianGrp.type) (x : G), x - x = 0 : Prop forall (S : SemiRing.type) (x : S), x * 1 + 0 = x @@ -1024,72 +1059,52 @@ forall x : Z, x * - (1 + x) = 0 + 1 : Prop COQC examples/Coq2020_material/CoqWS_expansion/withoutHB.v -Finished transaction in 16.837 secs (16.659u,0.04s) (successful) -Module Type - new_conceptLocked = - Sig - Parameter body : nat. - Parameter unlock : - body = - Init.Nat.of_num_uint - (Number.UIntDecimal - (Decimal.D9 - (Decimal.D9 - (Decimal.D9 - (Decimal.D9 (Decimal.D9 (Decimal.D9 Decimal.Nil))))))). - End -Module -new_concept - : new_conceptLocked -:= Struct - Definition body : nat. - Parameter unlock : - new_concept = - Init.Nat.of_num_uint - (Number.UIntDecimal - (Decimal.D9 - (Decimal.D9 - (Decimal.D9 - (Decimal.D9 (Decimal.D9 (Decimal.D9 Decimal.Nil))))))). - End - -Notation new_concept := new_concept.body +COQC tests/type_of_exported_ops.v +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop +COQC tests/duplicate_structure.v File "./examples/Coq2020_material/CoqWS_expansion/withoutHB.v", line 10, characters 50-62: Warning: The format modifier has no effect for only-parsing notations. [discarded-format-only-parsing,parsing,default] -COQC tests/type_of_exported_ops.v -COQC tests/duplicate_structure.v COQC tests/instance_params_no_type.v -File "./examples/hulk.v", line 315, characters 0-55: -Warning: -pulling in dependencies: [MissingJoin_isTop] - -Please list them or end the declaration with '&' -[HB.implicit-structure-dependency,HB,elpi,default] COQC tests/test_CS_db_filtering.v COQC tests/subtype.v COQC tests/infer.v -File "./examples/hulk.v", line 341, characters 0-55: -Warning: -pulling in dependencies: [GoodJoin_isTop] +HB.check: bar.type_ bool nat bool : Type +File "./tests/infer.v", line 20, characters 0-62: +Warning: Skipping test on Coq 8.18.0 as requested [HB.skip,HB,elpi,default] +bar.phant_type = +fun (A : Type) (P : foo.type) (_ : ssreflect.phant P) (B : Type) => +bar.type_ A P B + : Type -> forall P : foo.type, ssreflect.phant P -> Type -> Type -Please list them or end the declaration with '&' -[HB.implicit-structure-dependency,HB,elpi,default] -[1713741843.452178] HB: start module SubInhab -[1713741843.452867] HB: declare axioms record +Arguments bar.phant_type A%type_scope P _ B%type_scope +Notation bar.type _elpi_ctx_entry_3_was_A_ _elpi_ctx_entry_2_was_P_ + _elpi_ctx_entry_1_was_B_ := + (bar.phant_type _elpi_ctx_entry_3_was_A_ _ + (ssreflect.Phant _elpi_ctx_entry_2_was_P_) _elpi_ctx_entry_1_was_B_) +bar.phant_type bool Datatypes_nat__canonical__infer_foo + (ssreflect.Phant nat) bool + : Type +bar1.phant_type Datatypes_nat__canonical__infer_foo (ssreflect.Phant nat) + : Type +COQC tests/exports.v +COQC tests/log_impargs_record.v +[1713742258.861175] HB: start module SubInhab +[1713742258.867454] HB: declare axioms record w-params.cons T (sort (typ «HB.tests.subtype.280»)) c0 \ w-params.cons P (app [global (const «pred»), c0]) c1 \ w-params.nil sT (sort (typ «HB.tests.subtype.282»)) c2 \ [triple (indt «is_inhab.axioms_») [] c2, triple (indt «is_SUB.axioms_») [c0, c1] c2] -[1713741843.453503] HB: typing class field indt «is_inhab.axioms_» -[1713741843.454078] HB: typing class field indt «is_SUB.axioms_» -[1713741843.479782] HB: declare type record -[1713741843.493901] HB: structure: new mixins [] -[1713741843.494363] HB: structure: mixin first class [] -[1713741843.494452] HB: declaring clone abbreviation -[1713741843.509334] HB: declaring pack_ constant -[1713741843.513865] HB: declaring pack_ constant = +[1713742258.868435] HB: typing class field indt «is_inhab.axioms_» +[1713742258.869246] HB: typing class field indt «is_SUB.axioms_» +[1713742258.928075] HB: declare type record +[1713742258.966218] HB: structure: new mixins [] +[1713742258.971148] HB: structure: mixin first class [] +[1713742258.971601] HB: declaring clone abbreviation +[1713742259.007951] HB: declaring pack_ constant +[1713742259.020813] HB: declaring pack_ constant = fun `T` (sort (typ «axioms_.u0»)) c0 \ fun `P` (app [global (const «pred»), c0]) c1 \ fun `sT` (sort (typ «axioms_.u1»)) c2 \ @@ -1098,58 +1113,37 @@ app [global (indc «Pack»), c0, c1, c2, app [global (indc «Class»), c0, c1, c2, c3, c4]] -[1713741843.517664] HB: start module Exports -[1713741843.518280] HB: making coercion from type to target -[1713741843.518597] HB: declare sort coercion -[1713741843.519249] HB: exporting unification hints -[1713741843.520670] HB: declare coercion subtype_SubInhab__to__subtype_SUB -[1713741843.522824] HB: declare coercion hint +[1713742259.029511] HB: start module Exports +[1713742259.035513] HB: making coercion from type to target +[1713742259.036039] HB: declare sort coercion +[1713742259.036915] HB: exporting unification hints +[1713742259.038993] HB: declare coercion subtype_SubInhab__to__subtype_SUB +[1713742259.041439] HB: declare coercion hint subtype_SubInhab_class__to__subtype_SUB_class -[1713741843.534903] HB: declare unification hint +[1713742259.070389] HB: declare unification hint subtype_SubInhab__to__subtype_SUB -[1713741843.548850] HB: declare coercion subtype_SubInhab__to__subtype_Inhab -[1713741843.550646] HB: declare coercion hint +[1713742259.109412] HB: declare coercion subtype_SubInhab__to__subtype_Inhab +[1713742259.117180] HB: declare coercion hint subtype_SubInhab_class__to__subtype_Inhab_class -[1713741843.562894] HB: declare unification hint +[1713742259.148012] HB: declare unification hint subtype_SubInhab__to__subtype_Inhab -[1713741843.578415] HB: declare unification hint +[1713742259.191970] HB: declare unification hint join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB -[1713741843.592046] HB: exporting coercions from class to mixins -[1713741843.593215] HB: export class to mixin coercion for mixin +[1713742259.225077] HB: exporting coercions from class to mixins +[1713742259.226823] HB: export class to mixin coercion for mixin subtype_is_inhab -[1713741843.596026] HB: export class to mixin coercion for mixin +[1713742259.234433] HB: export class to mixin coercion for mixin subtype_is_SUB -[1713741843.597934] HB: accumulating various props -[1713741843.613150] HB: stop module Exports -[1713741843.624222] HB: declaring on_ abbreviation -[1713741843.644110] HB: declaring `copy` abbreviation -[1713741843.647182] HB: declaring on abbreviation -[1713741843.657222] HB: end modules; export +[1713742259.241622] HB: accumulating various props +[1713742259.277098] HB: stop module Exports +[1713742259.310228] HB: declaring on_ abbreviation +[1713742259.351282] HB: declaring `copy` abbreviation +[1713742259.358941] HB: declaring on abbreviation +[1713742259.383863] HB: end modules; export «HB.tests.subtype.SubInhab.Exports» -[1713741843.663217] HB: exporting operations -[1713741843.663611] HB: operations meta-data module: ElpiOperations -[1713741843.674837] HB: abbreviation factory-by-classname -HB.check: bar.type_ bool nat bool : Type -File "./tests/infer.v", line 20, characters 0-62: -Warning: Skipping test on Coq 8.18.0 as requested [HB.skip,HB,elpi,default] -bar.phant_type = -fun (A : Type) (P : foo.type) (_ : ssreflect.phant P) (B : Type) => -bar.type_ A P B - : Type -> forall P : foo.type, ssreflect.phant P -> Type -> Type - -Arguments bar.phant_type A%type_scope P _ B%type_scope -Notation bar.type _elpi_ctx_entry_3_was_A_ _elpi_ctx_entry_2_was_P_ - _elpi_ctx_entry_1_was_B_ := - (bar.phant_type _elpi_ctx_entry_3_was_A_ _ - (ssreflect.Phant _elpi_ctx_entry_2_was_P_) _elpi_ctx_entry_1_was_B_) -bar.phant_type bool Datatypes_nat__canonical__infer_foo - (ssreflect.Phant nat) bool - : Type -bar1.phant_type Datatypes_nat__canonical__infer_foo (ssreflect.Phant nat) - : Type -COQC tests/exports.v -COQC tests/log_impargs_record.v -COQC tests/compress_coe.v +[1713742259.399023] HB: exporting operations +[1713742259.404107] HB: operations meta-data module: ElpiOperations +[1713742259.429201] HB: abbreviation factory-by-classname (* Module A. @@ -1198,6 +1192,7 @@ Notation A X1 := ( A.phant_axioms X1). *) +COQC tests/compress_coe.v A.p : forall [T : Type] (record : A.axioms_ T) [x : T], A.f record x = x -> True @@ -1206,14 +1201,14 @@ A.p is transparent Expands to: Constant HB.tests.log_impargs_record.A.p COQC tests/funclass.v -[1713741846.851679] HB: exporting under the module path [] -[1713741846.852152] HB: exporting modules +[1713742263.345087] HB: exporting under the module path [] +[1713742263.346183] HB: exporting modules [Ring_of_TYPE.Exports, Ring.Exports, ElpiOperations1, RingExports, Dummy.Exports, URing.Exports, ElpiOperations2, dummy.Exports, Builders_3.dummy_Exports] -[1713741846.854985] HB: exporting CS instances +[1713742263.351187] HB: exporting CS instances [«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] -[1713741846.855807] HB: exporting Abbreviations [addr0, addrNK] +[1713742263.352656] HB: exporting Abbreviations [addr0, addrNK] forall (R : Enclosing.Ring.type) (x : R), x = x : Prop 0%G @@ -1241,6 +1236,18 @@ (Phantom (nat -> nat -> nat) Nat_mul__canonical__funclass_Monoid) : Monoid.axioms_ nat Init.Nat.mul : Monoid.axioms_ nat Init.Nat.mul +HB.check: +forall + w : wp.phant_type nat Nat_mul__canonical__funclass_Monoid + (Phantom (nat -> nat -> nat) Init.Nat.mul), w = w +: Prop +COQC tests/local_instance.v +p : pred nat + : pred nat +COQC tests/lock.v +Notation big := big.body +Expands to: Notation HB.tests.lock.X.big +COQC tests/interleave_context.v Datatypes_prod__canonical__compress_coe_D = fun D D' : D.type => {| @@ -1262,54 +1269,42 @@ : D.type -> D.type -> D.type Arguments Datatypes_prod__canonical__compress_coe_D D D' -COQC tests/local_instance.v -HB.check: -forall - w : wp.phant_type nat Nat_mul__canonical__funclass_Monoid - (Phantom (nat -> nat -> nat) Init.Nat.mul), w = w -: Prop -COQC tests/lock.v -p : pred nat - : pred nat -COQC tests/interleave_context.v +COQC tests/not_same_key.v default : nat : nat The command did fail as expected with message: The term "default" has type "nonempty.sort ?t" while it is expected to have type "nat". -Notation big := big.body -Expands to: Notation HB.tests.lock.X.big -COQC tests/not_same_key.v COQC tests/hb_pack.v -[1713741849.337642] HB: start module and section hasA -[1713741849.338375] HB: converting arguments +COQC tests/declare.v +[1713742269.543613] HB: start module and section hasA +[1713742269.544532] HB: converting arguments indt-decl (parameter T explicit X0 c0 \ record hasA (sort (typ X1)) Build_hasA (field [coercion off, canonical tt] a c0 c1 \ end-record)) to factories -[1713741849.338795] HB: processing key parameter -[1713741849.340179] HB: converting factories +[1713742269.545015] HB: processing key parameter +[1713742269.546095] HB: converting factories w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins -[1713741849.340622] HB: declaring context +[1713742269.546487] HB: declaring context w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] -[1713741849.340977] HB: declaring parameters and key as section variables +[1713742269.546993] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1713741849.348955] HB: declare mixin or factory -[1713741849.349215] HB: declare record axioms_ -[1713741849.369820] HB: declare notation Build -[1713741849.380560] HB: declare notation axioms -[1713741849.401558] HB: start module Exports -[1713741849.428414] HB: end modules and sections; export +[1713742269.565704] HB: declare mixin or factory +[1713742269.566064] HB: declare record axioms_ +[1713742269.600415] HB: declare notation Build +[1713742269.614311] HB: declare notation axioms +[1713742269.651128] HB: start module Exports +[1713742269.702407] HB: end modules and sections; export «HB.tests.hb_pack.hasA.Exports» hasA.type not a defined object. +hasB.type not a defined object. File "./tests/interleave_context.v", line 16, characters 0-52: Warning: pulling in dependencies: [interleave_context_HasA, interleave_context_HasB] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] -COQC tests/declare.v -hasB.type not a defined object. COQC tests/short.v hasAB.type not a defined object. hasA'.type not a defined object. @@ -1340,16 +1335,16 @@ : T * T AB3 : AB.type : AB.type -aType - : Type X : Foo.type A P : Foo.type A P +aType + : Type hasB.type not a defined object. T : Fun.type nat : Fun.type nat COQC tests/primitive_records.v -hasAB.type not a defined object. COQC tests/non_forgetful_inheritance.v +hasAB.type not a defined object. hasA'.type not a defined object. COQC tests/fix_loop.v Query assignments: @@ -1358,16 +1353,11 @@ File "./tests/non_forgetful_inheritance.v", line 35, characters 0-45: Warning: Could not enable unknown warning HB.non-forgetful-inheritance [unknown-warning,default] +COQC tests/hnf.v Query assignments: Ind = «A.axioms_» -COQC tests/hnf.v Query assignments: Ind = «A.type» -erefl ?t : ?t = ?t - : ?t = ?t -where -?t : [ |- Sq.type] -COQC tests/fun_instance.v Datatypes_nat__canonical__hnf_S = {| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_8 |} |} : S.type @@ -1380,22 +1370,64 @@ HB_unnamed_mixin_12 = Builders_2.HB_unnamed_factory_4 bool HB_unnamed_factory_9 : M.axioms_ bool +COQC tests/fun_instance.v +erefl ?t : ?t = ?t + : ?t = ?t +where +?t : [ |- Sq.type] COQC tests/issue284.v COQC tests/issue287.v COQC examples/demo2/stage10.v COQC examples/demo2/stage11.v -COQC examples/demo3/test_2_0.v +COQC examples/demo3/test_1_0.v File "./examples/demo2/stage10.v", line 4, characters 0-25: Warning: Hiding binding of key Q to Q_scope [hiding-delimiting-key,parsing,default] +Finished transaction in 44.231 secs (30.331u,0.157s) (successful) +Module Type + new_conceptLocked = + Sig + Parameter body : nat. + Parameter unlock : + body = + Init.Nat.of_num_uint + (Number.UIntDecimal + (Decimal.D9 + (Decimal.D9 + (Decimal.D9 + (Decimal.D9 (Decimal.D9 (Decimal.D9 Decimal.Nil))))))). + End +Module +new_concept + : new_conceptLocked +:= Struct + Definition body : nat. + Parameter unlock : + new_concept = + Init.Nat.of_num_uint + (Number.UIntDecimal + (Decimal.D9 + (Decimal.D9 + (Decimal.D9 + (Decimal.D9 (Decimal.D9 (Decimal.D9 Decimal.Nil))))))). + End + +Notation new_concept := new_concept.body File "./examples/demo2/stage11.v", line 3, characters 0-25: Warning: Hiding binding of key Q to Q_scope [hiding-delimiting-key,parsing,default] +COQC examples/demo3/test_2_0.v +File "./examples/hulk.v", line 315, characters 0-55: +Warning: +pulling in dependencies: [MissingJoin_isTop] + +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB,elpi,default] COQC tests/exports2.v -[1713741858.604836] HB: exporting under the module path [] -[1713741858.605676] HB: exporting modules [] -[1713741858.605994] HB: exporting CS instances [] -[1713741858.606195] HB: exporting Abbreviations [] +[1713742291.040812] HB: exporting under the module path [] +[1713742291.041466] HB: exporting modules [] +[1713742291.041860] HB: exporting CS instances [] +[1713742291.042249] HB: exporting Abbreviations [] Qcplus_opp_r: forall q : Qc, q + - q = Q2Qc 0 File "./examples/demo2/stage10.v", line 233, characters 0-27: Warning: The default and global localities for this command outside sections @@ -1408,6 +1440,12 @@ any surrounding modules. If you are fine with the change of semantics, disable this warning. [deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] +File "./examples/hulk.v", line 341, characters 0-55: +Warning: +pulling in dependencies: [GoodJoin_isTop] + +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB,elpi,default] File "./examples/demo2/stage11.v", line 364, characters 0-27: Warning: The default and global localities for this command outside sections are currently equivalent to the combination of the standard meaning of @@ -1420,30 +1458,30 @@ disable this warning. [deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] HB: skipping section opening -[1713741866.285677] HB: declare mixin instance +[1713742299.096046] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology -[1713741866.290475] HB: declare canonical mixin instance +[1713742299.102587] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology» -[1713741866.292755] HB: declare mixin instance +[1713742299.106081] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform -[1713741866.303499] HB: declare canonical mixin instance +[1713742299.121773] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform» -[1713741866.305585] HB: declare mixin instance +[1713742299.125018] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology -[1713741866.314072] HB: declare canonical mixin instance +[1713742299.136913] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology» -[1713741866.316076] HB: declare mixin instance +[1713742299.139942] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform -[1713741866.337692] HB: declare canonical mixin instance +[1713742299.176781] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform» -[1713741866.340883] HB: we can build a Stage11_UniformSpace_wo_Topology on +[1713742299.181587] HB: we can build a Stage11_UniformSpace_wo_Topology on Qc -[1713741866.341249] HB: declare canonical structure instance +[1713742299.182186] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology -[1713741866.341598] HB: Giving name HB_unnamed_mixin_49 to mixin instance +[1713742299.182740] HB: Giving name HB_unnamed_mixin_49 to mixin instance Builders_25.Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology Qc HB_unnamed_mixin_38 HB_unnamed_mixin_43 HB_unnamed_factory_44 -[1713741866.345610] HB: structure instance for +[1713742299.188040] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology is {| UniformSpace_wo_Topology.sort := Qc; @@ -1453,12 +1491,12 @@ HB_unnamed_mixin_49 |} |} -[1713741866.351683] HB: structure instance +[1713742299.195949] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology declared -[1713741866.353347] HB: we can build a Stage11_UniformSpace on Qc -[1713741866.353673] HB: declare canonical structure instance +[1713742299.198577] HB: we can build a Stage11_UniformSpace on Qc +[1713742299.199186] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace -[1713741866.354485] HB: structure instance for +[1713742299.200443] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace is {| UniformSpace.sort := Qc; @@ -1468,15 +1506,15 @@ UniformSpace.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_49 |} |} -[1713741866.360676] HB: structure instance +[1713742299.208475] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace declared -[1713741866.362603] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc -[1713741866.362933] HB: declare canonical structure instance +[1713742299.211437] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc +[1713742299.212029] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform -[1713741866.363890] HB: Giving name HB_unnamed_mixin_50 to mixin instance +[1713742299.213380] HB: Giving name HB_unnamed_mixin_50 to mixin instance Builders_25.to_JoinTAddAG_wo_Uniform Qc HB_unnamed_mixin_38 HB_unnamed_mixin_43 HB_unnamed_factory_44 -[1713741866.368324] HB: structure instance for +[1713742299.219353] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform is {| TAddAG_wo_Uniform.sort := Qc; @@ -1488,12 +1526,12 @@ HB_unnamed_mixin_50 |} |} -[1713741866.374343] HB: structure instance +[1713742299.227676] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform declared -[1713741866.377072] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc -[1713741866.377414] HB: declare canonical structure instance +[1713742299.232028] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc +[1713742299.232649] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined -[1713741866.378885] HB: structure instance for +[1713742299.234813] HB: structure instance for Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined is {| Uniform_TAddAG_unjoined.sort := Qc; @@ -1508,18 +1546,18 @@ HB_unnamed_mixin_49 |} |} -[1713741866.385178] HB: structure instance +[1713742299.243311] HB: structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined declared -[1713741866.389705] HB: we can build a Stage11_TAddAG on Qc -[1713741866.390066] HB: declare canonical structure instance +[1713742299.250672] HB: we can build a Stage11_TAddAG on Qc +[1713742299.251307] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG -[1713741866.391406] HB: Giving name HB_unnamed_mixin_51 to mixin instance +[1713742299.253183] HB: Giving name HB_unnamed_mixin_51 to mixin instance Builders_25.Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology Qc HB_unnamed_mixin_38 HB_unnamed_mixin_43 HB_unnamed_factory_44 -[1713741866.396815] HB: Giving name HB_unnamed_mixin_52 to mixin instance +[1713742299.260697] HB: Giving name HB_unnamed_mixin_52 to mixin instance Builders_25.Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform Qc HB_unnamed_mixin_38 HB_unnamed_mixin_43 HB_unnamed_factory_44 -[1713741866.401967] HB: structure instance for +[1713742299.267904] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG is {| TAddAG.sort := Qc; @@ -1533,7 +1571,7 @@ TAddAG.Stage11_Join_TAddAG_Uniform_mixin := HB_unnamed_mixin_52 |} |} -[1713741866.408738] HB: structure instance +[1713742299.277182] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG declared entourage : set (set (Qc * Qc)) : set (set (Qc * Qc)) @@ -1550,7 +1588,7 @@ create-stamp debian/debhelper-build-stamp dh_prep dh_auto_install - make -j3 install DESTDIR=/build/reproducible-path/coq-hierarchy-builder-1.6.0/debian/tmp AM_UPDATE_INFO_DIR=no "INSTALL=install --strip-program=true" + make -j4 install DESTDIR=/build/reproducible-path/coq-hierarchy-builder-1.6.0/debian/tmp AM_UPDATE_INFO_DIR=no "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.6.0' make -f Makefile.coq install make[2]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.6.0' @@ -1587,9 +1625,9 @@ dh_ocaml W: coq-hierarchy-builder doesn't resolve dependency on unit Hb dh_gencontrol -dpkg-gencontrol: warning: Depends field of package coq-hierarchy-builder: substitution variable ${shlibs:Depends} used, but is not defined dpkg-gencontrol: warning: Depends field of package libcoq-hierarchy-builder: substitution variable ${ocaml:Depends} used, but is not defined dpkg-gencontrol: warning: Depends field of package libcoq-hierarchy-builder: substitution variable ${shlibs:Depends} used, but is not defined +dpkg-gencontrol: warning: Depends field of package coq-hierarchy-builder: substitution variable ${shlibs:Depends} used, but is not defined dpkg-gencontrol: warning: package coq-hierarchy-builder: substitution variable ${ocaml:Depends} unused, but is defined dh_md5sums dh_builddeb @@ -1602,12 +1640,14 @@ dpkg-buildpackage: info: binary-only upload (no source included) dpkg-genchanges: info: including full source code in upload I: copying local configuration +I: user script /srv/workspace/pbuilder/14391/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/14391/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/14889 and its subdirectories -I: Current time: Sun Apr 21 11:24:48 -12 2024 -I: pbuilder-time-stamp: 1713741888 +I: removing directory /srv/workspace/pbuilder/14391 and its subdirectories +I: Current time: Mon Apr 22 13:32:13 +14 2024 +I: pbuilder-time-stamp: 1713742333