Diff of the two buildlogs: -- --- b1/build.log 2024-12-19 00:54:13.111437866 +0000 +++ b2/build.log 2024-12-19 00:55:36.271673935 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Tue Jan 20 19:15:54 -12 2026 -I: pbuilder-time-stamp: 1768979754 +I: Current time: Thu Dec 19 14:54:16 +14 2024 +I: pbuilder-time-stamp: 1734569656 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/unstable-reproducible-base.tgz] I: copying local configuration @@ -26,52 +26,84 @@ dpkg-source: info: unpacking coq-hierarchy-builder_1.8.0-1.debian.tar.xz I: Not using root during the build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/297944/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/945171/tmp/hooks/D01_modify_environment starting +debug: Running on codethink02-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 Dec 19 00:54 /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/945171/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/945171/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='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]="37" [3]="1" [4]="release" [5]="aarch64-unknown-linux-gnu") + BASH_VERSION='5.2.37(1)-release' + BUILDDIR=/build/reproducible-path + 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=12 ' - DISTRIBUTION='unstable' - HOME='/root' - HOST_ARCH='arm64' + DIRSTACK=() + DISTRIBUTION=unstable + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=aarch64 + HOST_ARCH=arm64 IFS=' ' - INVOCATION_ID='8cb354aa71654f22bc6c43e56f2945b8' - 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='297944' - PS1='# ' - PS2='> ' + INVOCATION_ID=0cb7e73d4a334270940aa9cde4e313e3 + 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=945171 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.NcO70O1e/pbuilderrc_MWKo --distribution unstable --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/unstable-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.NcO70O1e/b1 --logfile b1/build.log coq-hierarchy-builder_1.8.0-1.dsc' - SUDO_GID='109' - SUDO_UID='104' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://192.168.101.4: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.NcO70O1e/pbuilderrc_hus7 --distribution unstable --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/unstable-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.NcO70O1e/b2 --logfile b2/build.log coq-hierarchy-builder_1.8.0-1.dsc' + SUDO_GID=109 + SUDO_UID=104 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://192.168.101.4:3128 I: uname -a - Linux codethink01-arm64 6.1.0-28-cloud-arm64 #1 SMP Debian 6.1.119-1 (2024-11-22) aarch64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-28-cloud-arm64 #1 SMP Debian 6.1.119-1 (2024-11-22) aarch64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Nov 22 2024 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/297944/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Nov 22 14:40 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/945171/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -207,7 +239,7 @@ Get: 86 http://deb.debian.org/debian unstable/main arm64 libelpi-ocaml-dev arm64 2.0.5-1 [15.8 MB] Get: 87 http://deb.debian.org/debian unstable/main arm64 libcoq-elpi arm64 2.3.0-1 [11.9 MB] Get: 88 http://deb.debian.org/debian unstable/main arm64 wdiff arm64 1.2.2-6+b1 [119 kB] -Fetched 381 MB in 2s (225 MB/s) +Fetched 381 MB in 2s (231 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libpython3.12-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 ... 20085 files and directories currently installed.) @@ -509,8 +541,8 @@ Setting up tzdata (2024b-4) ... Current default time zone: 'Etc/UTC' -Local time is now: Wed Jan 21 07:16:26 UTC 2026. -Universal Time is now: Wed Jan 21 07:16:26 UTC 2026. +Local time is now: Thu Dec 19 00:54:45 UTC 2024. +Universal Time is now: Thu Dec 19 00:54:45 UTC 2024. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up autotools-dev (20220109.1) ... @@ -588,7 +620,11 @@ Building tag database... -> Finished parsing the build-deps I: Building the package -I: Running cd /build/reproducible-path/coq-hierarchy-builder-1.8.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.8.0-1_source.changes +I: user script /srv/workspace/pbuilder/945171/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for unstable +I: user script /srv/workspace/pbuilder/945171/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/coq-hierarchy-builder-1.8.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.8.0-1_source.changes dpkg-buildpackage: info: source package coq-hierarchy-builder dpkg-buildpackage: info: source version 1.8.0-1 dpkg-buildpackage: info: source distribution unstable @@ -648,8 +684,8 @@ COQC examples/demo1/hierarchy_2.v COQC examples/demo1/hierarchy_3.v COQC examples/demo1/hierarchy_4.v -COQC examples/demo1/hierarchy_5.v COQC examples/demo2/classical.v +COQC examples/demo1/hierarchy_5.v COQC examples/demo3/hierarchy_0.v COQC examples/demo3/hierarchy_1.v COQC examples/demo3/hierarchy_2.v @@ -670,40 +706,25 @@ Warning: Postfix notations (i.e. starting with a nonterminal symbol and ending with a terminal symbol) should usually be at level 1 (default). [postfix-notation-not-level-1,parsing,default] -File "./examples/demo1/hierarchy_2.v", line 39, characters 2-91: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -COQC examples/demo4/hierarchy_0.v File "./examples/demo1/hierarchy_3.v", line 39, characters 2-87: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] -File "./examples/demo1/hierarchy_5.v", line 39, characters 2-97: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -[1768979795.153663] HB: begin module for builders -[1768979795.153927] HB: begin module Super -[1768979795.154001] HB: ended module Super -[1768979795.154200] HB: postulating factories -[1768979795.154293] HB: processing key context-item -[1768979795.154492] HB: processing mixin parameter a -[1768979795.154745] HB: declaring parameters and key as section variables +[1734569698.932455] HB: begin module for builders +[1734569698.932775] HB: begin module Super +[1734569698.932872] HB: ended module Super +[1734569698.933148] HB: postulating factories +[1734569698.933277] HB: processing key context-item +[1734569698.933502] HB: processing mixin parameter a +[1734569698.933826] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -File "./examples/demo1/hierarchy_1.v", line 55, characters 0-123: +File "./examples/demo1/hierarchy_4.v", line 40, characters 2-97: Warning: HB: no new instance is generated [HB.no-new-instance,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] -File "./examples/demo1/hierarchy_5.v", line 68, characters 2-91: +File "./examples/demo1/hierarchy_5.v", line 39, characters 2-97: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] -COQC examples/demo5/hierarchy_0.v -[1768979795.378623] HB: start module and section AddComoid_of_Type -[1768979795.378964] HB: converting arguments +[1734569698.962680] HB: start module and section AddComoid_of_Type +[1734569698.963201] HB: converting arguments indt-decl (parameter A explicit X0 c0 \ record AddComoid_of_Type (sort (typ X1)) Build_AddComoid_of_Type @@ -728,19 +749,23 @@ (prod `x` (X9 c4) c5 \ app [global (indt «eq»), X10 c4 c5, app [c2, c1, c5], c5]) c5 \ end-record)) to factories -[1768979795.379284] HB: processing key parameter -[1768979795.379615] HB: converting factories +[1734569698.963779] HB: processing key parameter +[1734569698.964446] HB: converting factories w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] to mixins -[1768979795.379687] HB: declaring context +[1734569698.964728] HB: declaring context w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] -[1768979795.379816] HB: declaring parameters and key as section variables +File "./examples/demo1/hierarchy_1.v", line 55, characters 0-123: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +[1734569698.964976] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1768979795.380482] HB: declare mixin or factory -[1768979795.380566] HB: declare record axioms_ -[1768979795.385249] HB: declare notation Build -[1768979795.389015] HB: declare notation axioms -[1768979795.392388] HB: start module Exports -[1768979795.394538] HB: end modules and sections; export +[1734569698.965578] HB: declare mixin or factory +[1734569698.965691] HB: declare record axioms_ +COQC examples/demo4/hierarchy_0.v +[1734569698.970742] HB: declare notation Build +[1734569698.974671] HB: declare notation axioms +[1734569698.978660] HB: start module Exports +[1734569698.981237] HB: end modules and sections; export «HB.examples.readme.AddComoid_of_Type.Exports» (* @@ -797,49 +822,48 @@ Notation AddComoid_of_Type X1 := ( AddComoid_of_Type.phant_axioms X1). *) -[1768979795.411748] HB: start module AddComoid -[1768979795.412013] HB: declare axioms record +[1734569698.999536] HB: start module AddComoid +[1734569698.999945] HB: declare axioms record w-params.nil A (sort (typ «HB.examples.readme.25»)) c0 \ [triple (indt «AddComoid_of_Type.axioms_») [] c0] -[1768979795.412172] HB: typing class field +[1734569699.000395] HB: typing class field indt «AddComoid_of_Type.axioms_» -COQC examples/FSCD2020_material/V1.v -[1768979795.414013] HB: declare type record -[1768979795.415303] HB: structure: new mixins +[1734569699.002264] HB: declare type record +[1734569699.003945] HB: structure: new mixins [indt «AddComoid_of_Type.axioms_»] -[1768979795.415387] HB: structure: mixin first class +[1734569699.004209] HB: structure: mixin first class [mixin-first-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»)] -[1768979795.415539] HB: declaring clone abbreviation -[1768979795.418360] HB: declaring pack_ constant -[1768979795.418805] HB: declaring pack_ constant = +[1734569699.004321] HB: declaring clone abbreviation +[1734569699.007809] HB: declaring pack_ constant +[1734569699.008411] 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]] -[1768979795.419785] HB: start module Exports -[1768979795.420038] HB: making coercion from type to target -[1768979795.420079] HB: declare sort coercion -[1768979795.420398] HB: exporting unification hints -[1768979795.420549] HB: exporting coercions from class to mixins -[1768979795.420710] HB: export class to mixin coercion for mixin +[1734569699.009690] HB: start module Exports +[1734569699.010310] HB: making coercion from type to target +[1734569699.010536] HB: declare sort coercion +[1734569699.010881] HB: exporting unification hints +[1734569699.011146] HB: exporting coercions from class to mixins +[1734569699.011454] HB: export class to mixin coercion for mixin readme_AddComoid_of_Type -[1768979795.420957] HB: accumulating various props -[1768979795.421390] HB: stop module Exports -[1768979795.421820] HB: declaring on_ abbreviation -[1768979795.423796] HB: declaring `copy` abbreviation -[1768979795.424655] HB: declaring on abbreviation -[1768979795.425937] HB: end modules; export +[1734569699.012041] HB: accumulating various props +[1734569699.012692] HB: stop module Exports +[1734569699.013532] HB: declaring on_ abbreviation +[1734569699.016177] HB: declaring `copy` abbreviation +[1734569699.017255] HB: declaring on abbreviation +[1734569699.018976] HB: end modules; export «HB.examples.readme.AddComoid.Exports» -[1768979795.426496] HB: exporting operations -[1768979795.427355] HB: export operation zero -[1768979795.429471] HB: export operation add -[1768979795.431787] HB: export operation addrA -File "./examples/demo1/hierarchy_4.v", line 40, characters 2-97: +[1734569699.019782] HB: exporting operations +[1734569699.021076] HB: export operation zero +[1734569699.023423] HB: export operation add +[1734569699.026345] HB: export operation addrA +File "./examples/demo1/hierarchy_2.v", line 39, characters 2-91: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] -[1768979795.520700] HB: export operation addrC -[1768979795.522950] HB: export operation add0r -[1768979795.524738] HB: operations meta-data module: ElpiOperations -[1768979795.525903] HB: abbreviation factory-by-classname +[1734569699.123936] HB: export operation addrC +[1734569699.126768] HB: export operation add0r +[1734569699.128576] HB: operations meta-data module: ElpiOperations +[1734569699.130250] HB: abbreviation factory-by-classname (* Module AddComoid. @@ -936,21 +960,26 @@ *) forall (M : AddComoid.type) (x : M), x + x = 0 : Prop -[1768979795.531749] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_AddAG_of_AddComoid -[1768979795.531870] 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,elpi,default] +File "./examples/demo1/hierarchy_4.v", line 69, characters 2-91: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +File "./examples/demo1/hierarchy_5.v", line 68, characters 2-91: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +COQC examples/demo5/hierarchy_0.v +COQC examples/FSCD2020_material/V1.v AbelianGrp.phant_on_ BinNums_Z__canonical__readme_AbelianGrp (Phant BinNums_Z__canonical__readme_AbelianGrp) : AbelianGrp.axioms_ Z : AbelianGrp.axioms_ Z +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] HB: Z is canonically equipped with structures: - AbelianGrp (from "./examples/readme.v", line 32) @@ -958,48 +987,47 @@ (from "./examples/readme.v", line 31) COQC examples/FSCD2020_material/V2.v -File "./examples/demo1/hierarchy_4.v", line 69, characters 2-91: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -COQC examples/FSCD2020_material/V3.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] +[1734569699.513919] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_AddAG_of_AddComoid +[1734569699.514137] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_Ring_of_AddAG HB: A is canonically equipped with structures: - Equality Singleton (from "./examples/hulk.v", line 216) +COQC examples/FSCD2020_material/V3.v +COQC examples/FSCD2020_material/V4.v inhab : ?s where ?T : [ |- Type] ?s : [ |- s1.type ?T] -COQC examples/FSCD2020_material/V4.v eq_refl : inhab = 7 : inhab = 7 eq_refl : inhab = (7 :: nil)%list : inhab = (7 :: nil)%list where ?T : [ |- Type] +COQC examples/FSCD2020_talk/V1.v +COQC examples/FSCD2020_talk/V2.v fun X : s2.type nat => inhab : X : forall X : s2.type nat, X 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_talk/V1.v -COQC examples/FSCD2020_talk/V2.v COQC examples/FSCD2020_talk/V3.v +COQC examples/Coq2020_material/CoqWS_demo.v +COQC examples/Coq2020_material/CoqWS_abstract.v File "./examples/demo5/hierarchy_0.v", line 35, characters 2-91: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] -COQC examples/Coq2020_material/CoqWS_demo.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/Coq2020_material/CoqWS_abstract.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -1012,25 +1040,17 @@ File "./examples/demo5/hierarchy_0.v", line 68, characters 2-109: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] +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/Coq2020_material/CoqWS_expansion/withHB.v -Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. - -Arguments Monoid.Pack sort%type_scope class -Arguments Monoid.sort record -Arguments Monoid.class record -@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/Coq2020_material/CoqWS_expansion/withoutHB.v COQC tests/type_of_exported_ops.v -File "./examples/FSCD2020_talk/V3.v", line 28, characters 2-118: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -COQC tests/duplicate_structure.v -COQC tests/instance_params_no_type.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -1042,8 +1062,7 @@ : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add -COQC tests/test_CS_db_filtering.v -COQC tests/subtype.v +COQC tests/duplicate_structure.v add : ?s -> ?s -> ?s where @@ -1052,19 +1071,15 @@ : commutative add where ?s : [ |- CMonoid.type] -File "./examples/Coq2020_material/CoqWS_demo.v", line 73, characters 0-73: +File "./examples/FSCD2020_talk/V2.v", line 17, characters 0-66: Warning: -pulling in dependencies: [CoqWS_demo_CMonoid_of_Type] +pulling in dependencies: [V2_is_semigroup] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] -forall x y : ?t, x - (y + 0) = x - : Prop -where -?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) -File "./examples/FSCD2020_talk/V2.v", line 17, characters 0-66: +File "./examples/Coq2020_material/CoqWS_demo.v", line 73, characters 0-73: Warning: -pulling in dependencies: [V2_is_semigroup] +pulling in dependencies: [CoqWS_demo_CMonoid_of_Type] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] @@ -1072,22 +1087,38 @@ : commutative add where ?s : [ |- CMonoid.type] -COQC tests/exports.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/log_impargs_record.v -COQC tests/compress_coe.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/instance_params_no_type.v 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,elpi,default] +Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. + +Arguments Monoid.Pack sort%type_scope class +Arguments Monoid.sort record +Arguments Monoid.class record +@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 tests/test_CS_db_filtering.v +File "./examples/FSCD2020_talk/V3.v", line 28, characters 2-118: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +COQC tests/subtype.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/exports.v forall (R : Ring.type) (x y : R), 1 * x = y - x : Prop forall @@ -1100,10 +1131,22 @@ join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing ?t y : ?t |- Ring.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,default] 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 (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 +COQC tests/funclass.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -1115,11 +1158,14 @@ : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add -COQC tests/funclass.v +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop forall x : Z, x * - (1 + x) = 0 + 1 : Prop COQC tests/grefclass.v COQC tests/local_instance.v +COQC tests/lock.v +COQC tests/interleave_context.v File "./tests/instance_params_no_type.v", line 5, characters 0-70: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] @@ -1176,74 +1222,9 @@ Arguments foo.axioms_ (P A)%type_scope Arguments foo.Class (P A)%type_scope instance_params_no_type_is_foo_mixin Arguments foo.instance_params_no_type_is_foo_mixin (P A)%type_scope record -COQC tests/lock.v -COQC tests/interleave_context.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 -[1768979798.429994] HB: start module SubInhab -[1768979798.430253] 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] -[1768979798.430477] HB: typing class field indt «is_inhab.axioms_» -[1768979798.430657] HB: typing class field indt «is_SUB.axioms_» -[1768979798.432653] HB: declare type record -[1768979798.434280] HB: structure: new mixins [] -[1768979798.434513] HB: structure: mixin first class [] -[1768979798.434624] HB: declaring clone abbreviation -[1768979798.437233] HB: declaring pack_ constant -[1768979798.438178] 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 \ - fun `m` (app [global (indt «is_inhab.axioms_»), c2]) c3 \ - fun `m` (app [global (indt «is_SUB.axioms_»), c0, c1, c2]) c4 \ - app - [global (indc «Pack»), c0, c1, c2, - app [global (indc «Class»), c0, c1, c2, c3, c4]] -[1768979798.438977] HB: start module Exports -[1768979798.439186] HB: making coercion from type to target -[1768979798.439239] HB: declare sort coercion -[1768979798.439328] HB: exporting unification hints -[1768979798.439900] HB: declare coercion subtype_SubInhab__to__subtype_SUB -[1768979798.440477] HB: declare coercion hint -subtype_SubInhab_class__to__subtype_SUB_class -[1768979798.441943] HB: declare unification hint -subtype_SubInhab__to__subtype_SUB -[1768979798.443622] HB: declare coercion subtype_SubInhab__to__subtype_Inhab -[1768979798.444123] HB: declare coercion hint -subtype_SubInhab_class__to__subtype_Inhab_class -[1768979798.446252] HB: declare unification hint -subtype_SubInhab__to__subtype_Inhab -[1768979798.448461] HB: declare unification hint -join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB -[1768979798.450565] HB: exporting coercions from class to mixins -[1768979798.451034] HB: export class to mixin coercion for mixin -subtype_is_inhab -[1768979798.451769] HB: export class to mixin coercion for mixin -subtype_is_SUB -[1768979798.452435] HB: accumulating various props -[1768979798.453262] HB: stop module Exports -[1768979798.459632] HB: declaring on_ abbreviation -[1768979798.462592] HB: declaring `copy` abbreviation -[1768979798.463544] HB: declaring on abbreviation -[1768979798.464696] HB: end modules; export -«HB.tests.subtype.SubInhab.Exports» -[1768979798.466515] HB: exporting operations -[1768979798.466899] HB: operations meta-data module: ElpiOperations -[1768979798.467493] HB: abbreviation factory-by-classname -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop list_bar : forall P : b.type, is_bar.axioms_ P (list P) COQC tests/not_same_key.v -COQC tests/hb_pack.v (* Module A. @@ -1300,28 +1281,105 @@ Arguments A.p [T]%type_scope record [x] _ A.p is transparent Expands to: Constant HB.tests.log_impargs_record.A.p +COQC tests/hb_pack.v +[1734569701.979836] HB: start module SubInhab +[1734569701.980296] 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] +[1734569701.980695] HB: typing class field indt «is_inhab.axioms_» +[1734569701.981033] HB: typing class field indt «is_SUB.axioms_» +[1734569701.982994] HB: declare type record +[1734569701.984869] HB: structure: new mixins [] +[1734569701.985139] HB: structure: mixin first class [] +[1734569701.985241] HB: declaring clone abbreviation +[1734569701.988046] HB: declaring pack_ constant +[1734569701.989085] 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 \ + fun `m` (app [global (indt «is_inhab.axioms_»), c2]) c3 \ + fun `m` (app [global (indt «is_SUB.axioms_»), c0, c1, c2]) c4 \ + app + [global (indc «Pack»), c0, c1, c2, + app [global (indc «Class»), c0, c1, c2, c3, c4]] +[1734569701.990186] HB: start module Exports +[1734569701.990621] HB: making coercion from type to target +[1734569701.990781] HB: declare sort coercion +[1734569701.990977] HB: exporting unification hints +[1734569701.991679] HB: declare coercion subtype_SubInhab__to__subtype_SUB +[1734569701.992433] HB: declare coercion hint +subtype_SubInhab_class__to__subtype_SUB_class +[1734569701.994358] HB: declare unification hint +subtype_SubInhab__to__subtype_SUB +[1734569701.996466] HB: declare coercion subtype_SubInhab__to__subtype_Inhab +[1734569701.997261] HB: declare coercion hint +subtype_SubInhab_class__to__subtype_Inhab_class +[1734569701.999099] HB: declare unification hint +subtype_SubInhab__to__subtype_Inhab +[1734569702.002042] HB: declare unification hint +join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB +[1734569702.004128] HB: exporting coercions from class to mixins +[1734569702.004520] HB: export class to mixin coercion for mixin +subtype_is_inhab +[1734569702.005288] HB: export class to mixin coercion for mixin +subtype_is_SUB +[1734569702.006063] HB: accumulating various props COQC tests/declare.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". -COQC tests/short.v +[1734569702.006958] HB: stop module Exports +[1734569702.008710] HB: declaring on_ abbreviation +[1734569702.011319] HB: declaring `copy` abbreviation +[1734569702.012340] HB: declaring on abbreviation +[1734569702.013614] HB: end modules; export +«HB.tests.subtype.SubInhab.Exports» +[1734569702.015507] HB: exporting operations +[1734569702.015915] HB: operations meta-data module: ElpiOperations +[1734569702.016569] HB: abbreviation factory-by-classname 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/instance_before_structure.v -p : pred nat - : pred nat +Notation big := big.body +Expands to: Notation HB.tests.lock.X.big + +big.body : forall R I : Type, R -> list I -> (I -> bigbody R I) -> R + +big.body is not universe polymorphic +Arguments big.body (R I)%type_scope _ _%list_scope _%function_scope +Expands to: Constant HB.tests.lock.X.big.body 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/short.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 +COQC tests/instance_before_structure.v +HB.check: forall w : wp.type nat Init.Nat.mul, w = w : Prop COQC tests/primitive_records.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,elpi,default] +[1734569702.466815] HB: exporting under the module path [] +[1734569702.467342] HB: exporting modules +[Ring_of_TYPE.Exports, Ring.Exports, RingElpiOperations, RingExports, + Dummy.Exports, URing.Exports, URingElpiOperations, dummy.Exports, + Builders_1.Builders_Export_5] +[1734569702.469053] HB: exporting CS instances +[«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] +[1734569702.469843] HB: exporting Abbreviations [addr0, addrNK] +[1734569702.470241] HB: exporting Clauses X0 Datatypes_prod__canonical__compress_coe_D = fun D D' : D.type => {| @@ -1343,22 +1401,6 @@ : D.type -> D.type -> D.type Arguments Datatypes_prod__canonical__compress_coe_D D D' -COQC tests/non_forgetful_inheritance.v -[1768979799.268615] HB: exporting under the module path [] -[1768979799.268840] HB: exporting modules -[Ring_of_TYPE.Exports, Ring.Exports, RingElpiOperations, RingExports, - Dummy.Exports, URing.Exports, URingElpiOperations, dummy.Exports, - Builders_1.Builders_Export_5] -[1768979799.270088] HB: exporting CS instances -[«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] -[1768979799.270488] HB: exporting Abbreviations [addr0, addrNK] -[1768979799.270626] HB: exporting Clauses X0 -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] forall (R : Enclosing.Ring.type) (x : R), x = x : Prop 0%G @@ -1367,68 +1409,46 @@ ?s : [ |- Enclosing.Ring.type] Enclosing.zero : Z : Z +COQC tests/non_forgetful_inheritance.v COQC tests/fix_loop.v COQC tests/test_synthesis_params.v -Notation big := big.body -Expands to: Notation HB.tests.lock.X.big - -big.body : forall R I : Type, R -> list I -> (I -> bigbody R I) -> R - -big.body is not universe polymorphic -Arguments big.body (R I)%type_scope _ _%list_scope _%function_scope -Expands to: Constant HB.tests.lock.X.big.body -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 +p : pred nat + : pred nat +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". COQC tests/hnf.v -HB.check: forall w : wp.type nat Init.Nat.mul, w = w : Prop COQC tests/fun_instance.v -COQC tests/issue284.v -[1768979799.622169] HB: start module and section hasA -[1768979799.622441] HB: converting arguments +[1734569702.643099] HB: start module and section hasA +[1734569702.643563] 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 -[1768979799.622542] HB: processing key parameter -[1768979799.622831] HB: converting factories +[1734569702.643805] HB: processing key parameter +[1734569702.644220] HB: converting factories w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins -[1768979799.622891] HB: declaring context +[1734569702.644429] HB: declaring context w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] -[1768979799.622991] HB: declaring parameters and key as section variables +[1734569702.644639] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1768979799.623260] HB: declare mixin or factory -[1768979799.623310] HB: declare record axioms_ -[1768979799.625892] HB: declare notation Build -[1768979799.627012] HB: declare notation axioms -[1768979799.629018] HB: start module Exports -[1768979799.630368] HB: end modules and sections; export +[1734569702.645222] HB: declare mixin or factory +[1734569702.645367] HB: declare record axioms_ +[1734569702.647599] HB: declare notation Build +[1734569702.649024] HB: declare notation axioms +[1734569702.651354] HB: start module Exports +[1734569702.653105] HB: end modules and sections; export «HB.tests.hb_pack.hasA.Exports» hasA.type not a defined object. +COQC tests/issue284.v hasB.type not a defined object. aType : Type hasB.type not a defined object. -HB: nat is canonically equipped with structures: - - s1 - (from "./tests/instance_before_structure.v", line 11) - -File "./tests/instance_before_structure.v", line 16, characters 0-52: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -HB: nat is canonically equipped with structures: - - s1 - (from "./tests/instance_before_structure.v", line 11) - hasAB.type not a defined object. -HB: nat is canonically equipped with structures: - - s1 - (from "./tests/instance_before_structure.v", line 11) - hasA'.type not a defined object. -COQC tests/issue287.v forall T : AB.type, unkeyed {| @@ -1446,30 +1466,19 @@ : A.type A : A.type : A.type -File "./tests/non_forgetful_inheritance.v", line 35, characters 0-45: -Warning: Could not enable unknown warning HB.non-forgetful-inheritance -[unknown-warning,default] +HB: nat is canonically equipped with structures: + - s1 + (from "./tests/instance_before_structure.v", line 11) + AB1 : hasB.phant_axioms A -> AB.type : hasB.phant_axioms A -> AB.type -Debug: -elpi lets escape exception: non forgetful inheritance detected. - You have two solutions: -1. (Best practice) Reorganize your hierarchy to make -non_forgetful_inheritance_HasSq depend on non_forgetful_inheritance_Mul. -See the paper "Competing inheritance paths in -dependent type theory" (https://hal.inria.fr/hal-02463336) for more -explanations -2. Use the attribute #[non_forgetful_inheritance] to disable this check. -We strongly advise you encapsulate this instance inside a module, -in order to isolate it from the rest of the code, and to be able -to import it on demand. See the above paper and the file -https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v -to witness devastating effects. -[HB.non-forgetful-inheritance,HB,elpi,default] Bm : hasB.phant_axioms A : hasB.phant_axioms A AB2 : AB.type : AB.type +File "./tests/instance_before_structure.v", line 16, characters 0-52: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] pB : T * T : T * T AB3 : AB.type @@ -1479,6 +1488,22 @@ (from "./tests/instance_before_structure.v", line 11) HB: nat is canonically equipped with structures: + - s1 + (from "./tests/instance_before_structure.v", line 11) + +Query assignments: + Ind = «hasA.axioms_» +X : Foo.type A P + : Foo.type A P +Query assignments: + Ind = «A.axioms_» +Query assignments: + Ind = «A.type» +HB: nat is canonically equipped with structures: + - s1 + (from "./tests/instance_before_structure.v", line 11) + +HB: nat is canonically equipped with structures: - s3 s2 (from "./tests/instance_before_structure.v", line 30) @@ -1491,74 +1516,59 @@ : nat default3 : nat -X : Foo.type A P - : Foo.type A P +COQC tests/issue287.v hasAB.type not a defined object. -COQC tests/two_hier.v hasA'.type not a defined object. +COQC tests/two_hier.v +File "./tests/non_forgetful_inheritance.v", line 35, characters 0-45: +Warning: Could not enable unknown warning HB.non-forgetful-inheritance +[unknown-warning,default] +Debug: +elpi lets escape exception: non forgetful inheritance detected. + You have two solutions: +1. (Best practice) Reorganize your hierarchy to make +non_forgetful_inheritance_HasSq depend on non_forgetful_inheritance_Mul. +See the paper "Competing inheritance paths in +dependent type theory" (https://hal.inria.fr/hal-02463336) for more +explanations +2. Use the attribute #[non_forgetful_inheritance] to disable this check. +We strongly advise you encapsulate this instance inside a module, +in order to isolate it from the rest of the code, and to be able +to import it on demand. See the above paper and the file +https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v +to witness devastating effects. +[HB.non-forgetful-inheritance,HB,elpi,default] +T : Fun.type nat + : Fun.type nat +erefl : ?t = ?t + : ?t = ?t +where +?t : [ |- Sq.type] COQC tests/instance_merge_with_param.v COQC tests/instance_merge_with_distinct_param.v COQC tests/instance_merge.v +COQC tests/unit/enrich_type.v Datatypes_nat__canonical__hnf_S = {| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_8 |} |} : S.type HB_unnamed_mixin_8 = {| M.x := f.y nat HB_unnamed_factory_6 + 1 |} : M.axioms_ nat +COQC tests/unit/mixin_src_has_mixin_instance.v Datatypes_bool__canonical__hnf_S = {| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |} : S.type HB_unnamed_mixin_12 = Builders_1.HB_unnamed_factory_3 bool HB_unnamed_factory_9 : M.axioms_ bool -T : Fun.type nat - : Fun.type nat -COQC tests/unit/enrich_type.v -COQC tests/unit/mixin_src_has_mixin_instance.v COQC tests/unit/mk_src_map.v -Query assignments: - Ind = «hasA.axioms_» -Query assignments: - Ind = «A.axioms_» -Query assignments: - Ind = «A.type» COQC tests/unit/close_hole_term.v COQC tests/unit/struct.v COQC tests/factory_when_notation.v -erefl : ?t = ?t - : ?t = ?t -where -?t : [ |- Sq.type] COQC tests/saturate_on.v COQC tests/bug_435.v -File "./tests/unit/mixin_src_has_mixin_instance.v", line 12, characters 0-57: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -Query assignments: - M1_ = const «m1.phant_axioms» - Y = has-mixin-instance (cs-gref (indt «nat»)) (const «m1.phant_axioms») - (const «nat_m1») -Query assignments: - M1_ = const «m1.phant_axioms» - Y = has-mixin-instance (cs-gref (indt «list»)) (const «m1.phant_axioms») - (const «i1») -COQC tests/bug_447.v -HB: list is canonically equipped with structures: - - s2 - (from "./tests/instance_merge_with_param.v", line 12) - - s1 - (from "./tests/instance_merge_with_param.v", line 10) - -nat : s3.type - : s3.type -list nat : s3.type - : s3.type -list (list nat) : s3.type - : s3.type Query assignments: X = global (indt «nat») -fun t : s3.type => list t : s3.type - : s3.type -> s3.type Query assignments: X = app [global (indt «list»), X0] Y_ = X0 @@ -1646,53 +1656,10 @@ WEAK CONSTRAINTS: -COQC tests/unimported_relevant_class.v -HB: list is canonically equipped with structures: - - s3 - (from "./tests/instance_merge_with_param.v", line 23) - - s2 - (from "./tests/instance_merge_with_param.v", line 12) - - s1 - (from "./tests/instance_merge_with_param.v", line 10) - -COQC tests/unimported_irrelevant_class.v -Query assignments: - H_ = [] -struct_foo1__to__struct_foo = -fun s : foo1.type => {| foo.sort := s; foo.class := foo1.class s |} - : foo1.type -> foo.type (option nat) - -Arguments struct_foo1__to__struct_foo s -struct_foo1__to__struct_foo is a reversible coercion -File "./tests/unit/mk_src_map.v", line 6, characters 0-76: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -File "./tests/unit/mk_src_map.v", line 8, characters 0-79: +COQC tests/bug_447.v +File "./tests/unit/mixin_src_has_mixin_instance.v", line 12, characters 0-57: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] -list_foo' - : forall P A : Type, is_foo.axioms_ P (list A) -list_foo - : forall P : Type, is_foo.axioms_ P (list P) -nat : s3.type - : s3.type -list nat : s3.type - : s3.type -list (list nat) : s3.type - : s3.type -Query assignments: - MS = pi c0 \ - pi c1 \ - mixin-src (app [global (indt «list»), c1]) (indt «is_foo.axioms_») - (app [global (const «list_foo»), c0]) :- [coq.unify-eq c0 c1 ok] -Query assignments: - MS' = pi c0 \ - pi c1 \ - pi c2 \ - mixin-src (app [global (indt «list»), c2]) (indt «is_foo.axioms_») - (app [global (const «list_foo'»), c0, c1]) :- [coq.unify-eq c1 c2 ok] -fun t : s3.type => list t : s3.type - : s3.type -> s3.type Query assignments: X = app [global (indt «list»), X0] X1_ = X1 @@ -1718,8 +1685,18 @@ Query assignments: + M1_ = const «m1.phant_axioms» + Y = has-mixin-instance (cs-gref (indt «nat»)) (const «m1.phant_axioms») + (const «nat_m1») +Query assignments: Z = global (indt «nat») Query assignments: + M1_ = const «m1.phant_axioms» + Y = has-mixin-instance (cs-gref (indt «list»)) (const «m1.phant_axioms») + (const «i1») +nat : s3.type + : s3.type +Query assignments: X = app [global (const «Inj»), X0, X1, X2, X3, X4] X2_ = X0 X3_ = X1 @@ -1741,6 +1718,8 @@ evar (X2) (app [global (const «relation»), X0]) (X2) /* suspended on X2 */ evar (X1) (sort (typ «HB.tests.unit.close_hole_term.13»)) (X1) /* suspended on X1 */ evar (X0) (sort (typ «HB.tests.unit.close_hole_term.12»)) (X0) /* suspended on X0 */ +list nat : s3.type + : s3.type Universe constraints: UNIVERSES: {HB.tests.unit.close_hole_term.16 HB.tests.unit.close_hole_term.15 @@ -1772,7 +1751,61 @@ WEAK CONSTRAINTS: +list (list nat) : s3.type + : s3.type +COQC tests/unimported_relevant_class.v +fun t : s3.type => list t : s3.type + : s3.type -> s3.type +HB: list is canonically equipped with structures: + - s2 + (from "./tests/instance_merge_with_param.v", line 12) + - s1 + (from "./tests/instance_merge_with_param.v", line 10) + +COQC tests/unimported_irrelevant_class.v +File "./tests/unit/mk_src_map.v", line 6, characters 0-76: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +nat : s3.type + : s3.type +File "./tests/unit/mk_src_map.v", line 8, characters 0-79: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +list nat : s3.type + : s3.type +list (list nat) : s3.type + : s3.type +fun t : s3.type => list t : s3.type + : s3.type -> s3.type +list_foo' + : forall P A : Type, is_foo.axioms_ P (list A) +list_foo + : forall P : Type, is_foo.axioms_ P (list P) +Query assignments: + MS = pi c0 \ + pi c1 \ + mixin-src (app [global (indt «list»), c1]) (indt «is_foo.axioms_») + (app [global (const «list_foo»), c0]) :- [coq.unify-eq c0 c1 ok] +Query assignments: + MS' = pi c0 \ + pi c1 \ + pi c2 \ + mixin-src (app [global (indt «list»), c2]) (indt «is_foo.axioms_») + (app [global (const «list_foo'»), c0, c1]) :- [coq.unify-eq c1 c2 ok] +HB: list is canonically equipped with structures: + - s3 + (from "./tests/instance_merge_with_param.v", line 23) + - s2 + (from "./tests/instance_merge_with_param.v", line 12) + - s1 + (from "./tests/instance_merge_with_param.v", line 10) + COQC examples/demo1/test_0_0.v +COQC examples/demo1/test_1_0.v +COQC examples/demo1/test_2_0.v +File "./tests/saturate_on.v", line 5, characters 0-64: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] nat : s3'.type Datatypes_nat__canonical__two_hier_s3 : s3'.type Datatypes_nat__canonical__two_hier_s3 list nat : s3'.type Datatypes_nat__canonical__two_hier_s3 @@ -1781,39 +1814,41 @@ : forall x : s3.type, s3'.type x -> s3'.type x list (list nat) : s3'.type Datatypes_nat__canonical__two_hier_s3 : s3'.type Datatypes_nat__canonical__two_hier_s3 -File "./tests/saturate_on.v", line 5, characters 0-64: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -COQC examples/demo1/test_1_0.v list unit : Pointed.type : Pointed.type -COQC examples/demo1/test_2_0.v +COQC examples/demo1/test_3_0.v +COQC examples/demo1/test_3_3.v +Query assignments: + H_ = [] +struct_foo1__to__struct_foo = +fun s : foo1.type => {| foo.sort := s; foo.class := foo1.class s |} + : foo1.type -> foo.type (option nat) + +Arguments struct_foo1__to__struct_foo s +struct_foo1__to__struct_foo is a reversible coercion File "./tests/factory_when_notation.v", line 6, characters 0-40: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] -COQC examples/demo1/test_3_0.v -COQC examples/demo1/test_3_3.v COQC examples/demo1/test_4_0.v COQC examples/demo1/test_4_3.v -COQC examples/demo1/test_5_0.v -[1768979802.366962] HB: postulating X -[1768979802.373436] HB: declare canonical mixin instance +[1734569704.911610] HB: postulating X +[1734569704.914467] HB: declare canonical mixin instance «HB_unnamed_factory_5» -[1768979802.374059] HB: we can build a bug_435_B2 on unit -[1768979802.374241] HB: declare canonical structure instance +[1734569704.915242] HB: we can build a bug_435_B2 on unit +[1734569704.915601] HB: declare canonical structure instance Datatypes_unit__canonical__bug_435_B2 -[1768979802.374339] HB: structure instance for +[1734569704.915808] HB: structure instance for Datatypes_unit__canonical__bug_435_B2 is {| B2.sort := unit; B2.class := {| B2.bug_435_A2_mixin := HB_unnamed_factory_5 |} |} -[1768979802.375566] HB: structure instance +[1734569704.917342] HB: structure instance Datatypes_unit__canonical__bug_435_B2 declared -[1768979802.376146] HB: we can build a should_work_but_fails_B on unit -[1768979802.380510] HB: declare canonical structure instance +[1734569704.918174] HB: we can build a should_work_but_fails_B on unit +[1734569704.918563] HB: declare canonical structure instance Datatypes_unit__canonical__should_work_but_fails_B -[1768979802.380674] HB: structure instance for +[1734569704.918796] HB: structure instance for Datatypes_unit__canonical__should_work_but_fails_B is {| B.sort := unit; @@ -1823,43 +1858,44 @@ B.bug_435_A2_mixin := HB_unnamed_factory_5 |} |} -[1768979802.381026] HB: closing instance section +[1734569704.919374] HB: closing instance section unit : B.type ?t : B.type ?t where ?t : [ |- S.type] -COQC examples/demo1/test_5_3.v +COQC examples/demo1/test_5_0.v unit : B.type ?t : B.type ?t where ?t : [ |- S.type] +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 testTy : JustMixedParam.type ?T : JustMixedParam.type ?T where ?T : [ |- Type] +COQC tests/exports2.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] File "./examples/demo2/stage11.v", line 3, characters 0-25: Warning: Hiding binding of key Q to Q_scope [hiding-delimiting-key,parsing,default] +[1734569706.226639] HB: exporting under the module path [] +[1734569706.226750] HB: exporting modules [] +[1734569706.226793] HB: exporting CS instances [] +[1734569706.226829] HB: exporting Abbreviations [] +[1734569706.226864] HB: exporting Clauses X0 File "./examples/demo2/stage10.v", line 112, characters 2-115: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./examples/demo2/stage11.v", line 115, characters 2-100: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] -[1768979803.820337] HB: exporting under the module path [] -[1768979803.820501] HB: exporting modules [] -[1768979803.820562] HB: exporting CS instances [] -[1768979803.820617] HB: exporting Abbreviations [] -[1768979803.820768] HB: exporting Clauses X0 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 @@ -1890,30 +1926,30 @@ disable this warning. [deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] HB: skipping section opening -[1768979805.007631] HB: declare mixin instance +[1734569707.796422] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology -[1768979805.008999] HB: declare canonical mixin instance +[1734569707.797574] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology» -[1768979805.010133] HB: declare mixin instance +[1734569707.798743] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform -[1768979805.013725] HB: declare canonical mixin instance +[1734569707.802295] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform» -[1768979805.014825] HB: declare mixin instance +[1734569707.803430] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology -[1768979805.017560] HB: declare canonical mixin instance +[1734569707.805992] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology» -[1768979805.018573] HB: declare mixin instance +[1734569707.807046] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform -[1768979805.020598] HB: declare canonical mixin instance +[1734569707.808834] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform» -[1768979805.022031] HB: we can build a Stage11_UniformSpace_wo_Topology on +[1734569707.810263] HB: we can build a Stage11_UniformSpace_wo_Topology on Qc -[1768979805.022237] HB: declare canonical structure instance +[1734569707.810474] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology -[1768979805.022367] HB: Giving name HB_unnamed_mixin_46 to mixin instance +[1734569707.810617] HB: Giving name HB_unnamed_mixin_46 to mixin instance Builders_21.Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology Qc HB_unnamed_mixin_35 HB_unnamed_mixin_40 HB_unnamed_factory_41 -[1768979805.023264] HB: structure instance for +[1734569707.811624] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology is {| UniformSpace_wo_Topology.sort := Qc; @@ -1923,12 +1959,12 @@ HB_unnamed_mixin_46 |} |} -[1768979805.024612] HB: structure instance +[1734569707.812741] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology declared -[1768979805.025364] HB: we can build a Stage11_UniformSpace on Qc -[1768979805.025562] HB: declare canonical structure instance +[1734569707.813516] HB: we can build a Stage11_UniformSpace on Qc +[1734569707.813725] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace -[1768979805.025692] HB: structure instance for +[1734569707.813867] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace is {| UniformSpace.sort := Qc; @@ -1938,15 +1974,15 @@ UniformSpace.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_46 |} |} -[1768979805.026838] HB: structure instance +[1734569707.815023] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace declared -[1768979805.027679] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc -[1768979805.027861] HB: declare canonical structure instance +[1734569707.815863] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc +[1734569707.816059] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform -[1768979805.028043] HB: Giving name HB_unnamed_mixin_47 to mixin instance +[1734569707.816254] HB: Giving name HB_unnamed_mixin_47 to mixin instance Builders_21.to_JoinTAddAG_wo_Uniform Qc HB_unnamed_mixin_35 HB_unnamed_mixin_40 HB_unnamed_factory_41 -[1768979805.029356] HB: structure instance for +[1734569707.817357] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform is {| TAddAG_wo_Uniform.sort := Qc; @@ -1958,12 +1994,12 @@ HB_unnamed_mixin_47 |} |} -[1768979805.030493] HB: structure instance +[1734569707.818533] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform declared -[1768979805.031731] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc -[1768979805.031928] HB: declare canonical structure instance +[1734569707.819792] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc +[1734569707.819996] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined -[1768979805.032099] HB: structure instance for +[1734569707.820164] HB: structure instance for Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined is {| Uniform_TAddAG_unjoined.sort := Qc; @@ -1978,18 +2014,18 @@ HB_unnamed_mixin_46 |} |} -[1768979805.033611] HB: structure instance +[1734569707.821373] HB: structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined declared -[1768979805.035856] HB: we can build a Stage11_TAddAG on Qc -[1768979805.036284] HB: declare canonical structure instance +[1734569707.823707] HB: we can build a Stage11_TAddAG on Qc +[1734569707.823928] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG -[1768979805.036526] HB: Giving name HB_unnamed_mixin_48 to mixin instance +[1734569707.824150] HB: Giving name HB_unnamed_mixin_48 to mixin instance Builders_21.Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology Qc HB_unnamed_mixin_35 HB_unnamed_mixin_40 HB_unnamed_factory_41 -[1768979805.037814] HB: Giving name HB_unnamed_mixin_49 to mixin instance +[1734569707.825466] HB: Giving name HB_unnamed_mixin_49 to mixin instance Builders_21.Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform Qc HB_unnamed_mixin_35 HB_unnamed_mixin_40 HB_unnamed_factory_41 -[1768979805.039082] HB: structure instance for +[1734569707.826838] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG is {| TAddAG.sort := Qc; @@ -2003,13 +2039,13 @@ TAddAG.Stage11_Join_TAddAG_Uniform_mixin := HB_unnamed_mixin_49 |} |} -[1768979805.040619] HB: structure instance +[1734569707.828323] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG declared entourage : set (set (Qc * Qc)) : set (set (Qc * Qc)) -Finished transaction in 11.578 secs (9.162u,0.471s) (successful) +Finished transaction in 10.439 secs (9.442u,0.579s) (successful) Finished transaction in 0. secs (0.u,0.s) (successful) -Finished transaction in 9.176 secs (8.678u,0.487s) (successful) +Finished transaction in 9.182 secs (8.725u,0.456s) (successful) Module Type new_concept_Locked = Sig @@ -2119,12 +2155,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/945171/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/945171/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/297944 and its subdirectories -I: Current time: Tue Jan 20 19:17:11 -12 2026 -I: pbuilder-time-stamp: 1768979831 +I: removing directory /srv/workspace/pbuilder/945171 and its subdirectories +I: Current time: Thu Dec 19 14:55:35 +14 2024 +I: pbuilder-time-stamp: 1734569735