Diff of the two buildlogs: -- --- b1/build.log 2024-05-18 08:06:47.067280400 +0000 +++ b2/build.log 2024-05-18 08:08:42.782362161 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Fri Jun 20 02:26:47 -12 2025 -I: pbuilder-time-stamp: 1750429607 +I: Current time: Sat May 18 22:06:50 +14 2024 +I: pbuilder-time-stamp: 1716019610 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/unstable-reproducible-base.tgz] I: copying local configuration @@ -26,51 +26,83 @@ dpkg-source: info: unpacking coq-hierarchy-builder_1.7.0-1.debian.tar.xz I: Not using root during the build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/658974/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/1196912/tmp/hooks/D01_modify_environment starting +debug: Running on infom01-amd64. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +'/bin/sh' -> '/bin/bash' +lrwxrwxrwx 1 root root 9 May 18 08:06 /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/1196912/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/1196912/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build/reproducible-path' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' - BUILD_ARCH='amd64' - DEBIAN_FRONTEND='noninteractive' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:. + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="2" [2]="21" [3]="1" [4]="release" [5]="x86_64-pc-linux-gnu") + BASH_VERSION='5.2.21(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=amd64 + DEBIAN_FRONTEND=noninteractive DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=12 ' - DISTRIBUTION='unstable' - HOME='/root' - HOST_ARCH='amd64' + DIRSTACK=() + DISTRIBUTION=unstable + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=x86_64 + HOST_ARCH=amd64 IFS=' ' - INVOCATION_ID='7a351731893f4c47af24595683c47ee1' - 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='658974' - PS1='# ' - PS2='> ' + INVOCATION_ID=acd932b05a4b426db089f35957249cec + LANG=C + LANGUAGE=et_EE:et + LC_ALL=C + MACHTYPE=x86_64-pc-linux-gnu + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnu + PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path + PBCURRENTCOMMANDLINEOPERATION=build + PBUILDER_OPERATION=build + PBUILDER_PKGDATADIR=/usr/share/pbuilder + PBUILDER_PKGLIBDIR=/usr/lib/pbuilder + PBUILDER_SYSCONFDIR=/etc + PIPESTATUS=([0]="0") + POSIXLY_CORRECT=y + PPID=1196912 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.jAzlX3yQ/pbuilderrc_V8nZ --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.jAzlX3yQ/b1 --logfile b1/build.log coq-hierarchy-builder_1.7.0-1.dsc' - SUDO_GID='109' - SUDO_UID='104' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' + 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.jAzlX3yQ/pbuilderrc_MP8y --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.jAzlX3yQ/b2 --logfile b2/build.log coq-hierarchy-builder_1.7.0-1.dsc' + SUDO_GID=109 + SUDO_UID=104 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' I: uname -a - Linux infom02-amd64 6.6.13+bpo-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.6.13-1~bpo12+1 (2024-02-15) x86_64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-21-cloud-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.90-1 (2024-05-03) x86_64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Jun 20 14:05 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/658974/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 May 18 07:42 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/1196912/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -266,7 +298,7 @@ Get: 83 http://deb.debian.org/debian unstable/main amd64 libelpi-ocaml-dev amd64 1.18.2-1 [9602 kB] Get: 84 http://deb.debian.org/debian unstable/main amd64 libcoq-elpi amd64 2.1.0-1 [3464 kB] Get: 85 http://deb.debian.org/debian unstable/main amd64 wdiff amd64 1.2.2-6 [119 kB] -Fetched 356 MB in 5s (66.0 MB/s) +Fetched 356 MB in 3s (102 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libpython3.11-minimal:amd64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 19719 files and directories currently installed.) @@ -553,8 +585,8 @@ Setting up tzdata (2024a-4) ... Current default time zone: 'Etc/UTC' -Local time is now: Fri Jun 20 14:28:53 UTC 2025. -Universal Time is now: Fri Jun 20 14:28:53 UTC 2025. +Local time is now: Sat May 18 08:07:55 UTC 2024. +Universal Time is now: Sat May 18 08:07:55 UTC 2024. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up autotools-dev (20220109.1) ... @@ -633,7 +665,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-1_source.changes +I: user script /srv/workspace/pbuilder/1196912/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for unstable +I: user script /srv/workspace/pbuilder/1196912/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-1_source.changes dpkg-buildpackage: info: source package coq-hierarchy-builder dpkg-buildpackage: info: source version 1.7.0-1 dpkg-buildpackage: info: source distribution unstable @@ -698,16 +734,16 @@ COQC examples/hulk.v COQC examples/demo1/hierarchy_0.v COQC examples/demo1/hierarchy_1.v -COQC examples/demo1/hierarchy_2.v COQC examples/demo1/hierarchy_3.v +COQC examples/demo1/hierarchy_2.v COQC examples/demo1/hierarchy_4.v COQC examples/demo1/hierarchy_5.v COQC examples/demo2/classical.v COQC examples/demo3/hierarchy_0.v COQC examples/demo3/hierarchy_1.v COQC examples/demo3/hierarchy_2.v -[1750429754.465008] HB: start module and section AddComoid_of_Type -[1750429754.465513] HB: converting arguments +[1716019694.353438] HB: start module and section AddComoid_of_Type +[1716019694.353703] HB: converting arguments indt-decl (parameter A explicit X0 c0 \ record AddComoid_of_Type (sort (typ X1)) Build_AddComoid_of_Type @@ -733,19 +769,19 @@ app [global (indt «eq»), X10 c0 c1 c2 c3 c4 c5, app [c2, c1, c5], c5]) c5 \ end-record)) to factories -[1750429754.465896] HB: processing key parameter -[1750429754.466290] HB: converting factories +[1716019694.354203] HB: processing key parameter +[1716019694.358576] HB: converting factories w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] to mixins -[1750429754.466343] HB: declaring context +[1716019694.358659] HB: declaring context w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] -[1750429754.466453] HB: declaring parameters and key as section variables +[1716019694.358747] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1750429754.484026] HB: declare mixin or factory -[1750429754.484512] HB: declare record axioms_ -[1750429754.608728] HB: declare notation Build -[1750429754.617044] HB: declare notation axioms -[1750429754.629870] HB: start module Exports -[1750429754.647761] HB: end modules and sections; export +[1716019694.368353] HB: declare mixin or factory +[1716019694.374528] HB: declare record axioms_ +[1716019694.495093] HB: declare notation Build +[1716019694.502852] HB: declare notation axioms +[1716019694.514288] HB: start module Exports +[1716019694.530940] HB: end modules and sections; export «HB.examples.readme.AddComoid_of_Type.Exports» (* @@ -802,55 +838,46 @@ Notation AddComoid_of_Type X1 := ( AddComoid_of_Type.phant_axioms X1). *) -[1750429754.683537] HB: start module AddComoid -[1750429754.684068] HB: declare axioms record +[1716019694.556332] HB: start module AddComoid +[1716019694.556735] HB: declare axioms record w-params.nil A (sort (typ «HB.examples.readme.25»)) c0 \ [triple (indt «AddComoid_of_Type.axioms_») [] c0] -[1750429754.684428] HB: typing class field +[1716019694.556962] HB: typing class field indt «AddComoid_of_Type.axioms_» -[1750429754.694668] HB: declare type record -[1750429754.705459] HB: structure: new mixins +[1716019694.563984] HB: declare type record +[1716019694.571548] HB: structure: new mixins [indt «AddComoid_of_Type.axioms_»] -[1750429754.705815] HB: structure: mixin first class +[1716019694.571712] HB: structure: mixin first class [mixin-first-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»)] -[1750429754.706009] HB: declaring clone abbreviation -[1750429754.725901] HB: declaring pack_ constant -[1750429754.727066] HB: declaring pack_ constant = +[1716019694.571842] HB: declaring clone abbreviation +[1716019694.579278] HB: declaring pack_ constant +[1716019694.580059] 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]] -[1750429754.729590] HB: start module Exports -[1750429754.729965] HB: making coercion from type to target -[1750429754.730088] HB: declare sort coercion -[1750429754.730510] HB: exporting unification hints -[1750429754.730718] HB: exporting coercions from class to mixins -[1750429754.731057] HB: export class to mixin coercion for mixin +[1716019694.581518] HB: start module Exports +[1716019694.581810] HB: making coercion from type to target +[1716019694.581967] HB: declare sort coercion +[1716019694.582354] HB: exporting unification hints +[1716019694.582545] HB: exporting coercions from class to mixins +[1716019694.582811] HB: export class to mixin coercion for mixin readme_AddComoid_of_Type -[1750429754.731489] HB: accumulating various props -[1750429754.741091] HB: stop module Exports -[1750429754.747729] HB: declaring on_ abbreviation -[1750429754.802054] HB: declaring `copy` abbreviation -[1750429754.803587] HB: declaring on abbreviation -COQC examples/demo4/hierarchy_0.v -[1750429754.811260] HB: end modules; export +[1716019694.583146] HB: accumulating various props +[1716019694.589717] HB: stop module Exports +[1716019694.594195] HB: declaring on_ abbreviation +[1716019694.651218] HB: declaring `copy` abbreviation +[1716019694.652416] HB: declaring on abbreviation +[1716019694.657899] HB: end modules; export «HB.examples.readme.AddComoid.Exports» -[1750429754.812955] HB: exporting operations -[1750429754.814207] HB: export operation zero -[1750429754.817967] HB: export operation add -[1750429754.821957] HB: export operation addrA -COQC examples/demo5/hierarchy_0.v -[1750429754.831184] HB: export operation addrC -[1750429754.833065] HB: begin module for builders -[1750429754.833475] HB: begin module Super -[1750429754.833727] HB: ended module Super -[1750429754.835834] HB: export operation add0r -[1750429754.836677] HB: postulating factories -[1750429754.836846] HB: processing key context-item -[1750429754.837111] HB: processing mixin parameter a -[1750429754.837560] HB: declaring parameters and key as section variables -Here is the list of mixins to declare (the order matters): [] -[1750429754.842273] HB: operations meta-data module: ElpiOperations -[1750429754.863008] HB: abbreviation factory-by-classname +[1716019694.659082] HB: exporting operations +[1716019694.659998] HB: export operation zero +[1716019694.662631] HB: export operation add +[1716019694.665865] HB: export operation addrA +[1716019694.669150] HB: export operation addrC +[1716019694.672308] HB: export operation add0r +[1716019694.674672] HB: operations meta-data module: ElpiOperations +COQC examples/demo4/hierarchy_0.v +[1716019694.684083] HB: abbreviation factory-by-classname (* Module AddComoid. @@ -947,12 +974,27 @@ *) forall (M : AddComoid.type) (x : M), x + x = 0 : Prop -COQC examples/FSCD2020_material/V1.v +COQC examples/demo5/hierarchy_0.v AbelianGrp.phant_on_ BinNums_Z__canonical__readme_AbelianGrp (Phant BinNums_Z__canonical__readme_AbelianGrp) : AbelianGrp.axioms_ Z : AbelianGrp.axioms_ Z +HB: Z is canonically equipped with structures: + - AbelianGrp + (from "./examples/readme.v", line 32) + - AddComoid + (from "./examples/readme.v", line 31) + +COQC examples/FSCD2020_material/V1.v +[1716019695.125291] HB: begin module for builders +[1716019695.125695] HB: begin module Super +[1716019695.125877] HB: ended module Super +[1716019695.130037] HB: postulating factories +[1716019695.130226] HB: processing key context-item +[1716019695.130553] HB: processing mixin parameter a +[1716019695.130941] HB: declaring parameters and key as section variables +Here is the list of mixins to declare (the order matters): [] File "./examples/demo1/hierarchy_2.v", line 57, characters 0-57: Warning: pulling in dependencies: @@ -960,49 +1002,43 @@ Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] -HB: Z is canonically equipped with structures: - - AbelianGrp - (from "./examples/readme.v", line 32) - - AddComoid - (from "./examples/readme.v", line 31) - COQC examples/FSCD2020_material/V2.v +[1716019695.520583] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_AddAG_of_AddComoid +[1716019695.520877] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_Ring_of_AddAG +COQC examples/FSCD2020_material/V3.v inhab : ?s where ?T : [ |- Type] ?s : [ |- s1.type ?T] -COQC examples/FSCD2020_material/V3.v eq_refl : inhab = 7 : inhab = 7 +COQC examples/FSCD2020_material/V4.v eq_refl : inhab = (7 :: nil)%list : inhab = (7 :: nil)%list where ?T : [ |- Type] -COQC examples/FSCD2020_material/V4.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. -[1750429755.741560] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_AddAG_of_AddComoid -[1750429755.741866] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_Ring_of_AddAG -COQC examples/FSCD2020_talk/V1.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 COQC examples/FSCD2020_talk/V2.v -COQC examples/FSCD2020_talk/V3.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. HB: A is canonically equipped with structures: - Equality Singleton (from "./examples/hulk.v", line 216) +COQC examples/FSCD2020_talk/V3.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -1013,6 +1049,22 @@ COQC examples/Coq2020_material/CoqWS_demo.v COQC examples/Coq2020_material/CoqWS_abstract.v 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 +File "./examples/FSCD2020_talk/V2.v", line 17, characters 0-66: +Warning: +pulling in dependencies: [V2_is_semigroup] + +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB,elpi,default] +COQC tests/type_of_exported_ops.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -1022,13 +1074,9 @@ : 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/duplicate_structure.v +COQC tests/instance_params_no_type.v +COQC tests/test_CS_db_filtering.v add : ?s -> ?s -> ?s where @@ -1037,31 +1085,6 @@ : commutative add where ?s : [ |- CMonoid.type] -COQC tests/type_of_exported_ops.v -File "./examples/Coq2020_material/CoqWS_demo.v", line 73, characters 0-73: -Warning: -pulling in dependencies: [CoqWS_demo_CMonoid_of_Type] - -Please list them or end the declaration with '&' -[HB.implicit-structure-dependency,HB,elpi,default] -COQC tests/duplicate_structure.v -forall x y : ?t, x - (y + 0) = x - : Prop -where -?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) -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/instance_params_no_type.v -COQC tests/test_CS_db_filtering.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 @@ -1071,23 +1094,38 @@ : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add +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/subtype.v 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] + +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB,elpi,default] COQC tests/exports.v -COQC tests/log_impargs_record.v -forall x y : ?t, 1 + x = y * x +forall x y : ?t, x - (y + 0) = x : Prop where -?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) +?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) File "./examples/Coq2020_material/CoqWS_abstract.v", line 23, characters 0-71: Warning: pulling in dependencies: [CoqWS_abstract_CMonoid_of_Type] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] +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) +COQC tests/compress_coe.v +COQC tests/funclass.v forall (R : Ring.type) (x y : R), 1 * x = y - x : Prop forall @@ -1098,66 +1136,15 @@ ?t : [x : join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing ?t y : ?t |- Ring.type] (x, y cannot be used) -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop -COQC tests/compress_coe.v -COQC tests/funclass.v -add - : A -> A -> A -(* - -Module A. -Section A. -Variable T : Type. -Local Arguments T : clear implicits. -Section axioms_. -Local Unset Implicit Arguments. -Record axioms_ (T : Type) : Type := Axioms_ - { - a : T; - f : T -> T; - p : forall x : T, f x = x -> True; - q : forall h : f a = a, p a h = p a h; - }. -End axioms_. - -Global Arguments axioms_ : clear implicits. -Global Arguments Axioms_ [_] [_] _ _ _. -Global Arguments a [_] _. -Global Arguments f [_] _ _. -Global Arguments p [_] _ [_] _. -Global Arguments q [_] _ _. -End A. -Global Arguments axioms_ : clear implicits. -Global Arguments Axioms_ : clear implicits. -Definition phant_Build : forall (T : Type) (a : T) (f : T -> T) - (p : forall x : T, f x = x -> True), - (forall h : f a = a, p a h = p a h) -> axioms_ T := - fun (T : Type) (a : T) (f : T -> T) (p : forall x : T, f x = x -> True) - (q : forall h : f a = a, p a h = p a h) => - {| a := a; f := f; p := p; q := q |}. -Local Arguments phant_Build : clear implicits. -Notation Build X1 := ( phant_Build X1). -Definition phant_axioms : Type -> Type := fun T : Type => axioms_ T. -Local Arguments phant_axioms : clear implicits. -Notation axioms X1 := ( phant_axioms X1). -Definition identity_builder : forall T : Type, axioms_ T -> axioms_ T := - fun (T : Type) (x : axioms_ T) => x. -Local Arguments identity_builder : clear implicits. -Module Exports. -Global Arguments Axioms_ {_}. -End Exports. -End A. -Export A.Exports. -Notation A X1 := ( A.phant_axioms X1). - -*) +COQC tests/grefclass.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 nat_foo : forall P : Type, is_foo.axioms_ P nat list_foo @@ -1166,18 +1153,10 @@ : Prop forall (S : SemiRing.type) (x : S), x * 1 + 0 = x : Prop -COQC tests/grefclass.v forall (R : Ring.type) (x y : R), x * - (1 * y) = - x * y : Prop -A.p : -forall [T : Type] (record : A.axioms_ T) [x : T], A.f record x = x -> True - -A.p is not universe polymorphic -Arguments A.p [T]%type_scope record [x] _ -A.p is transparent -Expands to: Constant HB.tests.log_impargs_record.A.p -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop +add + : A -> A -> A foo.type : Type -> Type Record type (P : Type) : Type := Pack @@ -1213,35 +1192,26 @@ 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 -COQC tests/local_instance.v -COQC tests/lock.v forall x : Z, x * - (1 + x) = 0 + 1 : Prop -COQC tests/interleave_context.v -Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. - -Arguments Monoid.Pack sort%type_scope class -@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 -[1750429758.238858] HB: start module SubInhab -[1750429758.239237] HB: declare axioms record +COQC tests/local_instance.v +[1716019697.675850] HB: start module SubInhab +[1716019697.676217] 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] -[1750429758.239499] HB: typing class field indt «is_inhab.axioms_» -[1750429758.239725] HB: typing class field indt «is_SUB.axioms_» -[1750429758.245007] HB: declare type record -[1750429758.249907] HB: structure: new mixins [] -[1750429758.250071] HB: structure: mixin first class [] -[1750429758.250162] HB: declaring clone abbreviation -[1750429758.255084] HB: declaring pack_ constant -[1750429758.256237] HB: declaring pack_ constant = +[1716019697.676513] HB: typing class field indt «is_inhab.axioms_» +[1716019697.676745] HB: typing class field indt «is_SUB.axioms_» +[1716019697.681389] HB: declare type record +[1716019697.685987] HB: structure: new mixins [] +[1716019697.686108] HB: structure: mixin first class [] +[1716019697.686188] HB: declaring clone abbreviation +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop +[1716019697.690899] HB: declaring pack_ constant +[1716019697.691960] 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 \ @@ -1250,64 +1220,144 @@ app [global (indc «Pack»), c0, c1, c2, app [global (indc «Class»), c0, c1, c2, c3, c4]] -[1750429758.257452] HB: start module Exports -[1750429758.257677] HB: making coercion from type to target -[1750429758.257786] HB: declare sort coercion -[1750429758.258018] HB: exporting unification hints -[1750429758.258473] HB: declare coercion subtype_SubInhab__to__subtype_SUB -[1750429758.259090] HB: declare coercion hint +[1716019697.693149] HB: start module Exports +[1716019697.693340] HB: making coercion from type to target +[1716019697.693443] HB: declare sort coercion +[1716019697.693701] HB: exporting unification hints +[1716019697.694161] HB: declare coercion subtype_SubInhab__to__subtype_SUB +[1716019697.695025] HB: declare coercion hint subtype_SubInhab_class__to__subtype_SUB_class -[1750429758.262999] HB: declare unification hint +[1716019697.698814] HB: declare unification hint subtype_SubInhab__to__subtype_SUB -[1750429758.267809] HB: declare coercion subtype_SubInhab__to__subtype_Inhab -[1750429758.268557] HB: declare coercion hint +[1716019697.703205] HB: declare coercion subtype_SubInhab__to__subtype_Inhab +[1716019697.703751] HB: declare coercion hint subtype_SubInhab_class__to__subtype_Inhab_class -list_bar - : forall P : b.type, is_bar.axioms_ P (list P) -[1750429758.274039] HB: declare unification hint +[1716019697.707617] HB: declare unification hint subtype_SubInhab__to__subtype_Inhab -COQC tests/not_same_key.v -[1750429758.279586] HB: declare unification hint +[1716019697.712430] HB: declare unification hint join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB -[1750429758.284000] HB: exporting coercions from class to mixins -[1750429758.284404] HB: export class to mixin coercion for mixin +[1716019697.716545] HB: exporting coercions from class to mixins +[1716019697.716887] HB: export class to mixin coercion for mixin subtype_is_inhab -[1750429758.285294] HB: export class to mixin coercion for mixin +[1716019697.717690] HB: export class to mixin coercion for mixin subtype_is_SUB -[1750429758.285882] HB: accumulating various props -COQC tests/hb_pack.v -[1750429758.305285] HB: stop module Exports -[1750429758.309743] HB: declaring on_ abbreviation -[1750429758.314939] HB: declaring `copy` abbreviation -[1750429758.315865] HB: declaring on abbreviation -[1750429758.319389] HB: end modules; export +[1716019697.718293] HB: accumulating various props +[1716019697.734212] HB: stop module Exports +(* + +Module A. +Section A. +Variable T : Type. +Local Arguments T : clear implicits. +Section axioms_. +Local Unset Implicit Arguments. +Record axioms_ (T : Type) : Type := Axioms_ + { + a : T; + f : T -> T; + p : forall x : T, f x = x -> True; + q : forall h : f a = a, p a h = p a h; + }. +End axioms_. + +Global Arguments axioms_ : clear implicits. +Global Arguments Axioms_ [_] [_] _ _ _. +Global Arguments a [_] _. +Global Arguments f [_] _ _. +Global Arguments p [_] _ [_] _. +Global Arguments q [_] _ _. +End A. +Global Arguments axioms_ : clear implicits. +Global Arguments Axioms_ : clear implicits. +Definition phant_Build : forall (T : Type) (a : T) (f : T -> T) + (p : forall x : T, f x = x -> True), + (forall h : f a = a, p a h = p a h) -> axioms_ T := + fun (T : Type) (a : T) (f : T -> T) (p : forall x : T, f x = x -> True) + (q : forall h : f a = a, p a h = p a h) => + {| a := a; f := f; p := p; q := q |}. +Local Arguments phant_Build : clear implicits. +Notation Build X1 := ( phant_Build X1). +Definition phant_axioms : Type -> Type := fun T : Type => axioms_ T. +Local Arguments phant_axioms : clear implicits. +Notation axioms X1 := ( phant_axioms X1). +Definition identity_builder : forall T : Type, axioms_ T -> axioms_ T := + fun (T : Type) (x : axioms_ T) => x. +Local Arguments identity_builder : clear implicits. +Module Exports. +Global Arguments Axioms_ {_}. +End Exports. +End A. +Export A.Exports. +Notation A X1 := ( A.phant_axioms X1). + +*) +COQC tests/lock.v +[1716019697.737942] HB: declaring on_ abbreviation +[1716019697.742420] HB: declaring `copy` abbreviation +[1716019697.743195] HB: declaring on abbreviation +[1716019697.746099] HB: end modules; export «HB.tests.subtype.SubInhab.Exports» -[1750429758.321579] HB: exporting operations -[1750429758.321867] HB: operations meta-data module: ElpiOperations -[1750429758.325462] HB: abbreviation factory-by-classname -COQC tests/declare.v +[1716019697.747892] HB: exporting operations +[1716019697.748110] HB: operations meta-data module: ElpiOperations +[1716019697.751274] HB: abbreviation factory-by-classname +COQC tests/interleave_context.v +list_bar + : forall P : b.type, is_bar.axioms_ P (list P) +COQC tests/not_same_key.v +Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. + +Arguments Monoid.Pack sort%type_scope class +@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 +A.p : +forall [T : Type] (record : A.axioms_ T) [x : T], A.f record x = x -> True + +A.p is not universe polymorphic +Arguments A.p [T]%type_scope record [x] _ +A.p is transparent +Expands to: Constant HB.tests.log_impargs_record.A.p p : pred nat : pred nat -COQC tests/short.v id : forall {T : Type}, Monoid.type T -> T id is not universe polymorphic Arguments id {T}%type_scope {s} id is transparent Expands to: Constant HB.tests.funclass.id +COQC tests/hb_pack.v +COQC tests/declare.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 -[1750429758.553306] HB: exporting under the module path [] -[1750429758.553535] HB: exporting modules +COQC tests/short.v +Notation big := big.body +Expands to: Notation HB.tests.lock.X.big +COQC tests/instance_before_structure.v +COQC tests/primitive_records.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 +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". +[1716019698.154975] HB: exporting under the module path [] +[1716019698.155191] HB: exporting modules [Ring_of_TYPE.Exports, Ring.Exports, RingElpiOperations, RingExports, Dummy.Exports, URing.Exports, URingElpiOperations, dummy.Exports, Builders_1.Builders_Export_5] -[1750429758.554768] HB: exporting CS instances +[1716019698.156325] HB: exporting CS instances [«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] -[1750429758.555093] HB: exporting Abbreviations [addr0, addrNK] +[1716019698.156606] HB: exporting Abbreviations [addr0, addrNK] forall (R : Enclosing.Ring.type) (x : R), x = x : Prop 0%G @@ -1316,55 +1366,32 @@ ?s : [ |- Enclosing.Ring.type] Enclosing.zero : Z : Z -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 -Notation big := big.body -Expands to: Notation HB.tests.lock.X.big 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 -[1750429758.785181] HB: start module and section hasA -[1750429758.785752] HB: converting arguments +HB.check: forall w : wp.type nat Init.Nat.mul, w = w : Prop +[1716019698.289346] HB: start module and section hasA +[1716019698.289599] 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 -[1750429758.786165] HB: processing key parameter -[1750429758.786523] HB: converting factories +[1716019698.289708] HB: processing key parameter +[1716019698.290188] HB: converting factories w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins -[1750429758.786637] HB: declaring context +[1716019698.290324] HB: declaring context w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] -[1750429758.786774] HB: declaring parameters and key as section variables +[1716019698.290516] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1750429758.790116] HB: declare mixin or factory -[1750429758.790542] HB: declare record axioms_ -[1750429758.800850] HB: declare notation Build -[1750429758.806311] HB: declare notation axioms -[1750429758.815184] HB: start module Exports -[1750429758.826929] HB: end modules and sections; export +[1716019698.294423] HB: declare mixin or factory +[1716019698.294554] HB: declare record axioms_ +[1716019698.303327] HB: declare notation Build +[1716019698.308034] HB: declare notation axioms +[1716019698.316957] HB: start module Exports +[1716019698.329233] 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 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] COQC tests/hnf.v -hasB.type not a defined object. -aType - : Type Datatypes_prod__canonical__compress_coe_D = fun D D' : D.type => {| @@ -1386,22 +1413,72 @@ : D.type -> D.type -> D.type Arguments Datatypes_prod__canonical__compress_coe_D D D' -hasB.type not a defined object. COQC tests/fun_instance.v -COQC tests/issue284.v -hasAB.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] +hasB.type not a defined object. +aType + : Type +hasB.type not a defined object. +HB: nat is canonically equipped with structures: + - s1 + (from "./tests/instance_before_structure.v", line 11) + +HB: nat is canonically equipped with structures: + - s1 + (from "./tests/instance_before_structure.v", line 11) + +HB: nat is canonically equipped with structures: + - s1 + (from "./tests/instance_before_structure.v", line 11) + Query assignments: Ind = «hasA.axioms_» -COQC tests/issue287.v -hasA'.type not a defined object. +COQC tests/issue284.v HB: nat is canonically equipped with structures: - s1 (from "./tests/instance_before_structure.v", line 11) +hasAB.type not a defined object. HB: nat is canonically equipped with structures: + - s3 + s2 + (from "./tests/instance_before_structure.v", line 30) - s1 (from "./tests/instance_before_structure.v", line 11) +default1 + : nat +default2 + : nat +default3 + : nat +COQC tests/issue287.v +hasA'.type not a defined object. +COQC tests/two_hier.v +File "./tests/non_forgetful_inheritance.v", line 35, characters 0-45: +Warning: Could not enable unknown warning HB.non-forgetful-inheritance +[unknown-warning,default] +COQC tests/instance_merge_with_param.v +Debug: +elpi lets escape exception: non forgetful inheritance detected. + You have two solutions: +1. (Best practice) Reorganize your hierarchy to make +non_forgetful_inheritance_HasSq depend on non_forgetful_inheritance_Mul. +See the paper "Competing inheritance paths in +dependent type theory" (https://hal.inria.fr/hal-02463336) for more +explanations +2. Use the attribute #[non_forgetful_inheritance] to disable this check. +We strongly advise you encapsulate this instance inside a module, +in order to isolate it from the rest of the code, and to be able +to import it on demand. See the above paper and the file +https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v +to witness devastating effects. +[HB.non-forgetful-inheritance,HB,elpi,default] forall T : AB.type, unkeyed {| @@ -1419,107 +1496,58 @@ : A.type A : A.type : A.type -Query assignments: - Ind = «A.axioms_» +hasAB.type not a defined object. AB1 : hasB.phant_axioms A -> AB.type : hasB.phant_axioms A -> AB.type -File "./tests/non_forgetful_inheritance.v", line 35, characters 0-45: -Warning: Could not enable unknown warning HB.non-forgetful-inheritance -[unknown-warning,default] Bm : hasB.phant_axioms A : hasB.phant_axioms A AB2 : AB.type : AB.type -HB: nat is canonically equipped with structures: - - s1 - (from "./tests/instance_before_structure.v", line 11) - pB : T * T : T * T AB3 : AB.type : AB.type -Debug: -elpi lets escape exception: non forgetful inheritance detected. - You have two solutions: -1. (Best practice) Reorganize your hierarchy to make -non_forgetful_inheritance_HasSq depend on non_forgetful_inheritance_Mul. -See the paper "Competing inheritance paths in -dependent type theory" (https://hal.inria.fr/hal-02463336) for more -explanations -2. Use the attribute #[non_forgetful_inheritance] to disable this check. -We strongly advise you encapsulate this instance inside a module, -in order to isolate it from the rest of the code, and to be able -to import it on demand. See the above paper and the file -https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v -to witness devastating effects. -[HB.non-forgetful-inheritance,HB,elpi,default] -hasAB.type not a defined object. -HB: nat is canonically equipped with structures: - - s1 - (from "./tests/instance_before_structure.v", line 11) - -HB: nat is canonically equipped with structures: - - s3 - s2 - (from "./tests/instance_before_structure.v", line 30) - - s1 - (from "./tests/instance_before_structure.v", line 11) - -default1 - : nat -default2 - : nat -default3 - : nat +COQC tests/instance_merge_with_distinct_param.v hasA'.type not a defined object. -COQC tests/two_hier.v -COQC tests/instance_merge_with_param.v +Query assignments: + Ind = «A.axioms_» +COQC tests/instance_merge.v +X : Foo.type A P + : Foo.type A P Query assignments: Ind = «A.type» -COQC tests/instance_merge_with_distinct_param.v +COQC tests/unit/enrich_type.v +COQC tests/unit/mixin_src_has_mixin_instance.v +COQC tests/unit/mk_src_map.v Datatypes_nat__canonical__hnf_S = {| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_8 |} |} : S.type HB_unnamed_mixin_8 = {| M.x := f.y nat HB_unnamed_factory_6 + 1 |} : M.axioms_ nat +T : Fun.type nat + : Fun.type 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/unit/close_hole_term.v +COQC tests/unit/struct.v +COQC tests/factory_when_notation.v erefl ?t : ?t = ?t : ?t = ?t where ?t : [ |- Sq.type] -COQC tests/instance_merge.v -COQC tests/unit/enrich_type.v -X : Foo.type A P - : Foo.type A P -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 -T : Fun.type nat - : Fun.type nat -COQC examples/demo1/test_0_0.v -COQC examples/demo1/test_1_0.v HB: list is canonically equipped with structures: - s2 (from "./tests/instance_merge_with_param.v", line 12) - s1 (from "./tests/instance_merge_with_param.v", line 10) -nat : s3.type - : s3.type -list nat : s3.type - : s3.type -list (list nat) : s3.type - : s3.type -fun t : s3.type => list t : s3.type - : s3.type -> s3.type +COQC examples/demo1/test_0_0.v +COQC examples/demo1/test_1_0.v HB: list is canonically equipped with structures: - s3 (from "./tests/instance_merge_with_param.v", line 23) @@ -1537,14 +1565,36 @@ : 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 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 COQC examples/demo1/test_4_3.v +COQC examples/demo1/test_5_0.v +COQC examples/demo1/test_5_3.v +Query assignments: + M1 = const «m1.phant_axioms» + Y = has-mixin-instance (cs-gref (indt «nat»)) (const «m1.phant_axioms») + (const «nat_m1») Query assignments: X = app [global (indt «list»), X0] Y = X0 @@ -1571,22 +1621,6 @@ Query assignments: X = global (indt «nat») -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 -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_5_0.v -COQC examples/demo1/test_5_3.v -Query assignments: - Z = global (indt «nat») Query assignments: MS = pi c0 \ pi c1 \ @@ -1595,20 +1629,15 @@ COQC examples/demo2/stage10.v COQC examples/demo2/stage11.v COQC examples/demo3/test_0_0.v -Query assignments: - H = [] -struct_foo1__to__struct_foo = -fun s : foo1.type => {| foo.sort := s; foo.class := foo1.class s |} - : foo1.type -> foo.type (option nat) - -Arguments struct_foo1__to__struct_foo s -struct_foo1__to__struct_foo is a reversible coercion COQC examples/demo3/test_1_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/demo3/test_2_0.v +COQC tests/exports2.v +Query assignments: + Z = global (indt «nat») Query assignments: X = app [global (indt «list»), X0] Y = X0 @@ -1626,19 +1655,69 @@ WEAK CONSTRAINTS: -COQC tests/exports2.v +File "./examples/demo2/stage10.v", line 4, characters 0-25: +Warning: Hiding binding of key Q to Q_scope +[hiding-delimiting-key,parsing,default] Query assignments: MS' = pi c0 \ pi c1 \ pi c2 \ mixin-src (app [global (indt «list»), c2]) (indt «is_foo.axioms_») (app [global (const «list_foo'»), c0, c1]) :- [coq.unify-eq c1 c2 ok] +Query assignments: + H = [] +struct_foo1__to__struct_foo = +fun s : foo1.type => {| foo.sort := s; foo.class := foo1.class s |} + : foo1.type -> foo.type (option nat) + +Arguments struct_foo1__to__struct_foo s +struct_foo1__to__struct_foo is a reversible coercion +[1716019701.262659] HB: exporting under the module path [] +[1716019701.262811] HB: exporting modules [] +[1716019701.262859] HB: exporting CS instances [] +[1716019701.262903] HB: exporting Abbreviations [] File "./examples/demo2/stage11.v", line 3, characters 0-25: Warning: Hiding binding of key Q to Q_scope [hiding-delimiting-key,parsing,default] -File "./examples/demo2/stage10.v", line 4, characters 0-25: -Warning: Hiding binding of key Q to Q_scope -[hiding-delimiting-key,parsing,default] +Query assignments: + C = X0 + X = app + [global (indt «prod»), app [global (indt «list»), X1], + app [global (indt «list»), X0]] + X1 = X1 + Y = c0 \ c1 \ +app + [global (indt «prod»), app [global (indt «list»), c0], + app [global (indt «list»), c1]] +Syntactic constraints: + evar (X2) (sort (typ «HB.tests.unit.enrich_type.5»)) (X2) /* suspended on X2 */ + evar (X3) (sort (typ «HB.tests.unit.enrich_type.4»)) (X3) /* suspended on X3 */ +Universe constraints: +UNIVERSES: + {HB.tests.unit.enrich_type.6 HB.tests.unit.enrich_type.5 + HB.tests.unit.enrich_type.4 HB.tests.unit.enrich_type.3 + HB.tests.unit.enrich_type.2} |= + HB.tests.unit.enrich_type.4 < HB.tests.unit.enrich_type.2 + HB.tests.unit.enrich_type.5 < HB.tests.unit.enrich_type.3 + Set <= HB.tests.unit.enrich_type.6 + Set <= prod.u0 + Set <= prod.u1 + HB.tests.unit.enrich_type.4 <= HB.tests.unit.enrich_type.6 + HB.tests.unit.enrich_type.4 <= prod.u0 + HB.tests.unit.enrich_type.4 <= list.u0 + HB.tests.unit.enrich_type.5 <= HB.tests.unit.enrich_type.6 + HB.tests.unit.enrich_type.5 <= prod.u1 + HB.tests.unit.enrich_type.5 <= list.u0 +ALGEBRAIC UNIVERSES: + {} +FLEXIBLE UNIVERSES: + +SORTS: + α1 := Type + α2 := Type +WEAK CONSTRAINTS: + + Query assignments: X = app [global (const «Inj»), X0, X1, X2, X3, X4] Y = app [global (const «Inj»), X0, X1] @@ -1692,49 +1771,6 @@ WEAK CONSTRAINTS: -[1750429763.721652] HB: exporting under the module path [] -[1750429763.721948] HB: exporting modules [] -[1750429763.722029] HB: exporting CS instances [] -[1750429763.722156] HB: exporting Abbreviations [] -Query assignments: - C = X0 - X = app - [global (indt «prod»), app [global (indt «list»), X1], - app [global (indt «list»), X0]] - X1 = X1 - Y = c0 \ c1 \ -app - [global (indt «prod»), app [global (indt «list»), c0], - app [global (indt «list»), c1]] -Syntactic constraints: - evar (X2) (sort (typ «HB.tests.unit.enrich_type.5»)) (X2) /* suspended on X2 */ - evar (X3) (sort (typ «HB.tests.unit.enrich_type.4»)) (X3) /* suspended on X3 */ -Universe constraints: -UNIVERSES: - {HB.tests.unit.enrich_type.6 HB.tests.unit.enrich_type.5 - HB.tests.unit.enrich_type.4 HB.tests.unit.enrich_type.3 - HB.tests.unit.enrich_type.2} |= - HB.tests.unit.enrich_type.4 < HB.tests.unit.enrich_type.2 - HB.tests.unit.enrich_type.5 < HB.tests.unit.enrich_type.3 - Set <= HB.tests.unit.enrich_type.6 - Set <= prod.u0 - Set <= prod.u1 - HB.tests.unit.enrich_type.4 <= HB.tests.unit.enrich_type.6 - HB.tests.unit.enrich_type.4 <= prod.u0 - HB.tests.unit.enrich_type.4 <= list.u0 - HB.tests.unit.enrich_type.5 <= HB.tests.unit.enrich_type.6 - HB.tests.unit.enrich_type.5 <= prod.u1 - HB.tests.unit.enrich_type.5 <= list.u0 -ALGEBRAIC UNIVERSES: - {} -FLEXIBLE UNIVERSES: - -SORTS: - α1 := Type - α2 := Type -WEAK CONSTRAINTS: - - Query assignments: A = X0 B = X1 @@ -1778,7 +1814,7 @@ 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] -Finished transaction in 9.307 secs (6.982u,0.267s) (successful) +Finished transaction in 6.93 secs (6.501u,0.179s) (successful) Finished transaction in 0. secs (0.u,0.s) (successful) File "./examples/demo2/stage11.v", line 364, characters 0-27: Warning: The default and global localities for this command outside sections @@ -1792,30 +1828,30 @@ disable this warning. [deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] HB: skipping section opening -[1750429767.233536] HB: declare mixin instance +[1716019704.584297] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology -[1750429767.246467] HB: declare canonical mixin instance +[1716019704.594903] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology» -[1750429767.247571] HB: declare mixin instance +[1716019704.595777] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform -[1750429767.252011] HB: declare canonical mixin instance +[1716019704.599332] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform» -[1750429767.252889] HB: declare mixin instance +[1716019704.600038] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology -[1750429767.256111] HB: declare canonical mixin instance +[1716019704.602835] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology» -[1750429767.256895] HB: declare mixin instance +[1716019704.603498] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform -[1750429767.259500] HB: declare canonical mixin instance +[1716019704.605612] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform» -[1750429767.260585] HB: we can build a Stage11_UniformSpace_wo_Topology on +[1716019704.606567] HB: we can build a Stage11_UniformSpace_wo_Topology on Qc -[1750429767.260790] HB: declare canonical structure instance +[1716019704.606702] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology -[1750429767.261005] HB: Giving name HB_unnamed_mixin_46 to mixin instance +[1716019704.606837] 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 -[1750429767.262732] HB: structure instance for +[1716019704.608103] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology is {| UniformSpace_wo_Topology.sort := Qc; @@ -1825,12 +1861,12 @@ HB_unnamed_mixin_46 |} |} -[1750429767.265372] HB: structure instance +[1716019704.610190] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology declared -[1750429767.266039] HB: we can build a Stage11_UniformSpace on Qc -[1750429767.266227] HB: declare canonical structure instance +[1716019704.610774] HB: we can build a Stage11_UniformSpace on Qc +[1716019704.610932] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace -[1750429767.266572] HB: structure instance for +[1716019704.611211] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace is {| UniformSpace.sort := Qc; @@ -1840,15 +1876,15 @@ UniformSpace.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_46 |} |} -[1750429767.269048] HB: structure instance +[1716019704.613281] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace declared -[1750429767.269822] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc -[1750429767.270038] HB: declare canonical structure instance +[1716019704.613954] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc +[1716019704.614087] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform -[1750429767.270453] HB: Giving name HB_unnamed_mixin_47 to mixin instance +[1716019704.614381] 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 -[1750429767.272186] HB: structure instance for +[1716019704.615748] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform is {| TAddAG_wo_Uniform.sort := Qc; @@ -1860,12 +1896,12 @@ HB_unnamed_mixin_47 |} |} -[1750429767.274605] HB: structure instance +[1716019704.617728] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform declared -[1750429767.275647] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc -[1750429767.275857] HB: declare canonical structure instance +[1716019704.618621] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc +[1716019704.618751] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined -[1750429767.276420] HB: structure instance for +[1716019704.619183] HB: structure instance for Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined is {| Uniform_TAddAG_unjoined.sort := Qc; @@ -1880,18 +1916,18 @@ HB_unnamed_mixin_46 |} |} -[1750429767.278846] HB: structure instance +[1716019704.621253] HB: structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined declared -[1750429767.280470] HB: we can build a Stage11_TAddAG on Qc -[1750429767.280707] HB: declare canonical structure instance +[1716019704.623021] HB: we can build a Stage11_TAddAG on Qc +[1716019704.623165] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG -[1750429767.281247] HB: Giving name HB_unnamed_mixin_48 to mixin instance +[1716019704.623582] 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 -[1750429767.283147] HB: Giving name HB_unnamed_mixin_49 to mixin instance +[1716019704.625224] 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 -[1750429767.285034] HB: structure instance for +[1716019704.626762] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG is {| TAddAG.sort := Qc; @@ -1905,11 +1941,11 @@ TAddAG.Stage11_Join_TAddAG_Uniform_mixin := HB_unnamed_mixin_49 |} |} -[1750429767.287620] HB: structure instance +[1716019704.629478] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG declared entourage : set (set (Qc * Qc)) : set (set (Qc * Qc)) -Finished transaction in 7.328 secs (6.784u,0.108s) (successful) +Finished transaction in 6.502 secs (6.409u,0.092s) (successful) Module Type new_concept_Locked = Sig @@ -2014,12 +2050,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/1196912/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/1196912/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/658974 and its subdirectories -I: Current time: Fri Jun 20 02:29:46 -12 2025 -I: pbuilder-time-stamp: 1750429786 +I: removing directory /srv/workspace/pbuilder/1196912 and its subdirectories +I: Current time: Sat May 18 22:08:42 +14 2024 +I: pbuilder-time-stamp: 1716019722