Diff of the two buildlogs: -- --- b1/build.log 2024-12-19 00:30:12.944775681 +0000 +++ b2/build.log 2024-12-19 00:32:50.049652975 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Wed Dec 18 12:26:35 -12 2024 -I: pbuilder-time-stamp: 1734567995 +I: Current time: Wed Jan 21 20:53:14 +14 2026 +I: pbuilder-time-stamp: 1768978394 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/unstable-reproducible-base.tgz] I: copying local configuration @@ -26,52 +26,84 @@ dpkg-source: info: unpacking coq-hierarchy-builder_1.8.0-1.debian.tar.xz I: Not using root during the build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/2728966/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/3960371/tmp/hooks/D01_modify_environment starting +debug: Running on ionos15-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 Jan 21 06:53 /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/3960371/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/3960371/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' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=20 ' - DISTRIBUTION='unstable' - HOME='/root' - HOST_ARCH='amd64' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:. + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="2" [2]="37" [3]="1" [4]="release" [5]="x86_64-pc-linux-gnu") + BASH_VERSION='5.2.37(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=amd64 + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=42 ' + 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='419859a16ab54e4cafcb006090b52722' - 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='2728966' - PS1='# ' - PS2='> ' + INVOCATION_ID=c96cfd12a7eb460d80cbbc7dc0da7a9d + 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=3960371 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.Rr9JAfhm/pbuilderrc_T4nX --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.Rr9JAfhm/b1 --logfile b1/build.log coq-hierarchy-builder_1.8.0-1.dsc' - SUDO_GID='110' - SUDO_UID='105' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://46.16.76.132: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.Rr9JAfhm/pbuilderrc_Bp3a --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.Rr9JAfhm/b2 --logfile b2/build.log coq-hierarchy-builder_1.8.0-1.dsc' + SUDO_GID=111 + SUDO_UID=106 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://213.165.73.152:3128 I: uname -a - Linux ionos1-amd64 6.1.0-28-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.119-1 (2024-11-22) x86_64 GNU/Linux + Linux i-capture-the-hostname 6.11.5+bpo-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.11.5-1~bpo12+1 (2024-11-11) x86_64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Nov 22 14:40 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/2728966/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Nov 22 2024 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/3960371/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -278,7 +310,7 @@ Get: 86 http://deb.debian.org/debian unstable/main amd64 libelpi-ocaml-dev amd64 2.0.5-1 [15.3 MB] Get: 87 http://deb.debian.org/debian unstable/main amd64 libcoq-elpi amd64 2.3.0-1 [11.8 MB] Get: 88 http://deb.debian.org/debian unstable/main amd64 wdiff amd64 1.2.2-6 [119 kB] -Fetched 373 MB in 13s (29.0 MB/s) +Fetched 373 MB in 15s (25.7 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libpython3.12-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 ... 19967 files and directories currently installed.) @@ -580,8 +612,8 @@ Setting up tzdata (2024b-4) ... Current default time zone: 'Etc/UTC' -Local time is now: Thu Dec 19 00:28:31 UTC 2024. -Universal Time is now: Thu Dec 19 00:28:31 UTC 2024. +Local time is now: Wed Jan 21 06:54:39 UTC 2026. +Universal Time is now: Wed Jan 21 06:54:39 UTC 2026. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up autotools-dev (20220109.1) ... @@ -659,7 +691,11 @@ Building tag database... -> Finished parsing the build-deps I: Building the package -I: Running cd /build/reproducible-path/coq-hierarchy-builder-1.8.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.8.0-1_source.changes +I: user script /srv/workspace/pbuilder/3960371/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for unstable +I: user script /srv/workspace/pbuilder/3960371/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/coq-hierarchy-builder-1.8.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.8.0-1_source.changes dpkg-buildpackage: info: source package coq-hierarchy-builder dpkg-buildpackage: info: source version 1.8.0-1 dpkg-buildpackage: info: source distribution unstable @@ -688,7 +724,7 @@ dh_ocamlinit dh_auto_configure dh_auto_build - make -j20 "INSTALL=install --strip-program=true" + make -j42 "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.8.0' make config make[2]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.8.0' @@ -721,52 +757,200 @@ COQC examples/demo1/hierarchy_4.v COQC examples/demo1/hierarchy_5.v COQC examples/demo2/classical.v -COQC examples/demo3/hierarchy_1.v COQC examples/demo3/hierarchy_0.v +COQC examples/demo3/hierarchy_1.v COQC examples/demo3/hierarchy_2.v COQC examples/demo4/hierarchy_0.v COQC examples/demo5/hierarchy_0.v COQC examples/FSCD2020_material/V1.v COQC examples/FSCD2020_material/V2.v COQC examples/FSCD2020_material/V3.v -COQC examples/FSCD2020_material/V4.v COQC examples/FSCD2020_talk/V1.v +COQC examples/FSCD2020_material/V4.v +COQC examples/FSCD2020_talk/V3.v COQC examples/FSCD2020_talk/V2.v -File "./examples/demo1/hierarchy_5.v", line 39, characters 2-97: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] +COQC examples/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 +COQC tests/duplicate_structure.v +COQC tests/instance_params_no_type.v +COQC tests/subtype.v +COQC tests/test_CS_db_filtering.v +COQC tests/exports.v +COQC tests/log_impargs_record.v +COQC tests/compress_coe.v +COQC tests/funclass.v +COQC tests/grefclass.v +COQC tests/local_instance.v +COQC tests/lock.v +COQC tests/interleave_context.v +COQC tests/not_same_key.v +COQC tests/hb_pack.v +COQC tests/declare.v +COQC tests/short.v File "./examples/demo2/classical.v", line 422, characters 0-39: Warning: Notations "_ ^~ _" defined at level 10 with arguments constr at next level and "_ ^~" defined at level 2 with arguments constr at next level have incompatible prefixes. One of them will likely not work. [notation-incompatible-prefix,parsing,default] -[1734568131.509644] HB: begin module for builders -[1734568131.510354] HB: begin module Super -[1734568131.510584] HB: ended module Super -[1734568131.511804] HB: postulating factories -[1734568131.512098] HB: processing key context-item -[1734568131.513012] HB: processing mixin parameter a -[1734568131.513904] HB: declaring parameters and key as section variables -Here is the list of mixins to declare (the order matters): [] +Notation big := big.body +Expands to: Notation HB.tests.lock.X.big + +big.body : forall R I : Type, R -> list I -> (I -> bigbody R I) -> R + +big.body is not universe polymorphic +Arguments big.body (R I)%type_scope _ _%list_scope _%function_scope +Expands to: Constant HB.tests.lock.X.big.body +(* + +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). + +*) +p : pred nat + : pred nat +File "./tests/instance_params_no_type.v", line 5, characters 0-70: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +COQC tests/instance_before_structure.v +File "./tests/instance_params_no_type.v", line 6, characters 0-76: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +COQC tests/primitive_records.v +A.p : +forall [T : Type] (record : A.axioms_ T) [x : T], A.f record x = x -> True + +A.p is not universe polymorphic +A.p is a projection of A.axioms_ +Arguments A.p [T]%type_scope record [x] _ +A.p is transparent +Expands to: Constant HB.tests.log_impargs_record.A.p +File "./tests/instance_params_no_type.v", line 7, characters 0-78: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +list_foo' : forall P A : Type, is_foo.axioms_ P (list A) + +list_foo' is not universe polymorphic +Arguments list_foo' (P A)%type_scope +list_foo' is transparent +Expands to: Constant HB.tests.instance_params_no_type.list_foo' +default : nat + : nat inhab : ?s where ?T : [ |- Type] ?s : [ |- s1.type ?T] +The command did fail as expected with message: +The term "default" has type "nonempty.sort ?t" +while it is expected to have type "nat". eq_refl : inhab = 7 : inhab = 7 -File "./examples/demo1/hierarchy_1.v", line 55, characters 0-123: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -File "./examples/demo5/hierarchy_0.v", line 35, characters 2-91: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] +File "./examples/demo2/classical.v", line 625, characters 0-75: +Warning: Postfix notations (i.e. starting with a nonterminal symbol and +ending with a terminal symbol) should usually be at level 1 (default). +[postfix-notation-not-level-1,parsing,default] +COQC tests/non_forgetful_inheritance.v +File "./examples/demo2/classical.v", line 626, characters 0-75: +Warning: Postfix notations (i.e. starting with a nonterminal symbol and +ending with a terminal symbol) should usually be at level 1 (default). +[postfix-notation-not-level-1,parsing,default] +File "./examples/demo2/classical.v", line 657, characters 0-43: +Warning: Postfix notations (i.e. starting with a nonterminal symbol and +ending with a terminal symbol) should usually be at level 1 (default). +[postfix-notation-not-level-1,parsing,default] +nat_foo + : forall P : Type, is_foo.axioms_ P nat +list_foo + : forall P : Type, is_foo.axioms_ P (list P) eq_refl : inhab = (7 :: nil)%list : inhab = (7 :: nil)%list where ?T : [ |- Type] -[1734568131.763984] HB: start module and section AddComoid_of_Type -[1734568131.764914] HB: converting arguments +COQC tests/fix_loop.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 +Arguments foo.sort P%type_scope record +Arguments foo.class P%type_scope record +Module +foo +:= Struct + Record axioms_ (P A : Type) : Type := Class + { instance_params_no_type_is_foo_mixin : is_foo.axioms_ P A } as record. + Definition instance_params_no_type_is_foo_mixin : + forall P A : Type, axioms_ P A -> is_foo.axioms_ P A. + Record type (P : Type) : Type := Pack + { sort : Type; class : axioms_ P sort }. + Definition sort : forall P : Type, type P -> Type. + Definition class : + forall (P : Type) (record : type P), axioms_ P record. + Definition phant_clone : + forall (P A : Type) (cT : type P) (c : axioms_ P A), + unify Type Type A cT nomsg -> + unify (type P) (type P) cT {| sort := A; class := c |} nomsg -> type P. + Definition pack_ : forall P A : Type, is_foo.axioms_ P A -> type P. + Module Exports + Definition phant_on_ : + forall (P : Type) (A : type P), ssreflect.phant A -> axioms_ P A. + End +Record axioms_ (P A : Type) : Type := Class + { instance_params_no_type_is_foo_mixin : is_foo.axioms_ P A } as record. + +axioms_ has primitive projections with eta conversion. +Arguments foo.axioms_ (P A)%type_scope +Arguments foo.Class (P A)%type_scope instance_params_no_type_is_foo_mixin +Arguments foo.instance_params_no_type_is_foo_mixin (P A)%type_scope record +[1768978489.802105] HB: start module and section AddComoid_of_Type +[1768978489.802948] HB: converting arguments indt-decl (parameter A explicit X0 c0 \ record AddComoid_of_Type (sort (typ X1)) Build_AddComoid_of_Type @@ -791,19 +975,26 @@ (prod `x` (X9 c4) c5 \ app [global (indt «eq»), X10 c4 c5, app [c2, c1, c5], c5]) c5 \ end-record)) to factories -[1734568131.765462] HB: processing key parameter -[1734568131.766247] HB: converting factories +[1768978489.804053] HB: processing key parameter +[1768978489.804915] HB: converting factories w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] to mixins -[1734568131.766335] HB: declaring context +[1768978489.805245] HB: declaring context w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] -[1734568131.766566] HB: declaring parameters and key as section variables +[1768978489.805678] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1734568131.767440] HB: declare mixin or factory -[1734568131.767502] HB: declare record axioms_ -[1734568131.777730] HB: declare notation Build -[1734568131.791387] HB: declare notation axioms -[1734568131.798939] HB: start module Exports -[1734568131.805156] HB: end modules and sections; export +[1768978489.806951] HB: declare mixin or factory +[1768978489.807218] HB: declare record axioms_ +[1768978489.819348] HB: declare notation Build +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/test_synthesis_params.v +[1768978489.828296] HB: declare notation axioms +[1768978489.835504] HB: start module Exports +[1768978489.840219] HB: end modules and sections; export «HB.examples.readme.AddComoid_of_Type.Exports» (* @@ -860,57 +1051,121 @@ Notation AddComoid_of_Type X1 := ( AddComoid_of_Type.phant_axioms X1). *) -[1734568131.847882] HB: start module AddComoid -[1734568131.849355] HB: declare axioms record +COQC tests/hnf.v +File "./examples/demo1/hierarchy_5.v", line 39, characters 2-97: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +COQC tests/fun_instance.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] +COQC tests/issue284.v +[1768978489.880063] HB: start module AddComoid +[1768978489.880457] HB: declare axioms record w-params.nil A (sort (typ «HB.examples.readme.25»)) c0 \ [triple (indt «AddComoid_of_Type.axioms_») [] c0] -[1734568131.850000] HB: typing class field +[1768978489.880929] HB: typing class field indt «AddComoid_of_Type.axioms_» -[1734568131.857261] HB: declare type record -[1734568131.860814] HB: structure: new mixins +File "./examples/demo1/hierarchy_3.v", line 39, characters 2-87: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +File "./examples/demo1/hierarchy_4.v", line 40, characters 2-97: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +[1768978489.884342] HB: declare type record +[1768978489.887734] HB: structure: new mixins [indt «AddComoid_of_Type.axioms_»] -[1734568131.861015] HB: structure: mixin first class +[1768978489.887975] HB: structure: mixin first class [mixin-first-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»)] -[1734568131.861165] HB: declaring clone abbreviation -[1734568131.869458] HB: declaring pack_ constant -[1734568131.870352] HB: declaring pack_ constant = +[1768978489.888186] HB: declaring clone abbreviation +[1768978489.897374] HB: declaring pack_ constant +addrC + : commutative add +where +?s : [ |- CMonoid.type] +[1768978489.898512] 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]] -[1734568131.873061] HB: start module Exports -[1734568131.873688] HB: making coercion from type to target -[1734568131.873742] HB: declare sort coercion -[1734568131.874046] HB: exporting unification hints -[1734568131.874243] HB: exporting coercions from class to mixins -[1734568131.874478] HB: export class to mixin coercion for mixin +[1768978489.900496] HB: start module Exports +[1768978489.900981] HB: making coercion from type to target +[1768978489.901121] HB: declare sort coercion +[1768978489.901603] HB: exporting unification hints +[1768978489.902077] HB: exporting coercions from class to mixins +[1768978489.902470] HB: export class to mixin coercion for mixin readme_AddComoid_of_Type -[1734568131.874774] HB: accumulating various props -[1734568131.875600] HB: stop module Exports -[1734568131.876285] HB: declaring on_ abbreviation -[1734568131.881099] HB: declaring `copy` abbreviation -[1734568131.882177] HB: declaring on abbreviation -[1734568131.887906] HB: end modules; export +[1768978489.903069] HB: accumulating various props +[1768978489.904189] HB: stop module Exports +[1768978489.905032] HB: declaring on_ abbreviation +[1768978489.909698] HB: declaring `copy` abbreviation +[1768978489.911549] HB: declaring on abbreviation +[1768978489.913849] HB: end modules; export «HB.examples.readme.AddComoid.Exports» -[1734568131.889201] HB: exporting operations -[1734568131.891071] HB: export operation zero -[1734568131.902268] HB: export operation add -[1734568131.911421] HB: export operation addrA -File "./examples/demo2/classical.v", line 625, characters 0-75: -Warning: Postfix notations (i.e. starting with a nonterminal symbol and -ending with a terminal symbol) should usually be at level 1 (default). -[postfix-notation-not-level-1,parsing,default] -File "./examples/demo2/classical.v", line 626, characters 0-75: -Warning: Postfix notations (i.e. starting with a nonterminal symbol and -ending with a terminal symbol) should usually be at level 1 (default). -[postfix-notation-not-level-1,parsing,default] -File "./examples/demo2/classical.v", line 657, characters 0-43: -Warning: Postfix notations (i.e. starting with a nonterminal symbol and -ending with a terminal symbol) should usually be at level 1 (default). -[postfix-notation-not-level-1,parsing,default] -[1734568132.155253] HB: export operation addrC -[1734568132.160562] HB: export operation add0r -[1734568132.163137] HB: operations meta-data module: ElpiOperations -[1734568132.164982] HB: abbreviation factory-by-classname +[1768978489.914760] HB: exporting operations +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 +[1768978489.916819] HB: export operation zero +[1768978489.921234] HB: export operation add +[1768978489.926770] HB: export operation addrA +add + : ?s -> ?s -> ?s +where +?s : [ |- CMonoid.type] +addrC + : commutative add +where +?s : [ |- CMonoid.type] +aType + : Type +[1768978489.977337] HB: begin module for builders +File "./examples/demo1/hierarchy_2.v", line 39, characters 2-91: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +[1768978489.977688] HB: begin module Super +[1768978489.977866] HB: ended module Super +hasB.type not a defined object. +[1768978489.982870] HB: postulating factories +[1768978489.983127] HB: processing key context-item +[1768978489.983561] HB: processing mixin parameter a +[1768978489.984321] HB: declaring parameters and key as section variables +Here is the list of mixins to declare (the order matters): [] +COQC tests/issue287.v +File "./examples/demo5/hierarchy_0.v", line 35, characters 2-91: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +COQC tests/two_hier.v +[1768978490.066599] HB: start module and section hasA +[1768978490.067026] 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 +[1768978490.067270] HB: processing key parameter +[1768978490.067888] HB: converting factories +w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins +[1768978490.068031] HB: declaring context +w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] +[1768978490.068301] HB: declaring parameters and key as section variables +Here is the list of mixins to declare (the order matters): [] +[1768978490.068985] HB: declare mixin or factory +[1768978490.069093] HB: declare record axioms_ +File "./examples/demo1/hierarchy_1.v", line 55, characters 0-123: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +[1768978490.072680] HB: declare notation Build +COQC tests/instance_merge_with_param.v +[1768978490.074894] HB: declare notation axioms +[1768978490.078892] HB: start module Exports +[1768978490.079150] HB: export operation addrC +[1768978490.081877] HB: end modules and sections; export +«HB.tests.hb_pack.hasA.Exports» +[1768978490.083350] HB: export operation add0r +hasA.type not a defined object. +[1768978490.086062] HB: operations meta-data module: ElpiOperations +[1768978490.087727] HB: abbreviation factory-by-classname (* Module AddComoid. @@ -1007,470 +1262,224 @@ *) forall (M : AddComoid.type) (x : M), x + x = 0 : Prop -COQC examples/FSCD2020_talk/V3.v -COQC examples/Coq2020_material/CoqWS_demo.v -File "./examples/demo1/hierarchy_2.v", line 39, characters 2-91: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -COQC examples/Coq2020_material/CoqWS_abstract.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/Coq2020_material/CoqWS_expansion/withHB.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. -File "./examples/demo5/hierarchy_0.v", line 68, characters 2-109: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -COQC examples/Coq2020_material/CoqWS_expansion/withoutHB.v -COQC tests/type_of_exported_ops.v -File "./examples/demo1/hierarchy_2.v", line 57, characters 0-57: +File "./tests/interleave_context.v", line 16, characters 0-52: Warning: -pulling in dependencies: -[hierarchy_2_AddComoid_of_TYPE, hierarchy_2_AddAG_of_AddComoid] +pulling in dependencies: [interleave_context_HasA, interleave_context_HasB] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] -File "./examples/demo1/hierarchy_5.v", line 68, characters 2-91: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -File "./examples/demo1/hierarchy_4.v", line 40, characters 2-97: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -File "./examples/demo1/hierarchy_3.v", line 39, characters 2-87: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -[1734568133.325038] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_AddAG_of_AddComoid -[1734568133.325641] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_Ring_of_AddAG -Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. - -Arguments Monoid.Pack sort%type_scope class -Arguments Monoid.sort record -Arguments Monoid.class record -@add - : forall s : Monoid.type, s -> s -> s -@addNr - : forall s : Ring.type, left_inverse 0 opp add -COQC tests/duplicate_structure.v -Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. - -Arguments Monoid.Pack sort%type_scope class -Arguments Monoid.sort record -Arguments Monoid.class record -@add - : forall s : Monoid.type, s -> s -> s -@addNr - : forall s : AbelianGroup.type, left_inverse 0 opp add -@addrC - : forall s : AbelianGroup.type, commutative add -COQC tests/instance_params_no_type.v -COQC tests/test_CS_db_filtering.v -COQC tests/subtype.v -COQC tests/exports.v -File "./examples/demo1/hierarchy_4.v", line 69, characters 2-91: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -File "./examples/FSCD2020_talk/V2.v", line 17, characters 0-66: +File "./examples/Coq2020_material/CoqWS_abstract.v", line 23, characters 0-71: Warning: -pulling in dependencies: [V2_is_semigroup] +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 -add - : ?s -> ?s -> ?s -where -?s : [ |- CMonoid.type] -addrC - : commutative add -where -?s : [ |- CMonoid.type] -COQC tests/compress_coe.v -Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. - -Arguments Monoid.Pack sort%type_scope class -Arguments Monoid.sort record -Arguments Monoid.class record -@add - : forall s : Monoid.type, s -> s -> s -@addNr - : forall s : AbelianGroup.type, left_inverse 0 opp add -@addrC - : forall s : AbelianGroup.type, commutative add -addrC - : commutative add -where -?s : [ |- CMonoid.type] +COQC tests/instance_merge_with_distinct_param.v +hasB.type not a defined object. +[1768978490.190833] HB: start module SubInhab +[1768978490.191197] 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] +[1768978490.191674] HB: typing class field indt «is_inhab.axioms_» +[1768978490.192024] HB: typing class field indt «is_SUB.axioms_» +[1768978490.195422] HB: declare type record +[1768978490.198262] HB: structure: new mixins [] +[1768978490.198420] HB: structure: mixin first class [] +[1768978490.198486] HB: declaring clone abbreviation +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 +[1768978490.203876] HB: declaring pack_ constant +[1768978490.205486] HB: declaring pack_ constant = +fun `T` (sort (typ «axioms_.u0»)) c0 \ + fun `P` (app [global (const «pred»), c0]) c1 \ + fun `sT` (sort (typ «axioms_.u1»)) c2 \ + fun `m` (app [global (indt «is_inhab.axioms_»), c2]) c3 \ + fun `m` (app [global (indt «is_SUB.axioms_»), c0, c1, c2]) c4 \ + app + [global (indc «Pack»), c0, c1, c2, + app [global (indc «Class»), c0, c1, c2, c3, c4]] +[1768978490.206980] HB: start module Exports +[1768978490.207350] HB: making coercion from type to target +[1768978490.207509] HB: declare sort coercion +[1768978490.207743] HB: exporting unification hints +[1768978490.209106] HB: declare coercion subtype_SubInhab__to__subtype_SUB +[1768978490.210307] HB: declare coercion hint +subtype_SubInhab_class__to__subtype_SUB_class +[1768978490.213185] HB: declare unification hint +subtype_SubInhab__to__subtype_SUB 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] +[1768978490.216471] HB: declare coercion subtype_SubInhab__to__subtype_Inhab +[1768978490.217523] HB: declare coercion hint +subtype_SubInhab_class__to__subtype_Inhab_class +[1768978490.220232] HB: declare unification hint +subtype_SubInhab__to__subtype_Inhab +[1768978490.224087] HB: declare unification hint +join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB +[1768978490.227621] HB: exporting coercions from class to mixins +[1768978490.228020] HB: export class to mixin coercion for mixin +subtype_is_inhab +[1768978490.229208] HB: export class to mixin coercion for mixin +subtype_is_SUB +[1768978490.230238] HB: accumulating various props +[1768978490.231643] HB: stop module Exports +[1768978490.235034] HB: declaring on_ abbreviation +[1768978490.239500] HB: declaring `copy` abbreviation +list_bar + : forall P : b.type, is_bar.axioms_ P (list P) +[1768978490.241304] HB: declaring on abbreviation +[1768978490.243014] HB: end modules; export +«HB.tests.subtype.SubInhab.Exports» +File "./examples/demo1/hierarchy_5.v", line 68, characters 2-91: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +[1768978490.246588] HB: exporting operations +[1768978490.247018] HB: operations meta-data module: ElpiOperations +[1768978490.247763] HB: abbreviation factory-by-classname forall x y : ?t, x - (y + 0) = x : Prop where ?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) -File "./examples/Coq2020_material/CoqWS_expansion/withoutHB.v", line 10, characters 50-62: -Warning: The format modifier has no effect for only-parsing notations. -[discarded-format-only-parsing,parsing,default] -COQC tests/funclass.v -COQC tests/grefclass.v -COQC tests/local_instance.v -File "./examples/Coq2020_material/CoqWS_abstract.v", line 23, characters 0-71: +File "./examples/demo1/hierarchy_4.v", line 69, characters 2-91: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +AbelianGrp.phant_on_ BinNums_Z__canonical__readme_AbelianGrp + (Phant BinNums_Z__canonical__readme_AbelianGrp) +: +AbelianGrp.axioms_ Z + : AbelianGrp.axioms_ Z +HB.check: forall w : wp.type nat Init.Nat.mul, w = w : Prop +HB: Z is canonically equipped with structures: + - AbelianGrp + (from "./examples/readme.v", line 32) + - AddComoid + (from "./examples/readme.v", line 31) + +COQC tests/instance_merge.v +File "./examples/FSCD2020_talk/V2.v", line 17, characters 0-66: Warning: -pulling in dependencies: [CoqWS_abstract_CMonoid_of_Type] +pulling in dependencies: [V2_is_semigroup] + +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB,elpi,default] +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] -forall x y : ?t, 1 + x = y * x - : Prop -where -?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) -COQC tests/lock.v File "./examples/FSCD2020_talk/V3.v", line 28, characters 2-118: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] -forall (R : Ring.type) (x y : R), 1 * x = y - x - : Prop -forall - (x : join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing - ?t) (y : ?t), 1 * x = y - x - : Prop -where -?t : - [x : - join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing - ?t - y : ?t |- Ring.type] (x, y cannot be used) -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop -add - : A -> A -> A +hasAB.type not a defined object. +COQC tests/unit/enrich_type.v +hasA'.type not a defined object. +COQC tests/unit/mixin_src_has_mixin_instance.v +COQC tests/unit/mk_src_map.v +File "./examples/demo5/hierarchy_0.v", line 68, characters 2-109: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +COQC tests/unit/close_hole_term.v +COQC tests/unit/struct.v +COQC tests/factory_when_notation.v +COQC tests/saturate_on.v +COQC tests/bug_435.v forall (G : AbelianGrp.type) (x : G), x - x = 0 : Prop forall (S : SemiRing.type) (x : S), x * 1 + 0 = x : Prop forall (R : Ring.type) (x y : R), x * - (1 * y) = - x * y : Prop -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop -File "./tests/instance_params_no_type.v", line 5, characters 0-70: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop -File "./tests/instance_params_no_type.v", line 6, characters 0-76: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -File "./tests/instance_params_no_type.v", line 7, characters 0-78: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -list_foo' : forall P A : Type, is_foo.axioms_ P (list A) - -list_foo' is not universe polymorphic -Arguments list_foo' (P A)%type_scope -list_foo' is transparent -Expands to: Constant HB.tests.instance_params_no_type.list_foo' -(* - -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). - -*) -nat_foo - : forall P : Type, is_foo.axioms_ P nat -list_foo - : forall P : Type, is_foo.axioms_ P (list P) -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 tests/interleave_context.v -COQC tests/not_same_key.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 -Arguments foo.sort P%type_scope record -Arguments foo.class P%type_scope record -Module -foo -:= Struct - Record axioms_ (P A : Type) : Type := Class - { instance_params_no_type_is_foo_mixin : is_foo.axioms_ P A } as record. - Definition instance_params_no_type_is_foo_mixin : - forall P A : Type, axioms_ P A -> is_foo.axioms_ P A. - Record type (P : Type) : Type := Pack - { sort : Type; class : axioms_ P sort }. - Definition sort : forall P : Type, type P -> Type. - Definition class : - forall (P : Type) (record : type P), axioms_ P record. - Definition phant_clone : - forall (P A : Type) (cT : type P) (c : axioms_ P A), - unify Type Type A cT nomsg -> - unify (type P) (type P) cT {| sort := A; class := c |} nomsg -> type P. - Definition pack_ : forall P A : Type, is_foo.axioms_ P A -> type P. - Module Exports - Definition phant_on_ : - forall (P : Type) (A : type P), ssreflect.phant A -> axioms_ P A. - End -Record axioms_ (P A : Type) : Type := Class - { instance_params_no_type_is_foo_mixin : is_foo.axioms_ P A } as record. - -axioms_ has primitive projections with eta conversion. -Arguments foo.axioms_ (P A)%type_scope -Arguments foo.Class (P A)%type_scope instance_params_no_type_is_foo_mixin -Arguments foo.instance_params_no_type_is_foo_mixin (P A)%type_scope record -A.p : -forall [T : Type] (record : A.axioms_ T) [x : T], A.f record x = x -> True - -A.p is not universe polymorphic -A.p is a projection of A.axioms_ -Arguments A.p [T]%type_scope record [x] _ -A.p is transparent -Expands to: Constant HB.tests.log_impargs_record.A.p -COQC tests/hb_pack.v -COQC tests/declare.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class Arguments Monoid.sort record Arguments Monoid.class record +forall x y : ?t, 1 + x = y * x + : Prop +where +?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) @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/short.v -COQC tests/instance_before_structure.v -HB.check: -SemiRing_of_AddComoid.axioms_ -: -forall (A : Type) (m : AddMonoid_of_TYPE.axioms_ A), -AddComoid_of_AddMonoid.axioms_ A m -> Type -: -forall (A : Type) (m : AddMonoid_of_TYPE.axioms_ A), -AddComoid_of_AddMonoid.axioms_ A m -> Type -COQC tests/primitive_records.v -HB: A is canonically equipped with structures: - - Equality - Singleton - (from "./examples/hulk.v", line 216) - -COQC tests/non_forgetful_inheritance.v -COQC tests/fix_loop.v -COQC tests/test_synthesis_params.v -COQC tests/hnf.v -p : pred nat - : pred nat -list_bar - : forall P : b.type, is_bar.axioms_ P (list P) -COQC tests/fun_instance.v -default : nat - : nat -[1734568137.672305] HB: start module SubInhab -[1734568137.673964] 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] -[1734568137.675354] HB: typing class field indt «is_inhab.axioms_» -[1734568137.676002] HB: typing class field indt «is_SUB.axioms_» -COQC tests/issue284.v -[1734568137.684390] HB: declare type record -[1734568137.691089] HB: structure: new mixins [] -[1734568137.691898] HB: structure: mixin first class [] -[1734568137.692168] HB: declaring clone abbreviation -The command did fail as expected with message: -The term "default" has type "nonempty.sort ?t" -while it is expected to have type "nat". -[1734568137.705124] HB: declaring pack_ constant -[1734568137.708081] HB: declaring pack_ constant = -fun `T` (sort (typ «axioms_.u0»)) c0 \ - fun `P` (app [global (const «pred»), c0]) c1 \ - fun `sT` (sort (typ «axioms_.u1»)) c2 \ - fun `m` (app [global (indt «is_inhab.axioms_»), c2]) c3 \ - fun `m` (app [global (indt «is_SUB.axioms_»), c0, c1, c2]) c4 \ - app - [global (indc «Pack»), c0, c1, c2, - app [global (indc «Class»), c0, c1, c2, c3, c4]] -[1734568137.711171] HB: start module Exports -[1734568137.712227] HB: making coercion from type to target -[1734568137.712664] HB: declare sort coercion -[1734568137.713102] HB: exporting unification hints -[1734568137.715513] HB: declare coercion subtype_SubInhab__to__subtype_SUB -[1734568137.718116] HB: declare coercion hint -subtype_SubInhab_class__to__subtype_SUB_class -[1734568137.724518] HB: declare unification hint -subtype_SubInhab__to__subtype_SUB -[1734568137.735399] HB: declare coercion subtype_SubInhab__to__subtype_Inhab -[1734568137.738099] HB: declare coercion hint -subtype_SubInhab_class__to__subtype_Inhab_class -[1734568137.751497] HB: declare unification hint -subtype_SubInhab__to__subtype_Inhab -[1734568137.770266] HB: declare unification hint -join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB -[1734568137.777875] HB: exporting coercions from class to mixins -[1734568137.779221] HB: export class to mixin coercion for mixin -subtype_is_inhab -[1734568137.783518] HB: export class to mixin coercion for mixin -subtype_is_SUB -[1734568137.786381] HB: accumulating various props -[1734568137.790453] HB: stop module Exports -[1734568137.800756] HB: exporting under the module path [] -[1734568137.801750] HB: exporting modules + : forall s : Ring.type, left_inverse 0 opp add +COQC tests/bug_447.v +COQC tests/unimported_relevant_class.v +hasAB.type not a defined object. +[1768978490.623076] HB: exporting under the module path [] +[1768978490.623601] HB: exporting modules [Ring_of_TYPE.Exports, Ring.Exports, RingElpiOperations, RingExports, Dummy.Exports, URing.Exports, URingElpiOperations, dummy.Exports, Builders_1.Builders_Export_5] -[1734568137.801921] HB: declaring on_ abbreviation -[1734568137.806639] HB: exporting CS instances +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop +[1768978490.626179] HB: exporting CS instances [«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] -[1734568137.808193] HB: exporting Abbreviations [addr0, addrNK] -[1734568137.808712] HB: exporting Clauses X0 -[1734568137.816965] HB: declaring `copy` abbreviation -COQC tests/issue287.v -[1734568137.820421] HB: declaring on abbreviation -[1734568137.823510] HB: end modules; export -«HB.tests.subtype.SubInhab.Exports» +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] +[1768978490.627023] HB: exporting Abbreviations [addr0, addrNK] +[1768978490.627302] HB: exporting Clauses X0 +hasA'.type not a defined object. forall (R : Enclosing.Ring.type) (x : R), x = x : Prop 0%G : ?s where ?s : [ |- Enclosing.Ring.type] -[1734568137.832284] HB: exporting operations -[1734568137.833851] HB: operations meta-data module: ElpiOperations -[1734568137.835911] HB: abbreviation factory-by-classname Enclosing.zero : Z : Z -COQC tests/two_hier.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 -[1734568138.688073] HB: start module and section hasA -[1734568138.689592] 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 -[1734568138.689866] HB: processing key parameter -[1734568138.690585] HB: converting factories -w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins -[1734568138.691188] HB: declaring context -w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] -[1734568138.691432] HB: declaring parameters and key as section variables -Here is the list of mixins to declare (the order matters): [] -[1734568138.692109] HB: declare mixin or factory -[1734568138.692223] HB: declare record axioms_ -[1734568138.696643] HB: declare notation Build -[1734568138.700875] HB: declare notation axioms -[1734568138.707633] HB: start module Exports -[1734568138.717198] HB: end modules and sections; export -«HB.tests.hb_pack.hasA.Exports» -hasA.type not a defined object. -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 -hasB.type not a defined object. -COQC tests/instance_merge_with_param.v -Notation big := big.body -Expands to: Notation HB.tests.lock.X.big - -big.body : forall R I : Type, R -> list I -> (I -> bigbody R I) -> R - -big.body is not universe polymorphic -Arguments big.body (R I)%type_scope _ _%list_scope _%function_scope -Expands to: Constant HB.tests.lock.X.big.body +forall (R : Ring.type) (x y : R), 1 * x = y - x + : Prop +forall + (x : join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing + ?t) (y : ?t), 1 * x = y - x + : Prop +where +?t : + [x : + join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing + ?t + y : ?t |- Ring.type] (x, y cannot be used) Query assignments: Ind = «hasA.axioms_» -COQC tests/instance_merge_with_distinct_param.v -Query assignments: - Ind = «A.axioms_» -Query assignments: - Ind = «A.type» -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 -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.check: forall w : wp.type nat Init.Nat.mul, w = w : Prop -hasAB.type not a defined object. -hasA'.type not a defined object. -COQC tests/instance_merge.v +[1768978490.683187] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_AddAG_of_AddComoid +[1768978490.683505] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_Ring_of_AddAG +COQC tests/unimported_irrelevant_class.v +forall T : AB.type, +unkeyed + {| + AB.sort := T; + AB.class := + let hb_pack_hasA_mixin := AB.hb_pack_hasA_mixin _ (AB.class T) in + let hb_pack_hasB_mixin := AB.hb_pack_hasB_mixin _ (AB.class T) in + {| + AB.hb_pack_hasA_mixin := hb_pack_hasA_mixin; + AB.hb_pack_hasB_mixin := hb_pack_hasB_mixin + |} + |} + : Type Datatypes_prod__canonical__compress_coe_D = fun D D' : D.type => {| @@ -1492,87 +1501,84 @@ : D.type -> D.type -> D.type Arguments Datatypes_prod__canonical__compress_coe_D D D' -COQC tests/unit/enrich_type.v -forall T : AB.type, -unkeyed - {| - AB.sort := T; - AB.class := - let hb_pack_hasA_mixin := AB.hb_pack_hasA_mixin _ (AB.class T) in - let hb_pack_hasB_mixin := AB.hb_pack_hasB_mixin _ (AB.class T) in - {| - AB.hb_pack_hasA_mixin := hb_pack_hasA_mixin; - AB.hb_pack_hasB_mixin := hb_pack_hasB_mixin - |} - |} - : Type +COQC examples/demo1/test_0_0.v +Query assignments: + Ind = «A.axioms_» +Query assignments: + Ind = «A.type» A : A.type : A.type A : A.type : A.type +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop +COQC examples/demo1/test_1_0.v AB1 : hasB.phant_axioms A -> AB.type : hasB.phant_axioms A -> AB.type +Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. + +Arguments Monoid.Pack sort%type_scope class +Arguments Monoid.sort record +Arguments Monoid.class record +@add + : forall s : Monoid.type, s -> s -> s +@addNr + : forall s : AbelianGroup.type, left_inverse 0 opp add +@addrC + : forall s : AbelianGroup.type, commutative add Bm : hasB.phant_axioms A : hasB.phant_axioms A -COQC tests/unit/mixin_src_has_mixin_instance.v AB2 : AB.type : AB.type pB : T * T : T * T AB3 : AB.type : AB.type -erefl : ?t = ?t - : ?t = ?t -where -?t : [ |- Sq.type] -COQC tests/unit/mk_src_map.v +add + : A -> A -> A +COQC examples/demo3/test_0_0.v +COQC examples/demo3/test_1_0.v +HB: nat is canonically equipped with structures: + - s1 + (from "./tests/instance_before_structure.v", line 11) + +HB: A is canonically equipped with structures: + - Equality + Singleton + (from "./examples/hulk.v", line 216) + +File "./tests/instance_before_structure.v", line 16, characters 0-52: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +COQC tests/exports2.v +HB: nat is canonically equipped with structures: + - s1 + (from "./tests/instance_before_structure.v", line 11) X : Foo.type A P : Foo.type A P -COQC tests/unit/close_hole_term.v -COQC tests/unit/struct.v -COQC tests/factory_when_notation.v -COQC tests/saturate_on.v -T : Fun.type nat - : Fun.type nat -COQC tests/bug_435.v -COQC tests/bug_447.v + +COQC examples/demo1/test_2_0.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 -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/unimported_relevant_class.v -HB: nat is canonically equipped with structures: - - s1 - (from "./tests/instance_before_structure.v", line 11) - -File "./tests/instance_before_structure.v", line 16, characters 0-52: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -COQC tests/unimported_irrelevant_class.v HB: nat is canonically equipped with structures: - s1 (from "./tests/instance_before_structure.v", line 11) -aType - : 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] -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) - -hasB.type not a defined object. +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop +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 Debug: elpi lets escape exception: non forgetful inheritance detected. You have two solutions: @@ -1588,24 +1594,39 @@ 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] -COQC examples/demo1/test_0_0.v +erefl : ?t = ?t + : ?t = ?t +where +?t : [ |- Sq.type] +T : Fun.type nat + : Fun.type nat +COQC examples/demo3/test_2_0.v HB: nat is canonically equipped with structures: - s1 (from "./tests/instance_before_structure.v", line 11) -HB: list is canonically equipped with structures: - - s3 - (from "./tests/instance_merge_with_param.v", line 23) - - s2 - (from "./tests/instance_merge_with_param.v", line 12) - - s1 - (from "./tests/instance_merge_with_param.v", line 10) +Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. -COQC examples/demo1/test_1_0.v -HB: nat is canonically equipped with structures: - - s1 - (from "./tests/instance_before_structure.v", line 11) +Arguments Monoid.Pack sort%type_scope class +Arguments Monoid.sort record +Arguments Monoid.class record +@add + : forall s : Monoid.type, s -> s -> s +@addNr + : forall s : AbelianGroup.type, left_inverse 0 opp add +@addrC + : forall s : AbelianGroup.type, commutative add +Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. +Arguments Monoid.Pack sort%type_scope class +Arguments Monoid.sort record +Arguments Monoid.class record +@add + : forall s : Monoid.type, s -> s -> s +@addNr + : forall s : AbelianGroup.type, left_inverse 0 opp add +@addrC + : forall s : AbelianGroup.type, commutative add HB: nat is canonically equipped with structures: - s3 s2 @@ -1619,96 +1640,10 @@ : nat default3 : nat -COQC examples/demo1/test_2_0.v +COQC examples/demo2/stage11.v +COQC examples/demo2/stage10.v COQC examples/demo1/test_3_0.v -Query assignments: - X = app [global (indt «list»), X0] - X1_ = X1 - Y_ = X0 - Z = fun `x` X1 c0 \ app [global (indt «list»), c0] -Syntactic constraints: - evar (X0) (sort (typ «HB.tests.unit.close_hole_term.2»)) (X0) /* suspended on X0 */ -Universe constraints: -UNIVERSES: - {HB.tests.unit.close_hole_term.3 HB.tests.unit.close_hole_term.2 - HB.tests.unit.close_hole_term.1} |= - HB.tests.unit.close_hole_term.2 < HB.tests.unit.close_hole_term.1 - Set <= HB.tests.unit.close_hole_term.3 - HB.tests.unit.close_hole_term.2 <= HB.tests.unit.close_hole_term.3 - HB.tests.unit.close_hole_term.2 <= list.u0 -ALGEBRAIC UNIVERSES: - {} -FLEXIBLE UNIVERSES: - -SORTS: - α1 := Type -WEAK CONSTRAINTS: - - -Query assignments: - Z = global (indt «nat») -Query assignments: - X = app [global (const «Inj»), X0, X1, X2, X3, X4] - X2_ = X0 - X3_ = X1 - X4_ = X5 - X5_ = X6 - X6_ = X7 - X7_ = X8 - X8_ = X9 - Y = app [global (const «Inj»), X0, X1] - Z = fun `x` X5 c0 \ - fun `x` (X6 c0) c1 \ - fun `x` (X7 c0 c1) c2 \ - fun `x` (X8 c0 c1 c2) c3 \ - fun `x` (X9 c0 c1 c2 c3) c4 \ - app [global (const «Inj»), c0, c1, c2, c3, c4] -Syntactic constraints: - evar (X4) (prod `_` X0 c0 \ X1) (X4) /* suspended on X4 */ - evar (X3) (app [global (const «relation»), X1]) (X3) /* suspended on X3 */ - evar (X2) (app [global (const «relation»), X0]) (X2) /* suspended on X2 */ - evar (X1) (sort (typ «HB.tests.unit.close_hole_term.13»)) (X1) /* suspended on X1 */ - evar (X0) (sort (typ «HB.tests.unit.close_hole_term.12»)) (X0) /* suspended on X0 */ -Universe constraints: -UNIVERSES: - {HB.tests.unit.close_hole_term.16 HB.tests.unit.close_hole_term.15 - HB.tests.unit.close_hole_term.14 HB.tests.unit.close_hole_term.13 - HB.tests.unit.close_hole_term.12 HB.tests.unit.close_hole_term.11 - HB.tests.unit.close_hole_term.10} |= - Set < HB.tests.unit.close_hole_term.14 - Set < HB.tests.unit.close_hole_term.15 - HB.tests.unit.close_hole_term.12 < HB.tests.unit.close_hole_term.10 - HB.tests.unit.close_hole_term.13 < HB.tests.unit.close_hole_term.11 - Coq.Relations.Relation_Definitions.1 <= HB.tests.unit.close_hole_term.14 - Coq.Relations.Relation_Definitions.1 <= HB.tests.unit.close_hole_term.15 - HB.tests.unit.close_hole_term.12 <= Coq.Relations.Relation_Definitions.1 - HB.tests.unit.close_hole_term.12 <= Inj.u0 - HB.tests.unit.close_hole_term.12 <= HB.tests.unit.close_hole_term.16 - HB.tests.unit.close_hole_term.13 <= Coq.Relations.Relation_Definitions.1 - HB.tests.unit.close_hole_term.13 <= Inj.u1 - HB.tests.unit.close_hole_term.13 <= HB.tests.unit.close_hole_term.16 -ALGEBRAIC UNIVERSES: - {} -FLEXIBLE UNIVERSES: - -SORTS: - α6 := Type - α7 := Type - α8 := Type - α9 := Type - α10 := Type -WEAK CONSTRAINTS: - - COQC examples/demo1/test_3_3.v -nat : s3.type - : s3.type -list nat : s3.type - : s3.type -list (list nat) : s3.type - : s3.type -fun t : s3.type => list t : s3.type - : s3.type -> s3.type Query assignments: X = global (indt «nat») Query assignments: @@ -1767,10 +1702,6 @@ WEAK CONSTRAINTS: -nat : s3.type - : s3.type -list nat : s3.type - : s3.type Query assignments: A_ = X0 B_ = X1 @@ -1802,26 +1733,41 @@ WEAK CONSTRAINTS: -list (list nat) : s3.type - : s3.type -fun t : s3.type => list t : s3.type - : s3.type -> s3.type -COQC examples/demo1/test_4_0.v -COQC examples/demo1/test_4_3.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 -File "./tests/saturate_on.v", line 5, characters 0-64: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] File "./tests/unit/mk_src_map.v", line 6, characters 0-76: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] +Query assignments: + X = app [global (indt «list»), X0] + X1_ = X1 + Y_ = X0 + Z = fun `x` X1 c0 \ app [global (indt «list»), c0] +Syntactic constraints: + evar (X0) (sort (typ «HB.tests.unit.close_hole_term.2»)) (X0) /* suspended on X0 */ +Universe constraints: +UNIVERSES: + {HB.tests.unit.close_hole_term.3 HB.tests.unit.close_hole_term.2 + HB.tests.unit.close_hole_term.1} |= + HB.tests.unit.close_hole_term.2 < HB.tests.unit.close_hole_term.1 + Set <= HB.tests.unit.close_hole_term.3 + HB.tests.unit.close_hole_term.2 <= HB.tests.unit.close_hole_term.3 + HB.tests.unit.close_hole_term.2 <= list.u0 +ALGEBRAIC UNIVERSES: + {} +FLEXIBLE UNIVERSES: + +SORTS: + α1 := Type +WEAK CONSTRAINTS: + + +Query assignments: + Z = global (indt «nat») +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) + File "./tests/unit/mk_src_map.v", line 8, characters 0-79: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] @@ -1829,10 +1775,6 @@ : forall P A : Type, is_foo.axioms_ P (list A) list_foo : forall P : Type, is_foo.axioms_ P (list P) -File "./tests/factory_when_notation.v", line 6, characters 0-40: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] -hasAB.type not a defined object. Query assignments: MS = pi c0 \ pi c1 \ @@ -1844,24 +1786,65 @@ 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] -hasA'.type not a defined object. -COQC examples/demo1/test_5_0.v -COQC examples/demo1/test_5_3.v -COQC examples/demo2/stage10.v -COQC examples/demo2/stage11.v -nat : s3'.type Datatypes_nat__canonical__two_hier_s3 - : s3'.type Datatypes_nat__canonical__two_hier_s3 -list unit : Pointed.type - : Pointed.type -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 +Query assignments: + X = app [global (const «Inj»), X0, X1, X2, X3, X4] + X2_ = X0 + X3_ = X1 + X4_ = X5 + X5_ = X6 + X6_ = X7 + X7_ = X8 + X8_ = X9 + Y = app [global (const «Inj»), X0, X1] + Z = fun `x` X5 c0 \ + fun `x` (X6 c0) c1 \ + fun `x` (X7 c0 c1) c2 \ + fun `x` (X8 c0 c1 c2) c3 \ + fun `x` (X9 c0 c1 c2 c3) c4 \ + app [global (const «Inj»), c0, c1, c2, c3, c4] +Syntactic constraints: + evar (X4) (prod `_` X0 c0 \ X1) (X4) /* suspended on X4 */ + evar (X3) (app [global (const «relation»), X1]) (X3) /* suspended on X3 */ + evar (X2) (app [global (const «relation»), X0]) (X2) /* suspended on X2 */ + evar (X1) (sort (typ «HB.tests.unit.close_hole_term.13»)) (X1) /* suspended on X1 */ + evar (X0) (sort (typ «HB.tests.unit.close_hole_term.12»)) (X0) /* suspended on X0 */ +Universe constraints: +UNIVERSES: + {HB.tests.unit.close_hole_term.16 HB.tests.unit.close_hole_term.15 + HB.tests.unit.close_hole_term.14 HB.tests.unit.close_hole_term.13 + HB.tests.unit.close_hole_term.12 HB.tests.unit.close_hole_term.11 + HB.tests.unit.close_hole_term.10} |= + Set < HB.tests.unit.close_hole_term.14 + Set < HB.tests.unit.close_hole_term.15 + HB.tests.unit.close_hole_term.12 < HB.tests.unit.close_hole_term.10 + HB.tests.unit.close_hole_term.13 < HB.tests.unit.close_hole_term.11 + Coq.Relations.Relation_Definitions.1 <= HB.tests.unit.close_hole_term.14 + Coq.Relations.Relation_Definitions.1 <= HB.tests.unit.close_hole_term.15 + HB.tests.unit.close_hole_term.12 <= Coq.Relations.Relation_Definitions.1 + HB.tests.unit.close_hole_term.12 <= Inj.u0 + HB.tests.unit.close_hole_term.12 <= HB.tests.unit.close_hole_term.16 + HB.tests.unit.close_hole_term.13 <= Coq.Relations.Relation_Definitions.1 + HB.tests.unit.close_hole_term.13 <= Inj.u1 + HB.tests.unit.close_hole_term.13 <= HB.tests.unit.close_hole_term.16 +ALGEBRAIC UNIVERSES: + {} +FLEXIBLE UNIVERSES: + +SORTS: + α6 := Type + α7 := Type + α8 := Type + α9 := Type + α10 := Type +WEAK CONSTRAINTS: + + +File "./tests/saturate_on.v", line 5, characters 0-64: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] File "./tests/unit/mixin_src_has_mixin_instance.v", line 12, characters 0-57: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] -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») @@ -1870,32 +1853,90 @@ M1_ = const «m1.phant_axioms» Y = has-mixin-instance (cs-gref (indt «list»)) (const «m1.phant_axioms») (const «i1») -COQC examples/demo3/test_0_0.v -COQC examples/demo3/test_1_0.v -COQC examples/demo3/test_2_0.v -COQC tests/exports2.v -testTy : JustMixedParam.type ?T - : JustMixedParam.type ?T -where -?T : [ |- Type] -[1734568145.448477] HB: postulating X -[1734568145.452738] HB: declare canonical mixin instance +COQC examples/demo1/test_4_0.v +COQC examples/demo1/test_4_3.v +nat : s3.type + : s3.type +list nat : s3.type + : s3.type +list (list nat) : s3.type + : s3.type +fun t : s3.type => list t : s3.type + : s3.type -> s3.type +HB: list is canonically equipped with structures: + - s3 + (from "./tests/instance_merge_with_param.v", line 23) + - s2 + (from "./tests/instance_merge_with_param.v", line 12) + - s1 + (from "./tests/instance_merge_with_param.v", line 10) + +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 +File "./tests/factory_when_notation.v", line 6, characters 0-40: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] +COQC examples/demo1/test_5_0.v +COQC examples/demo1/test_5_3.v +list unit : Pointed.type + : Pointed.type +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 +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 +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 +[1768978491.933328] HB: exporting under the module path [] +[1768978491.933608] HB: exporting modules [] +[1768978491.933756] HB: exporting CS instances [] +[1768978491.933898] HB: exporting Abbreviations [] +[1768978491.934034] HB: exporting Clauses X0 +[1768978492.022683] HB: postulating X +[1768978492.025383] HB: declare canonical mixin instance «HB_unnamed_factory_5» -[1734568145.454023] HB: we can build a bug_435_B2 on unit -[1734568145.454368] HB: declare canonical structure instance +[1768978492.026099] HB: we can build a bug_435_B2 on unit +[1768978492.026386] HB: declare canonical structure instance Datatypes_unit__canonical__bug_435_B2 -[1734568145.454595] HB: structure instance for +[1768978492.026586] HB: structure instance for Datatypes_unit__canonical__bug_435_B2 is {| B2.sort := unit; B2.class := {| B2.bug_435_A2_mixin := HB_unnamed_factory_5 |} |} -[1734568145.457247] HB: structure instance +[1768978492.027944] HB: structure instance Datatypes_unit__canonical__bug_435_B2 declared -[1734568145.458503] HB: we can build a should_work_but_fails_B on unit -[1734568145.458865] HB: declare canonical structure instance +testTy : JustMixedParam.type ?T + : JustMixedParam.type ?T +where +?T : [ |- Type] +[1768978492.028611] HB: we can build a should_work_but_fails_B on unit +[1768978492.028885] HB: declare canonical structure instance Datatypes_unit__canonical__should_work_but_fails_B -[1734568145.459100] HB: structure instance for +[1768978492.029120] HB: structure instance for Datatypes_unit__canonical__should_work_but_fails_B is {| B.sort := unit; @@ -1905,7 +1946,7 @@ B.bug_435_A2_mixin := HB_unnamed_factory_5 |} |} -[1734568145.459651] HB: closing instance section +[1768978492.029499] HB: closing instance section unit : B.type ?t : B.type ?t where @@ -1920,20 +1961,12 @@ File "./examples/demo2/stage10.v", line 4, characters 0-25: Warning: Hiding binding of key Q to Q_scope [hiding-delimiting-key,parsing,default] -[1734568146.424244] HB: exporting under the module path [] -[1734568146.424911] HB: exporting modules [] -[1734568146.425198] HB: exporting CS instances [] -[1734568146.425440] HB: exporting Abbreviations [] -[1734568146.425670] HB: exporting Clauses X0 File "./examples/demo2/stage11.v", line 115, characters 2-100: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./examples/demo2/stage10.v", line 112, characters 2-115: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] -File "./examples/demo2/stage11.v", line 288, characters 2-117: -Warning: HB: no new instance is generated -[HB.no-new-instance,HB,elpi,default] Qcplus_opp_r: forall q : Qc, q + - q = Q2Qc 0 File "./examples/demo2/stage10.v", line 233, characters 0-27: Warning: The default and global localities for this command outside sections @@ -1946,6 +1979,9 @@ any surrounding modules. If you are fine with the change of semantics, disable this warning. [deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] +File "./examples/demo2/stage11.v", line 288, characters 2-117: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] File "./examples/demo2/stage11.v", line 314, characters 2-116: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] @@ -1961,30 +1997,30 @@ disable this warning. [deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] HB: skipping section opening -[1734568149.025724] HB: declare mixin instance +[1768978493.900531] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology -[1734568149.027636] HB: declare canonical mixin instance +[1768978493.901685] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology» -[1734568149.029210] HB: declare mixin instance +[1768978493.902884] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform -[1734568149.035643] HB: declare canonical mixin instance +[1768978493.906842] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform» -[1734568149.037520] HB: declare mixin instance +[1768978493.907926] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology -[1734568149.042310] HB: declare canonical mixin instance +[1768978493.910658] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology» -[1734568149.044017] HB: declare mixin instance +[1768978493.911671] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform -[1734568149.046927] HB: declare canonical mixin instance +[1768978493.913595] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform» -[1734568149.049167] HB: we can build a Stage11_UniformSpace_wo_Topology on +[1768978493.915007] HB: we can build a Stage11_UniformSpace_wo_Topology on Qc -[1734568149.049567] HB: declare canonical structure instance +[1768978493.915279] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology -[1734568149.049798] HB: Giving name HB_unnamed_mixin_46 to mixin instance +[1768978493.915537] 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 -[1734568149.051137] HB: structure instance for +[1768978493.916466] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology is {| UniformSpace_wo_Topology.sort := Qc; @@ -1994,12 +2030,12 @@ HB_unnamed_mixin_46 |} |} -[1734568149.052621] HB: structure instance +[1768978493.917540] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology declared -[1734568149.053800] HB: we can build a Stage11_UniformSpace on Qc -[1734568149.054128] HB: declare canonical structure instance +[1768978493.918452] HB: we can build a Stage11_UniformSpace on Qc +[1768978493.918713] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace -[1734568149.054361] HB: structure instance for +[1768978493.918910] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace is {| UniformSpace.sort := Qc; @@ -2009,15 +2045,15 @@ UniformSpace.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_46 |} |} -[1734568149.055921] HB: structure instance +[1768978493.919933] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace declared -[1734568149.057147] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc -[1734568149.057426] HB: declare canonical structure instance +[1768978493.920916] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc +[1768978493.921173] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform -[1734568149.057769] HB: Giving name HB_unnamed_mixin_47 to mixin instance +[1768978493.921420] 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 -[1734568149.059240] HB: structure instance for +[1768978493.922431] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform is {| TAddAG_wo_Uniform.sort := Qc; @@ -2029,12 +2065,12 @@ HB_unnamed_mixin_47 |} |} -[1734568149.060615] HB: structure instance +[1768978493.923526] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform declared -[1734568149.062506] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc -[1734568149.062890] HB: declare canonical structure instance +[1768978493.925043] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc +[1768978493.925293] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined -[1734568149.063172] HB: structure instance for +[1768978493.925545] HB: structure instance for Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined is {| Uniform_TAddAG_unjoined.sort := Qc; @@ -2049,18 +2085,18 @@ HB_unnamed_mixin_46 |} |} -[1734568149.064672] HB: structure instance +[1768978493.926683] HB: structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined declared -[1734568149.067814] HB: we can build a Stage11_TAddAG on Qc -[1734568149.068115] HB: declare canonical structure instance +[1768978493.929258] HB: we can build a Stage11_TAddAG on Qc +[1768978493.929518] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG -[1734568149.068440] HB: Giving name HB_unnamed_mixin_48 to mixin instance +[1768978493.929839] 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 -[1734568149.070238] HB: Giving name HB_unnamed_mixin_49 to mixin instance +[1768978493.931116] 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 -[1734568149.071914] HB: structure instance for +[1768978493.932379] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG is {| TAddAG.sort := Qc; @@ -2074,13 +2110,13 @@ TAddAG.Stage11_Join_TAddAG_Uniform_mixin := HB_unnamed_mixin_49 |} |} -[1734568149.073757] HB: structure instance +[1768978493.933767] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG declared entourage : set (set (Qc * Qc)) : set (set (Qc * Qc)) -Finished transaction in 23.996 secs (21.622u,1.712s) (successful) +Finished transaction in 10.421 secs (9.56u,0.856s) (successful) Finished transaction in 0. secs (0.u,0.s) (successful) -Finished transaction in 19.226 secs (17.892u,1.315s) (successful) +Finished transaction in 11.598 secs (10.411u,0.823s) (successful) Module Type new_concept_Locked = Sig @@ -2143,7 +2179,7 @@ debian/rules override_dh_auto_install make[1]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.8.0' dh_auto_install --destdir=debian/tmp/ - make -j20 install DESTDIR=/build/reproducible-path/coq-hierarchy-builder-1.8.0/debian/tmp AM_UPDATE_INFO_DIR=no "INSTALL=install --strip-program=true" + make -j42 install DESTDIR=/build/reproducible-path/coq-hierarchy-builder-1.8.0/debian/tmp AM_UPDATE_INFO_DIR=no "INSTALL=install --strip-program=true" make[2]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.8.0' make -f Makefile.coq install make[3]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.8.0' @@ -2190,12 +2226,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/3960371/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/3960371/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/2728966 and its subdirectories -I: Current time: Wed Dec 18 12:30:11 -12 2024 -I: pbuilder-time-stamp: 1734568211 +I: removing directory /srv/workspace/pbuilder/3960371 and its subdirectories +I: Current time: Wed Jan 21 20:55:45 +14 2026 +I: pbuilder-time-stamp: 1768978545