Diff of the two buildlogs: -- --- b1/build.log 2025-02-26 21:15:05.862191329 +0000 +++ b2/build.log 2025-02-26 21:17:04.196839705 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Tue Mar 31 15:34:08 -12 2026 -I: pbuilder-time-stamp: 1775014448 +I: Current time: Thu Feb 27 11:15:08 +14 2025 +I: pbuilder-time-stamp: 1740604508 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/trixie-reproducible-base.tgz] I: copying local configuration @@ -22,51 +22,83 @@ dpkg-source: info: unpacking coq-hierarchy-builder_1.8.1-1.debian.tar.xz I: Not using root during the build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/4189313/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/1345001/tmp/hooks/D01_modify_environment starting +debug: Running on infom01-amd64. +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 Feb 26 21:15 /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/1345001/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/1345001/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='amd64' - 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]="x86_64-pc-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=amd64 + DEBIAN_FRONTEND=noninteractive DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=12 ' - DISTRIBUTION='trixie' - HOME='/root' - HOST_ARCH='amd64' + DIRSTACK=() + DISTRIBUTION=trixie + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=x86_64 + HOST_ARCH=amd64 IFS=' ' - INVOCATION_ID='6aaa75a6be654f3fafb897ec8b76fe8b' - 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='4189313' - PS1='# ' - PS2='> ' + INVOCATION_ID=b3bfa74cec83488393970d3f081550ee + LANG=C + LANGUAGE=et_EE:et + LC_ALL=C + MACHTYPE=x86_64-pc-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=1345001 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.TSZoFa0z/pbuilderrc_2NtU --distribution trixie --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.TSZoFa0z/b1 --logfile b1/build.log coq-hierarchy-builder_1.8.1-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' + 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.TSZoFa0z/pbuilderrc_3cD9 --distribution trixie --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.TSZoFa0z/b2 --logfile b2/build.log coq-hierarchy-builder_1.8.1-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' I: uname -a - Linux infom02-amd64 6.12.9+bpo-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.12.9-1~bpo12+1 (2025-01-19) x86_64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-31-cloud-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.128-1 (2025-02-07) x86_64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Nov 22 2024 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/4189313/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Nov 22 14:40 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/1345001/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -195,7 +227,7 @@ Get: 79 http://deb.debian.org/debian trixie/main amd64 libelpi-ocaml-dev amd64 2.0.7-1 [15.3 MB] Get: 80 http://deb.debian.org/debian trixie/main amd64 libcoq-elpi amd64 2.4.0-1 [12.6 MB] Get: 81 http://deb.debian.org/debian trixie/main amd64 wdiff amd64 1.2.2-7 [122 kB] -Fetched 363 MB in 9s (42.0 MB/s) +Fetched 363 MB in 3s (106 MB/s) Preconfiguring packages ... Selecting previously unselected package libpython3.13-minimal:amd64. (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 ... 19799 files and directories currently installed.) @@ -470,8 +502,8 @@ Setting up tzdata (2025a-2) ... Current default time zone: 'Etc/UTC' -Local time is now: Wed Apr 1 03:37:05 UTC 2026. -Universal Time is now: Wed Apr 1 03:37:05 UTC 2026. +Local time is now: Wed Feb 26 21:16:27 UTC 2025. +Universal Time is now: Wed Feb 26 21:16:27 UTC 2025. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up autotools-dev (20220109.1) ... @@ -546,7 +578,11 @@ Building tag database... -> Finished parsing the build-deps I: Building the package -I: Running cd /build/reproducible-path/coq-hierarchy-builder-1.8.1/ && 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.1-1_source.changes +I: user script /srv/workspace/pbuilder/1345001/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for trixie +I: user script /srv/workspace/pbuilder/1345001/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/coq-hierarchy-builder-1.8.1/ && 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.1-1_source.changes dpkg-buildpackage: info: source package coq-hierarchy-builder dpkg-buildpackage: info: source version 1.8.1-1 dpkg-buildpackage: info: source distribution unstable @@ -592,8 +628,8 @@ make test-suite make[2]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.8.1' make -f Makefile.coq -make[3]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.8.1' /usr/bin/coq_makefile -f _CoqProject.test-suite -o Makefile.test-suite.coq +make[3]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.8.1' make[4]: Nothing to be done for 'real-all'. make[3]: Leaving directory '/build/reproducible-path/coq-hierarchy-builder-1.8.1' make -f Makefile.test-suite.coq @@ -604,10 +640,10 @@ COQC examples/demo1/hierarchy_0.v COQC examples/demo1/hierarchy_1.v COQC examples/demo1/hierarchy_3.v -COQC examples/demo1/hierarchy_4.v -COQC examples/demo1/hierarchy_5.v COQC examples/demo1/hierarchy_2.v +COQC examples/demo1/hierarchy_4.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 @@ -628,22 +664,8 @@ 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] -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] -COQC examples/demo4/hierarchy_0.v -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 -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] -[1775014650.901297] HB: start module and section AddComoid_of_Type -[1775014650.907233] HB: converting arguments +[1740604601.754805] HB: start module and section AddComoid_of_Type +[1740604601.755328] HB: converting arguments indt-decl (parameter A explicit X0 c0 \ record AddComoid_of_Type (sort (typ X1)) Build_AddComoid_of_Type @@ -668,20 +690,21 @@ (prod `x` (X9 c4) c5 \ app [global (indt «eq»), X10 c4 c5, app [c2, c1, c5], c5]) c5 \ end-record)) to factories -[1775014650.907785] HB: processing key parameter -[1775014650.908241] HB: converting factories +[1740604601.755609] HB: processing key parameter +[1740604601.755909] HB: converting factories w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] to mixins -[1775014650.908397] HB: declaring context +[1740604601.756011] HB: declaring context w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] -[1775014650.908645] HB: declaring parameters and key as section variables +[1740604601.756152] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1775014650.909233] HB: declare mixin or factory -[1775014650.909363] HB: declare record axioms_ -[1775014650.914481] HB: declare notation Build -[1775014650.927314] HB: declare notation axioms -[1775014650.930363] HB: start module Exports -[1775014650.936760] HB: end modules and sections; export +[1740604601.756525] HB: declare mixin or factory +[1740604601.756597] HB: declare record axioms_ +[1740604601.759465] HB: declare notation Build +[1740604601.761864] HB: declare notation axioms +[1740604601.763876] HB: start module Exports +[1740604601.765388] HB: end modules and sections; export «HB.examples.readme.AddComoid_of_Type.Exports» +COQC examples/demo4/hierarchy_0.v (* Module AddComoid_of_Type. @@ -737,68 +760,68 @@ Notation AddComoid_of_Type X1 := ( AddComoid_of_Type.phant_axioms X1). *) -[1775014650.975349] HB: start module AddComoid -[1775014650.975792] HB: declare axioms record +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_2.v", line 39, characters 2-91: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +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] +[1740604601.777216] HB: start module AddComoid +[1740604601.777446] HB: declare axioms record w-params.nil A (sort (typ «HB.examples.readme.25»)) c0 \ [triple (indt «AddComoid_of_Type.axioms_») [] c0] -[1775014650.976088] HB: typing class field +[1740604601.777570] HB: typing class field indt «AddComoid_of_Type.axioms_» -[1775014650.977885] HB: declare type record -[1775014650.979861] HB: structure: new mixins +[1740604601.778594] HB: declare type record +[1740604601.779398] HB: structure: new mixins [indt «AddComoid_of_Type.axioms_»] -[1775014650.980006] HB: structure: mixin first class +[1740604601.779469] HB: structure: mixin first class [mixin-first-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»)] -[1775014650.980149] HB: declaring clone abbreviation -[1775014650.983525] HB: begin module for builders -[1775014650.983950] HB: begin module Super -[1775014650.984186] HB: ended module Super -[1775014650.984515] HB: postulating factories -[1775014650.984734] HB: processing key context-item -[1775014650.984860] HB: declaring pack_ constant -[1775014650.985085] HB: processing mixin parameter a -[1775014650.985568] HB: declaring parameters and key as section variables -COQC examples/FSCD2020_material/V1.v -[1775014650.986281] HB: declaring pack_ constant = +[1740604601.779516] HB: declaring clone abbreviation +[1740604601.780386] HB: begin module for builders +[1740604601.780603] HB: begin module Super +[1740604601.780677] HB: ended module Super +[1740604601.780826] HB: postulating factories +[1740604601.780906] HB: processing key context-item +[1740604601.781077] HB: processing mixin parameter a +[1740604601.781511] HB: declaring parameters and key as section variables +[1740604601.781515] HB: declaring pack_ constant +Here is the list of mixins to declare (the order matters): [] +[1740604601.781787] 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]] -[1775014650.987781] HB: start module Exports -[1775014650.988064] HB: making coercion from type to target -[1775014650.988185] HB: declare sort coercion -[1775014650.988459] HB: exporting unification hints -[1775014650.988695] HB: exporting coercions from class to mixins -[1775014650.988888] HB: export class to mixin coercion for mixin +[1740604601.782560] HB: start module Exports +[1740604601.782755] HB: making coercion from type to target +[1740604601.782806] HB: declare sort coercion +[1740604601.782941] HB: exporting unification hints +[1740604601.783051] HB: exporting coercions from class to mixins +[1740604601.783187] HB: export class to mixin coercion for mixin readme_AddComoid_of_Type -[1775014650.989236] HB: accumulating various props -[1775014650.989955] HB: stop module Exports -[1775014650.990361] HB: declaring on_ abbreviation -Here is the list of mixins to declare (the order matters): [] -[1775014650.996434] HB: declaring `copy` abbreviation -[1775014650.997148] HB: declaring on abbreviation -[1775014651.004122] HB: end modules; export -«HB.examples.readme.AddComoid.Exports» -[1775014651.004607] HB: exporting operations -[1775014651.005639] HB: export operation zero -[1775014651.007631] HB: export operation add -[1775014651.010096] HB: export operation addrA -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_1.v", line 55, characters 0-123: +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/FSCD2020_material/V2.v -File "./examples/demo1/hierarchy_5.v", line 68, characters 2-91: +[1740604601.783354] HB: accumulating various props +[1740604601.783691] HB: stop module Exports +[1740604601.783971] HB: declaring on_ abbreviation +[1740604601.785252] HB: declaring `copy` abbreviation +[1740604601.785650] HB: declaring on abbreviation +[1740604601.786424] HB: end modules; export +«HB.examples.readme.AddComoid.Exports» +[1740604601.786744] HB: exporting operations +[1740604601.787296] HB: export operation zero +[1740604601.788463] HB: export operation add +[1740604601.789736] HB: export operation addrA +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] -[1775014651.167192] HB: export operation addrC -[1775014651.168737] HB: export operation add0r -[1775014651.169610] HB: operations meta-data module: ElpiOperations -[1775014651.175658] HB: abbreviation factory-by-classname +[1740604601.859713] HB: export operation addrC +[1740604601.861240] HB: export operation add0r +[1740604601.862087] HB: operations meta-data module: ElpiOperations +[1740604601.862820] HB: abbreviation factory-by-classname (* Module AddComoid. @@ -895,10 +918,7 @@ *) forall (M : AddComoid.type) (x : M), x + x = 0 : Prop -[1775014651.242776] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_AddAG_of_AddComoid -[1775014651.242932] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_Ring_of_AddAG +COQC examples/demo5/hierarchy_0.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] @@ -907,12 +927,24 @@ : AbelianGrp.axioms_ Z : AbelianGrp.axioms_ Z +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] HB: Z is canonically equipped with structures: - AbelianGrp (from "./examples/readme.v", line 32) - AddComoid (from "./examples/readme.v", line 31) +COQC examples/FSCD2020_material/V1.v +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] +COQC examples/FSCD2020_material/V2.v File "./examples/hulk.v", line 143, characters 0-63: Warning: pulling in dependencies: [Feather_HasEqDec] @@ -920,17 +952,18 @@ Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] COQC examples/FSCD2020_material/V3.v +[1740604602.060493] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_AddAG_of_AddComoid +[1740604602.060744] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_Ring_of_AddAG COQC examples/FSCD2020_material/V4.v -COQC examples/FSCD2020_talk/V1.v -COQC examples/FSCD2020_talk/V2.v HB: A is canonically equipped with structures: - Equality Singleton (from "./examples/hulk.v", line 216) -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/FSCD2020_talk/V1.v +COQC examples/FSCD2020_talk/V2.v COQC examples/FSCD2020_talk/V3.v inhab : ?s @@ -943,14 +976,16 @@ : inhab = (7 :: nil)%list where ?T : [ |- Type] -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] 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. +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 +COQC examples/Coq2020_material/CoqWS_abstract.v HB.check: SemiRing_of_AddComoid.axioms_ : @@ -959,6 +994,7 @@ : 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 @@ -968,10 +1004,16 @@ : forall s : Monoid.type, s -> s -> s @addNr : forall s : Ring.type, left_inverse 0 opp add -COQC examples/Coq2020_material/CoqWS_demo.v -COQC examples/Coq2020_material/CoqWS_abstract.v -COQC examples/Coq2020_material/CoqWS_expansion/withHB.v +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] COQC examples/Coq2020_material/CoqWS_expansion/withoutHB.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,elpi,default] COQC tests/type_of_exported_ops.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. @@ -986,13 +1028,6 @@ : forall s : AbelianGroup.type, commutative add COQC tests/duplicate_structure.v COQC tests/instance_params_no_type.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,elpi,default] -COQC tests/test_CS_db_filtering.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -1004,6 +1039,14 @@ : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add +add + : ?s -> ?s -> ?s +where +?s : [ |- CMonoid.type] +addrC + : commutative add +where +?s : [ |- CMonoid.type] addrC : commutative add where @@ -1011,15 +1054,25 @@ 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/test_CS_db_filtering.v COQC tests/subtype.v -add - : ?s -> ?s -> ?s -where -?s : [ |- CMonoid.type] -addrC - : commutative add +COQC tests/exports.v +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,elpi,default] +forall x y : ?t, x - (y + 0) = x + : Prop where -?s : [ |- CMonoid.type] +?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) +File "./examples/Coq2020_material/CoqWS_abstract.v", line 23, characters 0-71: +Warning: +pulling in dependencies: [CoqWS_abstract_CMonoid_of_Type] + +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 @@ -1031,42 +1084,47 @@ : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add -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] -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] -COQC tests/log_impargs_record.v -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,elpi,default] -COQC tests/compress_coe.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) +forall (R : Ring.type) (x y : R), 1 * x = y - x + : Prop +forall + (x : join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing + ?t) (y : ?t), 1 * x = y - x + : Prop +where +?t : + [x : + join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing + ?t + y : ?t |- Ring.type] (x, y cannot be used) +COQC tests/log_impargs_record.v +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 +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop +COQC tests/funclass.v +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop +add + : A -> A -> A +COQC tests/grefclass.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] File "./tests/instance_params_no_type.v", line 6, characters 0-76: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop File "./tests/instance_params_no_type.v", line 7, characters 0-78: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] @@ -1076,28 +1134,12 @@ Arguments list_foo' (P A)%type_scope list_foo' is transparent Expands to: Constant HB.tests.instance_params_no_type.list_foo' -forall x y : ?t, 1 + x = y * x +forall x : Z, x * - (1 + x) = 0 + 1 : Prop -where -?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) nat_foo : forall P : Type, is_foo.axioms_ P nat list_foo : forall P : Type, is_foo.axioms_ P (list P) -COQC tests/funclass.v -forall (R : Ring.type) (x y : R), 1 * x = y - x - : Prop -forall - (x : join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing - ?t) (y : ?t), 1 * x = y - x - : Prop -where -?t : - [x : - join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing - ?t - y : ?t |- Ring.type] (x, y cannot be used) -COQC tests/grefclass.v COQC tests/local_instance.v COQC tests/lock.v foo.type @@ -1137,17 +1179,65 @@ 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 -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop -add - : A -> A -> A -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop COQC tests/interleave_context.v list_bar : forall P : b.type, is_bar.axioms_ P (list P) COQC tests/not_same_key.v +[1740604603.377430] HB: start module SubInhab +[1740604603.377742] 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] +[1740604603.377972] HB: typing class field indt «is_inhab.axioms_» +[1740604603.378130] HB: typing class field indt «is_SUB.axioms_» +[1740604603.379263] HB: declare type record +[1740604603.380187] HB: structure: new mixins [] +[1740604603.380278] HB: structure: mixin first class [] +[1740604603.380339] HB: declaring clone abbreviation +[1740604603.381940] HB: declaring pack_ constant COQC tests/hb_pack.v +[1740604603.382483] 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]] +[1740604603.382947] HB: start module Exports +[1740604603.383124] HB: making coercion from type to target +[1740604603.383204] HB: declare sort coercion +[1740604603.383316] HB: exporting unification hints +[1740604603.383736] HB: declare coercion subtype_SubInhab__to__subtype_SUB +[1740604603.384129] HB: declare coercion hint +subtype_SubInhab_class__to__subtype_SUB_class +[1740604603.385038] HB: declare unification hint +subtype_SubInhab__to__subtype_SUB +[1740604603.386099] HB: declare coercion subtype_SubInhab__to__subtype_Inhab +[1740604603.386452] HB: declare coercion hint +subtype_SubInhab_class__to__subtype_Inhab_class +[1740604603.387373] HB: declare unification hint +subtype_SubInhab__to__subtype_Inhab +[1740604603.388606] HB: declare unification hint +join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB +[1740604603.389722] HB: exporting coercions from class to mixins +[1740604603.389883] HB: export class to mixin coercion for mixin +subtype_is_inhab +[1740604603.390247] HB: export class to mixin coercion for mixin +subtype_is_SUB +[1740604603.390531] HB: accumulating various props +[1740604603.390970] HB: stop module Exports +[1740604603.392123] HB: declaring on_ abbreviation +[1740604603.393501] HB: declaring `copy` abbreviation +[1740604603.394065] HB: declaring on abbreviation +[1740604603.394681] HB: end modules; export +«HB.tests.subtype.SubInhab.Exports» +[1740604603.395720] HB: exporting operations +[1740604603.395916] HB: operations meta-data module: ElpiOperations +[1740604603.396210] HB: abbreviation factory-by-classname (* Module A. @@ -1205,60 +1295,20 @@ A.p is transparent Expands to: Constant HB.tests.log_impargs_record.A.p COQC tests/declare.v -[1775014654.933752] HB: start module SubInhab -[1775014654.934076] 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] -[1775014654.934342] HB: typing class field indt «is_inhab.axioms_» -[1775014654.934548] HB: typing class field indt «is_SUB.axioms_» -[1775014654.935888] HB: declare type record -[1775014654.944001] HB: structure: new mixins [] -[1775014654.944121] HB: structure: mixin first class [] -[1775014654.944223] HB: declaring clone abbreviation -[1775014654.946220] HB: declaring pack_ constant -[1775014654.946836] 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]] -[1775014654.947406] HB: start module Exports -[1775014654.947679] HB: making coercion from type to target -[1775014654.947793] HB: declare sort coercion -[1775014654.947975] HB: exporting unification hints -[1775014654.948509] HB: declare coercion subtype_SubInhab__to__subtype_SUB -[1775014654.948978] HB: declare coercion hint -subtype_SubInhab_class__to__subtype_SUB_class -[1775014654.950097] HB: declare unification hint -subtype_SubInhab__to__subtype_SUB -[1775014654.951355] HB: declare coercion subtype_SubInhab__to__subtype_Inhab -[1775014654.951771] HB: declare coercion hint -subtype_SubInhab_class__to__subtype_Inhab_class -[1775014654.952808] HB: declare unification hint -subtype_SubInhab__to__subtype_Inhab -[1775014654.960321] HB: declare unification hint -join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB -[1775014654.961776] HB: exporting coercions from class to mixins -[1775014654.961998] HB: export class to mixin coercion for mixin -subtype_is_inhab -[1775014654.962518] HB: export class to mixin coercion for mixin -subtype_is_SUB -[1775014654.962907] HB: accumulating various props -[1775014654.963467] HB: stop module Exports -[1775014654.964595] HB: declaring on_ abbreviation -[1775014654.966224] HB: declaring `copy` abbreviation -[1775014654.966888] HB: declaring on abbreviation -[1775014654.971591] HB: end modules; export -«HB.tests.subtype.SubInhab.Exports» -[1775014654.972756] HB: exporting operations -[1775014654.972984] HB: operations meta-data module: ElpiOperations -[1775014654.973331] 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 +p : pred nat + : pred 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/short.v Notation big := big.body Expands to: Notation HB.tests.lock.X.big @@ -1267,73 +1317,40 @@ 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 -COQC tests/short.v +COQC tests/instance_before_structure.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". -p : pred nat - : pred nat -COQC tests/instance_before_structure.v COQC tests/primitive_records.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/non_forgetful_inheritance.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 -COQC tests/fix_loop.v -[1775014655.457224] HB: start module and section hasA -[1775014655.457653] 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 -[1775014655.457862] HB: processing key parameter -[1775014655.458274] HB: converting factories -w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins -[1775014655.458437] HB: declaring context -w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] -[1775014655.458674] HB: declaring parameters and key as section variables -Here is the list of mixins to declare (the order matters): [] -[1775014655.463102] HB: declare mixin or factory -[1775014655.463261] HB: declare record axioms_ -[1775014655.464668] HB: declare notation Build -[1775014655.465847] HB: declare notation axioms -[1775014655.467784] HB: start module Exports -[1775014655.469090] HB: end modules and sections; export -«HB.tests.hb_pack.hasA.Exports» -hasA.type not a defined object. -hasB.type not a defined object. -[1775014655.587684] HB: exporting under the module path [] -[1775014655.587882] HB: exporting modules +[1740604603.583667] HB: exporting under the module path [] +[1740604603.583949] HB: exporting modules [Ring_of_TYPE.Exports, Ring.Exports, RingElpiOperations, RingExports, Dummy.Exports, URing.Exports, URingElpiOperations, dummy.Exports, Builders_1.Builders_Export_5] -[1775014655.588787] HB: exporting CS instances +[1740604603.584809] HB: exporting CS instances [«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] -[1775014655.589078] HB: exporting Abbreviations [addr0, addrNK] -[1775014655.589209] HB: exporting Clauses X0 +[1740604603.585135] HB: exporting Abbreviations [addr0, addrNK] +[1740604603.585292] HB: exporting Clauses X0 forall (R : Enclosing.Ring.type) (x : R), x = x : Prop 0%G : ?s where ?s : [ |- Enclosing.Ring.type] +Enclosing.zero : Z + : Z +COQC tests/non_forgetful_inheritance.v +COQC tests/fix_loop.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 -Enclosing.zero : Z - : Z +HB.check: forall w : wp.type nat Init.Nat.mul, w = w : Prop +COQC tests/test_synthesis_params.v +COQC tests/hnf.v Datatypes_prod__canonical__compress_coe_D = fun D D' : D.type => {| @@ -1355,22 +1372,62 @@ : D.type -> D.type -> D.type Arguments Datatypes_prod__canonical__compress_coe_D D D' -HB.check: forall w : wp.type nat Init.Nat.mul, w = w : Prop +COQC tests/fun_instance.v +[1740604603.780959] HB: start module and section hasA +[1740604603.781203] 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 +[1740604603.781416] HB: processing key parameter +[1740604603.781664] HB: converting factories +w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins +[1740604603.781723] HB: declaring context +w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] +[1740604603.781807] HB: declaring parameters and key as section variables +Here is the list of mixins to declare (the order matters): [] +[1740604603.782044] HB: declare mixin or factory +[1740604603.782082] HB: declare record axioms_ +[1740604603.782937] HB: declare notation Build +[1740604603.783755] HB: declare notation axioms +[1740604603.784739] HB: start module Exports +[1740604603.785907] HB: end modules and sections; export +«HB.tests.hb_pack.hasA.Exports» +hasA.type not a defined object. +hasB.type not a defined object. File "./tests/interleave_context.v", line 16, characters 0-52: Warning: pulling in dependencies: [interleave_context_HasA, interleave_context_HasB] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] -COQC tests/test_synthesis_params.v -COQC tests/hnf.v -COQC tests/fun_instance.v aType : Type hasB.type not a defined object. -COQC tests/issue284.v +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] +Query assignments: + Ind = «hasA.axioms_» +HB: nat is canonically equipped with structures: + - s1 + (from "./tests/instance_before_structure.v", line 11) + hasAB.type not a defined object. +Query assignments: + Ind = «A.axioms_» +Query assignments: + Ind = «A.type» +COQC tests/issue284.v hasA'.type not a defined object. +HB: nat is canonically equipped with structures: + - s1 + (from "./tests/instance_before_structure.v", line 11) + forall T : AB.type, unkeyed {| @@ -1398,40 +1455,33 @@ : T * T AB3 : AB.type : AB.type -Query assignments: - Ind = «hasA.axioms_» -X : Foo.type A P - : Foo.type A P -HB: nat is canonically equipped with structures: - - s1 - (from "./tests/instance_before_structure.v", line 11) - -Query assignments: - Ind = «A.axioms_» -Query assignments: - Ind = «A.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] +COQC tests/issue287.v HB: nat is canonically equipped with structures: - s1 (from "./tests/instance_before_structure.v", line 11) +X : Foo.type A P + : Foo.type A P hasAB.type not a defined object. -hasA'.type not a defined object. HB: nat is canonically equipped with structures: + - s3 + s2 + (from "./tests/instance_before_structure.v", line 30) - s1 (from "./tests/instance_before_structure.v", line 11) -T : Fun.type nat - : Fun.type nat -COQC tests/issue287.v +default1 + : nat +default2 + : nat +default3 + : nat +hasA'.type not a defined object. COQC tests/two_hier.v -COQC tests/instance_merge_with_param.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] -COQC tests/instance_merge_with_distinct_param.v +COQC tests/instance_merge_with_param.v Debug: elpi lets escape exception: non forgetful inheritance detected. You have two solutions: @@ -1447,48 +1497,40 @@ 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] -HB: nat is canonically equipped with structures: - - s1 - (from "./tests/instance_before_structure.v", line 11) - erefl : ?t = ?t : ?t = ?t where ?t : [ |- Sq.type] -HB: nat is canonically equipped with structures: - - s3 - s2 - (from "./tests/instance_before_structure.v", line 30) - - s1 - (from "./tests/instance_before_structure.v", line 11) - -default1 - : nat -default2 - : nat -default3 - : nat +COQC tests/instance_merge_with_distinct_param.v +T : Fun.type nat + : Fun.type nat 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 +COQC tests/unit/enrich_type.v +COQC tests/unit/mixin_src_has_mixin_instance.v COQC tests/unit/mk_src_map.v COQC tests/unit/close_hole_term.v COQC tests/unit/struct.v COQC tests/factory_when_notation.v COQC tests/saturate_on.v COQC tests/bug_435.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) + Query assignments: X = global (indt «nat») Query assignments: @@ -1579,31 +1621,9 @@ COQC tests/bug_447.v -nat : s3.type - : s3.type -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 -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_relevant_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] -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_foo' - : forall P A : Type, is_foo.axioms_ P (list A) -list_foo - : forall P : Type, is_foo.axioms_ P (list P) Query assignments: X = app [global (indt «list»), X0] X1_ = X1 @@ -1630,28 +1650,13 @@ Query assignments: Z = global (indt «nat») -Query assignments: -File "./tests/unit/mixin_src_has_mixin_instance.v", line 12, characters 0-57: +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] - 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] -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») +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: X = app [global (const «Inj»), X0, X1, X2, X3, X4] X2_ = X0 @@ -1705,6 +1710,27 @@ WEAK CONSTRAINTS: +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] +nat : s3.type + : s3.type +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 +COQC tests/unimported_relevant_class.v +COQC tests/unimported_irrelevant_class.v HB: list is canonically equipped with structures: - s3 (from "./tests/instance_merge_with_param.v", line 23) @@ -1713,6 +1739,17 @@ - s1 (from "./tests/instance_merge_with_param.v", line 10) +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») nat : s3.type : s3.type list nat : s3.type @@ -1721,7 +1758,6 @@ : s3.type fun t : s3.type => list t : s3.type : s3.type -> s3.type -COQC tests/unimported_irrelevant_class.v COQC examples/demo1/test_0_0.v COQC examples/demo1/test_1_0.v COQC examples/demo1/test_2_0.v @@ -1736,6 +1772,7 @@ 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 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 @@ -1744,7 +1781,6 @@ : 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 -COQC examples/demo1/test_3_0.v COQC examples/demo1/test_3_3.v COQC examples/demo1/test_4_0.v File "./tests/saturate_on.v", line 5, characters 0-64: @@ -1754,24 +1790,25 @@ : Pointed.type COQC examples/demo1/test_4_3.v COQC examples/demo1/test_5_0.v -[1775014658.949618] HB: postulating X -[1775014658.955433] HB: declare canonical mixin instance +[1740604605.058845] HB: postulating X +[1740604605.060670] HB: declare canonical mixin instance «HB_unnamed_factory_5» -[1775014658.955961] HB: we can build a bug_435_B2 on unit -[1775014658.956167] HB: declare canonical structure instance +[1740604605.061122] HB: we can build a bug_435_B2 on unit +[1740604605.061309] HB: declare canonical structure instance Datatypes_unit__canonical__bug_435_B2 -[1775014658.956320] HB: structure instance for +[1740604605.061429] 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 |} |} -[1775014658.957153] HB: structure instance +COQC examples/demo1/test_5_3.v +[1740604605.062288] HB: structure instance Datatypes_unit__canonical__bug_435_B2 declared -[1775014658.957614] HB: we can build a should_work_but_fails_B on unit -[1775014658.957809] HB: declare canonical structure instance +[1740604605.062663] HB: we can build a should_work_but_fails_B on unit +[1740604605.062826] HB: declare canonical structure instance Datatypes_unit__canonical__should_work_but_fails_B -[1775014658.957981] HB: structure instance for +[1740604605.062951] HB: structure instance for Datatypes_unit__canonical__should_work_but_fails_B is {| B.sort := unit; @@ -1781,43 +1818,42 @@ B.bug_435_A2_mixin := HB_unnamed_factory_5 |} |} -[1775014658.958267] HB: closing instance section -testTy : JustMixedParam.type ?T - : JustMixedParam.type ?T -where -?T : [ |- Type] +[1740604605.063209] HB: closing instance section unit : B.type ?t : B.type ?t where ?t : [ |- S.type] -COQC examples/demo1/test_5_3.v +COQC examples/demo2/stage10.v unit : B.type ?t : B.type ?t where ?t : [ |- S.type] -COQC examples/demo2/stage10.v COQC examples/demo2/stage11.v COQC examples/demo3/test_0_0.v COQC examples/demo3/test_1_0.v +testTy : JustMixedParam.type ?T + : JustMixedParam.type ?T +where +?T : [ |- Type] COQC examples/demo3/test_2_0.v COQC tests/exports2.v -[1775014659.956562] HB: exporting under the module path [] -[1775014659.956823] HB: exporting modules [] -[1775014659.956981] HB: exporting CS instances [] -[1775014659.957120] HB: exporting Abbreviations [] -[1775014659.957250] HB: exporting Clauses X0 -File "./examples/demo2/stage10.v", line 4, characters 0-25: +[1740604605.614004] HB: exporting under the module path [] +[1740604605.614083] HB: exporting modules [] +[1740604605.614104] HB: exporting CS instances [] +[1740604605.614121] HB: exporting Abbreviations [] +[1740604605.614140] HB: exporting Clauses X0 +File "./examples/demo2/stage11.v", line 3, characters 0-25: Warning: Hiding binding of key Q to Q_scope [hiding-delimiting-key,parsing,default] -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 3, characters 0-25: +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 115, characters 2-100: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] +File "./examples/demo2/stage10.v", line 112, characters 2-115: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] 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 @@ -1848,30 +1884,30 @@ disable this warning. [deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] HB: skipping section opening -[1775014661.764478] HB: declare mixin instance +[1740604606.600768] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology -[1775014661.765211] HB: declare canonical mixin instance +[1740604606.601400] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology» -[1775014661.766013] HB: declare mixin instance +[1740604606.601966] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform -[1775014661.768324] HB: declare canonical mixin instance +[1740604606.603985] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform» -[1775014661.768958] HB: declare mixin instance +[1740604606.604515] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology -[1775014661.770584] HB: declare canonical mixin instance +[1740604606.605887] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology» -[1775014661.771211] HB: declare mixin instance +[1740604606.606352] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform -[1775014661.772342] HB: declare canonical mixin instance +[1740604606.607351] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform» -[1775014661.773212] HB: we can build a Stage11_UniformSpace_wo_Topology on +[1740604606.608064] HB: we can build a Stage11_UniformSpace_wo_Topology on Qc -[1775014661.773354] HB: declare canonical structure instance +[1740604606.608178] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology -[1775014661.773497] HB: Giving name HB_unnamed_mixin_46 to mixin instance +[1740604606.608250] 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 -[1775014661.774048] HB: structure instance for +[1740604606.608716] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology is {| UniformSpace_wo_Topology.sort := Qc; @@ -1881,12 +1917,12 @@ HB_unnamed_mixin_46 |} |} -[1775014661.774767] HB: structure instance +[1740604606.609298] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology declared -[1775014661.775275] HB: we can build a Stage11_UniformSpace on Qc -[1775014661.775414] HB: declare canonical structure instance +[1740604606.609669] HB: we can build a Stage11_UniformSpace on Qc +[1740604606.609754] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace -[1775014661.775519] HB: structure instance for +[1740604606.609814] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace is {| UniformSpace.sort := Qc; @@ -1896,15 +1932,15 @@ UniformSpace.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_46 |} |} -[1775014661.776202] HB: structure instance +[1740604606.610315] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace declared -[1775014661.776752] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc -[1775014661.776885] HB: declare canonical structure instance +[1740604606.610721] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc +[1740604606.610805] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform -[1775014661.777015] HB: Giving name HB_unnamed_mixin_47 to mixin instance +[1740604606.610932] 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 -[1775014661.777653] HB: structure instance for +[1740604606.611436] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform is {| TAddAG_wo_Uniform.sort := Qc; @@ -1916,12 +1952,12 @@ HB_unnamed_mixin_47 |} |} -[1775014661.778304] HB: structure instance +[1740604606.611946] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform declared -[1775014661.779199] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc -[1775014661.779376] HB: declare canonical structure instance +[1740604606.612589] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc +[1740604606.612676] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined -[1775014661.779553] HB: structure instance for +[1740604606.612765] HB: structure instance for Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined is {| Uniform_TAddAG_unjoined.sort := Qc; @@ -1936,18 +1972,18 @@ HB_unnamed_mixin_46 |} |} -[1775014661.780236] HB: structure instance +[1740604606.613301] HB: structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined declared -[1775014661.781705] HB: we can build a Stage11_TAddAG on Qc -[1775014661.781845] HB: declare canonical structure instance +[1740604606.614398] HB: we can build a Stage11_TAddAG on Qc +[1740604606.614483] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG -[1775014661.782002] HB: Giving name HB_unnamed_mixin_48 to mixin instance +[1740604606.614584] 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 -[1775014661.782742] HB: Giving name HB_unnamed_mixin_49 to mixin instance +[1740604606.615232] 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 -[1775014661.783508] HB: structure instance for +[1740604606.615837] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG is {| TAddAG.sort := Qc; @@ -1961,13 +1997,13 @@ TAddAG.Stage11_Join_TAddAG_Uniform_mixin := HB_unnamed_mixin_49 |} |} -[1775014661.784310] HB: structure instance +[1740604606.616516] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG declared entourage : set (set (Qc * Qc)) : set (set (Qc * Qc)) -Finished transaction in 10.175 secs (5.792u,0.812s) (successful) +Finished transaction in 6.133 secs (5.576u,0.506s) (successful) Finished transaction in 0. secs (0.u,0.s) (successful) -Finished transaction in 7.04 secs (6.35u,0.676s) (successful) +Finished transaction in 5.709 secs (5.309u,0.399s) (successful) Module Type new_concept_Locked = Sig @@ -2077,12 +2113,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/1345001/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/1345001/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/4189313 and its subdirectories -I: Current time: Tue Mar 31 15:38:05 -12 2026 -I: pbuilder-time-stamp: 1775014685 +I: removing directory /srv/workspace/pbuilder/1345001 and its subdirectories +I: Current time: Thu Feb 27 11:17:03 +14 2025 +I: pbuilder-time-stamp: 1740604623