Diff of the two buildlogs: -- --- b1/build.log 2024-05-11 12:22:33.166817901 +0000 +++ b2/build.log 2024-05-11 12:24:36.281580086 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Sat May 11 00:16:27 -12 2024 -I: pbuilder-time-stamp: 1715429787 +I: Current time: Sat Jun 14 08:45:37 +14 2025 +I: pbuilder-time-stamp: 1749840337 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.6.0-1.debian.tar.xz I: Not using root during the build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/3930154/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/1242516/tmp/hooks/D01_modify_environment starting +debug: Running on ionos5-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 Jun 13 18:45 /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/1242516/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/1242516/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='trixie' - 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]="21" [3]="1" [4]="release" [5]="x86_64-pc-linux-gnu") + BASH_VERSION='5.2.21(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=amd64 + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=42 ' + DIRSTACK=() + DISTRIBUTION=trixie + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=x86_64 + HOST_ARCH=amd64 IFS=' ' - INVOCATION_ID='229dcf9113be41689858c89e6683393f' - 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='3930154' - PS1='# ' - PS2='> ' + INVOCATION_ID=5e0e946a855140639a95295897e92797 + 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=1242516 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.onJpw8XX/pbuilderrc_1GwL --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.onJpw8XX/b1 --logfile b1/build.log coq-hierarchy-builder_1.6.0-1.dsc' - SUDO_GID='111' - SUDO_UID='106' - 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.onJpw8XX/pbuilderrc_ZlFu --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.onJpw8XX/b2 --logfile b2/build.log coq-hierarchy-builder_1.6.0-1.dsc' + SUDO_GID=110 + SUDO_UID=105 + 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 ionos11-amd64 6.1.0-21-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.90-1 (2024-05-03) x86_64 GNU/Linux + Linux i-capture-the-hostname 6.6.13+bpo-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.6.13-1~bpo12+1 (2024-02-15) x86_64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 May 10 11:25 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/3930154/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Jun 13 17:46 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/1242516/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -199,7 +231,7 @@ Get: 78 http://deb.debian.org/debian trixie/main amd64 libelpi-ocaml-dev amd64 1.17.4-3+b1 [9354 kB] Get: 79 http://deb.debian.org/debian trixie/main amd64 libcoq-elpi amd64 1.19.3-2+b1 [2577 kB] Get: 80 http://deb.debian.org/debian trixie/main amd64 wdiff amd64 1.2.2-6 [119 kB] -Fetched 353 MB in 7s (47.1 MB/s) +Fetched 353 MB in 7s (51.4 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libpython3.11-minimal:amd64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 19699 files and directories currently installed.) @@ -470,8 +502,8 @@ Setting up tzdata (2024a-4) ... Current default time zone: 'Etc/UTC' -Local time is now: Sat May 11 12:19:25 UTC 2024. -Universal Time is now: Sat May 11 12:19:25 UTC 2024. +Local time is now: Fri Jun 13 18:46:42 UTC 2025. +Universal Time is now: Fri Jun 13 18:46:42 UTC 2025. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up autotools-dev (20220109.1) ... @@ -546,7 +578,11 @@ Building tag database... -> Finished parsing the build-deps I: Building the package -I: Running cd /build/reproducible-path/coq-hierarchy-builder-1.6.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.6.0-1_source.changes +I: user script /srv/workspace/pbuilder/1242516/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for trixie +I: user script /srv/workspace/pbuilder/1242516/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/coq-hierarchy-builder-1.6.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.6.0-1_source.changes dpkg-buildpackage: info: source package coq-hierarchy-builder dpkg-buildpackage: info: source version 1.6.0-1 dpkg-buildpackage: info: source distribution unstable @@ -576,7 +612,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.6.0' make config make[2]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.6.0' @@ -594,8 +630,8 @@ make test-suite make[2]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.6.0' make -f Makefile.coq -make[3]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.6.0' /usr/bin/coq_makefile -f _CoqProject.test-suite -o Makefile.test-suite.coq +make[3]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.6.0' Warning: . and tests overlap (used in -R or -Q) Warning: . and examples overlap (used in -R or -Q) @@ -625,13 +661,97 @@ COQC examples/FSCD2020_material/V4.v COQC examples/FSCD2020_talk/V1.v COQC examples/FSCD2020_talk/V2.v -inhab - : ?s -where -?T : [ |- Type] -?s : [ |- s1.type ?T] -[1715430026.348790] HB: start module and section AddComoid_of_Type -[1715430026.349386] HB: converting arguments +COQC examples/FSCD2020_talk/V3.v +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/test_CS_db_filtering.v +COQC tests/subtype.v +COQC tests/infer.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 +Notation big := big.body +Expands to: Notation HB.tests.lock.X.big +COQC tests/short.v +(* + +Module A. +Section A. +Variable T : Type. +Local Arguments T : clear implicits. +Section axioms_. +Local Unset Implicit Arguments. +Record axioms_ (elpi_ctx_entry_0_ : Type) : Type := Axioms_ + { + a : elpi_ctx_entry_0_; + f : elpi_ctx_entry_0_ -> elpi_ctx_entry_0_; + p : forall x : elpi_ctx_entry_0_, 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). + +*) +[1749840419.839079] HB: start module and section hasA +[1749840419.839599] 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 +[1749840419.839856] HB: processing key parameter +[1749840419.840727] HB: converting factories +w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins +[1749840419.840910] HB: declaring context +w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] +[1749840419.841277] HB: declaring parameters and key as section variables +Here is the list of mixins to declare (the order matters): [] +[1749840419.853462] HB: declare mixin or factory +[1749840419.853743] HB: declare record axioms_ +[1749840419.886311] HB: declare notation Build +[1749840419.891538] HB: start module and section AddComoid_of_Type +[1749840419.892062] HB: converting arguments indt-decl (parameter A explicit X0 c0 \ record AddComoid_of_Type (sort (typ X1)) Build_AddComoid_of_Type @@ -657,26 +777,47 @@ app [global (indt «eq»), X10 c0 c1 c2 c3 c4 c5, app [c2, c1, c5], c5]) c5 \ end-record)) to factories -[1715430026.355266] HB: processing key parameter -[1715430026.357431] HB: converting factories +[1749840419.893711] HB: processing key parameter +[1749840419.894681] HB: converting factories w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] to mixins -[1715430026.366164] HB: declaring context +[1749840419.894951] HB: declaring context w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] -[1715430026.366614] HB: declaring parameters and key as section variables +[1749840419.895376] HB: declaring parameters and key as section variables +[1749840419.901479] HB: declare notation axioms Here is the list of mixins to declare (the order matters): [] -[1715430026.413290] HB: declare mixin or factory -[1715430026.413504] HB: declare record axioms_ +[1749840419.910582] HB: declare mixin or factory +[1749840419.910848] HB: declare record axioms_ +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] +[1749840419.934429] HB: start module Exports +inhab + : ?s +where +?T : [ |- Type] +?s : [ |- s1.type ?T] +[1749840419.972647] HB: declare notation Build +[1749840419.977372] HB: end modules and sections; export +«HB.tests.hb_pack.hasA.Exports» +hasA.type not a defined object. +[1749840420.000581] HB: declare notation axioms +COQC tests/primitive_records.v +[1749840420.034013] HB: start module Exports eq_refl : inhab = 7 : inhab = 7 -COQC examples/FSCD2020_talk/V3.v eq_refl : inhab = (7 :: nil)%list : inhab = (7 :: nil)%list where ?T : [ |- Type] -[1715430026.618488] HB: declare notation Build -[1715430026.688711] HB: declare notation axioms -[1715430026.838682] HB: start module Exports -[1715430027.825652] HB: end modules and sections; export +COQC tests/non_forgetful_inheritance.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 +[1749840420.219996] HB: end modules and sections; export «HB.examples.readme.AddComoid_of_Type.Exports» (* @@ -733,51 +874,81 @@ Notation AddComoid_of_Type X1 := ( AddComoid_of_Type.phant_axioms X1). *) -[1715430027.894255] HB: start module AddComoid -[1715430027.895949] HB: declare axioms record +[1749840420.251432] HB: start module AddComoid +[1749840420.251861] HB: declare axioms record w-params.nil A (sort (typ «HB.examples.readme.25»)) c0 \ [triple (indt «AddComoid_of_Type.axioms_») [] c0] -[1715430027.896462] HB: typing class field +[1749840420.252150] HB: typing class field indt «AddComoid_of_Type.axioms_» -[1715430027.925523] HB: declare type record -[1715430027.969180] HB: structure: new mixins +[1749840420.264114] HB: declare type record +[1749840420.278311] HB: structure: new mixins [indt «AddComoid_of_Type.axioms_»] -[1715430027.969975] HB: structure: mixin first class +[1749840420.278571] HB: structure: mixin first class [mixin-first-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»)] -[1715430027.970536] HB: declaring clone abbreviation -[1715430028.005998] HB: declaring pack_ constant -[1715430028.008828] HB: declaring pack_ constant = +[1749840420.278716] HB: declaring clone abbreviation +[1749840420.293640] HB: declaring pack_ constant +[1749840420.295048] 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]] -[1715430028.015955] HB: start module Exports -[1715430028.022914] HB: making coercion from type to target -[1715430028.023052] HB: declare sort coercion -[1715430028.023820] HB: exporting unification hints -[1715430028.024021] HB: exporting coercions from class to mixins -[1715430028.024483] HB: export class to mixin coercion for mixin +default : nat + : nat +[1749840420.298424] HB: start module Exports +[1749840420.298945] HB: making coercion from type to target +[1749840420.299049] HB: declare sort coercion +[1749840420.299589] HB: exporting unification hints +[1749840420.299926] HB: exporting coercions from class to mixins +[1749840420.300326] HB: export class to mixin coercion for mixin readme_AddComoid_of_Type -[1715430028.025192] HB: accumulating various props -[1715430028.099938] HB: stop module Exports -[1715430028.144220] HB: declaring on_ abbreviation -[1715430028.300547] HB: declaring `copy` abbreviation -[1715430028.319203] HB: declaring on abbreviation -[1715430028.419879] HB: end modules; export +[1749840420.300913] HB: accumulating various props +COQC tests/fix_loop.v +COQC tests/test_synthesis_params.v +COQC tests/hnf.v +COQC tests/fun_instance.v +[1749840420.316476] HB: stop module Exports +COQC tests/issue284.v +[1749840420.325356] HB: declaring on_ abbreviation +[1749840420.338611] HB: declaring `copy` abbreviation +[1749840420.340764] HB: declaring on abbreviation +[1749840420.351601] HB: end modules; export «HB.examples.readme.AddComoid.Exports» -[1715430028.434386] HB: exporting operations -[1715430028.436170] HB: export operation zero -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. -[1715430028.467564] HB: export operation add -[1715430028.532741] HB: export operation addrA -COQC examples/Coq2020_material/CoqWS_demo.v -[1715430028.608686] HB: export operation addrC -[1715430028.657350] HB: export operation add0r -[1715430028.703430] HB: operations meta-data module: ElpiOperations -[1715430028.825934] HB: abbreviation factory-by-classname +[1749840420.354057] HB: exporting operations +[1749840420.356026] HB: export operation zero +[1749840420.362332] HB: export operation add +[1749840420.369208] HB: export operation addrA +[1749840420.376363] HB: export operation addrC +[1749840420.383712] HB: export operation add0r +[1749840420.389240] HB: operations meta-data module: ElpiOperations +p : pred nat + : pred nat +HB.check: bar.type_ bool nat bool : Type +File "./tests/infer.v", line 20, characters 0-62: +Warning: Skipping test on Coq 8.18.0 as requested [HB.skip,HB,elpi,default] +bar.phant_type = +fun (A : Type) (P : foo.type) (_ : ssreflect.phant P) (B : Type) => +bar.type_ A P B + : Type -> forall P : foo.type, ssreflect.phant P -> Type -> Type + +Arguments bar.phant_type A%type_scope P _ B%type_scope +Notation bar.type _elpi_ctx_entry_3_was_A_ _elpi_ctx_entry_2_was_P_ + _elpi_ctx_entry_1_was_B_ := + (bar.phant_type _elpi_ctx_entry_3_was_A_ _ + (ssreflect.Phant _elpi_ctx_entry_2_was_P_) _elpi_ctx_entry_1_was_B_) +bar.phant_type bool Datatypes_nat__canonical__infer_foo + (ssreflect.Phant nat) bool + : Type +[1749840420.407987] HB: abbreviation factory-by-classname +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/issue287.v +[1749840420.435241] HB: begin module for builders +[1749840420.435740] HB: postulating factories +[1749840420.435886] HB: processing key context-item +[1749840420.436300] HB: processing mixin parameter a +[1749840420.436757] HB: declaring parameters and key as section variables +Here is the list of mixins to declare (the order matters): [] +COQC examples/demo1/test_0_0.v (* Module AddComoid. @@ -871,61 +1042,6 @@ *) forall (M : AddComoid.type) (x : M), x + x = 0 : Prop -[1715430029.668937] HB: begin module for builders -[1715430029.676686] HB: postulating factories -[1715430029.678231] HB: processing key context-item -[1715430029.679626] HB: processing mixin parameter a -[1715430029.680902] HB: declaring parameters and key as section variables -Here is the list of mixins to declare (the order matters): [] -COQC examples/Coq2020_material/CoqWS_abstract.v -COQC examples/Coq2020_material/CoqWS_expansion/withHB.v -File "./examples/FSCD2020_talk/V2.v", line 17, characters 0-66: -Warning: -pulling in dependencies: [V2_is_semigroup] - -Please list them or end the declaration with '&' -[HB.implicit-structure-dependency,HB,elpi,default] -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/Coq2020_material/CoqWS_expansion/withoutHB.v -COQC tests/type_of_exported_ops.v -COQC tests/duplicate_structure.v -Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. - -Arguments Monoid.Pack sort%type_scope class -@add - : forall s : Monoid.type, s -> s -> s -@addNr - : forall s : AbelianGroup.type, left_inverse 0 opp add -@addrC - : forall s : AbelianGroup.type, commutative add -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 tests/instance_params_no_type.v -COQC tests/test_CS_db_filtering.v -COQC tests/subtype.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/infer.v -[1715430033.664395] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_AddAG_of_AddComoid -[1715430033.674072] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_Ring_of_AddAG -COQC tests/exports.v add : ?s -> ?s -> ?s where @@ -934,196 +1050,90 @@ : commutative add where ?s : [ |- CMonoid.type] +fun X : s2.type nat => inhab : X + : forall X : s2.type nat, X addrC : commutative add where ?s : [ |- CMonoid.type] -COQC tests/log_impargs_record.v +fun X : s2.type nat => inj : nat -> X + : forall X : s2.type nat, nat -> X +s2_to_s1 not a defined object. +hasB.type not a defined object. +COQC examples/demo3/test_0_0.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 +File "./tests/funclass.v", line 19, characters 54-64: +Warning: Notation plus_assoc is deprecated since 8.16. +The Arith.Plus file is obsolete. Use Nat.add_assoc instead. +[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] +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 +bar1.phant_type Datatypes_nat__canonical__infer_foo (ssreflect.Phant nat) + : Type File "./examples/Coq2020_material/CoqWS_demo.v", line 73, characters 0-73: Warning: pulling in dependencies: [CoqWS_demo_CMonoid_of_Type] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] -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 -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 : Ring.type, left_inverse 0 opp add -COQC tests/compress_coe.v 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 -File "./examples/hulk.v", line 143, characters 0-63: +File "./examples/FSCD2020_talk/V2.v", line 17, characters 0-66: Warning: -pulling in dependencies: [Feather_HasEqDec] +pulling in dependencies: [V2_is_semigroup] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] +aType + : Type +COQC examples/demo1/test_1_0.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/grefclass.v -COQC tests/local_instance.v -COQC tests/lock.v -Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. - -Arguments Monoid.Pack sort%type_scope class -@add - : forall s : Monoid.type, s -> s -> s -@addNr - : forall s : AbelianGroup.type, left_inverse 0 opp add -@addrC - : forall s : AbelianGroup.type, commutative add -COQC tests/interleave_context.v -(* - -Module A. -Section A. -Variable T : Type. -Local Arguments T : clear implicits. -Section axioms_. -Local Unset Implicit Arguments. -Record axioms_ (elpi_ctx_entry_0_ : Type) : Type := Axioms_ - { - a : elpi_ctx_entry_0_; - f : elpi_ctx_entry_0_ -> elpi_ctx_entry_0_; - p : forall x : elpi_ctx_entry_0_, f x = x -> True; - q : forall h : f a = a, p a h = p a h; - }. -End axioms_. - -Global Arguments axioms_ : clear implicits. -Global Arguments Axioms_ [_] [_] _ _ _. -Global Arguments a [_] _. -Global Arguments f [_] _ _. -Global Arguments p [_] _ [_] _. -Global Arguments q [_] _ _. -End A. -Global Arguments axioms_ : clear implicits. -Global Arguments Axioms_ : clear implicits. -Definition phant_Build : forall (T : Type) (a : T) (f : T -> T) - (p : forall x : T, f x = x -> True), - (forall h : f a = a, p a h = p a h) -> axioms_ T := - fun (T : Type) (a : T) (f : T -> T) (p : forall x : T, f x = x -> True) - (q : forall h : f a = a, p a h = p a h) => - {| a := a; f := f; p := p; q := q |}. -Local Arguments phant_Build : clear implicits. -Notation Build X1 := ( phant_Build X1). -Definition phant_axioms : Type -> Type := fun T : Type => axioms_ T. -Local Arguments phant_axioms : clear implicits. -Notation axioms X1 := ( phant_axioms X1). -Definition identity_builder : forall T : Type, axioms_ T -> axioms_ T := - fun (T : Type) (x : axioms_ T) => x. -Local Arguments identity_builder : clear implicits. -Module Exports. -Global Arguments Axioms_ {_}. -End Exports. -End A. -Export A.Exports. -Notation A X1 := ( A.phant_axioms X1). - -*) -COQC tests/not_same_key.v -HB: A is canonically equipped with structures: - - Equality - Singleton - (from "./examples/hulk.v", line 216) - -COQC tests/hb_pack.v -default : nat - : nat -COQC tests/declare.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/short.v -p : pred nat - : pred nat -COQC tests/primitive_records.v -forall x y : ?t, 1 + x = y * x - : Prop -where -?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) -COQC tests/non_forgetful_inheritance.v -HB.check: bar.type_ bool nat bool : Type -File "./tests/infer.v", line 20, characters 0-62: -Warning: Skipping test on Coq 8.18.0 as requested [HB.skip,HB,elpi,default] -bar.phant_type = -fun (A : Type) (P : foo.type) (_ : ssreflect.phant P) (B : Type) => -bar.type_ A P B - : Type -> forall P : foo.type, ssreflect.phant P -> Type -> Type - -Arguments bar.phant_type A%type_scope P _ B%type_scope -Notation bar.type _elpi_ctx_entry_3_was_A_ _elpi_ctx_entry_2_was_P_ - _elpi_ctx_entry_1_was_B_ := - (bar.phant_type _elpi_ctx_entry_3_was_A_ _ - (ssreflect.Phant _elpi_ctx_entry_2_was_P_) _elpi_ctx_entry_1_was_B_) -bar.phant_type bool Datatypes_nat__canonical__infer_foo - (ssreflect.Phant nat) bool - : Type -COQC tests/fix_loop.v -A.p : -forall [T : Type] (record : A.axioms_ T) [x : T], A.f record x = x -> True +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] -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/test_synthesis_params.v -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) -Notation big := big.body -Expands to: Notation HB.tests.lock.X.big -bar1.phant_type Datatypes_nat__canonical__infer_foo (ssreflect.Phant nat) - : Type -COQC tests/hnf.v -COQC tests/fun_instance.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 -[1715430040.879009] HB: start module SubInhab -[1715430040.879412] HB: declare axioms record +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB,elpi,default] +[1749840420.938555] HB: start module SubInhab +[1749840420.939016] 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] -[1715430040.879871] HB: typing class field indt «is_inhab.axioms_» -[1715430040.880273] HB: typing class field indt «is_SUB.axioms_» -[1715430040.905203] HB: declare type record -[1715430040.938325] HB: structure: new mixins [] -[1715430040.938580] HB: structure: mixin first class [] -[1715430040.938677] HB: declaring clone abbreviation -[1715430040.968563] HB: declaring pack_ constant -[1715430040.972463] HB: declaring pack_ constant = +[1749840420.939740] HB: typing class field indt «is_inhab.axioms_» +[1749840420.940273] HB: typing class field indt «is_SUB.axioms_» +AbelianGrp.phant_on_ BinNums_Z__canonical__readme_AbelianGrp + (Phant BinNums_Z__canonical__readme_AbelianGrp) + : AbelianGrp.axioms_ Z + : AbelianGrp.axioms_ Z +[1749840420.953572] HB: declare type record +[1749840420.965812] HB: structure: new mixins [] +[1749840420.966190] HB: structure: mixin first class [] +[1749840420.966365] HB: declaring clone abbreviation +HB: Z is canonically equipped with structures: + - AbelianGrp + (from "./examples/readme.v", line 32) + - AddComoid + (from "./examples/readme.v", line 31) + +[1749840420.978772] HB: declaring pack_ constant +[1749840420.982274] 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 \ @@ -1132,142 +1142,63 @@ app [global (indc «Pack»), c0, c1, c2, app [global (indc «Class»), c0, c1, c2, c3, c4]] -[1715430040.975728] HB: start module and section hasA -[1715430040.976278] 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 -[1715430040.976466] HB: processing key parameter -[1715430040.977057] HB: converting factories -w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins -[1715430040.977180] HB: declaring context -w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] -[1715430040.977348] HB: declaring parameters and key as section variables -[1715430040.985315] HB: start module Exports -[1715430040.985858] HB: making coercion from type to target -[1715430040.986000] HB: declare sort coercion -[1715430040.986604] HB: exporting unification hints -[1715430040.991385] HB: declare coercion subtype_SubInhab__to__subtype_SUB -[1715430040.993273] HB: declare coercion hint +[1749840420.985346] HB: start module Exports +[1749840420.985936] HB: making coercion from type to target +[1749840420.986203] HB: declare sort coercion +[1749840420.986713] HB: exporting unification hints +[1749840420.987836] HB: declare coercion subtype_SubInhab__to__subtype_SUB +[1749840420.989410] HB: declare coercion hint subtype_SubInhab_class__to__subtype_SUB_class -Here is the list of mixins to declare (the order matters): [] -[1715430041.002310] HB: declare mixin or factory -[1715430041.002614] HB: declare record axioms_ -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop -[1715430041.014008] HB: declare unification hint +hasB.type not a defined object. +[1749840421.000131] HB: declare unification hint subtype_SubInhab__to__subtype_SUB -[1715430041.039876] HB: declare coercion subtype_SubInhab__to__subtype_Inhab -[1715430041.048088] HB: declare coercion hint +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 +[1749840421.012595] HB: declare coercion subtype_SubInhab__to__subtype_Inhab +[1749840421.014317] HB: declare coercion hint subtype_SubInhab_class__to__subtype_Inhab_class -[1715430041.056876] HB: declare notation Build -[1715430041.072351] HB: declare unification hint +[1749840421.025284] HB: declare unification hint subtype_SubInhab__to__subtype_Inhab -[1715430041.082595] HB: declare notation axioms -[1715430041.102614] HB: declare unification hint +[1749840421.039200] HB: declare unification hint join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB -[1715430041.127592] HB: exporting coercions from class to mixins -[1715430041.130945] HB: export class to mixin coercion for mixin +[1749840421.050729] HB: exporting coercions from class to mixins +[1749840421.051845] HB: export class to mixin coercion for mixin subtype_is_inhab -[1715430041.137295] HB: start module Exports -[1715430041.140768] HB: export class to mixin coercion for mixin +[1749840421.054368] HB: export class to mixin coercion for mixin subtype_is_SUB -[1715430041.142785] HB: accumulating various props -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop -[1715430041.169113] HB: stop module Exports -[1715430041.193328] HB: declaring on_ abbreviation -[1715430041.213510] HB: end modules and sections; export -«HB.tests.hb_pack.hasA.Exports» -COQC tests/issue284.v -[1715430041.220613] HB: declaring `copy` abbreviation -[1715430041.232413] HB: declaring on abbreviation -hasA.type not a defined object. -[1715430041.264755] HB: end modules; export -«HB.tests.subtype.SubInhab.Exports» -COQC tests/issue287.v -[1715430041.281513] HB: exporting operations -[1715430041.294190] HB: operations meta-data module: ElpiOperations -[1715430041.320357] HB: abbreviation factory-by-classname -COQC examples/demo1/test_0_0.v -add - : A -> A -> A -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 -Query assignments: - Ind = «hasA.axioms_» -File "./tests/funclass.v", line 19, characters 54-64: -Warning: Notation plus_assoc is deprecated since 8.16. -The Arith.Plus file is obsolete. Use Nat.add_assoc instead. -[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] -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. -aType - : Type -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop -Query assignments: - Ind = «A.axioms_» -COQC examples/demo1/test_1_0.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 -hasB.type not a defined object. -COQC examples/demo1/test_2_0.v -Datatypes_prod__canonical__compress_coe_D = -fun D D' : D.type => -{| - D.sort := D.sort D * D.sort D'; - D.class := - {| - D.compress_coe_hasA_mixin := - prodA (compress_coe_D__to__compress_coe_A D) - (compress_coe_D__to__compress_coe_A D'); - D.compress_coe_hasB_mixin := - prodB tt (compress_coe_D__to__compress_coe_B D) - (compress_coe_D__to__compress_coe_B D'); - D.compress_coe_hasC_mixin := - prodC tt tt (compress_coe_D__to__compress_coe_C D) - (compress_coe_D__to__compress_coe_C D'); - D.compress_coe_hasD_mixin := prodD D D' - |} -|} - : D.type -> D.type -> D.type +[1749840421.056369] HB: accumulating various props +[1749840421.069531] HB: stop module Exports +[1749840421.079324] HB: declaring on_ abbreviation +Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. -Arguments Datatypes_prod__canonical__compress_coe_D D D' -COQC examples/demo1/test_3_0.v -hasAB.type not a defined object. -hasA'.type not a defined object. +Arguments Monoid.Pack sort%type_scope class +@add + : forall s : Monoid.type, s -> s -> s +@addNr + : forall s : Ring.type, left_inverse 0 opp add +[1749840421.093272] HB: declaring `copy` abbreviation +[1749840421.095918] HB: declaring on abbreviation +[1749840421.105453] HB: end modules; export +«HB.tests.subtype.SubInhab.Exports» +[1749840421.110555] HB: exporting operations +[1749840421.111191] HB: operations meta-data module: ElpiOperations 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] -File "./tests/non_forgetful_inheritance.v", line 35, characters 0-45: -Warning: Could not enable unknown warning HB.non-forgetful-inheritance -[unknown-warning,default] -COQC examples/demo1/test_3_3.v -COQC examples/demo2/stage10.v +[1749840421.120266] HB: abbreviation factory-by-classname +hasAB.type not a defined object. +hasA'.type not a defined object. +COQC examples/demo3/test_1_0.v HB.check: forall w : wp.phant_type nat Nat_mul__canonical__funclass_Monoid (Phantom (nat -> nat -> nat) Init.Nat.mul), w = w : Prop -Query assignments: -COQC examples/demo2/stage11.v - Ind = «A.type» -COQC examples/demo3/test_0_0.v -COQC examples/demo3/test_1_0.v forall T : AB.type, unkeyed {| @@ -1281,38 +1212,65 @@ |} |} : Type -[1715430045.812151] HB: exporting under the module path [] -[1715430045.812680] HB: exporting modules -[Ring_of_TYPE.Exports, Ring.Exports, ElpiOperations1, RingExports, - Dummy.Exports, URing.Exports, ElpiOperations2, dummy.Exports, - Builders_3.dummy_Exports] -[1715430045.815482] HB: exporting CS instances -[«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] -[1715430045.816325] 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 A : A.type : A.type -COQC examples/demo3/test_2_0.v A : A.type : A.type -COQC tests/exports2.v AB1 : hasB.phant_axioms A -> AB.type : hasB.phant_axioms A -> AB.type +forall x y : ?t, 1 + x = y * x + : Prop +where +?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) Bm : hasB.phant_axioms A : hasB.phant_axioms A AB2 : AB.type : AB.type +Query assignments: + Ind = «hasA.axioms_» pB : T * T : T * T AB3 : AB.type : AB.type +hasAB.type not a defined object. +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 +hasA'.type not a defined object. +[1749840421.482346] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_AddAG_of_AddComoid +[1749840421.482663] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_Ring_of_AddAG +Datatypes_prod__canonical__compress_coe_D = +fun D D' : D.type => +{| + D.sort := D.sort D * D.sort D'; + D.class := + {| + D.compress_coe_hasA_mixin := + prodA (compress_coe_D__to__compress_coe_A D) + (compress_coe_D__to__compress_coe_A D'); + D.compress_coe_hasB_mixin := + prodB tt (compress_coe_D__to__compress_coe_B D) + (compress_coe_D__to__compress_coe_B D'); + D.compress_coe_hasC_mixin := + prodC tt tt (compress_coe_D__to__compress_coe_C D) + (compress_coe_D__to__compress_coe_C D'); + D.compress_coe_hasD_mixin := prodD D D' + |} +|} + : D.type -> D.type -> D.type + +Arguments Datatypes_prod__canonical__compress_coe_D D D' +File "./tests/non_forgetful_inheritance.v", line 35, characters 0-45: +Warning: Could not enable unknown warning HB.non-forgetful-inheritance +[unknown-warning,default] Datatypes_nat__canonical__hnf_S = {| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_8 |} |} : S.type @@ -1325,37 +1283,115 @@ HB_unnamed_mixin_12 = Builders_2.HB_unnamed_factory_4 bool HB_unnamed_factory_9 : M.axioms_ bool -COQC examples/demo1/test_4_0.v -HB.check: -SemiRing_of_AddComoid.axioms_ - : (forall (A : Type) (m : AddMonoid_of_TYPE.axioms_ A), - AddComoid_of_AddMonoid.axioms_ A m -> Type) -: -forall (A : Type) (m : AddMonoid_of_TYPE.axioms_ A), -AddComoid_of_AddMonoid.axioms_ A m -> Type -COQC examples/demo1/test_4_3.v -erefl ?t : ?t = ?t - : ?t = ?t -where -?t : [ |- Sq.type] -COQC examples/demo1/test_5_0.v +File "./examples/hulk.v", line 143, characters 0-63: +Warning: +pulling in dependencies: [Feather_HasEqDec] + +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB,elpi,default] X : Foo.type A P : Foo.type A P -COQC examples/demo1/test_5_3.v -hasAB.type not a defined object. +forall (G : AbelianGrp.type) (x : G), x - x = 0 + : Prop +[1749840421.632662] HB: exporting under the module path [] +[1749840421.633174] HB: exporting modules +[Ring_of_TYPE.Exports, Ring.Exports, ElpiOperations1, RingExports, + Dummy.Exports, URing.Exports, ElpiOperations2, dummy.Exports, + Builders_3.dummy_Exports] +forall (S : SemiRing.type) (x : S), x * 1 + 0 = x + : Prop +forall (R : Ring.type) (x y : R), x * - (1 * y) = - x * y + : Prop +[1749840421.635996] HB: exporting CS instances +[«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] +[1749840421.636833] HB: exporting Abbreviations [addr0, addrNK] +forall (R : Enclosing.Ring.type) (x : R), x = x + : Prop +0%G + : ?s +where +?s : [ |- Enclosing.Ring.type] +COQC examples/demo2/stage10.v +COQC examples/demo2/stage11.v +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) +Enclosing.zero : Z + : Z +COQC tests/exports2.v +Query assignments: + Ind = «A.axioms_» +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop T : Fun.type nat : Fun.type nat -hasA'.type not a defined object. -[1715430049.049238] HB: exporting under the module path [] -[1715430049.049901] HB: exporting modules [] -[1715430049.050103] HB: exporting CS instances [] -[1715430049.050313] HB: exporting Abbreviations [] +COQC examples/demo1/test_2_0.v +HB: A is canonically equipped with structures: + - Equality + Singleton + (from "./examples/hulk.v", line 216) + +Query assignments: + Ind = «A.type» +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 +COQC examples/demo3/test_2_0.v +COQC examples/demo1/test_3_0.v +COQC examples/demo1/test_3_3.v +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop +[1749840422.185759] HB: exporting under the module path [] +[1749840422.185923] HB: exporting modules [] +[1749840422.186026] HB: exporting CS instances [] +[1749840422.186671] 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] File "./examples/demo2/stage11.v", line 3, characters 0-25: Warning: Hiding binding of key Q to Q_scope [hiding-delimiting-key,parsing,default] +erefl ?t : ?t = ?t + : ?t = ?t +where +?t : [ |- Sq.type] +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 examples/demo1/test_4_0.v +COQC examples/demo1/test_4_3.v +HB.check: +SemiRing_of_AddComoid.axioms_ + : (forall (A : Type) (m : AddMonoid_of_TYPE.axioms_ A), + AddComoid_of_AddMonoid.axioms_ A m -> Type) +: +forall (A : Type) (m : AddMonoid_of_TYPE.axioms_ A), +AddComoid_of_AddMonoid.axioms_ A m -> Type +COQC examples/demo1/test_5_0.v +COQC examples/demo1/test_5_3.v 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 @@ -1380,30 +1416,30 @@ disable this warning. [deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] HB: skipping section opening -[1715430065.796597] HB: declare mixin instance +[1749840426.683542] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology -[1715430065.810815] HB: declare canonical mixin instance +[1749840426.686109] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology» -[1715430065.820699] HB: declare mixin instance +[1749840426.687317] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform -[1715430065.840974] HB: declare canonical mixin instance +[1749840426.692429] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform» -[1715430065.848201] HB: declare mixin instance +[1749840426.693473] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology -[1715430065.866094] HB: declare canonical mixin instance +[1749840426.697638] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology» -[1715430065.872240] HB: declare mixin instance +[1749840426.698690] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform -[1715430065.894408] HB: declare canonical mixin instance +[1749840426.701984] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform» -[1715430065.897996] HB: we can build a Stage11_UniformSpace_wo_Topology on +[1749840426.703559] HB: we can build a Stage11_UniformSpace_wo_Topology on Qc -[1715430065.898536] HB: declare canonical structure instance +[1749840426.703780] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology -[1715430065.898942] HB: Giving name HB_unnamed_mixin_49 to mixin instance +[1749840426.704031] HB: Giving name HB_unnamed_mixin_49 to mixin instance Builders_25.Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology Qc HB_unnamed_mixin_38 HB_unnamed_mixin_43 HB_unnamed_factory_44 -[1715430065.912063] HB: structure instance for +[1749840426.706096] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology is {| UniformSpace_wo_Topology.sort := Qc; @@ -1413,12 +1449,12 @@ HB_unnamed_mixin_49 |} |} -[1715430065.930406] HB: structure instance +[1749840426.709112] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology declared -[1715430065.932569] HB: we can build a Stage11_UniformSpace on Qc -[1715430065.932994] HB: declare canonical structure instance +[1749840426.710028] HB: we can build a Stage11_UniformSpace on Qc +[1749840426.710245] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace -[1715430065.942748] HB: structure instance for +[1749840426.710755] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace is {| UniformSpace.sort := Qc; @@ -1428,15 +1464,15 @@ UniformSpace.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_49 |} |} -[1715430065.955943] HB: structure instance +[1749840426.713559] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace declared -[1715430065.964049] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc -[1715430065.964739] HB: declare canonical structure instance +[1749840426.714611] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc +[1749840426.714830] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform -[1715430065.965783] HB: Giving name HB_unnamed_mixin_50 to mixin instance +[1749840426.715408] HB: Giving name HB_unnamed_mixin_50 to mixin instance Builders_25.to_JoinTAddAG_wo_Uniform Qc HB_unnamed_mixin_38 HB_unnamed_mixin_43 HB_unnamed_factory_44 -[1715430065.979267] HB: structure instance for +[1749840426.717540] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform is {| TAddAG_wo_Uniform.sort := Qc; @@ -1448,12 +1484,12 @@ HB_unnamed_mixin_50 |} |} -[1715430065.992468] HB: structure instance +[1749840426.720439] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform declared -[1715430066.001021] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc -[1715430066.001880] HB: declare canonical structure instance +[1749840426.721846] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc +[1749840426.722065] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined -[1715430066.007743] HB: structure instance for +[1749840426.722897] HB: structure instance for Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined is {| Uniform_TAddAG_unjoined.sort := Qc; @@ -1468,18 +1504,18 @@ HB_unnamed_mixin_49 |} |} -[1715430066.025492] HB: structure instance +[1749840426.725806] HB: structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined declared -[1715430066.039791] HB: we can build a Stage11_TAddAG on Qc -[1715430066.040725] HB: declare canonical structure instance +[1749840426.728337] HB: we can build a Stage11_TAddAG on Qc +[1749840426.728574] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG -[1715430066.042596] HB: Giving name HB_unnamed_mixin_51 to mixin instance +[1749840426.729360] HB: Giving name HB_unnamed_mixin_51 to mixin instance Builders_25.Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology Qc HB_unnamed_mixin_38 HB_unnamed_mixin_43 HB_unnamed_factory_44 -[1715430066.048363] HB: Giving name HB_unnamed_mixin_52 to mixin instance +[1749840426.731839] HB: Giving name HB_unnamed_mixin_52 to mixin instance Builders_25.Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform Qc HB_unnamed_mixin_38 HB_unnamed_mixin_43 HB_unnamed_factory_44 -[1715430066.064095] HB: structure instance for +[1749840426.734321] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG is {| TAddAG.sort := Qc; @@ -1493,13 +1529,13 @@ TAddAG.Stage11_Join_TAddAG_Uniform_mixin := HB_unnamed_mixin_52 |} |} -[1715430066.091150] HB: structure instance +[1749840426.737721] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG declared entourage : set (set (Qc * Qc)) : set (set (Qc * Qc)) -Finished transaction in 39.621 secs (21.917u,0.831s) (successful) -Finished transaction in 0.001 secs (0.001u,0.s) (successful) -Finished transaction in 28.01 secs (19.46u,0.548s) (successful) +Finished transaction in 10.331 secs (9.753u,0.571s) (successful) +Finished transaction in 0. secs (0.u,0.s) (successful) +Finished transaction in 9.046 secs (8.626u,0.42s) (successful) Module Type new_conceptLocked = Sig @@ -1554,7 +1590,7 @@ create-stamp debian/debhelper-build-stamp dh_prep dh_auto_install - make -j20 install DESTDIR=/build/reproducible-path/coq-hierarchy-builder-1.6.0/debian/tmp AM_UPDATE_INFO_DIR=no "INSTALL=install --strip-program=true" + make -j42 install DESTDIR=/build/reproducible-path/coq-hierarchy-builder-1.6.0/debian/tmp AM_UPDATE_INFO_DIR=no "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.6.0' make -f Makefile.coq install make[2]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.6.0' @@ -1591,14 +1627,14 @@ dh_ocaml W: coq-hierarchy-builder doesn't resolve dependency on unit Hb dh_gencontrol -dpkg-gencontrol: warning: Depends field of package coq-hierarchy-builder: substitution variable ${shlibs:Depends} used, but is not defined -dpkg-gencontrol: warning: package coq-hierarchy-builder: substitution variable ${ocaml:Depends} unused, but is defined dpkg-gencontrol: warning: Depends field of package libcoq-hierarchy-builder: substitution variable ${ocaml:Depends} used, but is not defined dpkg-gencontrol: warning: Depends field of package libcoq-hierarchy-builder: substitution variable ${shlibs:Depends} used, but is not defined +dpkg-gencontrol: warning: Depends field of package coq-hierarchy-builder: substitution variable ${shlibs:Depends} used, but is not defined +dpkg-gencontrol: warning: package coq-hierarchy-builder: substitution variable ${ocaml:Depends} unused, but is defined dh_md5sums dh_builddeb -dpkg-deb: building package 'coq-hierarchy-builder' in '../coq-hierarchy-builder_1.6.0-1_amd64.deb'. dpkg-deb: building package 'libcoq-hierarchy-builder' in '../libcoq-hierarchy-builder_1.6.0-1_amd64.deb'. +dpkg-deb: building package 'coq-hierarchy-builder' in '../coq-hierarchy-builder_1.6.0-1_amd64.deb'. dpkg-genbuildinfo --build=binary -O../coq-hierarchy-builder_1.6.0-1_amd64.buildinfo dpkg-genchanges --build=binary -O../coq-hierarchy-builder_1.6.0-1_amd64.changes dpkg-genchanges: info: binary-only upload (no source code included) @@ -1606,12 +1642,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/1242516/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/1242516/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/3930154 and its subdirectories -I: Current time: Sat May 11 00:22:32 -12 2024 -I: pbuilder-time-stamp: 1715430152 +I: removing directory /srv/workspace/pbuilder/1242516 and its subdirectories +I: Current time: Sat Jun 14 08:47:35 +14 2025 +I: pbuilder-time-stamp: 1749840455