Diff of the two buildlogs: -- --- b1/build.log 2024-11-23 10:59:35.739989074 +0000 +++ b2/build.log 2024-11-23 11:03:03.662591454 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Fri Nov 22 22:57:38 -12 2024 -I: pbuilder-time-stamp: 1732359458 +I: Current time: Sun Nov 24 00:59:39 +14 2024 +I: pbuilder-time-stamp: 1732359579 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/trixie-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/1569310/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/1489359/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 23 10:59 /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/1489359/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/1489359/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='trixie' - HOME='/root' - HOST_ARCH='arm64' + DIRSTACK=() + DISTRIBUTION=trixie + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=aarch64 + HOST_ARCH=arm64 IFS=' ' - INVOCATION_ID='4f3c7e2a9cff40088078a5842d6daf0e' - 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='1569310' - PS1='# ' - PS2='> ' + INVOCATION_ID=55dc5ecf335a4a94b8947e63b744dcf1 + 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=1489359 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.scoaqEck/pbuilderrc_Ixxx --distribution trixie --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.scoaqEck/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.scoaqEck/pbuilderrc_GRPg --distribution trixie --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.scoaqEck/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 codethink04-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 21:30 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/1569310/tmp/hooks/D02_print_environment finished +I: user script /srv/workspace/pbuilder/1489359/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 trixie/main arm64 libelpi-ocaml-dev arm64 1.18.2-5+b5 [13.8 MB] Get: 87 http://deb.debian.org/debian trixie/main arm64 libcoq-elpi arm64 2.1.0-1+b9 [2911 kB] Get: 88 http://deb.debian.org/debian trixie/main arm64 wdiff arm64 1.2.2-6+b1 [119 kB] -Fetched 377 MB in 3s (149 MB/s) +Fetched 377 MB in 4s (105 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 ... 20087 files and directories currently installed.) @@ -509,8 +541,8 @@ Setting up tzdata (2024b-3) ... Current default time zone: 'Etc/UTC' -Local time is now: Sat Nov 23 10:58:11 UTC 2024. -Universal Time is now: Sat Nov 23 10:58:11 UTC 2024. +Local time is now: Sat Nov 23 11:00:56 UTC 2024. +Universal Time is now: Sat Nov 23 11:00:56 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/1489359/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for trixie +I: user script /srv/workspace/pbuilder/1489359/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 @@ -661,17 +697,8 @@ COQC examples/demo3/hierarchy_0.v COQC examples/demo3/hierarchy_1.v COQC examples/demo3/hierarchy_2.v -COQC examples/demo4/hierarchy_0.v -[1732359512.774532] HB: begin module for builders -[1732359512.781304] HB: begin module Super -[1732359512.781671] HB: ended module Super -[1732359512.785110] HB: postulating factories -[1732359512.785437] HB: processing key context-item -[1732359512.785738] HB: processing mixin parameter a -[1732359512.786166] HB: declaring parameters and key as section variables -Here is the list of mixins to declare (the order matters): [] -[1732359512.875950] HB: start module and section AddComoid_of_Type -[1732359512.881200] HB: converting arguments +[1732359722.462517] HB: start module and section AddComoid_of_Type +[1732359722.475357] HB: converting arguments indt-decl (parameter A explicit X0 c0 \ record AddComoid_of_Type (sort (typ X1)) Build_AddComoid_of_Type @@ -697,19 +724,19 @@ app [global (indt «eq»), X10 c0 c1 c2 c3 c4 c5, app [c2, c1, c5], c5]) c5 \ end-record)) to factories -[1732359512.881678] HB: processing key parameter -[1732359512.882057] HB: converting factories +[1732359722.483073] HB: processing key parameter +[1732359722.483743] HB: converting factories w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] to mixins -[1732359512.882319] HB: declaring context +[1732359722.491054] HB: declaring context w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] -[1732359512.889043] HB: declaring parameters and key as section variables +[1732359722.491473] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1732359512.905174] HB: declare mixin or factory -[1732359512.905278] HB: declare record axioms_ -[1732359513.244776] HB: declare notation Build -[1732359513.285812] HB: declare notation axioms -[1732359513.343848] HB: start module Exports -[1732359513.408473] HB: end modules and sections; export +[1732359722.507279] HB: declare mixin or factory +[1732359722.507627] HB: declare record axioms_ +[1732359723.026874] HB: declare notation Build +[1732359723.081244] HB: declare notation axioms +[1732359723.181243] HB: start module Exports +[1732359723.301490] HB: end modules and sections; export «HB.examples.readme.AddComoid_of_Type.Exports» (* @@ -766,53 +793,54 @@ Notation AddComoid_of_Type X1 := ( AddComoid_of_Type.phant_axioms X1). *) -COQC examples/demo5/hierarchy_0.v -[1732359513.515542] HB: start module AddComoid -[1732359513.515846] HB: declare axioms record +COQC examples/demo4/hierarchy_0.v +[1732359723.436589] HB: start module AddComoid +[1732359723.447338] HB: declare axioms record w-params.nil A (sort (typ «HB.examples.readme.25»)) c0 \ [triple (indt «AddComoid_of_Type.axioms_») [] c0] -[1732359513.516018] HB: typing class field +[1732359723.447831] HB: typing class field indt «AddComoid_of_Type.axioms_» -[1732359513.544037] HB: declare type record -[1732359513.581921] HB: structure: new mixins +[1732359723.481213] HB: declare type record +[1732359723.525665] HB: structure: new mixins [indt «AddComoid_of_Type.axioms_»] -[1732359513.592964] HB: structure: mixin first class +[1732359723.539070] HB: structure: mixin first class [mixin-first-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»)] -[1732359513.593109] HB: declaring clone abbreviation -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] -[1732359513.617852] HB: declaring pack_ constant -[1732359513.618701] HB: declaring pack_ constant = +[1732359723.539457] HB: declaring clone abbreviation +[1732359723.573800] HB: declaring pack_ constant +[1732359723.587945] 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]] -[1732359513.626772] HB: start module Exports -[1732359513.627092] HB: making coercion from type to target -[1732359513.627136] HB: declare sort coercion -[1732359513.627418] HB: exporting unification hints -[1732359513.627533] HB: exporting coercions from class to mixins -[1732359513.627821] HB: export class to mixin coercion for mixin +[1732359723.601208] HB: start module Exports +[1732359723.607487] HB: making coercion from type to target +[1732359723.607819] HB: declare sort coercion +[1732359723.608407] HB: exporting unification hints +[1732359723.615191] HB: exporting coercions from class to mixins +[1732359723.615819] HB: export class to mixin coercion for mixin readme_AddComoid_of_Type -[1732359513.628131] HB: accumulating various props -[1732359513.638365] HB: stop module Exports -[1732359513.647798] HB: declaring on_ abbreviation -[1732359513.663664] HB: declaring `copy` abbreviation -[1732359513.664469] HB: declaring on abbreviation -[1732359514.057940] HB: end modules; export +[1732359723.616562] HB: accumulating various props +[1732359723.637882] HB: stop module Exports +[1732359723.669482] HB: declaring on_ abbreviation +[1732359723.716773] HB: declaring `copy` abbreviation +[1732359723.728186] HB: declaring on abbreviation +[1732359724.130360] HB: begin module for builders +[1732359724.143329] HB: begin module Super +[1732359724.147297] HB: ended module Super +[1732359724.150915] HB: postulating factories +[1732359724.167260] HB: processing key context-item +[1732359724.171327] HB: processing mixin parameter a +[1732359724.171830] HB: declaring parameters and key as section variables +Here is the list of mixins to declare (the order matters): [] +[1732359724.535823] HB: end modules; export «HB.examples.readme.AddComoid.Exports» -[1732359514.059179] HB: exporting operations -[1732359514.060181] HB: export operation zero -[1732359514.075325] HB: export operation add -[1732359514.092272] HB: export operation addrA -[1732359514.108581] HB: export operation addrC -[1732359514.124661] HB: export operation add0r -[1732359514.139855] HB: operations meta-data module: ElpiOperations -[1732359514.174599] HB: abbreviation factory-by-classname +[1732359724.537286] HB: exporting operations +[1732359724.548323] HB: export operation zero +[1732359724.558425] HB: export operation add +[1732359724.570697] HB: export operation addrA +[1732359724.603235] HB: export operation addrC +[1732359724.624425] HB: export operation add0r +[1732359724.628483] HB: operations meta-data module: ElpiOperations +[1732359724.699195] HB: abbreviation factory-by-classname (* Module AddComoid. @@ -909,23 +937,8 @@ *) forall (M : AddComoid.type) (x : M), x + x = 0 : Prop -[1732359514.256610] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_AddAG_of_AddComoid -[1732359514.261003] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_Ring_of_AddAG +COQC examples/demo5/hierarchy_0.v COQC examples/FSCD2020_material/V1.v -inhab - : ?s -where -?T : [ |- Type] -?s : [ |- s1.type ?T] -eq_refl : inhab = 7 - : inhab = 7 -eq_refl : inhab = (7 :: nil)%list - : inhab = (7 :: nil)%list -where -?T : [ |- Type] -COQC examples/FSCD2020_material/V2.v AbelianGrp.phant_on_ BinNums_Z__canonical__readme_AbelianGrp (Phant BinNums_Z__canonical__readme_AbelianGrp) : @@ -937,26 +950,51 @@ - AddComoid (from "./examples/readme.v", line 31) +File "./examples/demo1/hierarchy_2.v", line 57, characters 0-57: +Warning: +pulling in dependencies: +[hierarchy_2_AddComoid_of_TYPE, hierarchy_2_AddAG_of_AddComoid] + +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB,elpi,default] +COQC examples/FSCD2020_material/V2.v COQC examples/FSCD2020_material/V3.v +inhab + : ?s +where +?T : [ |- Type] +?s : [ |- s1.type ?T] COQC examples/FSCD2020_material/V4.v -COQC examples/FSCD2020_talk/V1.v -fun X : s2.type nat => inhab : X - : forall X : s2.type nat, X -fun X : s2.type nat => inj : nat -> X - : forall X : s2.type nat, nat -> X -s2_to_s1 not a defined object. -COQC examples/FSCD2020_talk/V2.v +eq_refl : inhab = 7 + : inhab = 7 +eq_refl : inhab = (7 :: nil)%list + : inhab = (7 :: nil)%list +where +?T : [ |- Type] 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] +[1732359728.594605] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_AddAG_of_AddComoid +[1732359728.615082] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_Ring_of_AddAG HB: A is canonically equipped with structures: - Equality Singleton (from "./examples/hulk.v", line 216) +fun X : s2.type nat => inhab : X + : forall X : s2.type nat, X +fun X : s2.type nat => inj : nat -> X + : forall X : s2.type nat, nat -> X +s2_to_s1 not a defined object. +COQC examples/FSCD2020_talk/V1.v +COQC examples/FSCD2020_talk/V2.v +COQC examples/FSCD2020_talk/V3.v +COQC examples/Coq2020_material/CoqWS_demo.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -964,7 +1002,7 @@ : forall s : Monoid.type, s -> s -> s @addNr : forall s : Ring.type, left_inverse 0 opp add -COQC examples/FSCD2020_talk/V3.v +COQC examples/Coq2020_material/CoqWS_abstract.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -974,8 +1012,6 @@ : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add -COQC examples/Coq2020_material/CoqWS_demo.v -COQC examples/Coq2020_material/CoqWS_abstract.v COQC examples/Coq2020_material/CoqWS_expansion/withHB.v COQC examples/Coq2020_material/CoqWS_expansion/withoutHB.v COQC tests/type_of_exported_ops.v @@ -985,7 +1021,6 @@ Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] -COQC tests/duplicate_structure.v HB.check: SemiRing_of_AddComoid.axioms_ : @@ -994,8 +1029,7 @@ : 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 +COQC tests/duplicate_structure.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -1005,11 +1039,8 @@ : 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 -COQC tests/exports.v +COQC tests/instance_params_no_type.v +COQC tests/test_CS_db_filtering.v add : ?s -> ?s -> ?s where @@ -1018,87 +1049,36 @@ : commutative add where ?s : [ |- CMonoid.type] +File "./examples/Coq2020_material/CoqWS_expansion/withoutHB.v", line 10, characters 50-62: +Warning: The format modifier has no effect for only-parsing notations. +[discarded-format-only-parsing,parsing,default] +COQC tests/subtype.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] -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 +COQC tests/exports.v forall x y : ?t, x - (y + 0) = x : Prop where ?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) +COQC tests/log_impargs_record.v addrC : commutative add where ?s : [ |- CMonoid.type] -COQC tests/log_impargs_record.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' -COQC tests/compress_coe.v -nat_foo - : forall P : Type, is_foo.axioms_ P nat -list_foo - : forall P : Type, is_foo.axioms_ P (list P) +forall x y : ?t, 1 + x = y * x + : Prop +where +?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) File "./examples/Coq2020_material/CoqWS_abstract.v", line 23, characters 0-71: 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/funclass.v -forall x y : ?t, 1 + x = y * x - : Prop -where -?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) -foo.type - : Type -> Type -Record type (P : Type) : Type := Pack - { sort : Type; class : foo.axioms_ P sort }. - -Arguments foo.type P%type_scope -Arguments foo.Pack (P sort)%type_scope class -Module -foo -:= Struct - Record axioms_ (P A : Type) : Type := Class - { instance_params_no_type_is_foo_mixin : is_foo.axioms_ P A }. - Definition instance_params_no_type_is_foo_mixin : - forall P A : Type, axioms_ P A -> is_foo.axioms_ P A. - Record type (P : Type) : Type := Pack - { sort : Type; class : axioms_ P sort }. - Definition sort : forall P : Type, type P -> Type. - Definition class : - forall (P : Type) (record : type P), axioms_ P record. - Definition phant_clone : - forall (P A : Type) (cT : type P) (c : axioms_ P A), - unify Type Type A cT nomsg -> - unify (type P) (type P) cT {| sort := A; class := c |} nomsg -> type P. - Definition pack_ : forall P A : Type, is_foo.axioms_ P A -> type P. - Module Exports - Definition phant_on_ : - forall (P : Type) (A : type P), ssreflect.phant A -> axioms_ P A. - End - -Record axioms_ (P A : Type) : Type := Class - { instance_params_no_type_is_foo_mixin : is_foo.axioms_ P A }. - -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 forall (R : Ring.type) (x y : R), 1 * x = y - x : Prop forall @@ -1109,15 +1089,10 @@ ?t : [x : join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing ?t y : ?t |- Ring.type] (x, y cannot be used) -COQC tests/grefclass.v +COQC tests/compress_coe.v +COQC tests/funclass.v forall x : Z, x * - (1 + x) = 0 + 1 : Prop -COQC tests/local_instance.v -add - : A -> A -> A -list_bar - : forall P : b.type, is_bar.axioms_ P (list P) -COQC tests/lock.v (* Module A. @@ -1166,31 +1141,96 @@ Notation A X1 := ( A.phant_axioms X1). *) +add + : A -> A -> A +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 +list_foo' : forall P A : Type, is_foo.axioms_ P (list A) + +list_foo' is not universe polymorphic +Arguments list_foo' (P A)%type_scope +list_foo' is transparent +Expands to: Constant HB.tests.instance_params_no_type.list_foo' +COQC tests/grefclass.v +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 +COQC tests/local_instance.v +COQC tests/lock.v +nat_foo + : forall P : Type, is_foo.axioms_ P nat +list_foo + : forall P : Type, is_foo.axioms_ P (list P) forall x : Z, x * - (1 + x) = 0 + 1 : Prop COQC tests/interleave_context.v +foo.type + : Type -> Type +Record type (P : Type) : Type := Pack + { sort : Type; class : foo.axioms_ P sort }. + +Arguments foo.type P%type_scope +Arguments foo.Pack (P sort)%type_scope class +Module +foo +:= Struct + Record axioms_ (P A : Type) : Type := Class + { instance_params_no_type_is_foo_mixin : is_foo.axioms_ P A }. + Definition instance_params_no_type_is_foo_mixin : + forall P A : Type, axioms_ P A -> is_foo.axioms_ P A. + Record type (P : Type) : Type := Pack + { sort : Type; class : axioms_ P sort }. + Definition sort : forall P : Type, type P -> Type. + Definition class : + forall (P : Type) (record : type P), axioms_ P record. + Definition phant_clone : + forall (P A : Type) (cT : type P) (c : axioms_ P A), + unify Type Type A cT nomsg -> + unify (type P) (type P) cT {| sort := A; class := c |} nomsg -> type P. + Definition pack_ : forall P A : Type, is_foo.axioms_ P A -> type P. + Module Exports + Definition phant_on_ : + forall (P : Type) (A : type P), ssreflect.phant A -> axioms_ P A. + End + +Record axioms_ (P A : Type) : Type := Class + { instance_params_no_type_is_foo_mixin : is_foo.axioms_ P A }. + +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 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/not_same_key.v -[1732359523.612873] HB: start module SubInhab -[1732359523.621301] HB: declare axioms record +[1732359739.342666] HB: start module SubInhab +[1732359739.351291] 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] -[1732359523.621633] HB: typing class field indt «is_inhab.axioms_» -[1732359523.621925] HB: typing class field indt «is_SUB.axioms_» -[1732359523.628770] HB: declare type record -[1732359523.659997] HB: structure: new mixins [] -[1732359523.668968] HB: structure: mixin first class [] -[1732359523.669237] HB: declaring clone abbreviation -[1732359523.676078] HB: declaring pack_ constant -[1732359523.690262] HB: declaring pack_ constant = +[1732359739.351877] HB: typing class field indt «is_inhab.axioms_» +[1732359739.359373] HB: typing class field indt «is_SUB.axioms_» +[1732359739.379330] HB: declare type record +[1732359739.403456] HB: structure: new mixins [] +[1732359739.403758] HB: structure: mixin first class [] +[1732359739.403870] HB: declaring clone abbreviation +[1732359739.427647] HB: declaring pack_ constant +[1732359739.429392] 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 \ @@ -1199,142 +1239,115 @@ app [global (indc «Pack»), c0, c1, c2, app [global (indc «Class»), c0, c1, c2, c3, c4]] -[1732359523.698547] HB: start module Exports -[1732359523.699047] HB: making coercion from type to target -[1732359523.699224] HB: declare sort coercion -[1732359523.699566] HB: exporting unification hints -[1732359523.700278] HB: declare coercion subtype_SubInhab__to__subtype_SUB -[1732359523.705866] HB: declare coercion hint +[1732359739.431639] HB: start module Exports +[1732359739.439314] HB: making coercion from type to target +[1732359739.439631] HB: declare sort coercion +[1732359739.440038] HB: exporting unification hints +[1732359739.440849] HB: declare coercion subtype_SubInhab__to__subtype_SUB +[1732359739.447956] HB: declare coercion hint subtype_SubInhab_class__to__subtype_SUB_class -[1732359523.712033] HB: declare unification hint +[1732359739.467067] HB: declare unification hint subtype_SubInhab__to__subtype_SUB -[1732359523.735968] HB: declare coercion subtype_SubInhab__to__subtype_Inhab -p : pred nat - : pred nat -[1732359523.745775] HB: declare coercion hint +[1732359739.491583] HB: declare coercion subtype_SubInhab__to__subtype_Inhab +[1732359739.492745] HB: declare coercion hint subtype_SubInhab_class__to__subtype_Inhab_class -[1732359523.752205] HB: declare unification hint +[1732359739.515857] HB: declare unification hint subtype_SubInhab__to__subtype_Inhab +[1732359739.538882] HB: declare unification hint +join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB forall x : Z, x * - (1 + x) = 0 + 1 : Prop -[1732359523.785043] HB: declare unification hint -join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB -COQC tests/hb_pack.v -[1732359523.804865] HB: exporting under the module path [] -[1732359523.807848] HB: exporting coercions from class to mixins -[1732359523.809130] HB: exporting modules -[Ring_of_TYPE.Exports, Ring.Exports, RingElpiOperations, RingExports, - Dummy.Exports, URing.Exports, URingElpiOperations, dummy.Exports, - Builders_1.Builders_Export_5] -[1732359523.810685] HB: exporting CS instances -[«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] -[1732359523.811318] HB: exporting Abbreviations [addr0, addrNK] -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 -[1732359523.817450] HB: export class to mixin coercion for mixin +[1732359739.565432] HB: exporting coercions from class to mixins +[1732359739.571592] HB: export class to mixin coercion for mixin subtype_is_inhab -[1732359523.818725] HB: export class to mixin coercion for mixin +[1732359739.579645] HB: export class to mixin coercion for mixin subtype_is_SUB -[1732359523.819604] HB: accumulating various props -forall (R : Enclosing.Ring.type) (x : R), x = x - : Prop -0%G - : ?s -where -?s : [ |- Enclosing.Ring.type] -Enclosing.zero : Z - : Z -COQC tests/declare.v -[1732359523.881240] HB: stop module Exports -[1732359523.890749] HB: declaring on_ abbreviation -[1732359523.902316] HB: declaring `copy` abbreviation -[1732359523.910095] HB: declaring on abbreviation -[1732359523.915398] HB: end modules; export +[1732359739.580817] HB: accumulating various props +[1732359739.640225] HB: stop module Exports +COQC tests/not_same_key.v +[1732359739.650291] HB: declaring on_ abbreviation +[1732359739.675222] HB: declaring `copy` abbreviation +[1732359739.676729] HB: declaring on abbreviation +[1732359739.682387] HB: end modules; export «HB.tests.subtype.SubInhab.Exports» -[1732359523.923350] HB: exporting operations -[1732359523.923844] HB: operations meta-data module: ElpiOperations -[1732359523.933289] HB: abbreviation factory-by-classname +[1732359739.689633] HB: exporting operations +[1732359739.693804] HB: operations meta-data module: ElpiOperations +[1732359739.708231] HB: abbreviation factory-by-classname +list_bar + : forall P : b.type, is_bar.axioms_ P (list P) +COQC tests/hb_pack.v +COQC tests/declare.v +p : pred nat + : pred nat COQC tests/short.v -COQC tests/instance_before_structure.v -Notation big := big.body -Expands to: Notation HB.tests.lock.X.big -COQC tests/primitive_records.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/non_forgetful_inheritance.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/fix_loop.v +Notation big := big.body +Expands to: Notation HB.tests.lock.X.big +COQC tests/instance_before_structure.v Monoid.phant_on_ nat Nat_add__canonical__funclass_Monoid (Phantom (nat -> nat -> nat) Nat_add__canonical__funclass_Monoid) : Monoid.axioms_ nat Init.Nat.add : Monoid.axioms_ nat Init.Nat.add -COQC tests/test_synthesis_params.v -[1732359525.223967] HB: start module and section hasA -[1732359525.229180] HB: converting arguments +default : nat + : nat +COQC tests/primitive_records.v +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/non_forgetful_inheritance.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 +[1732359741.640674] HB: start module and section hasA +[1732359741.641440] 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 -[1732359525.229529] HB: processing key parameter -[1732359525.229990] HB: converting factories +[1732359741.641786] HB: processing key parameter +[1732359741.642398] HB: converting factories w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins -[1732359525.230196] HB: declaring context +[1732359741.642705] HB: declaring context w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] -[1732359525.230483] HB: declaring parameters and key as section variables +[1732359741.642931] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1732359525.241128] HB: declare mixin or factory -[1732359525.241392] HB: declare record axioms_ -[1732359525.260323] HB: declare notation Build -[1732359525.270675] HB: declare notation axioms -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 -[1732359525.296654] HB: start module Exports -[1732359525.323108] HB: end modules and sections; export +[1732359741.649225] HB: declare mixin or factory +[1732359741.649549] HB: declare record axioms_ +[1732359741.662284] HB: declare notation Build +[1732359741.669789] HB: declare notation axioms +[1732359741.683338] HB: start module Exports +[1732359741.699793] HB: end modules and sections; export «HB.tests.hb_pack.hasA.Exports» hasA.type not a defined object. +[1732359741.859593] HB: exporting under the module path [] +[1732359741.860035] HB: exporting modules +[Ring_of_TYPE.Exports, Ring.Exports, RingElpiOperations, RingExports, + Dummy.Exports, URing.Exports, URingElpiOperations, dummy.Exports, + Builders_1.Builders_Export_5] +[1732359741.861801] HB: exporting CS instances +[«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] +[1732359741.863586] HB: exporting Abbreviations [addr0, addrNK] +forall (R : Enclosing.Ring.type) (x : R), x = x + : Prop +0%G + : ?s +where +?s : [ |- Enclosing.Ring.type] +Enclosing.zero : Z + : Z +COQC tests/fix_loop.v +COQC tests/test_synthesis_params.v HB.check: forall w : wp.type nat Init.Nat.mul, w = w : Prop -aType - : Type COQC tests/hnf.v hasB.type not a defined object. -hasB.type not a defined object. -File "./tests/interleave_context.v", line 16, characters 0-52: -Warning: -pulling in dependencies: [interleave_context_HasA, interleave_context_HasB] - -Please list them or end the declaration with '&' -[HB.implicit-structure-dependency,HB,elpi,default] -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) - -COQC tests/fun_instance.v -HB: nat is canonically equipped with structures: - - s1 - (from "./tests/instance_before_structure.v", line 11) - -hasAB.type not a defined object. Datatypes_prod__canonical__compress_coe_D = fun D D' : D.type => {| @@ -1356,35 +1369,52 @@ : D.type -> D.type -> D.type Arguments Datatypes_prod__canonical__compress_coe_D D D' +COQC tests/fun_instance.v +aType + : Type +hasB.type not a defined object. +File "./tests/interleave_context.v", line 16, characters 0-52: +Warning: +pulling in dependencies: [interleave_context_HasA, interleave_context_HasB] + +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB,elpi,default] +Query assignments: + Ind = «hasA.axioms_» +hasAB.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) -COQC tests/issue284.v +COQC tests/issue287.v hasA'.type not a defined object. +COQC tests/two_hier.v 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 -COQC tests/two_hier.v -Query assignments: - Ind = «hasA.axioms_» -COQC tests/instance_merge_with_param.v hasAB.type not a defined object. File "./tests/non_forgetful_inheritance.v", line 35, characters 0-45: Warning: Could not enable unknown warning HB.non-forgetful-inheritance [unknown-warning,default] -hasA'.type not a defined object. +HB: nat is canonically equipped with structures: + - s1 + (from "./tests/instance_before_structure.v", line 11) + +forall T : AB.type, +unkeyed + {| + 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 Debug: elpi lets escape exception: non forgetful inheritance detected. You have two solutions: @@ -1400,36 +1430,50 @@ 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 - {| - 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/instance_merge_with_distinct_param.v +hasA'.type not a defined object. AB1 : hasB.phant_axioms A -> AB.type : hasB.phant_axioms A -> AB.type -Query assignments: - Ind = «A.axioms_» 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) + +COQC tests/instance_merge_with_param.v pB : T * T : T * T AB3 : AB.type : AB.type +HB: nat is canonically equipped with structures: + - s3 + s2 + (from "./tests/instance_before_structure.v", line 30) + - s1 + (from "./tests/instance_before_structure.v", line 11) + +default1 + : nat +default2 + : nat +default3 + : nat +COQC tests/instance_merge_with_distinct_param.v +COQC tests/instance_merge.v +Query assignments: + Ind = «A.axioms_» +COQC tests/unit/enrich_type.v +COQC tests/unit/mixin_src_has_mixin_instance.v +COQC tests/unit/mk_src_map.v +X : Foo.type A P + : Foo.type A P +Query assignments: + Ind = «A.type» Datatypes_nat__canonical__hnf_S = {| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_8 |} |} : S.type @@ -1442,16 +1486,17 @@ HB_unnamed_mixin_12 = Builders_1.HB_unnamed_factory_3 bool HB_unnamed_factory_9 : M.axioms_ bool -COQC tests/instance_merge.v -COQC tests/unit/enrich_type.v -Query assignments: - Ind = «A.type» -COQC tests/unit/mixin_src_has_mixin_instance.v -COQC tests/unit/mk_src_map.v COQC tests/unit/close_hole_term.v -X : Foo.type A P - : Foo.type A P +T : Fun.type nat + : Fun.type nat COQC tests/unit/struct.v +erefl ?t : ?t = ?t + : ?t = ?t +where +?t : [ |- Sq.type] +COQC tests/factory_when_notation.v +COQC examples/demo1/test_0_0.v +COQC examples/demo1/test_1_0.v nat : s3.type : s3.type list nat : s3.type @@ -1460,24 +1505,6 @@ : s3.type fun t : s3.type => list t : s3.type : s3.type -> s3.type -COQC tests/factory_when_notation.v -T : Fun.type nat - : Fun.type nat -COQC examples/demo1/test_0_0.v -erefl ?t : ?t = ?t - : ?t = ?t -where -?t : [ |- Sq.type] -COQC examples/demo1/test_1_0.v -nat : s3'.type Datatypes_nat__canonical__two_hier_s3 - : s3'.type Datatypes_nat__canonical__two_hier_s3 -list nat : s3'.type Datatypes_nat__canonical__two_hier_s3 - : s3'.type Datatypes_nat__canonical__two_hier_s3 -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_2_0.v HB: list is canonically equipped with structures: - s2 (from "./tests/instance_merge_with_param.v", line 12) @@ -1492,11 +1519,20 @@ - s1 (from "./tests/instance_merge_with_param.v", line 10) -COQC examples/demo1/test_3_0.v list_foo' : forall P A : Type, is_foo.axioms_ P (list A) list_foo : forall P : Type, is_foo.axioms_ P (list P) +COQC examples/demo1/test_2_0.v +nat : s3'.type Datatypes_nat__canonical__two_hier_s3 + : s3'.type Datatypes_nat__canonical__two_hier_s3 +list nat : s3'.type Datatypes_nat__canonical__two_hier_s3 + : s3'.type Datatypes_nat__canonical__two_hier_s3 +Datatypes_list__canonical__two_hier_s3' + : forall x : s3.type, s3'.type x -> s3'.type x +list (list nat) : s3'.type Datatypes_nat__canonical__two_hier_s3 + : s3'.type Datatypes_nat__canonical__two_hier_s3 +COQC examples/demo1/test_3_0.v Query assignments: X = global (indt «nat») COQC examples/demo1/test_3_3.v @@ -1510,6 +1546,10 @@ fun t : s3.type => list t : s3.type : s3.type -> s3.type COQC examples/demo1/test_4_3.v +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 Query assignments: X = app [global (indt «list»), X0] @@ -1536,6 +1576,11 @@ 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: X = app [global (indt «list»), X0] Y = X0 Universe constraints: @@ -1552,26 +1597,28 @@ WEAK CONSTRAINTS: -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_3.v Query assignments: - Z = global (indt «nat») -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/demo2/stage10.v -COQC examples/demo2/stage11.v -Query assignments: M1 = const «m1.phant_axioms» Y = has-mixin-instance (cs-gref (indt «list»)) (const «m1.phant_axioms») (const «i1») +COQC examples/demo2/stage10.v +COQC examples/demo2/stage11.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 +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] COQC examples/demo3/test_0_0.v -COQC examples/demo3/test_1_0.v Query assignments: C = X0 X = app @@ -1611,16 +1658,52 @@ WEAK CONSTRAINTS: +COQC examples/demo3/test_1_0.v +Query assignments: + Z = global (indt «nat») COQC examples/demo3/test_2_0.v +COQC tests/exports2.v +File "./examples/demo2/stage11.v", line 3, characters 0-25: +Warning: Hiding binding of key Q to Q_scope +[hiding-delimiting-key,parsing,default] 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) + A = X0 + B = X1 + F = X2 + Inj = «Inj» + R = X3 + S = X4 + X = app [global (const «Inj»), X0, X1, X3, X4, X2] + _uvk_10_ = X1 + _uvk_9_ = X0 +Syntactic constraints: + evar (X1) (sort (typ «HB.tests.unit.enrich_type.16»)) (X1) /* suspended on X1 */ + evar (X0) (sort (typ «HB.tests.unit.enrich_type.15»)) (X0) /* suspended on X0 */ +Universe constraints: +UNIVERSES: + {HB.tests.unit.enrich_type.16 HB.tests.unit.enrich_type.15 + HB.tests.unit.enrich_type.14 HB.tests.unit.enrich_type.13} |= + HB.tests.unit.enrich_type.15 < HB.tests.unit.enrich_type.13 + HB.tests.unit.enrich_type.16 < HB.tests.unit.enrich_type.14 + HB.tests.unit.enrich_type.15 <= Inj.u0 + HB.tests.unit.enrich_type.16 <= Inj.u1 +ALGEBRAIC UNIVERSES: + {} +FLEXIBLE UNIVERSES: + +SORTS: + α7 := Type + α8 := Type +WEAK CONSTRAINTS: + -Arguments struct_foo1__to__struct_foo s -struct_foo1__to__struct_foo is a reversible coercion -COQC tests/exports2.v +[1732359750.748276] HB: exporting under the module path [] +[1732359750.748539] HB: exporting modules [] +[1732359750.748620] HB: exporting CS instances [] +[1732359750.748695] HB: exporting Abbreviations [] +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: X = app [global (const «Inj»), X0, X1, X2, X3, X4] Y = app [global (const «Inj»), X0, X1] @@ -1674,54 +1757,7 @@ WEAK CONSTRAINTS: -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] -File "./examples/demo2/stage10.v", line 4, characters 0-25: -Warning: Hiding binding of key Q to Q_scope -[hiding-delimiting-key,parsing,default] -[1732359533.786677] HB: exporting under the module path [] -[1732359533.786879] HB: exporting modules [] -[1732359533.786941] HB: exporting CS instances [] -[1732359533.787001] HB: exporting Abbreviations [] -Query assignments: - A = X0 - B = X1 - F = X2 - Inj = «Inj» - R = X3 - S = X4 - X = app [global (const «Inj»), X0, X1, X3, X4, X2] - _uvk_10_ = X1 - _uvk_9_ = X0 -Syntactic constraints: - evar (X1) (sort (typ «HB.tests.unit.enrich_type.16»)) (X1) /* suspended on X1 */ - evar (X0) (sort (typ «HB.tests.unit.enrich_type.15»)) (X0) /* suspended on X0 */ -Universe constraints: -UNIVERSES: - {HB.tests.unit.enrich_type.16 HB.tests.unit.enrich_type.15 - HB.tests.unit.enrich_type.14 HB.tests.unit.enrich_type.13} |= - HB.tests.unit.enrich_type.15 < HB.tests.unit.enrich_type.13 - HB.tests.unit.enrich_type.16 < HB.tests.unit.enrich_type.14 - HB.tests.unit.enrich_type.15 <= Inj.u0 - HB.tests.unit.enrich_type.16 <= Inj.u1 -ALGEBRAIC UNIVERSES: - {} -FLEXIBLE UNIVERSES: - -SORTS: - α7 := Type - α8 := Type -WEAK CONSTRAINTS: - - -File "./examples/demo2/stage11.v", line 3, characters 0-25: -Warning: Hiding binding of key Q to Q_scope -[hiding-delimiting-key,parsing,default] -Finished transaction in 18.467 secs (9.312u,0.601s) (successful) +Finished transaction in 23.527 secs (10.452u,0.705s) (successful) Finished transaction in 0. secs (0.u,0.s) (successful) Qcplus_opp_r: forall q : Qc, q + - q = Q2Qc 0 File "./examples/demo2/stage10.v", line 233, characters 0-27: @@ -1747,30 +1783,30 @@ disable this warning. [deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] HB: skipping section opening -[1732359539.544082] HB: declare mixin instance +[1732359755.564967] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology -[1732359539.547017] HB: declare canonical mixin instance +[1732359755.567660] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology» -[1732359539.548616] HB: declare mixin instance +[1732359755.568970] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform -[1732359539.572675] HB: declare canonical mixin instance +[1732359755.592552] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform» -[1732359539.575793] HB: declare mixin instance +[1732359755.593927] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology -[1732359539.580396] HB: declare canonical mixin instance +[1732359755.598347] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology» -[1732359539.582294] HB: declare mixin instance +[1732359755.599626] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform -[1732359539.587074] HB: declare canonical mixin instance +[1732359755.603285] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform» -[1732359539.589387] HB: we can build a Stage11_UniformSpace_wo_Topology on +[1732359755.605273] HB: we can build a Stage11_UniformSpace_wo_Topology on Qc -[1732359539.590395] HB: declare canonical structure instance +[1732359755.605551] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology -[1732359539.590860] HB: Giving name HB_unnamed_mixin_46 to mixin instance +[1732359755.605828] 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 -[1732359539.593616] HB: structure instance for +[1732359755.608394] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology is {| UniformSpace_wo_Topology.sort := Qc; @@ -1780,12 +1816,12 @@ HB_unnamed_mixin_46 |} |} -[1732359539.597424] HB: structure instance +[1732359755.612088] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology declared -[1732359539.598616] HB: we can build a Stage11_UniformSpace on Qc -[1732359539.599053] HB: declare canonical structure instance +[1732359755.613218] HB: we can build a Stage11_UniformSpace on Qc +[1732359755.613468] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace -[1732359539.599590] HB: structure instance for +[1732359755.613877] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace is {| UniformSpace.sort := Qc; @@ -1795,15 +1831,15 @@ UniformSpace.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_46 |} |} -[1732359539.603379] HB: structure instance +[1732359755.617636] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace declared -[1732359539.604773] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc -[1732359539.605051] HB: declare canonical structure instance +[1732359755.618802] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc +[1732359755.619072] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform -[1732359539.605550] HB: Giving name HB_unnamed_mixin_47 to mixin instance +[1732359755.619597] 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 -[1732359539.608093] HB: structure instance for +[1732359755.622263] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform is {| TAddAG_wo_Uniform.sort := Qc; @@ -1815,12 +1851,12 @@ HB_unnamed_mixin_47 |} |} -[1732359539.611971] HB: structure instance +[1732359755.626040] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform declared -[1732359539.613810] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc -[1732359539.614263] HB: declare canonical structure instance +[1732359755.627641] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc +[1732359755.627892] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined -[1732359539.615048] HB: structure instance for +[1732359755.628577] HB: structure instance for Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined is {| Uniform_TAddAG_unjoined.sort := Qc; @@ -1835,18 +1871,18 @@ HB_unnamed_mixin_46 |} |} -[1732359539.619029] HB: structure instance +[1732359755.632401] HB: structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined declared -[1732359539.621766] HB: we can build a Stage11_TAddAG on Qc -[1732359539.622206] HB: declare canonical structure instance +[1732359755.634810] HB: we can build a Stage11_TAddAG on Qc +[1732359755.635098] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG -[1732359539.622975] HB: Giving name HB_unnamed_mixin_48 to mixin instance +[1732359755.635762] 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 -[1732359539.626320] HB: Giving name HB_unnamed_mixin_49 to mixin instance +[1732359755.638836] 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 -[1732359539.629855] HB: structure instance for +[1732359755.641832] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG is {| TAddAG.sort := Qc; @@ -1860,11 +1896,11 @@ TAddAG.Stage11_Join_TAddAG_Uniform_mixin := HB_unnamed_mixin_49 |} |} -[1732359539.634115] HB: structure instance +[1732359755.645918] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG declared entourage : set (set (Qc * Qc)) : set (set (Qc * Qc)) -Finished transaction in 12.759 secs (9.899u,0.36s) (successful) +Finished transaction in 10.5 secs (10.021u,0.477s) (successful) Module Type new_concept_Locked = Sig @@ -1969,12 +2005,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/1489359/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/1489359/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/1569310 and its subdirectories -I: Current time: Fri Nov 22 22:59:34 -12 2024 -I: pbuilder-time-stamp: 1732359574 +I: removing directory /srv/workspace/pbuilder/1489359 and its subdirectories +I: Current time: Sun Nov 24 01:03:02 +14 2024 +I: pbuilder-time-stamp: 1732359782