Source: coq-hierarchy-builder Version: 1.2.1-11 Severity: serious Justification: FTBFS Tags: bookworm sid ftbfs User: lu...@debian.org Usertags: ftbfs-20220728 ftbfs-bookworm
Hi, During a rebuild of all packages in sid, your package failed to build on amd64. Relevant part (hopefully): > make[3]: Entering directory '/<<PKGBUILDDIR>>' > COQDEP VFILES > COQC examples/readme.v > COQC examples/hulk.v > COQC examples/demo1/hierarchy_1.v > COQC examples/demo1/hierarchy_0.v > COQC examples/demo1/hierarchy_2.v > COQC examples/demo1/hierarchy_3.v > COQC examples/demo1/hierarchy_4.v > COQC examples/demo1/hierarchy_5.v > [1659086976.184132] HB: start module and section AddComoid_of_Type > [1659086976.184758] HB: converting arguments > indt-decl > (parameter A explicit X0 c0 \ > record AddComoid_of_Type (sort (typ X1)) Build_AddComoid_of_Type > (field [coercion ff, canonical tt] zero c0 c1 \ > field [coercion ff, canonical tt] add > (prod `_` c0 c2 \ prod `_` c0 c3 \ c0) c2 \ > field [coercion ff, canonical tt] addrA > (prod `x` (X2 c0 c1 c2) c3 \ > prod `y` (X3 c0 c1 c2 c3) c4 \ > prod `z` (X4 c0 c1 c2 c3 c4) c5 \ > app > [global (indt «eq»), X5 c0 c1 c2 c3 c4 c5, > app [c2, c3, app [c2, c4, c5]], app [c2, app [c2, c3, c4], > c5]]) > c3 \ > field [coercion ff, canonical tt] addrC > (prod `x` (X6 c0 c1 c2 c3) c4 \ > prod `y` (X7 c0 c1 c2 c3 c4) c5 \ > app > [global (indt «eq»), X8 c0 c1 c2 c3 c4 c5, app [c2, c4, c5], > app [c2, c5, c4]]) c4 \ > field [coercion ff, canonical tt] add0r > (prod `x` (X9 c0 c1 c2 c3 c4) c5 \ > app > [global (indt «eq»), X10 c0 c1 c2 c3 c4 c5, app [c2, c1, c5], > c5]) c5 \ end-record)) to factories > [1659086976.186365] HB: processing key parameter > [1659086976.187092] HB: converting factories > w-params.nil A (sort (typ «readme.2»)) c0 \ [] to mixins > [1659086976.187468] HB: declaring context > w-params.nil A (sort (typ «readme.2»)) c0 \ [] > [1659086976.187764] HB: declaring parameters and key as section variables > [1659086976.197692] HB: declare mixin or factory > [1659086976.198044] HB: declare record axioms_: sort (typ X1) > [1659086976.228213] HB: declare notation Build > [1659086976.245750] HB: declare notation axioms > [1659086976.263949] HB: start module Exports > [1659086976.293276] HB: end modules and sections; export > «HB.examples.readme.AddComoid_of_Type.Exports» > (* > > Module AddComoid_of_Type. > Section AddComoid_of_Type. > Variable A : Type. > Local Arguments A : clear implicits. > Section axioms_. > Local Unset Implicit Arguments. > Record axioms_ (A : Type) : Type := Axioms_ > { > zero : elpi_ctx_entry_0_; > add : elpi_ctx_entry_0_ -> elpi_ctx_entry_0_ -> elpi_ctx_entry_0_; > addrA : forall x y z : elpi_ctx_entry_0_, add x (add y z) = add (add x y) > z; > addrC : forall x y : elpi_ctx_entry_0_, add x y = add y x; > add0r : forall x : elpi_ctx_entry_0_, add zero x = x; > }. > End axioms_. > > (*clause _ _ > (decl-location (indt «axioms_») > File "./examples/readme.v", line 4, column 0, character 78:)*) > Global Arguments axioms_ : clear implicits. > (*clause _ _ > (decl-location (indc «Axioms_») > File "./examples/readme.v", line 4, column 0, character 78:)*) > Global Arguments Axioms_ : clear implicits. > (*clause _ _ > (decl-location (const «zero») > File "./examples/readme.v", line 4, column 0, character 78:)*) > Global Arguments zero : clear implicits. > (*clause _ _ > (decl-location (const «add») > File "./examples/readme.v", line 4, column 0, character 78:)*) > Global Arguments add : clear implicits. > (*clause _ _ > (decl-location (const «addrA») > File "./examples/readme.v", line 4, column 0, character 78:)*) > Global Arguments addrA : clear implicits. > (*clause _ _ > (decl-location (const «addrC») > File "./examples/readme.v", line 4, column 0, character 78:)*) > Global Arguments addrC : clear implicits. > (*clause _ _ > (decl-location (const «add0r») > File "./examples/readme.v", line 4, column 0, character 78:)*) > Global Arguments add0r : clear implicits. > End AddComoid_of_Type. > Global Arguments axioms_ : clear implicits. > Global Arguments Axioms_ : clear implicits. > (*clause _ _ > (decl-location (const «phant_Build») > File "./examples/readme.v", line 4, column 0, character 78:)*) > Definition phant_Build : forall (A : Type) (zero : A) (add : A -> A -> A), > (forall x y z : A, add x (add y z) = add (add x y) > z) -> > (forall x y : A, add x y = add y x) -> > (forall x : A, add zero x = x) -> axioms_ A := > fun (A : Type) (zero : A) (add : A -> A -> A) > (addrA : forall x y z : A, add x (add y z) = add (add x y) z) > (addrC : forall x y : A, add x y = add y x) > (add0r : forall x : A, add zero x = x) => > {| > zero := zero; add := add; addrA := addrA; addrC := addrC; add0r := add0r > |}. > Local Arguments phant_Build : clear implicits. > Notation Build X1 := ( phant_Build X1). > (*clause _ _ > (decl-location (const «phant_axioms») > File "./examples/readme.v", line 4, column 0, character 78:)*) > Definition phant_axioms : Type -> Type := fun A : Type => axioms_ A. > Local Arguments phant_axioms : clear implicits. > Notation axioms X1 := ( phant_axioms X1). > (*clause _ _ > (decl-location (const «identity_builder») > File "./examples/readme.v", line 4, column 0, character 78:)*) > Definition identity_builder : forall A : Type, axioms_ A -> axioms_ A := > fun (A : Type) (x : axioms_ A) => x. > Local Arguments identity_builder : clear implicits. > Module Exports. > (*clause _ _ > (from (indt «axioms_») (indt «axioms_») (const «identity_builder»))*) > (*clause _ _ > (phant-abbrev (indt «axioms_») (const «phant_axioms») > «HB.examples.readme.AddComoid_of_Type.axioms»)*) > (*clause _ _ > (gref-deps (indt «axioms_») > (w-params.nil A (sort (typ «readme.2»)) c0 \ []))*) > (*clause _ _ > (gref-deps (indc «Axioms_») > (w-params.nil A (sort (typ «readme.2»)) c0 \ []))*) > (*clause _ _ > (gref-deps (const «zero») > (w-params.nil A (sort (typ «readme.2»)) c0 \ > [triple (indt «axioms_») [] c0]))*) > (*clause _ _ > (gref-deps (const «add») > (w-params.nil A (sort (typ «readme.2»)) c0 \ > [triple (indt «axioms_») [] c0]))*) > (*clause _ _ > (gref-deps (const «addrA») > (w-params.nil A (sort (typ «readme.2»)) c0 \ > [triple (indt «axioms_») [] c0]))*) > (*clause _ _ > (gref-deps (const «addrC») > (w-params.nil A (sort (typ «readme.2»)) c0 \ > [triple (indt «axioms_») [] c0]))*) > (*clause _ _ > (gref-deps (const «add0r») > (w-params.nil A (sort (typ «readme.2»)) c0 \ > [triple (indt «axioms_») [] c0]))*) > (*clause _ _ (factory-constructor (indt «axioms_») (indc «Axioms_»))*) > (*clause _ _ (factory-nparams (indt «axioms_») 0)*) > (*clause _ _ (factory-builder-nparams «phant_Build» 0)*) > (*clause _ _ > (phant-abbrev (indc «Axioms_») (const «phant_Build») > «HB.examples.readme.AddComoid_of_Type.Build»)*) > Global Arguments Axioms_ {_}. > End Exports. > End AddComoid_of_Type. > Export AddComoid_of_Type.Exports. > (*clause _ _ > (module-to-export ./examples/readme.v AddComoid_of_Type.Exports > «HB.examples.readme.AddComoid_of_Type.Exports»)*) > Notation AddComoid_of_Type X1 := ( AddComoid_of_Type.phant_axioms X1). > > *) > [1659086976.379429] HB: start module AddComoid > [1659086976.379945] HB: declare axioms record > w-params.nil A (sort (typ «readme.21»)) c0 \ > [triple (indt «AddComoid_of_Type.axioms_») [] c0] > [1659086976.380431] HB: typing class field > indt «AddComoid_of_Type.axioms_» > [1659086976.397539] HB: declare type record > [1659086976.416698] HB: structure: new mixins > [indt «AddComoid_of_Type.axioms_»] > [1659086976.417061] HB: structure: mixin first class > [mixin-first-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»)] > [1659086976.417282] HB: declaring clone abbreviation > [1659086976.525637] HB: declaring pack_ constant > [1659086976.526699] HB: declaring pack_ constant = > fun `A` (sort (typ «readme.21»)) c0 \ > fun `m` (app [global (indt «AddComoid_of_Type.axioms_»), c0]) c1 \ > app [global (indc «Pack»), c0, app [global (indc «Class»), c0, c1]] > [1659086976.529454] HB: start module Exports > [1659086976.529863] HB: making coercion from type to target > [1659086976.529993] HB: declare sort coercion > [1659086976.530381] HB: exporting unification hints > [1659086976.530694] HB: exporting coercions from class to mixins > [1659086976.531021] HB: export class to mixin coercion for mixin > readme_AddComoid_of_Type > [1659086976.531539] HB: accumulating various props > [1659086976.543080] HB: stop module Exports > [1659086976.543824] HB: declaring on_ abbreviation > [1659086976.552591] HB: declaring `copy` abbreviation > [1659086976.553662] HB: declaring on abbreviation > [1659086976.554823] HB: eta expanded instances > [1659086976.556478] HB: postulating A > [1659086976.573177] HB: declare mixin instance > readme_AddComoid__to__readme_AddComoid_of_Type > [1659086976.578849] HB: we can build a readme_AddComoid on eta A > [1659086976.579390] HB: declare canonical structure instance > structures_eta__canonical__readme_AddComoid > [1659086976.579874] HB: Giving name HB_unnamed_mixin_4 to mixin instance > readme_AddComoid_of_Type_mixin (eta A) HB_unnamed_factory_2 > [1659086976.583379] HB: structure instance for > structures_eta__canonical__readme_AddComoid is > {| > sort := eta A; > class := {| readme_AddComoid_of_Type_mixin := HB_unnamed_mixin_4 |} > |} > [1659086976.587547] HB: structure instance > structures_eta__canonical__readme_AddComoid declared > [1659086976.587806] HB: closing instance section > COQC examples/demo2/classical.v > [1659086976.589837] HB: end modules; export > «HB.examples.readme.AddComoid.Exports» > [1659086976.591565] HB: export > «HB.examples.readme.AddComoid.EtaAndMixinExports» > [1659086976.593292] HB: exporting operations > [1659086976.594280] HB: export operation zero > [1659086976.597699] HB: export operation add > [1659086976.601742] HB: export operation addrA > [1659086976.606274] HB: export operation addrC > [1659086976.610863] HB: export operation add0r > [1659086976.614503] HB: operations meta-data module: ElpiOperations > [1659086976.625060] HB: abbreviation factory-by-classname > (* > > Module AddComoid. > Section axioms_. > Local Unset Implicit Arguments. > Record axioms_ (A : Type) : Type := Class > { readme_AddComoid_of_Type_mixin : AddComoid_of_Type.axioms_ A; }. > End axioms_. > > (*clause _ _ > (decl-location (indt «axioms_») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Global Arguments axioms_ : clear implicits. > (*clause _ _ > (decl-location (indc «Class») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Global Arguments Class : clear implicits. > (*clause _ _ > (decl-location (const «readme_AddComoid_of_Type_mixin») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Global Arguments readme_AddComoid_of_Type_mixin : clear implicits. > Section type. > Local Unset Implicit Arguments. > Record type : Type := Pack { sort : Type; class : axioms_ sort; }. > End type. > > (*clause _ _ > (decl-location (indt «type») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Global Arguments type : clear implicits. > (*clause _ _ > (decl-location (indc «Pack») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Global Arguments Pack : clear implicits. > (*clause _ _ > (decl-location (const «sort») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Global Arguments sort : clear implicits. > (*clause _ _ > (decl-location (const «class») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Global Arguments class : clear implicits. > (*clause _ _ > (decl-location (const «phant_clone») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Definition phant_clone : forall (A : Type) (cT : type) (c : axioms_ A) > (_ : unify Type Type A (sort cT) nomsg) > (_ : unify type type cT (Pack A c) nomsg), type := > fun (A : Type) (cT : type) (c : axioms_ A) > (_ : unify Type Type A (sort cT) nomsg) > (_ : unify type type cT (Pack A c) nomsg) => Pack A c. > Local Arguments phant_clone : clear implicits. > Notation clone X2 X1 := ( phant_clone X2 X1 _ (@id_phant _ _) (@id_phant _ > _)). > (*clause _ _ > (decl-location (const «pack_») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Definition pack_ := > fun (A : Type) (m : AddComoid_of_Type.axioms_ A) => Pack A (Class A m). > Local Arguments pack_ : clear implicits. > Module Exports. > Coercion sort : readme.AddComoid.type >-> Sortclass. > Coercion readme_AddComoid_of_Type_mixin : readme.AddComoid.axioms_ >-> > readme.AddComoid_of_Type.axioms_. > (*clause _ _ (factory-nparams (indt «axioms_») 0)*) > (*clause _ _ > (from (indt «axioms_») (indt «AddComoid_of_Type.axioms_») > (const «readme_AddComoid_of_Type_mixin»))*) > (*clause _ _ (factory-alias->gref (indt «axioms_») (indt «axioms_»))*) > (*clause _ _ (is-structure (indt «type»))*) > (*clause _ _ > (class-def > (class (indt «axioms_») (indt «type») > (w-params.nil A (sort (typ «readme.21»)) c0 \ > [triple (indt «AddComoid_of_Type.axioms_») [] c0])))*) > (*clause _ _ > (gref-deps (indt «axioms_») > (w-params.nil A (sort (typ «readme.21»)) c0 \ []))*) > (*clause _ _ > (gref-deps (indc «Class») > (w-params.nil A (sort (typ «readme.21»)) c0 \ > [triple (indt «AddComoid_of_Type.axioms_») [] c0]))*) > (*clause _ _ > (gref-deps (const «pack_») > (w-params.nil A (sort (typ «readme.21»)) c0 \ > [triple (indt «AddComoid_of_Type.axioms_») [] c0]))*) > (*clause _ _ > (mixin-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»))*) > (*clause _ _ (structure-key «sort» «class» (indt «type»))*) > End Exports. > Import Exports. > (*clause _ _ > (decl-location (const «phant_on_») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Definition phant_on_ : forall (A : type) (_ : phant (sort A)), axioms_ (sort > A) := > fun (A : type) (_ : phant (sort A)) => class A. > Local Arguments phant_on_ : clear implicits. > Notation on_ X1 := ( phant_on_ _ (Phant X1)). > Notation copy X2 X1 := ( phant_on_ _ (Phant X1) : axioms_ X2). > Notation on X1 := ( phant_on_ _ (Phant _) : axioms_ X1). > Module EtaAndMixinExports. > Section hb_instance_1. > Variable A : type. > Local Arguments A : clear implicits. > (*clause _ _ > (decl-location (const «HB_unnamed_factory_2») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Definition HB_unnamed_factory_2 : axioms_ (@eta Type (sort A)) := class A. > Local Arguments HB_unnamed_factory_2 : clear implicits. > (*clause _ _ > (decl-location (const «readme_AddComoid__to__readme_AddComoid_of_Type») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Definition readme_AddComoid__to__readme_AddComoid_of_Type : > AddComoid_of_Type.axioms_ > (@eta Type > (sort A)) := > readme_AddComoid_of_Type_mixin (@eta Type (sort A)) HB_unnamed_factory_2. > Local Arguments readme_AddComoid__to__readme_AddComoid_of_Type : clear > implicits. > (*clause _ _ > (decl-location (const «HB_unnamed_mixin_4») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Definition HB_unnamed_mixin_4 := > readme_AddComoid_of_Type_mixin (@eta Type (sort A)) HB_unnamed_factory_2. > Local Arguments HB_unnamed_mixin_4 : clear implicits. > (*clause _ _ > (decl-location (const «structures_eta__canonical__readme_AddComoid») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Definition structures_eta__canonical__readme_AddComoid : type := > Pack (@eta Type (sort A)) (Class (@eta Type (sort A)) HB_unnamed_mixin_4). > Local Arguments structures_eta__canonical__readme_AddComoid : clear implicits. > Global Canonical structures_eta__canonical__readme_AddComoid. > End hb_instance_1. > End EtaAndMixinExports. > End AddComoid. > Export AddComoid.Exports. > (*clause _ _ > (module-to-export ./examples/readme.v AddComoid.Exports > «HB.examples.readme.AddComoid.Exports»)*) > Export AddComoid.EtaAndMixinExports. > (*clause _ _ > (module-to-export ./examples/readme.v AddComoid.EtaAndMixinExports > «HB.examples.readme.AddComoid.EtaAndMixinExports»)*) > (*clause _ _ > (decl-location (const «zero») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Definition zero : forall s : AddComoid.type, AddComoid.sort s := > fun s : AddComoid.type => > AddComoid_of_Type.zero (AddComoid.sort s) > (AddComoid.readme_AddComoid_of_Type_mixin (AddComoid.sort s) > (AddComoid.class s)). > Local Arguments zero : clear implicits. > Global Arguments zero {_}. > (*clause _ _ > (decl-location (const «add») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Definition add : forall (s : AddComoid.type) (_ : AddComoid.sort s) > (_ : AddComoid.sort s), AddComoid.sort s := > fun (s : AddComoid.type) (H H0 : AddComoid.sort s) => > AddComoid_of_Type.add (AddComoid.sort s) > (AddComoid.readme_AddComoid_of_Type_mixin (AddComoid.sort s) > (AddComoid.class s)) H H0. > Local Arguments add : clear implicits. > Global Arguments add {_}. > (*clause _ _ > (decl-location (const «addrA») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Definition addrA : forall (s : AddComoid.type) (x y z : AddComoid.sort s), > @eq (AddComoid.sort s) (@add s x (@add s y z)) > (@add s (@add s x y) z) := > fun (s : AddComoid.type) (x y z : AddComoid.sort s) => > AddComoid_of_Type.addrA (AddComoid.sort s) > (AddComoid.readme_AddComoid_of_Type_mixin (AddComoid.sort s) > (AddComoid.class s)) x y z. > Local Arguments addrA : clear implicits. > Global Arguments addrA {_}. > (*clause _ _ > (decl-location (const «addrC») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Definition addrC : forall (s : AddComoid.type) (x y : AddComoid.sort s), > @eq (AddComoid.sort s) (@add s x y) (@add s y x) := > fun (s : AddComoid.type) (x y : AddComoid.sort s) => > AddComoid_of_Type.addrC (AddComoid.sort s) > (AddComoid.readme_AddComoid_of_Type_mixin (AddComoid.sort s) > (AddComoid.class s)) x y. > Local Arguments addrC : clear implicits. > Global Arguments addrC {_}. > (*clause _ _ > (decl-location (const «add0r») > File "./examples/readme.v", line 12, column 0, character 307:)*) > Definition add0r : forall (s : AddComoid.type) (x : AddComoid.sort s), > @eq (AddComoid.sort s) (@add s (@zero s) x) x := > fun (s : AddComoid.type) (x : AddComoid.sort s) => > AddComoid_of_Type.add0r (AddComoid.sort s) > (AddComoid.readme_AddComoid_of_Type_mixin (AddComoid.sort s) > (AddComoid.class s)) x. > Local Arguments add0r : clear implicits. > Global Arguments add0r {_}. > Module ElpiOperations5. > (*clause _ _ > (exported-op (indt «AddComoid_of_Type.axioms_») > «AddComoid_of_Type.add0r» «add0r»)*) > (*clause _ _ > (exported-op (indt «AddComoid_of_Type.axioms_») > «AddComoid_of_Type.addrC» «addrC»)*) > (*clause _ _ > (exported-op (indt «AddComoid_of_Type.axioms_») > «AddComoid_of_Type.addrA» «addrA»)*) > (*clause _ _ > (exported-op (indt «AddComoid_of_Type.axioms_») «AddComoid_of_Type.add» > «add»)*) > (*clause _ _ > (exported-op (indt «AddComoid_of_Type.axioms_») > «AddComoid_of_Type.zero» «zero»)*) > (*clause _ _ > (mixin-first-class (indt «AddComoid_of_Type.axioms_») > (indt «AddComoid.axioms_»))*) > End ElpiOperations5. > Export ElpiOperations5. > (*clause _ _ > (module-to-export ./examples/readme.v ElpiOperations5 > «HB.examples.readme.ElpiOperations5»)*) > Notation AddComoid X1 := ( AddComoid.axioms_ X1). > > *) > forall (M : AddComoid.type) (x : M), x + x = 0 > : Prop > [1659086976.952049] HB: begin module for builders > [1659086976.952403] HB: postulating factories > [1659086976.952618] HB: processing key context-item > [1659086976.952988] HB: processing mixin parameter a > [1659086976.953348] HB: declaring parameters and key as section variables > 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 mixins: > - readme.AbelianGrp > (from "./examples/readme.v", line 32) > - readme.AddComoid > (from "./examples/readme.v", line 31) > > COQC examples/demo3/hierarchy_0.v > COQC examples/demo3/hierarchy_1.v > 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] > [1659086978.052230] HB: declare builder from hierarchy_2_Ring_of_AddComoid > to hierarchy_2_AddAG_of_AddComoid > [1659086978.052658] HB: declare builder from hierarchy_2_Ring_of_AddComoid > to hierarchy_2_Ring_of_AddAG > 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] > COQC examples/demo3/hierarchy_2.v > COQC examples/demo4/hierarchy_0.v > COQC examples/demo5/hierarchy_0.v > HB: A is canonically equipped with mixins: > - Feather.Equality > Feather.Singleton > (from "./examples/hulk.v", line 216) > > COQC examples/FSCD2020_material/V1.v > inhab > : ?s > where > ?T : [ |- Type] > ?s : [ |- s1.type ?T] > eq_refl : inhab = 7 > : inhab = 7 > COQC examples/FSCD2020_material/V2.v > eq_refl : inhab = (7 :: nil)%list > : inhab = (7 :: nil)%list > where > ?T : [ |- Type] > fun X : s2.type nat => inhab : X > : forall X : s2.type nat, X > fun X : s2.type nat => inj : nat -> X > : forall X : s2.type nat, nat -> X > s2_to_s1 not a defined object. > COQC examples/FSCD2020_material/V3.v > COQC examples/FSCD2020_material/V4.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 : Ring.type, left_inverse 0 opp add > COQC examples/FSCD2020_talk/V1.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/FSCD2020_talk/V2.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 examples/FSCD2020_talk/V3.v > COQC examples/Coq2020_material/CoqWS_demo.v > COQC examples/Coq2020_material/CoqWS_abstract.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] > 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/Coq2020_material/CoqWS_expansion/withHB.v > COQC examples/Coq2020_material/CoqWS_expansion/withoutHB.v > add > : ?s -> ?s -> ?s > where > ?s : [ |- CMonoid.type] > addrC > : commutative add > where > ?s : [ |- CMonoid.type] > COQC tests/type_of_exported_ops.v > File "./examples/Coq2020_material/CoqWS_demo.v", line 73, characters 0-73: > Warning: > pulling in dependencies: [CoqWS_demo_CMonoid_of_Type] > > Please list them or end the declaration with '&' > [HB.implicit-structure-dependency,HB] > forall x y : ?t, x - (y + 0) = x > : Prop > where > ?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) > addrC > : commutative add > where > ?s : [ |- CMonoid.type] > File "./examples/Coq2020_material/CoqWS_expansion/withoutHB.v", line 10, > characters 50-62: > Warning: The format modifier has no effect for only-parsing notations. > [discarded-format-only-parsing,parsing] > COQC tests/duplicate_structure.v > COQC tests/instance_params_no_type.v > forall x y : ?t, 1 + x = y * x > : Prop > where > ?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) > File "./examples/Coq2020_material/CoqWS_abstract.v", line 23, characters 0-71: > Warning: > pulling in dependencies: [CoqWS_abstract_CMonoid_of_Type] > > Please list them or end the declaration with '&' > [HB.implicit-structure-dependency,HB] > 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) > COQC tests/test_CS_db_filtering.v > forall x : Z, x * - (1 + x) = 0 + 1 > : Prop > COQC tests/subtype.v > 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 tests/infer.v > forall (G : AbelianGrp.type) (x : G), x - x = 0 > : Prop > forall (S : SemiRing.type) (x : S), x * 1 + 0 = x > : Prop > forall (R : Ring.type) (x y : R), x * - (1 * y) = - x * y > : Prop > COQC tests/exports.v > COQC tests/log_impargs_record.v > forall x : Z, x * - (1 + x) = 0 + 1 > : Prop > forall x : Z, x * - (1 + x) = 0 + 1 > : Prop > COQC tests/compress_coe.v > COQC tests/funclass.v > (* > > 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 : 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). > > *) > A.p : > forall [T : Type] (record : A.axioms_ T) [x : T], A.f record x = x -> True > > A.p is not universe polymorphic > Arguments A.p [T]%type_scope record [x] _ > A.p is transparent > Expands to: Constant HB.tests.log_impargs_record.A.p > COQC tests/local_instance.v > 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/lock.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 > [1659086985.775062] HB: start module SubInhab > [1659086985.775493] HB: declare axioms record > w-params.cons T (sort (typ «subtype.307»)) c0 \ > w-params.cons P (app [global (const «pred»), c0]) c1 \ > w-params.nil sT (sort (typ «subtype.309»)) c2 \ > [triple (indt «is_inhab.axioms_») [] c2, > triple (indt «is_SUB.axioms_») [c0, c1] c2] > [1659086985.776089] HB: typing class field indt «is_inhab.axioms_» > [1659086985.776478] HB: typing class field indt «is_SUB.axioms_» > bar1.phant_type Datatypes_nat__canonical__infer_foo (ssreflect.Phant nat) > : Type > [1659086985.784695] HB: declare type record > [1659086985.792382] HB: structure: new mixins [] > [1659086985.792660] HB: structure: mixin first class [] > [1659086985.792780] HB: declaring clone abbreviation > [1659086985.800557] HB: declaring pack_ constant > [1659086985.802091] HB: declaring pack_ constant = > fun `T` (sort (typ «subtype.307»)) c0 \ > fun `P` (app [global (const «pred»), c0]) c1 \ > fun `sT` (sort (typ «subtype.309»)) 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]] > [1659086985.804463] HB: start module Exports > [1659086985.804816] HB: making coercion from type to target > [1659086985.804990] HB: declare sort coercion > [1659086985.805285] HB: exporting unification hints > [1659086985.807072] HB: declare coercion subtype_SubInhab__to__subtype_SUB > [1659086985.808058] HB: declare coercion hint > subtype_SubInhab_class__to__subtype_SUB_class > [1659086985.814845] HB: declare unification hint > subtype_SubInhab__to__subtype_SUB > [1659086985.821699] HB: declare coercion path compression rules > [1659086985.823584] HB: declare coercion subtype_SubInhab__to__subtype_Inhab > COQC tests/not_same_key.v > [1659086985.824554] HB: declare coercion hint > subtype_SubInhab_class__to__subtype_Inhab_class > [1659086985.831794] HB: declare unification hint > subtype_SubInhab__to__subtype_Inhab > [1659086985.839196] HB: declare coercion path compression rules > [1659086985.840682] HB: declare unification hint > join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB > [1659086985.848454] HB: exporting coercions from class to mixins > [1659086985.849111] HB: export class to mixin coercion for mixin > subtype_is_inhab > [1659086985.850440] HB: export class to mixin coercion for mixin > subtype_is_SUB > [1659086985.851438] HB: accumulating various props > [1659086985.863588] HB: stop module Exports > [1659086985.866132] HB: declaring on_ abbreviation > [1659086985.874905] HB: declaring `copy` abbreviation > [1659086985.875889] HB: declaring on abbreviation > [1659086985.877532] HB: eta expanded instances > 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 > [1659086985.880186] HB: postulating T > [1659086985.885992] HB: postulating P > [1659086985.887669] HB: postulating sT > [1659086985.905846] HB: declare mixin instance > subtype_SubInhab__to__subtype_is_inhab > [1659086985.938244] HB: declare mixin instance > subtype_SubInhab__to__subtype_is_SUB > [1659086985.949165] HB: skipping already existing subtype_Inhab instance on > eta sT > [1659086985.950097] HB: skipping already existing subtype_Nontrivial > instance on eta sT > [1659086985.950920] HB: skipping already existing subtype_SUB instance on > eta sT > [1659086985.952851] HB: we can build a subtype_SubInhab on eta sT > [1659086985.953198] HB: declare canonical structure instance > structures_eta__canonical__subtype_SubInhab > [1659086985.953853] HB: structure instance for > structures_eta__canonical__subtype_SubInhab is > {| > sort := eta sT; > class := > {| > subtype_is_inhab_mixin := HB_unnamed_mixin_4 sT; > subtype_is_SUB_mixin := HB_unnamed_mixin_19 T P sT > |} > |} > [1659086985.959829] HB: structure instance > structures_eta__canonical__subtype_SubInhab declared > [1659086985.960088] HB: closing instance section > [1659086985.961806] HB: end modules; export > «HB.tests.subtype.SubInhab.Exports» > [1659086985.964779] HB: export > «HB.tests.subtype.SubInhab.EtaAndMixinExports» > [1659086985.965924] HB: exporting operations > [1659086985.966276] HB: operations meta-data module: ElpiOperations > [1659086985.967469] HB: abbreviation factory-by-classname > default : nat > : nat > The command did fail as expected with message: > The term "default" has type "nonempty.sort ?t" > while it is expected to have type "nat". > Notation big := big.body > Expands to: Notation HB.tests.lock.X.big > COQC tests/factory_sort_tac.v > COQC tests/declare.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 > [1659086986.387718] HB: exporting under the module path [] > [1659086986.388290] HB: exporting modules > [Ring_of_TYPE.Exports, Ring.Exports, Ring.EtaAndMixinExports, > ElpiOperations5, RingExports, Dummy.Exports, URing.Exports, > URing.EtaAndMixinExports, ElpiOperations11, dummy.Exports, > Builders_12.dummy_Exports] > [1659086986.390571] HB: exporting CS instances > [«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] > [1659086986.391315] HB: exporting Abbreviations [addr0, addrNK] > forall (R : Enclosing.Ring.type) (x : R), x = x > : Prop > 0%G > : ?s > where > ?s : [ |- Enclosing.Ring.type] > Enclosing.zero : Z > : Z > COQC tests/short.v > HB.check: > forall > w : wp.phant_type nat Nat_mul__canonical__funclass_Monoid > (Phantom (nat -> nat -> nat) Init.Nat.mul), w = w > : Prop > COQC tests/primitive_records.v > COQC tests/non_forgetful_inheritance.v > COQC tests/fix_loop.v > [1659086986.787859] HB: start module and section hasA > [1659086986.788361] HB: converting arguments > indt-decl > (parameter T explicit X0 c0 \ > record hasA (sort (typ X1)) Build_hasA > (field [coercion ff, canonical tt] a c0 c1 \ end-record)) to factories > [1659086986.788761] HB: processing key parameter > [1659086986.789324] HB: converting factories > w-params.nil T (sort (typ «factory_sort_tac.8»)) c0 \ [] to mixins > [1659086986.789662] HB: declaring context > w-params.nil T (sort (typ «factory_sort_tac.8»)) c0 \ [] > [1659086986.789934] HB: declaring parameters and key as section variables > [1659086986.796823] HB: declare mixin or factory > [1659086986.797109] HB: declare record axioms_: sort (typ X1) > [1659086986.808821] HB: declare notation Build > [1659086986.817968] HB: declare notation axioms > [1659086986.829976] HB: start module Exports > [1659086986.843863] HB: end modules and sections; export > «HB.tests.factory_sort_tac.hasA.Exports» > hasA.type not a defined object. > 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' > COQC tests/test_synthesis_params.v > hasB.type not a defined object. > aType > : Type > hasB.type not a defined object. > COQC tests/hnf.v > Query assignments: > Ind = «hasA.axioms_» > hasAB.type not a defined object. > hasA'.type not a defined object. > Query assignments: > Ind = «A.axioms_» > COQC examples/demo1/test_0_0.v > hasAB.type not a defined object. > hasA'.type not a defined object. > COQC examples/demo1/test_1_0.v > forall T : AB.type, > unkeyed > {| > AB.sort := T; > AB.class := > let factory_sort_tac_hasA_mixin := > AB.factory_sort_tac_hasA_mixin T (AB.class T) in > let factory_sort_tac_hasB_mixin := > AB.factory_sort_tac_hasB_mixin T (AB.class T) in > {| > AB.factory_sort_tac_hasA_mixin := factory_sort_tac_hasA_mixin; > AB.factory_sort_tac_hasB_mixin := factory_sort_tac_hasB_mixin > |} > |} > : Type > A : A.type > : A.type > A : A.type > : A.type > AB1 : hasB.phant_axioms A -> AB.type > : hasB.phant_axioms A -> AB.type > Bm : hasB.phant_axioms A > : hasB.phant_axioms A > Query assignments: > AB2 : AB.type > : AB.type > Ind = «A.type» > pB : T * T > : T * T > AB3 : AB.type > : AB.type > COQC examples/demo1/test_2_0.v > Datatypes_nat__canonical__hnf_S = > {| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |} > : S.type > HB_unnamed_mixin_12 = > {| M.x := f.y nat HB_unnamed_factory_10 + 1 |} > : M.axioms_ nat > X : Foo.type A P > : Foo.type A P > Datatypes_bool__canonical__hnf_S = > {| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_16 |} |} > : S.type > HB_unnamed_mixin_16 = > Builders_6.HB_unnamed_factory_8 bool HB_unnamed_factory_13 > : M.axioms_ bool > COQC examples/demo1/test_3_0.v > COQC examples/demo1/test_3_3.v > COQC examples/demo1/test_4_0.v > erefl ?t : ?t = ?t > : ?t = ?t > where > ?t : [ |- Sq.type] > COQC examples/demo1/test_4_3.v > COQC examples/demo1/test_5_0.v > COQC examples/demo1/test_5_3.v > COQC examples/demo2/stage10.v > COQC examples/demo2/stage11.v > COQC examples/demo3/test_0_0.v > COQC examples/demo3/test_1_0.v > COQC examples/demo3/test_2_0.v > COQC tests/exports2.v > [1659086990.609848] HB: exporting under the module path [] > [1659086990.610290] HB: exporting modules [] > [1659086990.610557] HB: exporting CS instances [] > [1659086990.610784] HB: exporting Abbreviations [] > Qcplus_opp_r: forall q : Qc, q + - q = Q2Qc 0 > Finished transaction in 16.025 secs (15.356u,0.665s) (successful) > Finished transaction in 0. secs (0.u,0.s) (successful) > HB: skipping section opening > [1659086995.463922] HB: declare mixin instance > Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology > [1659086995.466632] HB: declare canonical mixin instance > «Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology» > [1659086995.467741] HB: declare mixin instance > Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology > [1659086995.471717] HB: declare canonical mixin instance > «Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology» > [1659086995.472763] HB: declare mixin instance > Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform > [1659086995.477625] HB: declare canonical mixin instance > «Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform» > [1659086995.478613] HB: declare mixin instance > Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform > [1659086995.497107] HB: declare canonical mixin instance > «Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform» > [1659086995.498707] HB: we can build a Stage11_UniformSpace_wo_Topology on > Qc > [1659086995.498990] HB: declare canonical structure instance > Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology > [1659086995.499225] HB: Giving name HB_unnamed_mixin_92 to mixin instance > Builders_68.Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology Qc > HB_unnamed_mixin_81 HB_unnamed_mixin_86 HB_unnamed_factory_87 > [1659086995.501570] HB: structure instance for > Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology is > {| > UniformSpace_wo_Topology.sort := Qc; > UniformSpace_wo_Topology.class := > {| > UniformSpace_wo_Topology.Stage11_Uniform_wo_Topology_mixin := > HB_unnamed_mixin_92 > |} > |} > [1659086995.503969] HB: structure instance > Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology declared > [1659086995.504803] HB: we can build a Stage11_UniformSpace on Qc > [1659086995.505028] HB: declare canonical structure instance > Qcanon_Qc__canonical__Stage11_UniformSpace > [1659086995.505471] HB: structure instance for > Qcanon_Qc__canonical__Stage11_UniformSpace is > {| > UniformSpace.sort := Qc; > UniformSpace.class := > {| > UniformSpace.Stage11_Topological_mixin := HB_unnamed_mixin_86; > UniformSpace.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_92 > |} > |} > [1659086995.507771] HB: structure instance > Qcanon_Qc__canonical__Stage11_UniformSpace declared > [1659086995.508617] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc > [1659086995.508845] HB: declare canonical structure instance > Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform > [1659086995.509341] HB: Giving name HB_unnamed_mixin_93 to mixin instance > Builders_68.to_JoinTAddAG_wo_Uniform Qc HB_unnamed_mixin_81 > HB_unnamed_mixin_86 > HB_unnamed_factory_87 > [1659086995.511630] HB: structure instance for > Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform is > {| > TAddAG_wo_Uniform.sort := Qc; > TAddAG_wo_Uniform.class := > {| > TAddAG_wo_Uniform.Stage11_AddAG_of_TYPE_mixin := HB_unnamed_mixin_81; > TAddAG_wo_Uniform.Stage11_Topological_mixin := HB_unnamed_mixin_86; > TAddAG_wo_Uniform.Stage11_JoinTAddAG_wo_Uniform_mixin := > HB_unnamed_mixin_93 > |} > |} > [1659086995.513759] HB: structure instance > Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform declared > [1659086995.514906] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc > [1659086995.515124] HB: declare canonical structure instance > Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined > [1659086995.515795] HB: structure instance for > Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined is > {| > Uniform_TAddAG_unjoined.sort := Qc; > Uniform_TAddAG_unjoined.class := > {| > Uniform_TAddAG_unjoined.Stage11_AddAG_of_TYPE_mixin := > HB_unnamed_mixin_81; > Uniform_TAddAG_unjoined.Stage11_Topological_mixin := > HB_unnamed_mixin_86; > Uniform_TAddAG_unjoined.Stage11_JoinTAddAG_wo_Uniform_mixin := > HB_unnamed_mixin_93; > Uniform_TAddAG_unjoined.Stage11_Uniform_wo_Topology_mixin := > HB_unnamed_mixin_92 > |} > |} > [1659086995.517990] HB: structure instance > Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined declared > [1659086995.519839] HB: we can build a Stage11_TAddAG on Qc > [1659086995.520058] HB: declare canonical structure instance > Qcanon_Qc__canonical__Stage11_TAddAG > [1659086995.520712] HB: Giving name HB_unnamed_mixin_94 to mixin instance > Builders_68.Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology Qc > HB_unnamed_mixin_81 HB_unnamed_mixin_86 HB_unnamed_factory_87 > [1659086995.523238] HB: Giving name HB_unnamed_mixin_95 to mixin instance > Builders_68.Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform Qc > HB_unnamed_mixin_81 HB_unnamed_mixin_86 HB_unnamed_factory_87 > [1659086995.525663] HB: structure instance for > Qcanon_Qc__canonical__Stage11_TAddAG is > {| > TAddAG.sort := Qc; > TAddAG.class := > {| > TAddAG.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_92; > TAddAG.Stage11_AddAG_of_TYPE_mixin := HB_unnamed_mixin_81; > TAddAG.Stage11_Topological_mixin := HB_unnamed_mixin_86; > TAddAG.Stage11_Join_Uniform_Topology_mixin := HB_unnamed_mixin_94; > TAddAG.Stage11_JoinTAddAG_wo_Uniform_mixin := HB_unnamed_mixin_93; > TAddAG.Stage11_Join_TAddAG_Uniform_mixin := HB_unnamed_mixin_95 > |} > |} > [1659086995.528024] HB: structure instance > Qcanon_Qc__canonical__Stage11_TAddAG declared > entourage : set (set (Qc * Qc)) > : set (set (Qc * Qc)) > Finished transaction in 11.107 secs (10.591u,0.515s) (successful) > Module Type > new_conceptLocked = > Sig > Parameter body : nat. > Parameter unlock : > body = > Init.Nat.of_num_uint > (Number.UIntDecimal > (Decimal.D9 > (Decimal.D9 > (Decimal.D9 > (Decimal.D9 (Decimal.D9 (Decimal.D9 Decimal.Nil))))))). > End > Module > new_concept > : new_conceptLocked > := Struct > Definition body : nat. > Parameter unlock : > new_concept = > Init.Nat.of_num_uint > (Number.UIntDecimal > (Decimal.D9 > (Decimal.D9 > (Decimal.D9 > (Decimal.D9 (Decimal.D9 (Decimal.D9 Decimal.Nil))))))). > End > > Notation new_concept := new_concept.body > File "./examples/hulk.v", line 315, characters 0-55: > Warning: > pulling in dependencies: [MissingJoin_isTop] > > Please list them or end the declaration with '&' > [HB.implicit-structure-dependency,HB] > File "./examples/hulk.v", line 341, characters 0-55: > Warning: > pulling in dependencies: [GoodJoin_isTop] > > Please list them or end the declaration with '&' > [HB.implicit-structure-dependency,HB] > OUTPUT DIFF tests/compress_coe.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 > > Arguments Datatypes_prod__canonical__compress_coe_D D D' > OUTPUT DIFF tests/about.v > HB: AddMonoid_of_TYPE is a factory > (from "./examples/demo1/hierarchy_5.v", line 10) > HB: AddMonoid_of_TYPE operations and axioms are: > - zero > - add > - addrA > - add0r > - addr0 > HB: AddMonoid_of_TYPE requires the following mixins: > HB: AddMonoid_of_TYPE provides the following mixins: > - hierarchy_5.AddMonoid_of_TYPE > > HB: AddMonoid_of_TYPE.Build is a factory constructor > (from "./examples/demo1/hierarchy_5.v", line 10) > HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with: > HB: AddMonoid_of_TYPE.Build provides the following mixins: > - hierarchy_5.AddMonoid_of_TYPE > HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0 > - S : Type > - zero : AddMonoid.sort S > - add : S -> S -> S > - addrA : associative add > - add0r : left_id 0%G add > - addr0 : right_id 0%G add > > HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73) > HB: AddAG.type characterizing operations and axioms are: > - addNr > - opp > HB: hierarchy_5.AddAG is a factory for the following mixins: > - hierarchy_5.AddMonoid_of_TYPE > - hierarchy_5.AddComoid_of_AddMonoid > - hierarchy_5.AddAG_of_AddComoid (* new, not from inheritance *) > HB: hierarchy_5.AddAG inherits from: > - hierarchy_5.AddMonoid > - hierarchy_5.AddComoid > HB: hierarchy_5.AddAG is inherited by: > - hierarchy_5.Ring > > HB: hierarchy_5.AddMonoid.type is a structure > (from "./examples/demo1/hierarchy_5.v", line 17) > HB: hierarchy_5.AddMonoid.type characterizing operations and axioms are: > - addr0 > - add0r > - addrA > - add > - zero > HB: hierarchy_5.AddMonoid is a factory for the following mixins: > - hierarchy_5.AddMonoid_of_TYPE (* new, not from inheritance *) > HB: hierarchy_5.AddMonoid inherits from: > HB: hierarchy_5.AddMonoid is inherited by: > - hierarchy_5.AddComoid > - hierarchy_5.AddAG > - hierarchy_5.BiNearRing > - hierarchy_5.SemiRing > - hierarchy_5.Ring > > HB: Ring_of_AddAG is a factory > (from "./examples/demo1/hierarchy_5.v", line 108) > HB: Ring_of_AddAG operations and axioms are: > - one > - mul > - mulrA > - mulr1 > - mul1r > - mulrDl > - mulrDr > HB: Ring_of_AddAG requires the following mixins: > - hierarchy_5.AddMonoid_of_TYPE > - hierarchy_5.AddComoid_of_AddMonoid > - hierarchy_5.AddAG_of_AddComoid > HB: Ring_of_AddAG provides the following mixins: > - hierarchy_5.BiNearRing_of_AddMonoid > Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and > mul0r are derived from addrC and the other ring axioms, following a proof > of Hankel (Gerhard Betsch. On the beginnings and development of near-ring > theory. In Near-rings and near-fields. Proceedings of the conference held > in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics > and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, > 1995). > > HB: Ring_of_AddAG.Build is a factory constructor > (from "./examples/demo1/hierarchy_5.v", line 108) > HB: Ring_of_AddAG.Build requires its subject to be already equipped with: > - hierarchy_5.AddMonoid_of_TYPE > - hierarchy_5.AddComoid_of_AddMonoid > - hierarchy_5.AddAG_of_AddComoid > HB: Ring_of_AddAG.Build provides the following mixins: > - hierarchy_5.BiNearRing_of_AddMonoid > HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl > mulrDr > - A : Type > - one : A > - mul : A -> A -> A > - mulrA : associative mul > - mulr1 : left_id one mul > - mul1r : right_id one mul > - mulrDl : left_distributive mul add > - mulrDr : right_distributive mul add > Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and > mul0r are derived from addrC and the other ring axioms, following a proof > of Hankel (Gerhard Betsch. On the beginnings and development of near-ring > theory. In Near-rings and near-fields. Proceedings of the conference held > in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics > and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, > 1995). > > HB: add is an operation of structure hierarchy_5.AddMonoid > (from "./examples/demo1/hierarchy_5.v", line 17) > HB: add comes from mixin hierarchy_5.AddMonoid_of_TYPE > (from "./examples/demo1/hierarchy_5.v", line 10) > > HB: AddAG.sort is a canonical projection > (from "./examples/demo1/hierarchy_5.v", line 73) > HB: AddAG.sort has the following canonical values: > - @eta > - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196) > - Z > > HB: AddAG.sort is a coercion from hierarchy_5.AddAG to Sortclass > (from "./examples/demo1/hierarchy_5.v", line 73) > > HB: Z is canonically equipped with mixins: > - hierarchy_5.AddMonoid > hierarchy_5.AddComoid > hierarchy_5.AddAG > (from "(stdin)", line 5) > - hierarchy_5.BiNearRing > hierarchy_5.SemiRing > hierarchy_5.Ring > (from "(stdin)", line 10) > > HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from > hierarchy_5.Ring to hierarchy_5.SemiRing > (from "./examples/demo1/hierarchy_5.v", line 196) > > HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from > hierarchy_5.Ring to hierarchy_5.SemiRing > (from "./examples/demo1/hierarchy_5.v", line 196) > > HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to > hierarchy_5.BiNearRing_of_AddMonoid > HB: synthesized in file File "(stdin)", line 5, column [-122,-] {+0,+} > make[4]: *** [Makefile.test-suite.coq.local:22: post-all] Error 1 The full build log is available from: http://qa-logs.debian.net/2022/07/28/coq-hierarchy-builder_1.2.1-11_unstable.log All bugs filed during this archive rebuild are listed at: https://bugs.debian.org/cgi-bin/pkgreport.cgi?tag=ftbfs-20220728;users=lu...@debian.org or: https://udd.debian.org/bugs/?release=na&merged=ign&fnewerval=7&flastmodval=7&fusertag=only&fusertagtag=ftbfs-20220728&fusertaguser=lu...@debian.org&allbugs=1&cseverity=1&ctags=1&caffected=1#results A list of current common problems and possible solutions is available at http://wiki.debian.org/qa.debian.org/FTBFS . You're welcome to contribute! If you reassign this bug to another package, please marking it as 'affects'-ing this package. See https://www.debian.org/Bugs/server-control#affects If you fail to reproduce this, please provide a build log and diff it with mine so that we can identify if something relevant changed in the meantime.