Diff of the two buildlogs: -- --- b1/build.log 2024-11-22 07:00:37.051011553 +0000 +++ b2/build.log 2024-11-22 07:05:56.300712057 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Thu Dec 25 01:22:09 -12 2025 -I: pbuilder-time-stamp: 1766668929 +I: Current time: Fri Nov 22 21:00:40 +14 2024 +I: pbuilder-time-stamp: 1732258840 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/unstable-reproducible-base.tgz] I: copying local configuration @@ -26,52 +26,84 @@ dpkg-source: info: unpacking coq-hierarchy-builder_1.7.0-2.debian.tar.xz I: Not using root during the build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/1963874/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/3051591/tmp/hooks/D01_modify_environment starting +debug: Running on codethink02-arm64. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +'/bin/sh' -> '/bin/bash' +lrwxrwxrwx 1 root root 9 Nov 22 07:00 /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/3051591/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/3051591/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]="32" [3]="1" [4]="release" [5]="aarch64-unknown-linux-gnu") + BASH_VERSION='5.2.32(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=arm64 + DEBIAN_FRONTEND=noninteractive DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=12 ' - DISTRIBUTION='unstable' - HOME='/root' - HOST_ARCH='arm64' + DIRSTACK=() + DISTRIBUTION=unstable + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=aarch64 + HOST_ARCH=arm64 IFS=' ' - INVOCATION_ID='4997372934c74efab3592d971c6adb0a' - 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='1963874' - PS1='# ' - PS2='> ' + INVOCATION_ID=1ca35fb13a9c448584ec04c5b1ce2e7c + 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=3051591 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.6DVA80Jb/pbuilderrc_FbC3 --distribution unstable --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/unstable-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.6DVA80Jb/b1 --logfile b1/build.log coq-hierarchy-builder_1.7.0-2.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.6DVA80Jb/pbuilderrc_77wi --distribution unstable --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/unstable-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.6DVA80Jb/b2 --logfile b2/build.log coq-hierarchy-builder_1.7.0-2.dsc' + SUDO_GID=109 + SUDO_UID=104 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://192.168.101.4:3128 I: uname -a - Linux codethink01-arm64 6.1.0-27-cloud-arm64 #1 SMP Debian 6.1.115-1 (2024-11-01) aarch64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-27-cloud-arm64 #1 SMP Debian 6.1.115-1 (2024-11-01) aarch64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Aug 4 2024 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/1963874/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Aug 4 21:30 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/3051591/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -207,7 +239,7 @@ Get: 86 http://deb.debian.org/debian unstable/main arm64 libelpi-ocaml-dev arm64 1.19.6-1 [14.2 MB] Get: 87 http://deb.debian.org/debian unstable/main arm64 libcoq-elpi arm64 2.2.3-1+b1 [7970 kB] Get: 88 http://deb.debian.org/debian unstable/main arm64 wdiff arm64 1.2.2-6+b1 [119 kB] -Fetched 375 MB in 2s (198 MB/s) +Fetched 375 MB in 8s (48.0 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libpython3.12-minimal:arm64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 20084 files and directories currently installed.) @@ -509,8 +541,8 @@ Setting up tzdata (2024b-3) ... Current default time zone: 'Etc/UTC' -Local time is now: Thu Dec 25 13:22:40 UTC 2025. -Universal Time is now: Thu Dec 25 13:22:40 UTC 2025. +Local time is now: Fri Nov 22 07:02:18 UTC 2024. +Universal Time is now: Fri Nov 22 07:02:18 UTC 2024. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up autotools-dev (20220109.1) ... @@ -588,7 +620,11 @@ Building tag database... -> Finished parsing the build-deps I: Building the package -I: Running cd /build/reproducible-path/coq-hierarchy-builder-1.7.0/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../coq-hierarchy-builder_1.7.0-2_source.changes +I: user script /srv/workspace/pbuilder/3051591/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for unstable +I: user script /srv/workspace/pbuilder/3051591/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/coq-hierarchy-builder-1.7.0/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-genchanges -S > ../coq-hierarchy-builder_1.7.0-2_source.changes dpkg-buildpackage: info: source package coq-hierarchy-builder dpkg-buildpackage: info: source version 1.7.0-2 dpkg-buildpackage: info: source distribution unstable @@ -638,8 +674,8 @@ make test-suite make[2]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.7.0' make -f Makefile.coq -/usr/bin/coq_makefile -f _CoqProject.test-suite -o Makefile.test-suite.coq make[3]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.7.0' +/usr/bin/coq_makefile -f _CoqProject.test-suite -o Makefile.test-suite.coq Warning: . and tests overlap (used in -R or -Q) Warning: . and examples overlap (used in -R or -Q) @@ -678,8 +714,9 @@ 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] -[1766668979.788254] HB: start module and section AddComoid_of_Type -[1766668979.788698] HB: converting arguments +COQC examples/demo4/hierarchy_0.v +[1732259015.475157] HB: start module and section AddComoid_of_Type +[1732259015.475533] HB: converting arguments indt-decl (parameter A explicit X0 c0 \ record AddComoid_of_Type (sort (typ X1)) Build_AddComoid_of_Type @@ -705,19 +742,19 @@ app [global (indt «eq»), X10 c0 c1 c2 c3 c4 c5, app [c2, c1, c5], c5]) c5 \ end-record)) to factories -[1766668979.789156] HB: processing key parameter -[1766668979.789554] HB: converting factories +[1732259015.475997] HB: processing key parameter +[1732259015.476421] HB: converting factories w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] to mixins -[1766668979.789691] HB: declaring context +[1732259015.483027] HB: declaring context w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] -[1766668979.789817] HB: declaring parameters and key as section variables +[1732259015.483371] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1766668979.790370] HB: declare mixin or factory -[1766668979.790460] HB: declare record axioms_ -[1766668979.794766] HB: declare notation Build -[1766668979.798309] HB: declare notation axioms -[1766668979.801861] HB: start module Exports -[1766668979.804231] HB: end modules and sections; export +[1732259015.487690] HB: declare mixin or factory +[1732259015.487837] HB: declare record axioms_ +[1732259015.508064] HB: declare notation Build +[1732259015.521998] HB: declare notation axioms +[1732259015.542118] HB: start module Exports +[1732259015.564271] HB: end modules and sections; export «HB.examples.readme.AddComoid_of_Type.Exports» (* @@ -774,55 +811,61 @@ Notation AddComoid_of_Type X1 := ( AddComoid_of_Type.phant_axioms X1). *) -[1766668979.829386] HB: start module AddComoid -[1766668979.829745] HB: declare axioms record +COQC examples/demo5/hierarchy_0.v +[1732259015.714217] HB: start module AddComoid +[1732259015.739241] HB: declare axioms record w-params.nil A (sort (typ «HB.examples.readme.25»)) c0 \ [triple (indt «AddComoid_of_Type.axioms_») [] c0] -[1766668979.829954] HB: typing class field +[1732259015.743171] HB: typing class field indt «AddComoid_of_Type.axioms_» -[1766668979.831394] HB: declare type record -[1766668979.832929] HB: structure: new mixins +[1732259015.748363] HB: declare type record +[1732259015.749807] HB: structure: new mixins [indt «AddComoid_of_Type.axioms_»] -[1766668979.833114] HB: structure: mixin first class +[1732259015.762713] HB: structure: mixin first class [mixin-first-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»)] -[1766668979.833194] HB: declaring clone abbreviation -[1766668979.836349] HB: declaring pack_ constant -[1766668979.836951] HB: declaring pack_ constant = +[1732259015.763007] HB: declaring clone abbreviation +[1732259015.765923] HB: declaring pack_ constant +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] +[1732259015.783435] 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]] -[1766668979.838083] HB: start module Exports -[1766668979.838482] HB: making coercion from type to target -[1766668979.838575] HB: declare sort coercion -[1766668979.838905] HB: exporting unification hints -[1766668979.839071] HB: exporting coercions from class to mixins -[1766668979.839263] HB: export class to mixin coercion for mixin +[1732259015.787901] HB: start module Exports +[1732259015.795346] HB: making coercion from type to target +[1732259015.796356] HB: declare sort coercion +[1732259015.796826] HB: exporting unification hints +[1732259015.797041] HB: exporting coercions from class to mixins +[1732259015.797381] HB: export class to mixin coercion for mixin readme_AddComoid_of_Type -[1766668979.839559] HB: accumulating various props -[1766668979.840368] HB: stop module Exports -[1766668979.841037] HB: declaring on_ abbreviation -[1766668979.843262] HB: declaring `copy` abbreviation -[1766668979.844179] HB: declaring on abbreviation -[1766668979.845695] HB: end modules; export +[1732259015.804423] HB: accumulating various props +[1732259015.811785] HB: stop module Exports +[1732259015.813034] HB: declaring on_ abbreviation +[1732259015.815156] HB: declaring `copy` abbreviation +[1732259015.819786] HB: declaring on abbreviation +[1732259015.828279] HB: end modules; export «HB.examples.readme.AddComoid.Exports» -[1766668979.846243] HB: exporting operations -[1766668979.847061] HB: export operation zero -[1766668979.849143] HB: export operation add -[1766668979.851544] HB: export operation addrA -[1766668979.854461] HB: export operation addrC -[1766668979.857521] HB: export operation add0r -COQC examples/demo4/hierarchy_0.v -[1766668979.896633] HB: begin module for builders -[1766668979.897065] HB: begin module Super -[1766668979.897193] HB: ended module Super -[1766668979.897469] HB: postulating factories -[1766668979.897624] HB: processing key context-item -[1766668979.898055] HB: processing mixin parameter a -[1766668979.898444] HB: declaring parameters and key as section variables +[1732259015.839593] HB: exporting operations +[1732259015.843785] HB: export operation zero +[1732259015.845779] HB: export operation add +[1732259015.853154] HB: export operation addrA +[1732259015.869492] HB: export operation addrC +[1732259015.883861] HB: export operation add0r +[1732259016.077773] HB: begin module for builders +[1732259016.091247] HB: begin module Super +[1732259016.091598] HB: ended module Super +[1732259016.092055] HB: postulating factories +[1732259016.092266] HB: processing key context-item +[1732259016.092582] HB: processing mixin parameter a +[1732259016.092986] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -COQC examples/demo5/hierarchy_0.v -[1766668979.909974] HB: operations meta-data module: ElpiOperations -[1766668979.911990] HB: abbreviation factory-by-classname +[1732259016.180185] HB: operations meta-data module: ElpiOperations +[1732259016.181852] HB: abbreviation factory-by-classname (* Module AddComoid. @@ -919,13 +962,7 @@ *) forall (M : AddComoid.type) (x : M), x + x = 0 : Prop -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/V1.v AbelianGrp.phant_on_ BinNums_Z__canonical__readme_AbelianGrp (Phant BinNums_Z__canonical__readme_AbelianGrp) : @@ -937,43 +974,42 @@ - AddComoid (from "./examples/readme.v", line 31) -COQC examples/FSCD2020_material/V1.v -COQC examples/FSCD2020_material/V2.v -COQC examples/FSCD2020_material/V3.v -[1766668980.304277] HB: declare builder from hierarchy_2_Ring_of_AddComoid +[1732259017.424416] HB: declare builder from hierarchy_2_Ring_of_AddComoid to hierarchy_2_AddAG_of_AddComoid -[1766668980.304485] HB: declare builder from hierarchy_2_Ring_of_AddComoid +[1732259017.424558] HB: declare builder from hierarchy_2_Ring_of_AddComoid to hierarchy_2_Ring_of_AddAG -COQC examples/FSCD2020_material/V4.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] -COQC examples/FSCD2020_talk/V1.v -HB: A is canonically equipped with structures: - - Equality - Singleton - (from "./examples/hulk.v", line 216) - +COQC examples/FSCD2020_material/V3.v +COQC examples/FSCD2020_material/V4.v inhab : ?s where ?T : [ |- Type] ?s : [ |- s1.type ?T] -COQC examples/FSCD2020_talk/V2.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 +HB: A is canonically equipped with structures: + - Equality + Singleton + (from "./examples/hulk.v", line 216) + 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/V2.v COQC examples/FSCD2020_talk/V3.v COQC examples/Coq2020_material/CoqWS_demo.v COQC examples/Coq2020_material/CoqWS_abstract.v @@ -987,15 +1023,6 @@ @addNr : forall s : Ring.type, left_inverse 0 opp add 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/Coq2020_material/CoqWS_expansion/withoutHB.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -1007,8 +1034,7 @@ : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add -COQC tests/type_of_exported_ops.v -COQC tests/duplicate_structure.v +COQC examples/Coq2020_material/CoqWS_expansion/withoutHB.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -1016,23 +1042,14 @@ 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 -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/instance_params_no_type.v -COQC tests/test_CS_db_filtering.v -COQC tests/subtype.v add : ?s -> ?s -> ?s where ?s : [ |- CMonoid.type] +@addNr + : forall s : AbelianGroup.type, left_inverse 0 opp add +@addrC + : forall s : AbelianGroup.type, commutative add addrC : commutative add where @@ -1043,11 +1060,9 @@ Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] -forall x y : ?t, x - (y + 0) = x - : Prop -where -?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) -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] Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -1055,15 +1070,31 @@ Arguments Monoid.class record @add : forall s : Monoid.type, s -> s -> s +COQC tests/type_of_exported_ops.v @addNr : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add +forall x y : ?t, x - (y + 0) = x + : Prop +where +?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) +COQC tests/duplicate_structure.v +COQC tests/instance_params_no_type.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 tests/test_CS_db_filtering.v forall x y : ?t, 1 + x = y * x : Prop where ?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) -COQC tests/log_impargs_record.v +COQC tests/subtype.v forall (R : Ring.type) (x y : R), 1 * x = y - x : Prop forall @@ -1078,42 +1109,47 @@ y : ?t |- Ring.type] (x, y cannot be used) forall x : Z, x * - (1 + x) = 0 + 1 : Prop +COQC tests/exports.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] +add + : A -> A -> A +COQC tests/log_impargs_record.v +COQC tests/compress_coe.v +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop +COQC tests/funclass.v addrC : commutative add where ?s : [ |- CMonoid.type] -COQC tests/compress_coe.v -add - : A -> A -> A 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] -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 forall (G : AbelianGrp.type) (x : G), x - x = 0 : Prop forall (S : SemiRing.type) (x : S), x * 1 + 0 = x : Prop forall (R : Ring.type) (x y : R), x * - (1 * y) = - x * y : Prop -COQC tests/grefclass.v forall x : Z, x * - (1 + x) = 0 + 1 : Prop -COQC tests/local_instance.v -COQC tests/lock.v 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' -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop +COQC tests/local_instance.v +COQC tests/lock.v nat_foo : forall P : Type, is_foo.axioms_ P nat list_foo @@ -1156,63 +1192,6 @@ 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 -list_bar - : forall P : b.type, is_bar.axioms_ P (list P) -COQC tests/not_same_key.v -[1766668983.212386] HB: start module SubInhab -[1766668983.212670] 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] -[1766668983.212930] HB: typing class field indt «is_inhab.axioms_» -[1766668983.213202] HB: typing class field indt «is_SUB.axioms_» -[1766668983.215207] HB: declare type record -[1766668983.223967] HB: structure: new mixins [] -[1766668983.224133] HB: structure: mixin first class [] -[1766668983.224186] HB: declaring clone abbreviation -[1766668983.227137] HB: declaring pack_ constant -[1766668983.228158] 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]] -[1766668983.234928] HB: start module Exports -[1766668983.235280] HB: making coercion from type to target -[1766668983.235404] HB: declare sort coercion -[1766668983.235572] HB: exporting unification hints -[1766668983.236222] HB: declare coercion subtype_SubInhab__to__subtype_SUB -[1766668983.237188] HB: declare coercion hint -subtype_SubInhab_class__to__subtype_SUB_class -[1766668983.239107] HB: declare unification hint -subtype_SubInhab__to__subtype_SUB -[1766668983.241249] HB: declare coercion subtype_SubInhab__to__subtype_Inhab -[1766668983.241977] HB: declare coercion hint -subtype_SubInhab_class__to__subtype_Inhab_class -[1766668983.243898] HB: declare unification hint -subtype_SubInhab__to__subtype_Inhab -[1766668983.246421] HB: declare unification hint -join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB -[1766668983.248586] HB: exporting coercions from class to mixins -[1766668983.248929] HB: export class to mixin coercion for mixin -subtype_is_inhab -[1766668983.249799] HB: export class to mixin coercion for mixin -subtype_is_SUB -[1766668983.250440] HB: accumulating various props -[1766668983.251628] HB: stop module Exports -[1766668983.253581] HB: declaring on_ abbreviation -[1766668983.256266] HB: declaring `copy` abbreviation -[1766668983.257154] HB: declaring on abbreviation -[1766668983.258352] HB: end modules; export -«HB.tests.subtype.SubInhab.Exports» -[1766668983.260323] HB: exporting operations -[1766668983.260780] HB: operations meta-data module: ElpiOperations -[1766668983.261459] HB: abbreviation factory-by-classname (* Module A. @@ -1261,7 +1240,6 @@ Notation A X1 := ( A.phant_axioms X1). *) -COQC tests/hb_pack.v A.p : forall [T : Type] (record : A.axioms_ T) [x : T], A.f record x = x -> True @@ -1270,27 +1248,18 @@ Arguments A.p [T]%type_scope record [x] _ A.p is transparent Expands to: Constant HB.tests.log_impargs_record.A.p -COQC tests/declare.v -COQC tests/short.v -p : pred nat - : pred nat -[1766668983.680404] HB: exporting under the module path [] -[1766668983.680876] HB: exporting modules +COQC tests/not_same_key.v +COQC tests/hb_pack.v +list_bar + : forall P : b.type, is_bar.axioms_ P (list P) +[1732259030.898152] HB: exporting under the module path [] +[1732259030.901138] HB: exporting modules [Ring_of_TYPE.Exports, Ring.Exports, RingElpiOperations, RingExports, Dummy.Exports, URing.Exports, URingElpiOperations, dummy.Exports, Builders_1.Builders_Export_5] -Notation big := big.body -Expands to: Notation HB.tests.lock.X.big - -big.body : forall R I : Type, R -> list I -> (I -> bigbody R I) -> R - -big.body is not universe polymorphic -Arguments big.body (R I)%type_scope _ _%list_scope _%function_scope -Expands to: Constant HB.tests.lock.X.big.body -COQC tests/instance_before_structure.v -[1766668983.682672] HB: exporting CS instances +[1732259030.902852] HB: exporting CS instances [«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] -[1766668983.683095] HB: exporting Abbreviations [addr0, addrNK] +[1732259030.907434] HB: exporting Abbreviations [addr0, addrNK] forall (R : Enclosing.Ring.type) (x : R), x = x : Prop 0%G @@ -1299,14 +1268,113 @@ ?s : [ |- Enclosing.Ring.type] Enclosing.zero : Z : Z +COQC tests/declare.v +COQC tests/short.v +[1732259031.189930] HB: start module SubInhab +[1732259031.204338] 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] +[1732259031.207463] HB: typing class field indt «is_inhab.axioms_» +[1732259031.211387] HB: typing class field indt «is_SUB.axioms_» +[1732259031.213362] HB: declare type record +[1732259031.226404] HB: structure: new mixins [] +[1732259031.235050] HB: structure: mixin first class [] +[1732259031.235309] HB: declaring clone abbreviation +[1732259031.238367] HB: declaring pack_ constant +[1732259031.255873] 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]] +[1732259031.256938] HB: start module Exports +[1732259031.257333] HB: making coercion from type to target +[1732259031.257529] HB: declare sort coercion +[1732259031.257735] HB: exporting unification hints +[1732259031.258483] HB: declare coercion subtype_SubInhab__to__subtype_SUB +[1732259031.267713] HB: declare coercion hint +subtype_SubInhab_class__to__subtype_SUB_class +[1732259031.274205] HB: declare unification hint +subtype_SubInhab__to__subtype_SUB +[1732259031.280993] HB: declare coercion subtype_SubInhab__to__subtype_Inhab +[1732259031.295775] HB: declare coercion hint +subtype_SubInhab_class__to__subtype_Inhab_class +[1732259031.304881] HB: declare unification hint +subtype_SubInhab__to__subtype_Inhab +[1732259031.321301] HB: declare unification hint +join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB +[1732259031.325166] HB: exporting coercions from class to mixins +[1732259031.347372] HB: export class to mixin coercion for mixin +subtype_is_inhab +[1732259031.351736] HB: export class to mixin coercion for mixin +subtype_is_SUB +[1732259031.354123] HB: accumulating various props +[1732259031.355594] HB: stop module Exports +[1732259031.361748] HB: declaring on_ abbreviation +[1732259031.381747] HB: declaring `copy` abbreviation +[1732259031.387829] HB: declaring on abbreviation +[1732259031.400333] HB: end modules; export +«HB.tests.subtype.SubInhab.Exports» +[1732259031.408753] HB: exporting operations +[1732259031.410091] HB: operations meta-data module: ElpiOperations +[1732259031.410870] HB: abbreviation factory-by-classname +p : pred nat + : pred nat +id : forall {T : Type}, Monoid.type T -> T + +id is not universe polymorphic +Arguments id {T}%type_scope {s} +id is transparent +Expands to: Constant HB.tests.funclass.id +COQC tests/instance_before_structure.v 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/primitive_records.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 +aType + : Type +hasB.type not a defined object. 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 +hasAB.type not a defined object. +hasA'.type not a defined object. +COQC tests/test_synthesis_params.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] +Notation big := big.body +Expands to: Notation HB.tests.lock.X.big + +big.body : forall R I : Type, R -> list I -> (I -> bigbody R I) -> R + +big.body is not universe polymorphic +Arguments big.body (R I)%type_scope _ _%list_scope _%function_scope +Expands to: Constant HB.tests.lock.X.big.body +COQC tests/hnf.v +HB.check: forall w : wp.type nat Init.Nat.mul, w = w : Prop +COQC tests/fun_instance.v +COQC tests/issue284.v Datatypes_prod__canonical__compress_coe_D = fun D D' : D.type => {| @@ -1328,126 +1396,43 @@ : D.type -> D.type -> D.type Arguments Datatypes_prod__canonical__compress_coe_D D D' -COQC tests/test_synthesis_params.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 -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 -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] -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 -[1766668984.254110] HB: start module and section hasA -[1766668984.254631] HB: converting arguments +COQC tests/issue287.v +COQC tests/two_hier.v +[1732259037.333232] HB: start module and section hasA +[1732259037.351252] 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 -[1766668984.254871] HB: processing key parameter -[1766668984.255326] HB: converting factories +[1732259037.351401] HB: processing key parameter +[1732259037.351738] HB: converting factories w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins -[1766668984.255550] HB: declaring context +[1732259037.351805] HB: declaring context w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] -[1766668984.255743] HB: declaring parameters and key as section variables +[1732259037.351900] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1766668984.256302] HB: declare mixin or factory -[1766668984.256450] HB: declare record axioms_ -[1766668984.258100] HB: declare notation Build -[1766668984.259504] HB: declare notation axioms -[1766668984.261738] HB: start module Exports -[1766668984.263379] HB: end modules and sections; export +[1732259037.352199] HB: declare mixin or factory +[1732259037.352245] HB: declare record axioms_ +[1732259037.353522] HB: declare notation Build +[1732259037.354503] HB: declare notation axioms +[1732259037.368356] HB: start module Exports +[1732259037.376359] HB: end modules and sections; export «HB.tests.hb_pack.hasA.Exports» hasA.type not a defined object. -HB.check: forall w : wp.type nat Init.Nat.mul, w = w : Prop -hasB.type not a defined object. -COQC tests/hnf.v -COQC tests/fun_instance.v -aType - : Type hasB.type not a defined object. -COQC tests/issue284.v -hasAB.type not a defined object. -hasA'.type not a defined object. HB: nat is canonically equipped with structures: - s1 (from "./tests/instance_before_structure.v", line 11) -COQC tests/issue287.v HB: nat is canonically equipped with structures: - s1 (from "./tests/instance_before_structure.v", line 11) -forall T : AB.type, -unkeyed - {| - AB.sort := T; - AB.class := - let hb_pack_hasA_mixin := AB.hb_pack_hasA_mixin _ (AB.class T) in - let hb_pack_hasB_mixin := AB.hb_pack_hasB_mixin _ (AB.class T) in - {| - AB.hb_pack_hasA_mixin := hb_pack_hasA_mixin; - AB.hb_pack_hasB_mixin := hb_pack_hasB_mixin - |} - |} - : Type -A : A.type - : A.type -A : A.type - : A.type -AB1 : hasB.phant_axioms A -> AB.type - : hasB.phant_axioms A -> AB.type HB: nat is canonically equipped with structures: - s1 (from "./tests/instance_before_structure.v", line 11) -Bm : hasB.phant_axioms A - : hasB.phant_axioms A -AB2 : AB.type - : AB.type -pB : T * T - : T * T -AB3 : AB.type - : AB.type -HB: nat is canonically equipped with structures: - - s1 - (from "./tests/instance_before_structure.v", line 11) - -Query assignments: - Ind = «hasA.axioms_» -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 hasAB.type not a defined object. -COQC tests/two_hier.v -X : Foo.type A P - : Foo.type A P -hasA'.type not a defined object. -COQC tests/instance_merge_with_param.v -COQC tests/instance_merge_with_distinct_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] @@ -1466,43 +1451,108 @@ https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v to witness devastating effects. [HB.non-forgetful-inheritance,HB,elpi,default] -T : Fun.type nat - : Fun.type nat +HB: nat is canonically equipped with structures: + - s1 + (from "./tests/instance_before_structure.v", line 11) + +hasA'.type not a defined object. +COQC tests/instance_merge_with_param.v +COQC tests/instance_merge_with_distinct_param.v COQC tests/instance_merge.v COQC tests/unit/enrich_type.v -Query assignments: - Ind = «A.axioms_» +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/unit/mixin_src_has_mixin_instance.v COQC tests/unit/mk_src_map.v +COQC tests/unit/close_hole_term.v +forall T : AB.type, +unkeyed + {| + AB.sort := T; + AB.class := + let hb_pack_hasA_mixin := AB.hb_pack_hasA_mixin _ (AB.class T) in + let hb_pack_hasB_mixin := AB.hb_pack_hasB_mixin _ (AB.class T) in + {| + AB.hb_pack_hasA_mixin := hb_pack_hasA_mixin; + AB.hb_pack_hasB_mixin := hb_pack_hasB_mixin + |} + |} + : Type +A : A.type + : A.type +A : A.type + : A.type +COQC tests/unit/struct.v +AB1 : hasB.phant_axioms A -> AB.type + : hasB.phant_axioms A -> AB.type 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 -Query assignments: - Ind = «A.type» +Bm : hasB.phant_axioms A + : hasB.phant_axioms A +AB2 : AB.type + : AB.type 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/close_hole_term.v -erefl : ?t = ?t - : ?t = ?t -where -?t : [ |- Sq.type] -COQC tests/unit/struct.v +Query assignments: +pB : T * T + : T * T + Ind = «hasA.axioms_» +AB3 : AB.type + : AB.type COQC tests/factory_when_notation.v +X : Foo.type A P + : Foo.type A P +T : Fun.type nat + : Fun.type nat COQC examples/demo1/test_0_0.v -COQC examples/demo1/test_1_0.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 +Query assignments: + Ind = «A.axioms_» +Query assignments: + M1 = const «m1.phant_axioms» + Y = has-mixin-instance (cs-gref (indt «nat»)) (const «m1.phant_axioms») + (const «nat_m1») +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 +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 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 examples/demo1/test_1_0.v HB: list is canonically equipped with structures: - s3 (from "./tests/instance_merge_with_param.v", line 23) @@ -1511,39 +1561,35 @@ - s1 (from "./tests/instance_merge_with_param.v", line 10) +COQC examples/demo1/test_2_0.v +Query assignments: + Ind = «A.type» nat : s3.type : s3.type list nat : s3.type : s3.type list (list nat) : s3.type : s3.type -COQC examples/demo1/test_2_0.v 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 +erefl : ?t = ?t + : ?t = ?t +where +?t : [ |- Sq.type] list_foo' : forall P A : Type, is_foo.axioms_ P (list A) list_foo : forall P : Type, is_foo.axioms_ P (list P) -nat : s3.type - : s3.type -list nat : s3.type - : s3.type -list (list nat) : s3.type - : s3.type -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 -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 -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_4_0.v 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_3.v +COQC examples/demo1/test_5_0.v +Query assignments: X = app [global (indt «list»), X0] Y = X0 Z = fun `x` X1 c0 \ app [global (indt «list»), c0] @@ -1568,18 +1614,10 @@ Query assignments: - M1 = const «m1.phant_axioms» - Y = has-mixin-instance (cs-gref (indt «nat»)) (const «m1.phant_axioms») - (const «nat_m1») -COQC examples/demo1/test_4_3.v -Query assignments: X = global (indt «nat») -COQC examples/demo1/test_5_0.v -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] +COQC examples/demo1/test_5_3.v +COQC examples/demo2/stage10.v +COQC examples/demo2/stage11.v Query assignments: H = [] struct_foo1__to__struct_foo = @@ -1588,13 +1626,17 @@ Arguments struct_foo1__to__struct_foo s struct_foo1__to__struct_foo is a reversible coercion -COQC examples/demo1/test_5_3.v -COQC examples/demo2/stage10.v +COQC examples/demo3/test_0_0.v +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: Z = global (indt «nat») -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 Query assignments: X = app [global (indt «list»), X0] Y = X0 @@ -1613,12 +1655,6 @@ Query assignments: - M1 = const «m1.phant_axioms» - Y = has-mixin-instance (cs-gref (indt «list»)) (const «m1.phant_axioms») - (const «i1») -COQC examples/demo3/test_2_0.v -COQC tests/exports2.v -Query assignments: MS' = pi c0 \ pi c1 \ pi c2 \ @@ -1683,6 +1719,10 @@ File "./examples/demo2/stage11.v", line 3, characters 0-25: Warning: Hiding binding of key Q to Q_scope [hiding-delimiting-key,parsing,default] +[1732259054.268717] HB: exporting under the module path [] +[1732259054.283072] HB: exporting modules [] +[1732259054.283344] HB: exporting CS instances [] +[1732259054.283468] HB: exporting Abbreviations [] Query assignments: C = X0 X = app @@ -1722,10 +1762,18 @@ WEAK CONSTRAINTS: -[1766668988.743996] HB: exporting under the module path [] -[1766668988.744126] HB: exporting modules [] -[1766668988.744166] HB: exporting CS instances [] -[1766668988.744214] HB: exporting Abbreviations [] +Qcplus_opp_r: forall q : Qc, q + - q = Q2Qc 0 +File "./examples/demo2/stage10.v", line 233, characters 0-27: +Warning: The default and global localities for this command outside sections +are currently equivalent to the combination of the standard meaning of +"global" (as described in the reference manual), "export" and re-exporting +for every surrounding module. It will change to just "global" (with the +meaning used by the "Set" command) in a future release. +To preserve the current meaning in a forward compatible way, use the +attribute "#[global,export]" and repeat the command with just "#[export]" in +any surrounding modules. If you are fine with the change of semantics, +disable this warning. +[deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] Query assignments: A = X0 B = X1 @@ -1757,18 +1805,6 @@ WEAK CONSTRAINTS: -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 -are currently equivalent to the combination of the standard meaning of -"global" (as described in the reference manual), "export" and re-exporting -for every surrounding module. It will change to just "global" (with the -meaning used by the "Set" command) in a future release. -To preserve the current meaning in a forward compatible way, use the -attribute "#[global,export]" and repeat the command with just "#[export]" in -any surrounding modules. If you are fine with the change of semantics, -disable this warning. -[deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] File "./examples/demo2/stage11.v", line 364, characters 0-27: Warning: The default and global localities for this command outside sections are currently equivalent to the combination of the standard meaning of @@ -1781,30 +1817,30 @@ disable this warning. [deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] HB: skipping section opening -[1766668990.640109] HB: declare mixin instance +[1732259063.396335] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology -[1766668990.641421] HB: declare canonical mixin instance +[1732259063.397753] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology» -[1766668990.642682] HB: declare mixin instance +[1732259063.399173] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform -[1766668990.646384] HB: declare canonical mixin instance +[1732259063.404169] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform» -[1766668990.647499] HB: declare mixin instance +[1732259063.412117] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology -[1766668990.650532] HB: declare canonical mixin instance +[1732259063.415200] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology» -[1766668990.651586] HB: declare mixin instance +[1732259063.424130] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform -[1766668990.653564] HB: declare canonical mixin instance +[1732259063.426877] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform» -[1766668990.655042] HB: we can build a Stage11_UniformSpace_wo_Topology on +[1732259063.428549] HB: we can build a Stage11_UniformSpace_wo_Topology on Qc -[1766668990.655277] HB: declare canonical structure instance +[1732259063.435464] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology -[1766668990.655425] HB: Giving name HB_unnamed_mixin_46 to mixin instance +[1732259063.435866] 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 -[1766668990.656445] HB: structure instance for +[1732259063.437056] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology is {| UniformSpace_wo_Topology.sort := Qc; @@ -1814,12 +1850,12 @@ HB_unnamed_mixin_46 |} |} -[1766668990.657706] HB: structure instance +[1732259063.438487] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology declared -[1766668990.658546] HB: we can build a Stage11_UniformSpace on Qc -[1766668990.658798] HB: declare canonical structure instance +[1732259063.439486] HB: we can build a Stage11_UniformSpace on Qc +[1732259063.439836] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace -[1766668990.658947] HB: structure instance for +[1732259063.440051] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace is {| UniformSpace.sort := Qc; @@ -1829,15 +1865,15 @@ UniformSpace.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_46 |} |} -[1766668990.660347] HB: structure instance +[1732259063.444200] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace declared -[1766668990.661363] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc -[1766668990.661620] HB: declare canonical structure instance +[1732259063.445229] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc +[1732259063.451172] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform -[1766668990.661871] HB: Giving name HB_unnamed_mixin_47 to mixin instance +[1732259063.451655] 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 -[1766668990.663197] HB: structure instance for +[1732259063.453050] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform is {| TAddAG_wo_Uniform.sort := Qc; @@ -1849,12 +1885,12 @@ HB_unnamed_mixin_47 |} |} -[1766668990.664526] HB: structure instance +[1732259063.454545] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform declared -[1766668990.665815] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc -[1766668990.666072] HB: declare canonical structure instance +[1732259063.455966] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc +[1732259063.459257] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined -[1766668990.666255] HB: structure instance for +[1732259063.459655] HB: structure instance for Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined is {| Uniform_TAddAG_unjoined.sort := Qc; @@ -1869,18 +1905,18 @@ HB_unnamed_mixin_46 |} |} -[1766668990.667572] HB: structure instance +[1732259063.461129] HB: structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined declared -[1766668990.669780] HB: we can build a Stage11_TAddAG on Qc -[1766668990.670039] HB: declare canonical structure instance +[1732259063.469152] HB: we can build a Stage11_TAddAG on Qc +[1732259063.469617] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG -[1766668990.670287] HB: Giving name HB_unnamed_mixin_48 to mixin instance +[1732259063.469964] 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 -[1766668990.671802] HB: Giving name HB_unnamed_mixin_49 to mixin instance +[1732259063.471574] 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 -[1766668990.673383] HB: structure instance for +[1732259063.476339] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG is {| TAddAG.sort := Qc; @@ -1894,13 +1930,13 @@ TAddAG.Stage11_Join_TAddAG_Uniform_mixin := HB_unnamed_mixin_49 |} |} -[1766668990.675117] HB: structure instance +[1732259063.478126] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG declared entourage : set (set (Qc * Qc)) : set (set (Qc * Qc)) -Finished transaction in 10.824 secs (9.554u,0.576s) (successful) +Finished transaction in 48.712 secs (8.826u,0.563s) (successful) Finished transaction in 0. secs (0.u,0.s) (successful) -Finished transaction in 9.683 secs (9.291u,0.392s) (successful) +Finished transaction in 32.487 secs (9.016u,0.52s) (successful) Module Type new_concept_Locked = Sig @@ -2006,12 +2042,14 @@ dpkg-buildpackage: info: binary-only upload (no source included) dpkg-genchanges: info: not including original source code in upload I: copying local configuration +I: user script /srv/workspace/pbuilder/3051591/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/3051591/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/1963874 and its subdirectories -I: Current time: Thu Dec 25 01:23:35 -12 2025 -I: pbuilder-time-stamp: 1766669015 +I: removing directory /srv/workspace/pbuilder/3051591 and its subdirectories +I: Current time: Fri Nov 22 21:05:55 +14 2024 +I: pbuilder-time-stamp: 1732259155