Diff of the two buildlogs: -- --- b1/build.log 2025-02-26 11:49:53.534780808 +0000 +++ b2/build.log 2025-02-26 11:52:32.787610592 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Tue Feb 25 23:47:40 -12 2025 -I: pbuilder-time-stamp: 1740570460 +I: Current time: Wed Apr 1 08:12:55 +14 2026 +I: pbuilder-time-stamp: 1774980775 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/trixie-reproducible-base.tgz] I: copying local configuration @@ -22,52 +22,84 @@ 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/2843829/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/3438715/tmp/hooks/D01_modify_environment starting +debug: Running on codethink03-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 Mar 31 18:13 /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/3438715/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/3438715/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='trixie' - HOME='/root' - HOST_ARCH='arm64' + DIRSTACK=() + DISTRIBUTION=trixie + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=aarch64 + HOST_ARCH=arm64 IFS=' ' - INVOCATION_ID='87637c99cc4d44d7b0a4cbbcf72e1a63' - 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='2843829' - PS1='# ' - PS2='> ' + INVOCATION_ID=3f9fa8957b2c49f3a2741bed12b67685 + 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=3438715 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.cisCIlaj/pbuilderrc_bOqK --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.cisCIlaj/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' - 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.cisCIlaj/pbuilderrc_hKQA --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.cisCIlaj/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' + http_proxy=http://192.168.101.4:3128 I: uname -a - Linux codethink04-arm64 6.1.0-31-cloud-arm64 #1 SMP Debian 6.1.128-1 (2025-02-07) aarch64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-31-cloud-arm64 #1 SMP Debian 6.1.128-1 (2025-02-07) aarch64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Nov 22 14:40 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/2843829/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Nov 22 2024 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/3438715/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -196,7 +228,7 @@ Get: 79 http://deb.debian.org/debian trixie/main arm64 libelpi-ocaml-dev arm64 2.0.7-1 [15.9 MB] Get: 80 http://deb.debian.org/debian trixie/main arm64 libcoq-elpi arm64 2.4.0-1 [13.1 MB] Get: 81 http://deb.debian.org/debian trixie/main arm64 wdiff arm64 1.2.2-7 [121 kB] -Fetched 372 MB in 12s (32.1 MB/s) +Fetched 372 MB in 3s (143 MB/s) Preconfiguring packages ... Selecting previously unselected package libpython3.13-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 ... 19914 files and directories currently installed.) @@ -471,8 +503,8 @@ Setting up tzdata (2025a-2) ... Current default time zone: 'Etc/UTC' -Local time is now: Wed Feb 26 11:48:45 UTC 2025. -Universal Time is now: Wed Feb 26 11:48:45 UTC 2025. +Local time is now: Tue Mar 31 18:13:54 UTC 2026. +Universal Time is now: Tue Mar 31 18:13:54 UTC 2026. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up autotools-dev (20220109.1) ... @@ -547,7 +579,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/3438715/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for trixie +I: user script /srv/workspace/pbuilder/3438715/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 @@ -612,8 +648,34 @@ COQC examples/demo3/hierarchy_0.v COQC examples/demo3/hierarchy_1.v COQC examples/demo3/hierarchy_2.v -[1740570538.572203] HB: start module and section AddComoid_of_Type -[1740570538.578172] HB: converting arguments +File "./examples/demo2/classical.v", line 422, characters 0-39: +Warning: Notations "_ ^~ _" defined at level 10 with arguments constr +at next level and "_ ^~" defined at level 2 with arguments constr +at next level have incompatible prefixes. One of them will likely not work. +[notation-incompatible-prefix,parsing,default] +File "./examples/demo2/classical.v", line 625, characters 0-75: +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/demo2/classical.v", line 626, characters 0-75: +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/demo2/classical.v", line 657, characters 0-43: +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] +COQC examples/demo4/hierarchy_0.v +[1774980856.394886] HB: start module and section AddComoid_of_Type +[1774980856.397733] HB: begin module for builders +[1774980856.397981] HB: begin module Super +[1774980856.398053] HB: ended module Super +[1774980856.398268] HB: postulating factories +[1774980856.398374] HB: processing key context-item +[1774980856.398599] HB: processing mixin parameter a +[1774980856.398895] HB: declaring parameters and key as section variables +Here is the list of mixins to declare (the order matters): [] +[1774980856.395218] HB: converting arguments indt-decl (parameter A explicit X0 c0 \ record AddComoid_of_Type (sort (typ X1)) Build_AddComoid_of_Type @@ -638,19 +700,23 @@ (prod `x` (X9 c4) c5 \ app [global (indt «eq»), X10 c4 c5, app [c2, c1, c5], c5]) c5 \ end-record)) to factories -[1740570538.578645] HB: processing key parameter -[1740570538.579195] HB: converting factories +[1774980856.419848] HB: processing key parameter +[1774980856.425146] HB: converting factories w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] to mixins -[1740570538.579484] HB: declaring context +[1774980856.431485] HB: declaring context w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] -[1740570538.579729] HB: declaring parameters and key as section variables +[1774980856.431798] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1740570538.580430] HB: declare mixin or factory -[1740570538.580558] HB: declare record axioms_ -[1740570538.585280] HB: declare notation Build -[1740570538.597628] HB: declare notation axioms -[1740570538.601660] HB: start module Exports -[1740570538.608375] HB: end modules and sections; export +[1774980856.432340] HB: declare mixin or factory +[1774980856.432405] HB: declare record axioms_ +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] +[1774980856.455088] HB: declare notation Build +[1774980856.466879] HB: declare notation axioms +[1774980856.494861] HB: start module Exports +COQC examples/demo5/hierarchy_0.v +[1774980856.525489] HB: end modules and sections; export «HB.examples.readme.AddComoid_of_Type.Exports» (* @@ -707,62 +773,52 @@ Notation AddComoid_of_Type X1 := ( AddComoid_of_Type.phant_axioms X1). *) -File "./examples/demo2/classical.v", line 422, characters 0-39: -Warning: Notations "_ ^~ _" defined at level 10 with arguments constr -at next level and "_ ^~" defined at level 2 with arguments constr -at next level have incompatible prefixes. One of them will likely not work. -[notation-incompatible-prefix,parsing,default] -[1740570538.648484] HB: start module AddComoid -[1740570538.648917] HB: declare axioms record +COQC examples/FSCD2020_material/V1.v +[1774980856.640092] HB: start module AddComoid +[1774980856.640379] HB: declare axioms record w-params.nil A (sort (typ «HB.examples.readme.25»)) c0 \ [triple (indt «AddComoid_of_Type.axioms_») [] c0] -[1740570538.649182] HB: typing class field +[1774980856.640558] HB: typing class field indt «AddComoid_of_Type.axioms_» -[1740570538.650901] HB: declare type record -[1740570538.655366] HB: structure: new mixins +[1774980856.642117] HB: declare type record +[1774980856.663792] HB: structure: new mixins [indt «AddComoid_of_Type.axioms_»] -[1740570538.655545] HB: structure: mixin first class +[1774980856.663908] HB: structure: mixin first class [mixin-first-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»)] -[1740570538.655622] HB: declaring clone abbreviation -[1740570538.658971] HB: declaring pack_ constant -[1740570538.666336] HB: declaring pack_ constant = +[1774980856.663958] HB: declaring clone abbreviation +[1774980856.667223] HB: declaring pack_ constant +[1774980856.687883] 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]] -[1740570538.667427] HB: start module Exports -[1740570538.667813] HB: making coercion from type to target -[1740570538.667906] HB: declare sort coercion -[1740570538.668154] HB: exporting unification hints -[1740570538.668351] HB: exporting coercions from class to mixins -[1740570538.668547] HB: export class to mixin coercion for mixin +[1774980856.688946] HB: start module Exports +[1774980856.689257] HB: making coercion from type to target +[1774980856.689306] HB: declare sort coercion +[1774980856.689505] HB: exporting unification hints +[1774980856.689760] HB: exporting coercions from class to mixins +[1774980856.689927] HB: export class to mixin coercion for mixin readme_AddComoid_of_Type -[1740570538.668994] HB: accumulating various props -[1740570538.669529] HB: stop module Exports -[1740570538.670173] HB: declaring on_ abbreviation -[1740570538.676301] HB: declaring `copy` abbreviation -[1740570538.677182] HB: declaring on abbreviation -[1740570538.683301] HB: end modules; export +[1774980856.690183] HB: accumulating various props +[1774980856.690666] HB: stop module Exports +[1774980856.691228] HB: declaring on_ abbreviation +[1774980856.709610] HB: declaring `copy` abbreviation +[1774980856.710349] HB: declaring on abbreviation +[1774980856.727780] HB: end modules; export «HB.examples.readme.AddComoid.Exports» -[1740570538.684089] HB: exporting operations -[1740570538.685241] HB: export operation zero -[1740570538.687432] HB: export operation add -[1740570538.696576] HB: export operation addrA -File "./examples/demo2/classical.v", line 625, characters 0-75: -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/demo2/classical.v", line 626, characters 0-75: -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/demo2/classical.v", line 657, characters 0-43: -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] -[1740570538.877967] HB: export operation addrC -[1740570538.880484] HB: export operation add0r -[1740570538.887449] HB: operations meta-data module: ElpiOperations -[1740570538.888908] HB: abbreviation factory-by-classname +[1774980856.728359] HB: exporting operations +[1774980856.729330] HB: export operation zero +[1774980856.731284] HB: export operation add +[1774980856.753952] 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] +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] +[1774980857.239331] HB: export operation addrC +[1774980857.265842] HB: export operation add0r +[1774980857.277047] HB: operations meta-data module: ElpiOperations +[1774980857.288786] HB: abbreviation factory-by-classname (* Module AddComoid. @@ -859,42 +915,36 @@ *) forall (M : AddComoid.type) (x : M), x + x = 0 : Prop -[1740570538.929333] HB: begin module for builders -[1740570538.934114] HB: begin module Super -[1740570538.934499] HB: ended module Super -[1740570538.934893] HB: postulating factories -[1740570538.935140] HB: processing key context-item -[1740570538.935484] HB: processing mixin parameter a -[1740570538.935928] HB: declaring parameters and key as section variables -Here is the list of mixins to declare (the order matters): [] -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_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_1.v", line 55, characters 0-123: -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] -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 +COQC examples/FSCD2020_material/V3.v +inhab + : ?s +where +?T : [ |- Type] +?s : [ |- s1.type ?T] +eq_refl : inhab = 7 + : inhab = 7 +eq_refl : inhab = (7 :: nil)%list + : inhab = (7 :: nil)%list +where +?T : [ |- Type] AbelianGrp.phant_on_ BinNums_Z__canonical__readme_AbelianGrp (Phant BinNums_Z__canonical__readme_AbelianGrp) : AbelianGrp.axioms_ Z : AbelianGrp.axioms_ Z +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] HB: Z is canonically equipped with structures: - AbelianGrp (from "./examples/readme.v", line 32) - AddComoid (from "./examples/readme.v", line 31) -COQC examples/demo5/hierarchy_0.v File "./examples/demo1/hierarchy_2.v", line 57, characters 0-57: Warning: pulling in dependencies: @@ -902,52 +952,14 @@ Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] -COQC examples/FSCD2020_material/V1.v -COQC examples/FSCD2020_material/V2.v -File "./examples/hulk.v", line 143, characters 0-63: -Warning: -pulling in dependencies: [Feather_HasEqDec] - -Please list them or end the declaration with '&' -[HB.implicit-structure-dependency,HB,elpi,default] -File "./examples/demo1/hierarchy_5.v", line 68, characters 2-91: -Warning: HB: no new instance is generated -[HB.no-new-instance,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] -[1740570539.936583] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_AddAG_of_AddComoid -[1740570539.936928] 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 -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/V3.v -COQC examples/Coq2020_material/CoqWS_demo.v -File "./examples/demo5/hierarchy_0.v", line 35, characters 2-91: +COQC examples/FSCD2020_material/V4.v +COQC examples/FSCD2020_talk/V1.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] Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. @@ -959,19 +971,19 @@ : forall s : Monoid.type, s -> s -> s @addNr : forall s : Ring.type, left_inverse 0 opp add -COQC examples/Coq2020_material/CoqWS_abstract.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_talk/V2.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/withHB.v -HB.check: -SemiRing_of_AddComoid.axioms_ -: -forall (A : Type) (m : AddMonoid_of_TYPE.axioms_ A), -AddComoid_of_AddMonoid.axioms_ A m -> Type -: -forall (A : Type) (m : AddMonoid_of_TYPE.axioms_ A), -AddComoid_of_AddMonoid.axioms_ A m -> Type +COQC examples/FSCD2020_talk/V3.v +COQC examples/Coq2020_material/CoqWS_demo.v +[1774980859.013894] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_AddAG_of_AddComoid +[1774980859.019523] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_Ring_of_AddAG Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -983,27 +995,6 @@ : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add -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 -COQC tests/duplicate_structure.v -COQC tests/instance_params_no_type.v -add - : ?s -> ?s -> ?s -where -?s : [ |- CMonoid.type] -addrC - : commutative add -where -?s : [ |- CMonoid.type] -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] Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -1015,6 +1006,20 @@ : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add +COQC examples/Coq2020_material/CoqWS_abstract.v +COQC examples/Coq2020_material/CoqWS_expansion/withHB.v +COQC examples/Coq2020_material/CoqWS_expansion/withoutHB.v +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] +add + : ?s -> ?s -> ?s +where +?s : [ |- CMonoid.type] +addrC + : commutative add +where +?s : [ |- CMonoid.type] File "./examples/Coq2020_material/CoqWS_demo.v", line 73, characters 0-73: Warning: pulling in dependencies: [CoqWS_demo_CMonoid_of_Type] @@ -1025,25 +1030,19 @@ : Prop where ?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) -COQC tests/test_CS_db_filtering.v -addrC - : commutative add -where -?s : [ |- CMonoid.type] -COQC tests/subtype.v -COQC tests/exports.v -COQC tests/log_impargs_record.v -forall x y : ?t, 1 + x = y * x - : Prop -where -?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) -File "./examples/Coq2020_material/CoqWS_abstract.v", line 23, characters 0-71: +File "./examples/hulk.v", line 143, characters 0-63: Warning: -pulling in dependencies: [CoqWS_abstract_CMonoid_of_Type] +pulling in dependencies: [Feather_HasEqDec] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] -COQC tests/compress_coe.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] +forall x y : ?t, 1 + x = y * x + : Prop +where +?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 @@ -1056,92 +1055,45 @@ join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing ?t y : ?t |- Ring.type] (x, y cannot be used) +COQC tests/type_of_exported_ops.v forall x : Z, x * - (1 + x) = 0 + 1 : Prop -Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. - -Arguments Monoid.Pack sort%type_scope class -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 add : A -> A -> A -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/funclass.v -COQC tests/grefclass.v -COQC tests/local_instance.v forall x : Z, x * - (1 + x) = 0 + 1 : Prop -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] -COQC tests/lock.v -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] -list_foo' : forall P A : Type, is_foo.axioms_ P (list A) +HB: A is canonically equipped with structures: + - Equality + Singleton + (from "./examples/hulk.v", line 216) -list_foo' is not universe polymorphic -Arguments list_foo' (P A)%type_scope -list_foo' is transparent -Expands to: Constant HB.tests.instance_params_no_type.list_foo' -nat_foo - : forall P : Type, is_foo.axioms_ P nat -list_foo - : forall P : Type, is_foo.axioms_ P (list P) -foo.type - : Type -> Type -Record type (P : Type) : Type := Pack - { sort : Type; class : foo.axioms_ P sort }. +COQC tests/duplicate_structure.v +File "./examples/FSCD2020_talk/V2.v", line 17, characters 0-66: +Warning: +pulling in dependencies: [V2_is_semigroup] -Arguments foo.type P%type_scope -Arguments foo.Pack (P sort)%type_scope class -Arguments foo.sort P%type_scope record -Arguments foo.class P%type_scope record -Module -foo -:= Struct - Record axioms_ (P A : Type) : Type := Class - { instance_params_no_type_is_foo_mixin : is_foo.axioms_ P A } as record. - Definition instance_params_no_type_is_foo_mixin : - forall P A : Type, axioms_ P A -> is_foo.axioms_ P A. - Record type (P : Type) : Type := Pack - { sort : Type; class : axioms_ P sort }. - Definition sort : forall P : Type, type P -> Type. - Definition class : - forall (P : Type) (record : type P), axioms_ P record. - Definition phant_clone : - forall (P A : Type) (cT : type P) (c : axioms_ P A), - unify Type Type A cT nomsg -> - unify (type P) (type P) cT {| sort := A; class := c |} nomsg -> type P. - Definition pack_ : forall P A : Type, is_foo.axioms_ P A -> type P. - Module Exports - Definition phant_on_ : - forall (P : Type) (A : type P), ssreflect.phant A -> axioms_ P A. - End -Record axioms_ (P A : Type) : Type := Class - { instance_params_no_type_is_foo_mixin : is_foo.axioms_ P A } as record. +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB,elpi,default] +COQC tests/instance_params_no_type.v +COQC tests/test_CS_db_filtering.v +COQC tests/subtype.v +COQC tests/exports.v +addrC + : commutative add +where +?s : [ |- CMonoid.type] +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 +File "./examples/Coq2020_material/CoqWS_abstract.v", line 23, characters 0-71: +Warning: +pulling in dependencies: [CoqWS_abstract_CMonoid_of_Type] -axioms_ has primitive projections with eta conversion. -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 (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 +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB,elpi,default] +COQC tests/compress_coe.v +COQC tests/funclass.v (* Module A. @@ -1190,6 +1142,7 @@ Notation A X1 := ( A.phant_axioms X1). *) +COQC tests/grefclass.v A.p : forall [T : Type] (record : A.axioms_ T) [x : T], A.f record x = x -> True @@ -1198,29 +1151,78 @@ Arguments A.p [T]%type_scope record [x] _ A.p is transparent Expands to: Constant HB.tests.log_impargs_record.A.p -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop -COQC tests/interleave_context.v -COQC tests/not_same_key.v -list_bar - : forall P : b.type, is_bar.axioms_ P (list P) -COQC tests/hb_pack.v -COQC tests/declare.v -[1740570545.298006] HB: start module SubInhab -[1740570545.298507] HB: declare axioms record +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] +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] +list_foo' : forall P A : Type, is_foo.axioms_ P (list A) + +list_foo' is not universe polymorphic +Arguments list_foo' (P A)%type_scope +list_foo' is transparent +Expands to: Constant HB.tests.instance_params_no_type.list_foo' +COQC tests/local_instance.v +nat_foo + : forall P : Type, is_foo.axioms_ P nat +list_foo + : forall P : Type, is_foo.axioms_ P (list P) +[1774980862.487768] HB: start module SubInhab +[1774980862.488250] 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] -[1740570545.298955] HB: typing class field indt «is_inhab.axioms_» -[1740570545.299302] HB: typing class field indt «is_SUB.axioms_» -[1740570545.301353] HB: declare type record -[1740570545.303306] HB: structure: new mixins [] -[1740570545.309893] HB: structure: mixin first class [] -[1740570545.310115] HB: declaring clone abbreviation -[1740570545.313012] HB: declaring pack_ constant -[1740570545.314081] HB: declaring pack_ constant = +foo.type + : Type -> Type +[1774980862.489120] HB: typing class field indt «is_inhab.axioms_» +[1774980862.489446] HB: typing class field indt «is_SUB.axioms_» +Record type (P : Type) : Type := Pack + { sort : Type; class : foo.axioms_ P sort }. + +Arguments foo.type P%type_scope +Arguments foo.Pack (P sort)%type_scope class +Arguments foo.sort P%type_scope record +Arguments foo.class P%type_scope record +Module +foo +:= Struct + Record axioms_ (P A : Type) : Type := Class + { instance_params_no_type_is_foo_mixin : is_foo.axioms_ P A } as record. + Definition instance_params_no_type_is_foo_mixin : + forall P A : Type, axioms_ P A -> is_foo.axioms_ P A. + Record type (P : Type) : Type := Pack + { sort : Type; class : axioms_ P sort }. + Definition sort : forall P : Type, type P -> Type. + Definition class : + forall (P : Type) (record : type P), axioms_ P record. + Definition phant_clone : + forall (P A : Type) (cT : type P) (c : axioms_ P A), + unify Type Type A cT nomsg -> + unify (type P) (type P) cT {| sort := A; class := c |} nomsg -> type P. + Definition pack_ : forall P A : Type, is_foo.axioms_ P A -> type P. + Module Exports + Definition phant_on_ : + forall (P : Type) (A : type P), ssreflect.phant A -> axioms_ P A. + End +[1774980862.491451] HB: declare type record +Record axioms_ (P A : Type) : Type := Class + { instance_params_no_type_is_foo_mixin : is_foo.axioms_ P A } as record. + +axioms_ has primitive projections with eta conversion. +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 +[1774980862.493267] HB: structure: new mixins [] +[1774980862.493682] HB: structure: mixin first class [] +[1774980862.493772] HB: declaring clone abbreviation +[1774980862.496810] HB: declaring pack_ constant +[1774980862.497966] 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 \ @@ -1229,66 +1231,80 @@ app [global (indc «Pack»), c0, c1, c2, app [global (indc «Class»), c0, c1, c2, c3, c4]] -[1740570545.315145] HB: start module Exports -[1740570545.315557] HB: making coercion from type to target -[1740570545.315712] HB: declare sort coercion -[1740570545.315910] HB: exporting unification hints -[1740570545.316654] HB: declare coercion subtype_SubInhab__to__subtype_SUB -[1740570545.322659] HB: declare coercion hint +[1774980862.498979] HB: start module Exports +[1774980862.499365] HB: making coercion from type to target +[1774980862.499522] HB: declare sort coercion +[1774980862.499681] HB: exporting unification hints +[1774980862.500344] HB: declare coercion subtype_SubInhab__to__subtype_SUB +[1774980862.501016] HB: declare coercion hint subtype_SubInhab_class__to__subtype_SUB_class -[1740570545.324736] HB: declare unification hint +forall (G : AbelianGrp.type) (x : G), x - x = 0 + : Prop +[1774980862.502812] HB: declare unification hint subtype_SubInhab__to__subtype_SUB -[1740570545.327046] HB: declare coercion subtype_SubInhab__to__subtype_Inhab -[1740570545.334605] HB: declare coercion hint +forall (S : SemiRing.type) (x : S), x * 1 + 0 = x + : Prop +[1774980862.504991] HB: declare coercion subtype_SubInhab__to__subtype_Inhab +[1774980862.506837] HB: declare coercion hint subtype_SubInhab_class__to__subtype_Inhab_class -[1740570545.336598] HB: declare unification hint +[1774980862.508825] HB: declare unification hint subtype_SubInhab__to__subtype_Inhab -[1740570545.339214] HB: declare unification hint +[1774980862.511042] HB: declare unification hint join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB -[1740570545.341391] HB: exporting coercions from class to mixins -[1740570545.346118] HB: export class to mixin coercion for mixin +[1774980862.515046] HB: exporting coercions from class to mixins +[1774980862.515445] HB: export class to mixin coercion for mixin subtype_is_inhab -[1740570545.347042] HB: export class to mixin coercion for mixin +[1774980862.516149] HB: export class to mixin coercion for mixin subtype_is_SUB -[1740570545.347805] HB: accumulating various props -[1740570545.348695] HB: stop module Exports -[1740570545.350771] HB: declaring on_ abbreviation -[1740570545.360264] HB: declaring `copy` abbreviation -[1740570545.361312] HB: declaring on abbreviation -[1740570545.362673] HB: end modules; export +[1774980862.516660] HB: accumulating various props +[1774980862.517376] HB: stop module Exports +[1774980862.519177] HB: declaring on_ abbreviation +[1774980862.521863] HB: declaring `copy` abbreviation +[1774980862.523791] HB: declaring on abbreviation +forall (R : Ring.type) (x y : R), x * - (1 * y) = - x * y + : Prop +[1774980862.525084] HB: end modules; export «HB.tests.subtype.SubInhab.Exports» -[1740570545.364671] HB: exporting operations -[1740570545.370098] HB: operations meta-data module: ElpiOperations -[1740570545.371011] HB: abbreviation factory-by-classname -p : pred nat - : pred nat +[1774980862.526863] HB: exporting operations +[1774980862.527130] HB: operations meta-data module: ElpiOperations +[1774980862.527685] HB: abbreviation factory-by-classname +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 +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop +COQC tests/lock.v +list_bar + : forall P : b.type, is_bar.axioms_ P (list P) +COQC tests/interleave_context.v +COQC tests/not_same_key.v +COQC tests/hb_pack.v +COQC tests/declare.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/short.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 -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/instance_before_structure.v -[1740570545.699904] HB: exporting under the module path [] -[1740570545.706050] HB: exporting modules +[1774980863.416773] HB: exporting under the module path [] +[1774980863.417038] HB: exporting modules [Ring_of_TYPE.Exports, Ring.Exports, RingElpiOperations, RingExports, Dummy.Exports, URing.Exports, URingElpiOperations, dummy.Exports, Builders_1.Builders_Export_5] -[1740570545.707700] HB: exporting CS instances +[1774980863.418426] HB: exporting CS instances [«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] -[1740570545.708378] HB: exporting Abbreviations [addr0, addrNK] -[1740570545.708698] HB: exporting Clauses X0 +[1774980863.418917] HB: exporting Abbreviations [addr0, addrNK] +[1774980863.419137] HB: exporting Clauses X0 forall (R : Enclosing.Ring.type) (x : R), x = x : Prop 0%G @@ -1297,12 +1313,30 @@ ?s : [ |- Enclosing.Ring.type] Enclosing.zero : Z : Z -COQC tests/primitive_records.v +COQC tests/short.v +COQC tests/instance_before_structure.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 +HB.check: forall w : wp.type nat Init.Nat.mul, w = w : Prop +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 +COQC tests/primitive_records.v +@addNr + : forall s : AbelianGroup.type, left_inverse 0 opp add +@addrC + : forall s : AbelianGroup.type, commutative add +p : pred nat + : pred nat +COQC tests/non_forgetful_inheritance.v +COQC tests/fix_loop.v Notation big := big.body Expands to: Notation HB.tests.lock.X.big @@ -1311,33 +1345,42 @@ 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/non_forgetful_inheritance.v -COQC tests/fix_loop.v -HB.check: forall w : wp.type nat Init.Nat.mul, w = w : Prop -[1740570546.005785] HB: start module and section hasA -[1740570546.006302] HB: converting arguments +COQC tests/test_synthesis_params.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/hnf.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] +[1774980864.602427] HB: start module and section hasA +[1774980864.607684] 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 -COQC tests/test_synthesis_params.v -[1740570546.006606] HB: processing key parameter -[1740570546.007027] HB: converting factories +[1774980864.607988] HB: processing key parameter +[1774980864.608438] HB: converting factories w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins -[1740570546.007208] HB: declaring context +[1774980864.608682] HB: declaring context w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] -[1740570546.007389] HB: declaring parameters and key as section variables +[1774980864.608903] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1740570546.007892] HB: declare mixin or factory -[1740570546.008009] HB: declare record axioms_ -[1740570546.009495] HB: declare notation Build -[1740570546.010918] HB: declare notation axioms -[1740570546.012964] HB: start module Exports -[1740570546.014581] HB: end modules and sections; export +[1774980864.615653] HB: declare mixin or factory +[1774980864.615882] HB: declare record axioms_ +[1774980864.617372] HB: declare notation Build +[1774980864.618629] HB: declare notation axioms +[1774980864.621059] HB: start module Exports +[1774980864.628919] HB: end modules and sections; export «HB.tests.hb_pack.hasA.Exports» hasA.type not a defined object. -COQC tests/hnf.v hasB.type not a defined object. +COQC tests/fun_instance.v Datatypes_prod__canonical__compress_coe_D = fun D D' : D.type => {| @@ -1359,17 +1402,9 @@ : D.type -> D.type -> D.type Arguments Datatypes_prod__canonical__compress_coe_D D D' -COQC tests/fun_instance.v hasAB.type not a defined object. hasA'.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] -aType - : Type +COQC tests/issue284.v forall T : AB.type, unkeyed {| @@ -1387,9 +1422,9 @@ : A.type A : A.type : A.type -hasB.type not a defined object. AB1 : hasB.phant_axioms A -> AB.type : hasB.phant_axioms A -> AB.type +COQC tests/issue287.v Bm : hasB.phant_axioms A : hasB.phant_axioms A AB2 : AB.type @@ -1398,8 +1433,6 @@ : T * T AB3 : AB.type : AB.type -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) @@ -1407,32 +1440,37 @@ 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) - -COQC tests/issue284.v +aType + : Type HB: nat is canonically equipped with structures: - s1 (from "./tests/instance_before_structure.v", line 11) Query assignments: Ind = «hasA.axioms_» -hasAB.type not a defined object. +hasB.type not a defined object. +X : Foo.type A P + : Foo.type A P Query assignments: -hasA'.type not a defined object. Ind = «A.axioms_» +COQC tests/two_hier.v Query assignments: Ind = «A.type» -COQC tests/issue287.v -COQC tests/two_hier.v +HB: nat is canonically equipped with structures: + - s1 + (from "./tests/instance_before_structure.v", line 11) + COQC tests/instance_merge_with_param.v -T : Fun.type nat - : Fun.type nat HB: nat is canonically equipped with structures: - s1 (from "./tests/instance_before_structure.v", line 11) +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 HB: nat is canonically equipped with structures: - s3 s2 @@ -1446,10 +1484,28 @@ : nat default3 : nat +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/instance_merge_with_distinct_param.v +COQC tests/instance_merge.v +hasAB.type not a defined object. +COQC tests/unit/enrich_type.v +hasA'.type not a defined object. +COQC tests/unit/mixin_src_has_mixin_instance.v +COQC tests/unit/mk_src_map.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 +erefl : ?t = ?t + : ?t = ?t +where +?t : [ |- Sq.type] Debug: elpi lets escape exception: non forgetful inheritance detected. You have two solutions: @@ -1465,31 +1521,34 @@ 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] -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 -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/instance_merge.v -COQC tests/unit/enrich_type.v -erefl : ?t = ?t - : ?t = ?t -where -?t : [ |- Sq.type] -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) + +nat : s3.type + : s3.type +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) +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/bug_447.v Query assignments: X = global (indt «nat») Query assignments: @@ -1548,11 +1607,6 @@ WEAK CONSTRAINTS: -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: A_ = X0 B_ = X1 @@ -1560,7 +1614,6 @@ Inj_ = «Inj» R_ = X3 S_ = X4 - X = app [global (const «Inj»), X0, X1, X3, X4, X2] X1_ = X0 X2_ = X1 @@ -1585,15 +1638,9 @@ WEAK CONSTRAINTS: -COQC tests/bug_447.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) - +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] Query assignments: X = app [global (indt «list»), X0] X1_ = X1 @@ -1620,17 +1667,27 @@ Query assignments: Z = global (indt «nat») -File "./tests/unit/mk_src_map.v", line 6, characters 0-76: +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) +COQC tests/unimported_relevant_class.v Query assignments: X = app [global (const «Inj»), X0, X1, X2, X3, X4] X2_ = X0 X3_ = X1 X4_ = X5 X5_ = X6 +Query assignments: X6_ = X7 X7_ = X8 + 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] X8_ = X9 Y = app [global (const «Inj»), X0, X1] Z = fun `x` X5 c0 \ @@ -1676,30 +1733,6 @@ WEAK CONSTRAINTS: -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] -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] -COQC tests/unimported_relevant_class.v -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: - M1_ = const «m1.phant_axioms» -Query assignments: - 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») - 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 \ @@ -1716,11 +1749,7 @@ : s3.type fun t : s3.type => list t : s3.type : s3.type -> s3.type -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_1_0.v -COQC examples/demo1/test_2_0.v Query assignments: H_ = [] struct_foo1__to__struct_foo = @@ -1729,50 +1758,56 @@ Arguments struct_foo1__to__struct_foo s struct_foo1__to__struct_foo is a reversible coercion -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 examples/demo1/test_3_0.v -COQC examples/demo1/test_3_3.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] +list unit : Pointed.type + : Pointed.type +COQC examples/demo1/test_2_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 : s3'.type Datatypes_nat__canonical__two_hier_s3 +COQC examples/demo1/test_3_0.v Datatypes_list__canonical__two_hier_s3' : 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_3.v +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] +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 examples/demo1/test_4_0.v -list unit : Pointed.type - : Pointed.type COQC examples/demo1/test_4_3.v -COQC examples/demo1/test_5_0.v -[1740570550.528969] HB: postulating X -[1740570550.536451] HB: declare canonical mixin instance +[1774980869.597288] HB: postulating X +[1774980869.604650] HB: declare canonical mixin instance «HB_unnamed_factory_5» -[1740570550.537332] HB: we can build a bug_435_B2 on unit -[1740570550.537754] HB: declare canonical structure instance +[1774980869.605718] HB: we can build a bug_435_B2 on unit +[1774980869.607622] HB: declare canonical structure instance Datatypes_unit__canonical__bug_435_B2 -[1740570550.538026] HB: structure instance for +[1774980869.608583] 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 |} |} -[1740570550.543071] HB: structure instance +[1774980869.610215] HB: structure instance Datatypes_unit__canonical__bug_435_B2 declared -[1740570550.543949] HB: we can build a should_work_but_fails_B on unit -[1740570550.544395] HB: declare canonical structure instance +[1774980869.616661] HB: we can build a should_work_but_fails_B on unit +[1774980869.617057] HB: declare canonical structure instance Datatypes_unit__canonical__should_work_but_fails_B -[1740570550.544664] HB: structure instance for +[1774980869.617301] HB: structure instance for Datatypes_unit__canonical__should_work_but_fails_B is {| B.sort := unit; @@ -1782,41 +1817,42 @@ B.bug_435_A2_mixin := HB_unnamed_factory_5 |} |} -[1740570550.545243] HB: closing instance section -COQC examples/demo1/test_5_3.v +[1774980869.617837] HB: closing instance section unit : B.type ?t : B.type ?t where ?t : [ |- S.type] -COQC examples/demo2/stage10.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: +[1774980872.278229] HB: exporting under the module path [] +[1774980872.283517] HB: exporting modules [] +[1774980872.283781] HB: exporting CS instances [] +[1774980872.283912] HB: exporting Abbreviations [] +[1774980872.284023] 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/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] -[1740570552.438369] HB: exporting under the module path [] -[1740570552.438643] HB: exporting modules [] -[1740570552.438775] HB: exporting CS instances [] -[1740570552.438893] HB: exporting Abbreviations [] -[1740570552.438998] HB: exporting Clauses X0 -File "./examples/demo2/stage10.v", line 112, characters 2-115: +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/stage11.v", line 115, characters 2-100: +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 @@ -1849,30 +1885,30 @@ disable this warning. [deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] HB: skipping section opening -[1740570554.197486] HB: declare mixin instance +[1774980876.480808] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology -[1740570554.198995] HB: declare canonical mixin instance +[1774980876.482156] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology» -[1740570554.200486] HB: declare mixin instance +[1774980876.483698] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform -[1740570554.204389] HB: declare canonical mixin instance +[1774980876.493670] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform» -[1740570554.205872] HB: declare mixin instance +[1774980876.495113] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology -[1740570554.208748] HB: declare canonical mixin instance +[1774980876.501888] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology» -[1740570554.210189] HB: declare mixin instance +[1774980876.504395] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform -[1740570554.212313] HB: declare canonical mixin instance +[1774980876.507750] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform» -[1740570554.214128] HB: we can build a Stage11_UniformSpace_wo_Topology on +[1774980876.509395] HB: we can build a Stage11_UniformSpace_wo_Topology on Qc -[1740570554.214576] HB: declare canonical structure instance +[1774980876.509787] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology -[1740570554.214841] HB: Giving name HB_unnamed_mixin_46 to mixin instance +[1774980876.510014] 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 -[1740570554.215987] HB: structure instance for +[1774980876.511156] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology is {| UniformSpace_wo_Topology.sort := Qc; @@ -1882,12 +1918,12 @@ HB_unnamed_mixin_46 |} |} -[1740570554.217489] HB: structure instance +[1774980876.512564] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology declared -[1740570554.218574] HB: we can build a Stage11_UniformSpace on Qc -[1740570554.218954] HB: declare canonical structure instance +[1774980876.513519] HB: we can build a Stage11_UniformSpace on Qc +[1774980876.513862] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace -[1740570554.219177] HB: structure instance for +[1774980876.514065] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace is {| UniformSpace.sort := Qc; @@ -1897,15 +1933,15 @@ UniformSpace.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_46 |} |} -[1740570554.220607] HB: structure instance +[1774980876.515447] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace declared -[1740570554.221760] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc -[1740570554.222198] HB: declare canonical structure instance +[1774980876.516515] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc +[1774980876.516871] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform -[1740570554.222507] HB: Giving name HB_unnamed_mixin_47 to mixin instance +[1774980876.517148] 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 -[1740570554.223875] HB: structure instance for +[1774980876.518387] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform is {| TAddAG_wo_Uniform.sort := Qc; @@ -1917,12 +1953,12 @@ HB_unnamed_mixin_47 |} |} -[1740570554.225396] HB: structure instance +[1774980876.519904] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform declared -[1740570554.227020] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc -[1740570554.227400] HB: declare canonical structure instance +[1774980876.521370] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc +[1774980876.521734] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined -[1740570554.227686] HB: structure instance for +[1774980876.521985] HB: structure instance for Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined is {| Uniform_TAddAG_unjoined.sort := Qc; @@ -1937,18 +1973,18 @@ HB_unnamed_mixin_46 |} |} -[1740570554.229230] HB: structure instance +[1774980876.523487] HB: structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined declared -[1740570554.231764] HB: we can build a Stage11_TAddAG on Qc -[1740570554.232153] HB: declare canonical structure instance +[1774980876.525838] HB: we can build a Stage11_TAddAG on Qc +[1774980876.526233] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG -[1740570554.232492] HB: Giving name HB_unnamed_mixin_48 to mixin instance +[1774980876.526547] 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 -[1740570554.234173] HB: Giving name HB_unnamed_mixin_49 to mixin instance +[1774980876.528143] 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 -[1740570554.235824] HB: structure instance for +[1774980876.529692] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG is {| TAddAG.sort := Qc; @@ -1962,13 +1998,13 @@ TAddAG.Stage11_Join_TAddAG_Uniform_mixin := HB_unnamed_mixin_49 |} |} -[1740570554.237713] HB: structure instance +[1774980876.531606] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG declared entourage : set (set (Qc * Qc)) : set (set (Qc * Qc)) -Finished transaction in 16.389 secs (9.289u,0.569s) (successful) +Finished transaction in 20.945 secs (9.174u,0.557s) (successful) Finished transaction in 0. secs (0.u,0.s) (successful) -Finished transaction in 11.28 secs (9.026u,0.516s) (successful) +Finished transaction in 18.22 secs (9.u,0.559s) (successful) Module Type new_concept_Locked = Sig @@ -2078,12 +2114,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/3438715/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/3438715/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/2843829 and its subdirectories -I: Current time: Tue Feb 25 23:49:52 -12 2025 -I: pbuilder-time-stamp: 1740570592 +I: removing directory /srv/workspace/pbuilder/3438715 and its subdirectories +I: Current time: Wed Apr 1 08:15:30 +14 2026 +I: pbuilder-time-stamp: 1774980930