Bug#1016303: coq-hierarchy-builder: FTBFS: make[4]: *** [Makefile.test-suite.coq.local:22: post-all] Error 1
Source: coq-hierarchy-builder
Version: 1.2.1-11
Severity: serious
Justification: FTBFS
Tags: bookworm sid ftbfs
User: lucas@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=lucas@debian.org
or:
https://udd.debian.org/bugs/?release=na&merged=ign&fnewerval=7&flastmodval=7&fusertag=only&fusertagtag=ftbfs-20220728&fusertaguser=lucas@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.
Reply to: