Diff of the two buildlogs: -- --- b1/build.log 2023-05-13 01:22:50.916685067 +0000 +++ b2/build.log 2023-05-13 01:29:44.906544109 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Thu Jun 13 19:40:38 -12 2024 -I: pbuilder-time-stamp: 1718350838 +I: Current time: Sat May 13 15:22:54 +14 2023 +I: pbuilder-time-stamp: 1683940974 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-hierarchy-builder_1.4.0.orig.tar.gz] I: copying [./coq-hierarchy-builder_1.4.0-2.debian.tar.xz] I: Extracting source -gpgv: Signature made Tue Oct 25 18:55:06 2022 -12 +gpgv: Signature made Wed Oct 26 20:55:06 2022 +14 gpgv: using RSA key 812EEFD8A3FBA4ACE4DF114B04C53BD7FE030551 gpgv: issuer "jpuydt@debian.org" gpgv: Can't check signature: No public key @@ -26,52 +26,84 @@ dpkg-source: info: unpacking coq-hierarchy-builder_1.4.0-2.debian.tar.xz I: Not using root during the build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/29157/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/14948/tmp/hooks/D01_modify_environment starting +debug: Running on codethink16-arm64. +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 13 15:23 /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/14948/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/14948/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='arm64' - DEBIAN_FRONTEND='noninteractive' + 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]="aarch64-unknown-linux-gnu") + 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=arm64 + DEBIAN_FRONTEND=noninteractive DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=8' - DISTRIBUTION='bookworm' - HOME='/var/lib/jenkins' - HOST_ARCH='arm64' + DIRSTACK=() + DISTRIBUTION=bookworm + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/var/lib/jenkins + HOSTNAME=i-capture-the-hostname + HOSTTYPE=aarch64 + HOST_ARCH=arm64 IFS=' ' - 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='29157' - PS1='# ' - PS2='> ' + LANG=C + LANGUAGE=nl_BE:nl + LC_ALL=C + MACHTYPE=aarch64-unknown-linux-gnu + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnu + 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=14948 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.qIxIkDUo/pbuilderrc_uyA6 --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.qIxIkDUo/b1 --logfile b1/build.log coq-hierarchy-builder_1.4.0-2.dsc' - SUDO_GID='117' - SUDO_UID='110' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - USERNAME='root' - _='/usr/bin/systemd-run' - http_proxy='http://192.168.101.16:3128' + 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.qIxIkDUo/pbuilderrc_7Pxi --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.qIxIkDUo/b2 --logfile b2/build.log --extrapackages usrmerge coq-hierarchy-builder_1.4.0-2.dsc' + SUDO_GID=117 + SUDO_UID=110 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + USERNAME=root + _='I: set' + http_proxy=http://192.168.101.16:3128 I: uname -a - Linux codethink15-arm64 4.15.0-210-generic #221-Ubuntu SMP Tue Apr 18 08:32:48 UTC 2023 aarch64 GNU/Linux + Linux i-capture-the-hostname 4.15.0-210-generic #221-Ubuntu SMP Tue Apr 18 08:32:48 UTC 2023 aarch64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Jun 11 04:47 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/29157/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 May 12 00:25 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/14948/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -196,7 +228,7 @@ Get: 75 http://deb.debian.org/debian bookworm/main arm64 libelpi-ocaml-dev arm64 1.16.8-1+b2 [10.9 MB] Get: 76 http://deb.debian.org/debian bookworm/main arm64 libcoq-elpi arm64 1.16.0-2+b1 [2513 kB] Get: 77 http://deb.debian.org/debian bookworm/main arm64 wdiff arm64 1.2.2-5 [119 kB] -Fetched 370 MB in 1min 12s (5138 kB/s) +Fetched 370 MB in 7s (54.5 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libpython3.11-minimal:arm64. (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 ... 19616 files and directories currently installed.) @@ -520,8 +552,17 @@ 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-hierarchy-builder-1.4.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.4.0-2_source.changes +I: user script /srv/workspace/pbuilder/14948/tmp/hooks/A99_set_merged_usr starting +Re-configuring usrmerge... +I: user script /srv/workspace/pbuilder/14948/tmp/hooks/A99_set_merged_usr finished +hostname: Temporary failure in name resolution +I: Running cd /build/coq-hierarchy-builder-1.4.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.4.0-2_source.changes dpkg-buildpackage: info: source package coq-hierarchy-builder dpkg-buildpackage: info: source version 1.4.0-2 dpkg-buildpackage: info: source distribution unstable @@ -564,8 +605,8 @@ make test-suite make[2]: Entering directory '/build/coq-hierarchy-builder-1.4.0' make -f Makefile.coq -/usr/bin/coq_makefile -f _CoqProject.test-suite -o Makefile.test-suite.coq make[3]: Entering directory '/build/coq-hierarchy-builder-1.4.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) @@ -583,8 +624,8 @@ COQC examples/demo1/hierarchy_3.v COQC examples/demo1/hierarchy_4.v COQC examples/demo1/hierarchy_5.v -[1718351003.495661] HB: start module and section AddComoid_of_Type -[1718351003.496848] HB: converting arguments +[1683941123.175142] HB: start module and section AddComoid_of_Type +[1683941123.176032] HB: converting arguments indt-decl (parameter A explicit X0 c0 \ record AddComoid_of_Type (sort (typ X1)) Build_AddComoid_of_Type @@ -610,19 +651,19 @@ app [global (indt «eq»), X10 c0 c1 c2 c3 c4 c5, app [c2, c1, c5], c5]) c5 \ end-record)) to factories -[1718351003.498652] HB: processing key parameter -[1718351003.500214] HB: converting factories +[1683941123.190184] HB: processing key parameter +[1683941123.191906] HB: converting factories w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] to mixins -[1718351003.500488] HB: declaring context +[1683941123.192261] HB: declaring context w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] -[1718351003.500927] HB: declaring parameters and key as section variables +[1683941123.192726] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1718351003.522400] HB: declare mixin or factory -[1718351003.522625] HB: declare record axioms_ -[1718351003.588568] HB: declare notation Build -[1718351003.626976] HB: declare notation axioms -[1718351003.678162] HB: start module Exports -[1718351003.737235] HB: end modules and sections; export +[1683941123.275253] HB: declare mixin or factory +[1683941123.275484] HB: declare record axioms_ +[1683941123.507111] HB: declare notation Build +[1683941123.655166] HB: declare notation axioms +[1683941123.883665] HB: start module Exports +[1683941124.115582] HB: end modules and sections; export «HB.examples.readme.AddComoid_of_Type.Exports» (* @@ -679,65 +720,65 @@ Notation AddComoid_of_Type X1 := ( AddComoid_of_Type.phant_axioms X1). *) -[1718351003.940973] HB: start module AddComoid -[1718351003.941648] HB: declare axioms record +[1683941124.975008] HB: start module AddComoid +[1683941124.975700] HB: declare axioms record w-params.nil A (sort (typ «HB.examples.readme.25»)) c0 \ [triple (indt «AddComoid_of_Type.axioms_») [] c0] -[1718351003.942308] HB: typing class field +[1683941124.976333] HB: typing class field indt «AddComoid_of_Type.axioms_» -[1718351004.184477] HB: declare type record -[1718351004.237781] HB: structure: new mixins +[1683941125.912839] HB: declare type record +[1683941126.026812] HB: structure: new mixins [indt «AddComoid_of_Type.axioms_»] -[1718351004.238068] HB: structure: mixin first class +[1683941126.027125] HB: structure: mixin first class [mixin-first-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»)] -[1718351004.238269] HB: declaring clone abbreviation -[1718351004.294431] HB: declaring pack_ constant -[1718351004.301204] HB: declaring pack_ constant = +[1683941126.027337] HB: declaring clone abbreviation +[1683941126.146522] HB: declaring pack_ constant +[1683941126.149292] HB: declaring pack_ constant = fun `A` (sort (typ «HB.examples.readme.25»)) c0 \ fun `m` (app [global (indt «AddComoid_of_Type.axioms_»), c0]) c1 \ app [global (indc «Pack»), c0, app [global (indc «Class»), c0, c1]] -[1718351004.310936] HB: start module Exports -[1718351004.315787] HB: making coercion from type to target -[1718351004.315957] HB: declare sort coercion -[1718351004.316907] HB: exporting unification hints -[1718351004.317394] HB: exporting coercions from class to mixins -[1718351004.318107] HB: export class to mixin coercion for mixin +[1683941126.193580] HB: start module Exports +[1683941126.194493] HB: making coercion from type to target +[1683941126.194664] HB: declare sort coercion +[1683941126.195724] HB: exporting unification hints +[1683941126.196274] HB: exporting coercions from class to mixins +[1683941126.197076] HB: export class to mixin coercion for mixin readme_AddComoid_of_Type -[1718351004.323313] HB: accumulating various props -[1718351004.374260] HB: stop module Exports -[1718351004.379882] HB: declaring on_ abbreviation -[1718351004.427993] HB: declaring `copy` abbreviation -[1718351004.439223] HB: declaring on abbreviation -[1718351004.443527] HB: eta expanded instances -[1718351004.457151] HB: postulating A -[1718351004.539337] HB: declare mixin instance +[1683941126.210574] HB: accumulating various props +[1683941126.320613] HB: stop module Exports +[1683941126.334278] HB: declaring on_ abbreviation +[1683941126.435088] HB: declaring `copy` abbreviation +[1683941126.454149] HB: declaring on abbreviation +[1683941126.466715] HB: eta expanded instances +[1683941126.488917] HB: postulating A +[1683941126.664323] HB: declare mixin instance readme_AddComoid__to__readme_AddComoid_of_Type -[1718351004.566415] HB: we can build a readme_AddComoid on eta A -[1718351004.575364] HB: declare canonical structure instance +[1683941126.719963] HB: we can build a readme_AddComoid on eta A +[1683941126.720800] HB: declare canonical structure instance structures_eta__canonical__readme_AddComoid -[1718351004.576437] HB: Giving name HB_unnamed_mixin_4 to mixin instance +[1683941126.730114] HB: Giving name HB_unnamed_mixin_4 to mixin instance readme_AddComoid_of_Type_mixin (eta A) HB_unnamed_factory_2 -[1718351004.588097] HB: structure instance for +[1683941126.761465] HB: structure instance for structures_eta__canonical__readme_AddComoid is {| sort := eta A; class := {| readme_AddComoid_of_Type_mixin := HB_unnamed_mixin_4 |} |} -[1718351004.616746] HB: structure instance +[1683941126.814663] HB: structure instance structures_eta__canonical__readme_AddComoid declared -[1718351004.617033] HB: closing instance section -[1718351004.621984] HB: end modules; export +[1683941126.814963] HB: closing instance section +[1683941126.828248] HB: end modules; export «HB.examples.readme.AddComoid.Exports» -[1718351004.633373] HB: export +[1683941126.841804] HB: export «HB.examples.readme.AddComoid.EtaAndMixinExports» -[1718351004.637266] HB: exporting operations -[1718351004.648418] HB: export operation zero -[1718351004.661505] HB: export operation add -[1718351004.688133] HB: export operation addrA -[1718351004.708537] HB: export operation addrC -[1718351004.736056] HB: export operation add0r -[1718351004.749055] HB: operations meta-data module: ElpiOperations -[1718351004.789444] HB: abbreviation factory-by-classname +[1683941126.845212] HB: exporting operations +[1683941126.860452] HB: export operation zero +[1683941126.902126] HB: export operation add +[1683941126.949046] HB: export operation addrA +[1683941127.029875] HB: export operation addrC +[1683941127.098624] HB: export operation add0r +[1683941127.131090] HB: operations meta-data module: ElpiOperations +[1683941127.247865] HB: abbreviation factory-by-classname (* Module AddComoid. @@ -853,11 +894,11 @@ forall (M : AddComoid.type) (x : M), x + x = 0 : Prop COQC examples/demo2/classical.v -[1718351005.758718] HB: begin module for builders -[1718351005.767728] HB: postulating factories -[1718351005.768264] HB: processing key context-item -[1718351005.769136] HB: processing mixin parameter a -[1718351005.770109] HB: declaring parameters and key as section variables +[1683941130.558534] HB: begin module for builders +[1683941130.578054] HB: postulating factories +[1683941130.578413] HB: processing key context-item +[1683941130.579264] HB: processing mixin parameter a +[1683941130.580128] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] AbelianGrp.phant_on_ BinNums_Z__canonical__readme_AbelianGrp (Phant BinNums_Z__canonical__readme_AbelianGrp) @@ -878,27 +919,24 @@ Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB] +[1683941143.791434] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_AddAG_of_AddComoid +[1683941143.791828] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_Ring_of_AddAG 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] -[1718351011.332883] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_AddAG_of_AddComoid -[1718351011.333237] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_Ring_of_AddAG +COQC examples/demo3/hierarchy_2.v +COQC examples/demo4/hierarchy_0.v HB: A is canonically equipped with structures: - Equality Singleton (from "./examples/hulk.v", line 216) -COQC examples/demo3/hierarchy_2.v -COQC examples/demo3/test_0_0.v -COQC examples/demo4/hierarchy_0.v COQC examples/demo5/hierarchy_0.v -COQC examples/FSCD2020_material/V1.v -COQC examples/FSCD2020_material/V2.v inhab : ?s where @@ -906,6 +944,8 @@ ?s : [ |- s1.type ?T] eq_refl : inhab = 7 : inhab = 7 +COQC examples/FSCD2020_material/V1.v +COQC examples/FSCD2020_material/V2.v eq_refl : inhab = (7 :: nil)%list : inhab = (7 :: nil)%list where @@ -916,6 +956,7 @@ : forall X : s2.type nat, nat -> X s2_to_s1 not a defined object. COQC examples/FSCD2020_material/V3.v +COQC examples/FSCD2020_material/V4.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -923,7 +964,13 @@ : forall s : Monoid.type, s -> s -> s @addNr : forall s : Ring.type, left_inverse 0 opp add -COQC examples/FSCD2020_material/V4.v +HB.check: +SemiRing_of_AddComoid.axioms_ + : (forall (A : Type) (m : AddMonoid_of_TYPE.axioms_ A), + AddComoid_of_AddMonoid.axioms_ A m -> Type) +: +forall (A : Type) (m : AddMonoid_of_TYPE.axioms_ A), +AddComoid_of_AddMonoid.axioms_ A m -> Type COQC examples/FSCD2020_talk/V1.v COQC examples/FSCD2020_talk/V2.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. @@ -935,13 +982,6 @@ : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add -HB.check: -SemiRing_of_AddComoid.axioms_ - : (forall (A : Type) (m : AddMonoid_of_TYPE.axioms_ A), - AddComoid_of_AddMonoid.axioms_ A m -> Type) -: -forall (A : Type) (m : AddMonoid_of_TYPE.axioms_ A), -AddComoid_of_AddMonoid.axioms_ A m -> Type COQC examples/FSCD2020_talk/V3.v COQC examples/Coq2020_material/CoqWS_demo.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. @@ -954,15 +994,7 @@ @addrC : forall s : AbelianGroup.type, commutative add COQC examples/Coq2020_material/CoqWS_abstract.v -File "./examples/FSCD2020_talk/V2.v", line 17, characters 0-66: -Warning: -pulling in dependencies: [V2_is_semigroup] - -Please list them or end the declaration with '&' -[HB.implicit-structure-dependency,HB] COQC examples/Coq2020_material/CoqWS_expansion/withHB.v -COQC examples/Coq2020_material/CoqWS_expansion/withoutHB.v -COQC tests/type_of_exported_ops.v add : ?s -> ?s -> ?s where @@ -971,39 +1003,44 @@ : commutative add where ?s : [ |- CMonoid.type] +File "./examples/FSCD2020_talk/V2.v", line 17, characters 0-66: +Warning: +pulling in dependencies: [V2_is_semigroup] + +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB] File "./examples/Coq2020_material/CoqWS_demo.v", line 73, characters 0-73: Warning: pulling in dependencies: [CoqWS_demo_CMonoid_of_Type] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB] -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] +COQC examples/Coq2020_material/CoqWS_expansion/withoutHB.v +forall x y : ?t, x - (y + 0) = x + : Prop +where +?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) +COQC tests/type_of_exported_ops.v addrC : commutative add where ?s : [ |- CMonoid.type] COQC tests/duplicate_structure.v -COQC tests/instance_params_no_type.v -forall x y : ?t, x - (y + 0) = x +forall x y : ?t, 1 + x = y * x : Prop where -?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) +?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) +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] File "./examples/Coq2020_material/CoqWS_abstract.v", line 23, characters 0-71: Warning: pulling in dependencies: [CoqWS_abstract_CMonoid_of_Type] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB] +COQC tests/instance_params_no_type.v COQC tests/test_CS_db_filtering.v -forall x y : ?t, 1 + x = y * x - : Prop -where -?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) -COQC tests/subtype.v -COQC tests/infer.v -COQC tests/exports.v forall (R : Ring.type) (x y : R), 1 * x = y - x : Prop forall @@ -1014,14 +1051,19 @@ ?t : [x : join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing ?t y : ?t |- Ring.type] (x, y cannot be used) +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop +COQC tests/subtype.v +add + : A -> A -> A +COQC tests/infer.v +COQC tests/exports.v forall (G : AbelianGrp.type) (x : G), x - x = 0 : Prop forall (S : SemiRing.type) (x : S), x * 1 + 0 = x : Prop forall (R : Ring.type) (x y : R), x * - (1 * y) = - x * y : Prop -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -1034,11 +1076,9 @@ forall x : Z, x * - (1 + x) = 0 + 1 : Prop COQC tests/log_impargs_record.v -add - : A -> A -> A -COQC tests/compress_coe.v forall x : Z, x * - (1 + x) = 0 + 1 : Prop +COQC tests/compress_coe.v COQC tests/funclass.v (* @@ -1089,6 +1129,14 @@ *) COQC tests/grefclass.v +A.p : +forall [T : Type] (record : A.axioms_ T) [x : T], A.f record x = x -> True + +A.p is not universe polymorphic +Arguments A.p [T]%type_scope record [x] _ +A.p is transparent +Expands to: Constant HB.tests.log_impargs_record.A.p +COQC tests/local_instance.v HB.check: bar.type_ bool Datatypes_nat__canonical__infer_foo bool : Type File "./tests/infer.v", line 20, characters 0-58: Warning: Skipping test on Coq 8.16.1 as requested [HB.skip,HB] @@ -1105,21 +1153,27 @@ bar.phant_type bool Datatypes_nat__canonical__infer_foo (ssreflect.Phant nat) bool : Type -[1718351034.775304] HB: start module SubInhab -[1718351034.775888] HB: declare axioms record +[1683941220.142742] HB: start module SubInhab +[1683941220.143361] HB: declare axioms record w-params.cons T (sort (typ «HB.tests.subtype.345»)) c0 \ w-params.cons P (app [global (const «pred»), c0]) c1 \ w-params.nil sT (sort (typ «HB.tests.subtype.347»)) c2 \ [triple (indt «is_inhab.axioms_») [] c2, triple (indt «is_SUB.axioms_») [c0, c1] c2] -[1718351034.776715] HB: typing class field indt «is_inhab.axioms_» -[1718351034.777464] HB: typing class field indt «is_SUB.axioms_» -[1718351034.806766] HB: declare type record -[1718351034.830963] HB: structure: new mixins [] -[1718351034.831225] HB: structure: mixin first class [] -[1718351034.831341] HB: declaring clone abbreviation -[1718351034.859810] HB: declaring pack_ constant -[1718351034.866848] HB: declaring pack_ constant = +[1683941220.144221] HB: typing class field indt «is_inhab.axioms_» +[1683941220.145021] HB: typing class field indt «is_SUB.axioms_» +id : forall {T : Type}, Monoid.type T -> T + +id is not universe polymorphic +Arguments id {T}%type_scope {s} +id is transparent +Expands to: Constant HB.tests.funclass.id +[1683941220.216225] HB: declare type record +[1683941220.289610] HB: structure: new mixins [] +[1683941220.289871] HB: structure: mixin first class [] +[1683941220.289992] HB: declaring clone abbreviation +[1683941220.362851] HB: declaring pack_ constant +[1683941220.390192] HB: declaring pack_ constant = fun `T` (sort (typ «HB.tests.subtype.345»)) c0 \ fun `P` (app [global (const «pred»), c0]) c1 \ fun `sT` (sort (typ «HB.tests.subtype.347»)) c2 \ @@ -1128,60 +1182,66 @@ app [global (indc «Pack»), c0, c1, c2, app [global (indc «Class»), c0, c1, c2, c3, c4]] -[1718351034.872370] HB: start module Exports -[1718351034.872945] HB: making coercion from type to target -[1718351034.873184] HB: declare sort coercion -[1718351034.873938] HB: exporting unification hints -[1718351034.878754] HB: declare coercion subtype_SubInhab__to__subtype_SUB -[1718351034.881803] HB: declare coercion hint +[1683941220.407622] HB: start module Exports +[1683941220.408214] HB: making coercion from type to target +[1683941220.408428] HB: declare sort coercion +[1683941220.409143] HB: exporting unification hints +[1683941220.430433] HB: declare coercion subtype_SubInhab__to__subtype_SUB +bar1.phant_type Datatypes_nat__canonical__infer_foo (ssreflect.Phant nat) + : Type +[1683941220.433292] HB: declare coercion hint subtype_SubInhab_class__to__subtype_SUB_class -[1718351034.904027] HB: declare unification hint +[1683941220.504179] HB: declare unification hint subtype_SubInhab__to__subtype_SUB -A.p : -forall [T : Type] (record : A.axioms_ T) [x : T], A.f record x = x -> True - -A.p is not universe polymorphic -Arguments A.p [T]%type_scope record [x] _ -A.p is transparent -Expands to: Constant HB.tests.log_impargs_record.A.p -[1718351034.922862] HB: declare coercion path compression rules -[1718351034.927602] HB: declare coercion subtype_SubInhab__to__subtype_Inhab -[1718351034.930179] HB: declare coercion hint +[1683941220.571317] HB: declare coercion path compression rules +[1683941220.596115] HB: declare coercion subtype_SubInhab__to__subtype_Inhab +[1683941220.603337] HB: declare coercion hint subtype_SubInhab_class__to__subtype_Inhab_class -[1718351034.948378] HB: declare unification hint +File "./tests/funclass.v", line 19, characters 54-64: +Warning: Notation plus_assoc is deprecated since 8.16. +The Arith.Plus file is obsolete. Use Nat.add_assoc instead. +[deprecated-syntactic-definition,deprecated] +[1683941220.666810] HB: declare unification hint subtype_SubInhab__to__subtype_Inhab -[1718351034.970851] HB: declare coercion path compression rules -[1718351035.023196] HB: declare unification hint +[1683941220.734199] HB: declare coercion path compression rules +COQC tests/lock.v +p : pred nat + : pred nat +[1683941220.886830] HB: declare unification hint join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB -[1718351035.043152] HB: exporting coercions from class to mixins -[1718351035.044493] HB: export class to mixin coercion for mixin +[1683941220.971044] HB: exporting coercions from class to mixins +[1683941220.972492] HB: export class to mixin coercion for mixin subtype_is_inhab -[1718351035.048822] HB: export class to mixin coercion for mixin +[1683941220.985015] HB: export class to mixin coercion for mixin subtype_is_SUB -[1718351035.052119] HB: accumulating various props -[1718351035.091347] HB: stop module Exports -[1718351035.099340] HB: declaring on_ abbreviation -COQC tests/local_instance.v -[1718351035.122440] HB: declaring `copy` abbreviation -[1718351035.125125] HB: declaring on abbreviation -[1718351035.131208] HB: eta expanded instances -[1718351035.141749] HB: postulating T -[1718351035.158436] HB: postulating P -[1718351035.165601] HB: postulating sT -[1718351035.222449] HB: declare mixin instance +[1683941220.992448] HB: accumulating various props +[1683941221.101350] HB: stop module Exports +COQC tests/interleave_context.v +Monoid.phant_on_ nat Nat_add__canonical__funclass_Monoid + (Phantom (nat -> nat -> nat) Nat_add__canonical__funclass_Monoid) + : Monoid.axioms_ nat Init.Nat.add + : Monoid.axioms_ nat Init.Nat.add +[1683941221.134476] HB: declaring on_ abbreviation +[1683941221.222594] HB: declaring `copy` abbreviation +[1683941221.224917] HB: declaring on abbreviation +[1683941221.246691] HB: eta expanded instances +[1683941221.273305] HB: postulating T +[1683941221.334083] HB: postulating P +[1683941221.347707] HB: postulating sT +[1683941221.546889] HB: declare mixin instance subtype_SubInhab__to__subtype_is_inhab -[1718351035.268932] HB: declare mixin instance +[1683941221.705356] HB: declare mixin instance subtype_SubInhab__to__subtype_is_SUB -[1718351035.305767] HB: skipping already existing subtype_Inhab instance on +[1683941221.830611] HB: skipping already existing subtype_Inhab instance on eta sT -[1718351035.308262] HB: skipping already existing subtype_Nontrivial +[1683941221.833003] HB: skipping already existing subtype_Nontrivial instance on eta sT -[1718351035.310352] HB: skipping already existing subtype_SUB instance on +[1683941221.847748] HB: skipping already existing subtype_SUB instance on eta sT -[1718351035.319906] HB: we can build a subtype_SubInhab on eta sT -[1718351035.320639] HB: declare canonical structure instance +[1683941221.867221] HB: we can build a subtype_SubInhab on eta sT +[1683941221.867999] HB: declare canonical structure instance structures_eta__canonical__subtype_SubInhab -[1718351035.322513] HB: structure instance for +[1683941221.878438] HB: structure instance for structures_eta__canonical__subtype_SubInhab is {| sort := eta sT; @@ -1191,55 +1251,35 @@ subtype_is_SUB_mixin := HB_unnamed_mixin_19 T P sT |} |} -[1718351035.342630] HB: structure instance +[1683941221.935511] HB: structure instance structures_eta__canonical__subtype_SubInhab declared -[1718351035.342915] HB: closing instance section -[1718351035.347151] HB: end modules; export +[1683941221.935813] HB: closing instance section +[1683941221.947867] HB: end modules; export «HB.tests.subtype.SubInhab.Exports» -[1718351035.359683] HB: export +[1683941221.969749] HB: export «HB.tests.subtype.SubInhab.EtaAndMixinExports» -[1718351035.362005] HB: exporting operations -[1718351035.362622] HB: operations meta-data module: ElpiOperations -[1718351035.367010] HB: abbreviation factory-by-classname -bar1.phant_type Datatypes_nat__canonical__infer_foo (ssreflect.Phant nat) - : Type -COQC tests/lock.v -p : pred nat - : pred nat -COQC tests/interleave_context.v -Notation big := big.body -Expands to: Notation HB.tests.lock.X.big +[1683941221.972242] HB: exporting operations +[1683941221.972900] HB: operations meta-data module: ElpiOperations +[1683941221.980474] HB: abbreviation factory-by-classname default : nat : nat -COQC tests/not_same_key.v -id : forall {T : Type}, Monoid.type T -> T - -id is not universe polymorphic -Arguments id {T}%type_scope {s} -id is transparent -Expands to: Constant HB.tests.funclass.id -COQC tests/hb_pack.v -File "./tests/funclass.v", line 19, characters 54-64: -Warning: Notation plus_assoc is deprecated since 8.16. -The Arith.Plus file is obsolete. Use Nat.add_assoc instead. -[deprecated-syntactic-definition,deprecated] The command did fail as expected with message: The term "default" has type "nonempty.sort ?t" while it is expected to have type "nat". -Monoid.phant_on_ nat Nat_add__canonical__funclass_Monoid - (Phantom (nat -> nat -> nat) Nat_add__canonical__funclass_Monoid) - : Monoid.axioms_ nat Init.Nat.add - : Monoid.axioms_ nat Init.Nat.add -COQC tests/declare.v -[1718351038.271139] HB: exporting under the module path [] -[1718351038.272136] HB: exporting modules +COQC tests/not_same_key.v +Monoid.phant_on_ nat Nat_mul__canonical__funclass_Monoid + (Phantom (nat -> nat -> nat) Nat_mul__canonical__funclass_Monoid) + : Monoid.axioms_ nat Init.Nat.mul + : Monoid.axioms_ nat Init.Nat.mul +[1683941224.689980] HB: exporting under the module path [] +[1683941224.690931] HB: exporting modules [Ring_of_TYPE.Exports, Ring.Exports, Ring.EtaAndMixinExports, ElpiOperations5, RingExports, Dummy.Exports, URing.Exports, URing.EtaAndMixinExports, ElpiOperations11, dummy.Exports, Builders_12.dummy_Exports] -[1718351038.282690] HB: exporting CS instances +[1683941224.713634] HB: exporting CS instances [«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] -[1718351038.292535] HB: exporting Abbreviations [addr0, addrNK] +[1683941224.715294] HB: exporting Abbreviations [addr0, addrNK] forall (R : Enclosing.Ring.type) (x : R), x = x : Prop 0%G @@ -1248,33 +1288,39 @@ ?s : [ |- Enclosing.Ring.type] Enclosing.zero : Z : Z +COQC tests/hb_pack.v +Notation big := big.body +Expands to: Notation HB.tests.lock.X.big +COQC tests/declare.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/short.v -[1718351039.339832] HB: start module and section hasA -[1718351039.340604] HB: converting arguments +COQC tests/primitive_records.v +[1683941229.254774] HB: start module and section hasA +[1683941229.255483] 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 -[1718351039.341036] HB: processing key parameter -[1718351039.342429] HB: converting factories +[1683941229.255904] HB: processing key parameter +[1683941229.257220] HB: converting factories w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins -[1718351039.342707] HB: declaring context +[1683941229.269819] HB: declaring context w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] -[1718351039.351325] HB: declaring parameters and key as section variables +[1683941229.270365] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1718351039.371763] HB: declare mixin or factory -[1718351039.371989] HB: declare record axioms_ -[1718351039.418808] HB: declare notation Build -[1718351039.453582] HB: declare notation axioms -Monoid.phant_on_ nat Nat_mul__canonical__funclass_Monoid - (Phantom (nat -> nat -> nat) Nat_mul__canonical__funclass_Monoid) - : Monoid.axioms_ nat Init.Nat.mul - : Monoid.axioms_ nat Init.Nat.mul -[1718351039.530072] HB: start module Exports -COQC tests/primitive_records.v -[1718351039.581565] HB: end modules and sections; export +[1683941229.303380] HB: declare mixin or factory +[1683941229.303605] HB: declare record axioms_ +[1683941229.370832] HB: declare notation Build +[1683941229.433810] HB: declare notation axioms +[1683941229.550869] HB: start module Exports +[1683941229.651000] HB: end modules and sections; export «HB.tests.hb_pack.hasA.Exports» hasA.type not a defined object. +COQC tests/non_forgetful_inheritance.v Datatypes_prod__canonical__compress_coe_D = fun D D' : D.type => {| @@ -1296,29 +1342,24 @@ : D.type -> D.type -> D.type Arguments Datatypes_prod__canonical__compress_coe_D D D' +COQC tests/fix_loop.v 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] -COQC tests/non_forgetful_inheritance.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/fix_loop.v +hasB.type not a defined object. aType : Type hasB.type not a defined object. -hasB.type not a defined object. COQC tests/test_synthesis_params.v +COQC tests/hnf.v Query assignments: Ind = «hasA.axioms_» hasAB.type not a defined object. -COQC tests/hnf.v hasA'.type not a defined object. +hasAB.type not a defined object. forall T : AB.type, unkeyed {| @@ -1342,30 +1383,29 @@ : hasB.phant_axioms A AB2 : AB.type : AB.type -hasAB.type not a defined object. pB : T * T : T * T AB3 : AB.type : AB.type +Query assignments: + Ind = «A.axioms_» hasA'.type not a defined object. COQC tests/fun_instance.v +COQC tests/issue284.v X : Foo.type A P : Foo.type A P Query assignments: - Ind = «A.axioms_» -COQC tests/issue284.v + Ind = «A.type» +COQC tests/issue287.v T : Fun.type nat : Fun.type nat -COQC tests/issue287.v -Query assignments: - Ind = «A.type» -COQC examples/demo1/test_0_0.v Datatypes_nat__canonical__hnf_S = {| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |} : S.type HB_unnamed_mixin_12 = {| M.x := f.y nat HB_unnamed_factory_10 + 1 |} : M.axioms_ nat +COQC examples/demo1/test_0_0.v Datatypes_bool__canonical__hnf_S = {| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_16 |} |} : S.type @@ -1373,11 +1413,11 @@ Builders_6.HB_unnamed_factory_8 bool HB_unnamed_factory_13 : M.axioms_ bool COQC examples/demo1/test_1_0.v -COQC examples/demo1/test_2_0.v erefl ?t : ?t = ?t : ?t = ?t where ?t : [ |- Sq.type] +COQC examples/demo1/test_2_0.v COQC examples/demo1/test_3_0.v COQC examples/demo1/test_3_3.v COQC examples/demo1/test_4_0.v @@ -1386,41 +1426,42 @@ COQC examples/demo1/test_5_3.v COQC examples/demo2/stage10.v COQC examples/demo2/stage11.v +COQC examples/demo3/test_0_0.v COQC examples/demo3/test_1_0.v COQC examples/demo3/test_2_0.v COQC tests/exports2.v -[1718351053.966117] HB: exporting under the module path [] -[1718351053.966526] HB: exporting modules [] -[1718351053.966792] HB: exporting CS instances [] -[1718351053.967091] HB: exporting Abbreviations [] +[1683941265.055180] HB: exporting under the module path [] +[1683941265.055622] HB: exporting modules [] +[1683941265.055893] HB: exporting CS instances [] +[1683941265.056165] HB: exporting Abbreviations [] Qcplus_opp_r: forall q : Qc, q + - q = Q2Qc 0 -Finished transaction in 51.81 secs (41.631u,0.642s) (successful) -Finished transaction in 0.001 secs (0.001u,0.s) (successful) +Finished transaction in 127.729 secs (42.554u,0.745s) (successful) +Finished transaction in 0.002 secs (0.002u,0.s) (successful) HB: skipping section opening -[1718351070.925777] HB: declare mixin instance +[1683941286.812428] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology -[1718351070.933298] HB: declare canonical mixin instance +[1683941286.821166] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology» -[1718351070.937210] HB: declare mixin instance +[1683941286.825444] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology -[1718351070.952753] HB: declare canonical mixin instance +[1683941286.843284] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology» -[1718351070.956898] HB: declare mixin instance +[1683941286.847998] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform -[1718351070.977317] HB: declare canonical mixin instance +[1683941286.870593] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform» -[1718351070.980853] HB: declare mixin instance +[1683941286.874782] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform -[1718351070.991564] HB: declare canonical mixin instance +[1683941286.887347] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform» -[1718351070.996936] HB: we can build a Stage11_UniformSpace_wo_Topology on +[1683941286.893460] HB: we can build a Stage11_UniformSpace_wo_Topology on Qc -[1718351070.997724] HB: declare canonical structure instance +[1683941286.894347] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology -[1718351070.998309] HB: Giving name HB_unnamed_mixin_92 to mixin instance +[1683941286.895033] HB: Giving name HB_unnamed_mixin_92 to mixin instance Builders_68.Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology Qc HB_unnamed_mixin_81 HB_unnamed_mixin_86 HB_unnamed_factory_87 -[1718351071.004434] HB: structure instance for +[1683941286.902264] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology is {| UniformSpace_wo_Topology.sort := Qc; @@ -1430,12 +1471,12 @@ HB_unnamed_mixin_92 |} |} -[1718351071.013217] HB: structure instance +[1683941286.913111] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology declared -[1718351071.016098] HB: we can build a Stage11_UniformSpace on Qc -[1718351071.016679] HB: declare canonical structure instance +[1683941286.916786] HB: we can build a Stage11_UniformSpace on Qc +[1683941286.917659] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace -[1718351071.018108] HB: structure instance for +[1683941286.919417] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace is {| UniformSpace.sort := Qc; @@ -1445,15 +1486,15 @@ UniformSpace.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_92 |} |} -[1718351071.026997] HB: structure instance +[1683941286.930358] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace declared -[1718351071.030241] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc -[1718351071.030809] HB: declare canonical structure instance +[1683941286.934462] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc +[1683941286.935187] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform -[1718351071.032370] HB: Giving name HB_unnamed_mixin_93 to mixin instance +[1683941286.937016] HB: Giving name HB_unnamed_mixin_93 to mixin instance Builders_68.to_JoinTAddAG_wo_Uniform Qc HB_unnamed_mixin_81 HB_unnamed_mixin_86 HB_unnamed_factory_87 -[1718351071.038948] HB: structure instance for +[1683941286.945321] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform is {| TAddAG_wo_Uniform.sort := Qc; @@ -1465,12 +1506,12 @@ HB_unnamed_mixin_93 |} |} -[1718351071.047784] HB: structure instance +[1683941286.956416] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform declared -[1718351071.052369] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc -[1718351071.052960] HB: declare canonical structure instance +[1683941286.962290] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc +[1683941286.963082] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined -[1718351071.055403] HB: structure instance for +[1683941286.966120] HB: structure instance for Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined is {| Uniform_TAddAG_unjoined.sort := Qc; @@ -1485,18 +1526,18 @@ HB_unnamed_mixin_92 |} |} -[1718351071.064911] HB: structure instance +[1683941286.977462] HB: structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined declared -[1718351071.073086] HB: we can build a Stage11_TAddAG on Qc -[1718351071.073712] HB: declare canonical structure instance +[1683941286.987057] HB: we can build a Stage11_TAddAG on Qc +[1683941286.987812] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG -[1718351071.075898] HB: Giving name HB_unnamed_mixin_94 to mixin instance +[1683941286.990528] HB: Giving name HB_unnamed_mixin_94 to mixin instance Builders_68.Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology Qc HB_unnamed_mixin_81 HB_unnamed_mixin_86 HB_unnamed_factory_87 -[1718351071.083917] HB: Giving name HB_unnamed_mixin_95 to mixin instance +[1683941287.000100] HB: Giving name HB_unnamed_mixin_95 to mixin instance Builders_68.Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform Qc HB_unnamed_mixin_81 HB_unnamed_mixin_86 HB_unnamed_factory_87 -[1718351071.091302] HB: structure instance for +[1683941287.009462] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG is {| TAddAG.sort := Qc; @@ -1510,11 +1551,11 @@ TAddAG.Stage11_Join_TAddAG_Uniform_mixin := HB_unnamed_mixin_95 |} |} -[1718351071.101280] HB: structure instance +[1683941287.021740] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG declared entourage : set (set (Qc * Qc)) : set (set (Qc * Qc)) -Finished transaction in 41.582 secs (41.001u,0.58s) (successful) +Finished transaction in 47.223 secs (46.587u,0.58s) (successful) Module Type new_conceptLocked = Sig @@ -1606,9 +1647,9 @@ 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: package coq-hierarchy-builder: substitution variable ${ocaml:Depends} unused, but is 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: package coq-hierarchy-builder: substitution variable ${ocaml:Depends} unused, but is defined dh_md5sums dh_builddeb dpkg-deb: building package 'libcoq-hierarchy-builder' in '../libcoq-hierarchy-builder_1.4.0-2_arm64.deb'. @@ -1620,12 +1661,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/14948/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/14948/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/29157 and its subdirectories -I: Current time: Thu Jun 13 19:45:49 -12 2024 -I: pbuilder-time-stamp: 1718351149 +I: removing directory /srv/workspace/pbuilder/14948 and its subdirectories +I: Current time: Sat May 13 15:29:43 +14 2023 +I: pbuilder-time-stamp: 1683941383