[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Bug#1016303: marked as done (coq-hierarchy-builder: FTBFS: make[4]: *** [Makefile.test-suite.coq.local:22: post-all] Error 1)



Your message dated Sat, 30 Jul 2022 16:04:16 +0000
with message-id <E1oHowq-000Ar3-74@fasolo.debian.org>
and subject line Bug#1016303: fixed in coq-hierarchy-builder 1.3.0-1
has caused the Debian Bug report #1016303,
regarding coq-hierarchy-builder: FTBFS: make[4]: *** [Makefile.test-suite.coq.local:22: post-all] Error 1
to be marked as done.

This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.

(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact owner@bugs.debian.org
immediately.)


-- 
1016303: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1016303
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message ---
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.

--- End Message ---
--- Begin Message ---
Source: coq-hierarchy-builder
Source-Version: 1.3.0-1
Done: Julien Puydt <jpuydt@debian.org>

We believe that the bug you reported is fixed in the latest version of
coq-hierarchy-builder, which is due to be installed in the Debian FTP archive.

A summary of the changes between this version and the previous one is
attached.

Thank you for reporting the bug, which will now be closed.  If you
have further comments please address them to 1016303@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Julien Puydt <jpuydt@debian.org> (supplier of updated coq-hierarchy-builder package)

(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@ftp-master.debian.org)


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Format: 1.8
Date: Sat, 30 Jul 2022 17:44:16 +0200
Source: coq-hierarchy-builder
Architecture: source
Version: 1.3.0-1
Distribution: unstable
Urgency: medium
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Julien Puydt <jpuydt@debian.org>
Closes: 1016303
Changes:
 coq-hierarchy-builder (1.3.0-1) unstable; urgency=medium
 .
   * New upstream release.
   * Add patch so upstream test suite passes with a more recent elpi
     (Closes: #1016303).
Checksums-Sha1:
 c8835462ed8504ff8c6f0dd3197566081895484d 2229 coq-hierarchy-builder_1.3.0-1.dsc
 45b9670ce4dc977d2af1edb7ccfc7b79f22bc217 200135 coq-hierarchy-builder_1.3.0.orig.tar.gz
 de5067cd9c8afa4f2ef8aabf5c3ba2dee6f111b2 3348 coq-hierarchy-builder_1.3.0-1.debian.tar.xz
 9c6a9ec21cd462da15fb97b9102ce09c02ff4047 7577 coq-hierarchy-builder_1.3.0-1_source.buildinfo
Checksums-Sha256:
 4683f36c36f30bcde1d0afeaee2b2dd70af46b78c60ed6959213c19631294d25 2229 coq-hierarchy-builder_1.3.0-1.dsc
 8d4ca09a08793be19501ea2d9e82da1cd413feb9a15e5a6e0c183404b8145c76 200135 coq-hierarchy-builder_1.3.0.orig.tar.gz
 a1eb2fa42297555e4215fcee73d1e6a808d851c7fce31e5a38dbdbe78aeb217c 3348 coq-hierarchy-builder_1.3.0-1.debian.tar.xz
 c5607680eb81f3a8d1ca4a20e3d5dee27ae3ec39cc42871788b7085c8c83d66c 7577 coq-hierarchy-builder_1.3.0-1_source.buildinfo
Files:
 c2de8e1b4c4277ce07f4ff5f2ade862d 2229 ocaml optional coq-hierarchy-builder_1.3.0-1.dsc
 42ef8d7c9f81a71b360214b2397fd52b 200135 ocaml optional coq-hierarchy-builder_1.3.0.orig.tar.gz
 b687348c4036880abc5a7c77b0c7f1ec 3348 ocaml optional coq-hierarchy-builder_1.3.0-1.debian.tar.xz
 d9647b1843f414bfc1695c7ca54e0f8a 7577 ocaml optional coq-hierarchy-builder_1.3.0-1_source.buildinfo

-----BEGIN PGP SIGNATURE-----

iQJGBAEBCgAwFiEEgS7v2KP7pKzk3xFLBMU71/4DBVEFAmLlUgcSHGpwdXlkdEBk
ZWJpYW4ub3JnAAoJEATFO9f+AwVRczcP/1L+ED8ZYKMHSGGjI/KmxatCavnWLXqE
oLeeqgXPCh99pO1I+Epj/C1Di4y7vcDKT4zdoFe3EVyJ5YH5hfDqabFMWI9eQtzb
pjVVFfpoI0llsNwcVXKeXY3ThHmIDr796HaiXM2snm8SAYq6E2MVJP+p0TNJ6UZ0
LM9dn3FWkiNiZmz7X4bZM2++o+7IOD/RjbvHUMx1R/nM5sUefdGjdf4TkCLvxlAs
JS6ftkxApzgLamhFYes8UbjQ5Qz553CX7VgvyPmFPm1+m23pw3s2+A8iwKf9jHMd
a1uZ8rJZ0wLPwesct8WYLzJHjAxRzcncgnXziL9sK3+vCGh+qSWaUx7cfx9wgCwa
qpSoGxEM17oKT9izYwoOvkpNNnm489Z8k5LxoGmVgNTV/Zqyj/U3R6Xp9JXYmLLH
daelYTsP1KvvURwRaa5ENZ1tdzTPPNHLFwkkowV2sKDWduX2pRo+GBJwoArPlFBU
BagVVVO8I4lVNTxeJy3jUZnNt4d4BQ30DwW2ycw0uiNNDDzaEBccDHECL4RiqA4e
SubkqzehmJMYdrcGZ/UUgZVwzAA8b0LheCHyxVOueExVKdZ6RkhwtlLWN/EPxJm2
Pbr66gdd6fcBbjvGoKCSbhuZrw6VICCWbuqeDlaC4827SjBdxc4hh5wLV9bRMBVi
Fxgl8QZORUDZ
=czfj
-----END PGP SIGNATURE-----

--- End Message ---

Reply to: