Stream: Hierarchy Builder devs & users

Topic: Github Notifications


view this post on Zulip HB Github Bot (May 18 2020 at 11:01):

CohenCyril pushed 1 commit to branch parameters.

view this post on Zulip HB Github Bot (May 18 2020 at 14:37):

CohenCyril pushed 1 commit to branch parameters.

view this post on Zulip HB Github Bot (May 18 2020 at 14:37):

CohenCyril updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := { ... }.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

view this post on Zulip HB Github Bot (May 18 2020 at 15:36):

gares pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (May 18 2020 at 15:38):

gares pushed 1 commit to branch coq-elpi-1.4.

view this post on Zulip HB Github Bot (May 18 2020 at 15:39):

gares opened PR #70 port to coq-elpi 1.4 from coq-elpi-1.4 to master:

to be merged when coq-elpi 1.4 is out

view this post on Zulip HB Github Bot (May 18 2020 at 15:40):

gares edited PR #70 port to coq-elpi 1.4 from coq-elpi-1.4 to master:

to be merged when coq-elpi 1.4 is out

Fix #52

view this post on Zulip HB Github Bot (May 18 2020 at 17:08):

gares pushed 3 commits to branch coq-master.

view this post on Zulip HB Github Bot (May 19 2020 at 07:45):

gares pushed 1 commit to branch coq-elpi-1.4.

view this post on Zulip HB Github Bot (May 19 2020 at 07:45):

gares updated PR #70 port to coq-elpi 1.4 from coq-elpi-1.4 to master:

to be merged when coq-elpi 1.4 is out

Fix #52

view this post on Zulip HB Github Bot (May 19 2020 at 07:52):

gares pushed 1 commit to branch coq-master.

view this post on Zulip HB Github Bot (May 19 2020 at 07:52):

gares pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (May 19 2020 at 07:53):

gares pushed 1 commit to branch coq-elpi-1.4.

view this post on Zulip HB Github Bot (May 19 2020 at 07:53):

gares updated PR #70 port to coq-elpi 1.4 from coq-elpi-1.4 to master:

to be merged when coq-elpi 1.4 is out

Fix #52

view this post on Zulip HB Github Bot (May 19 2020 at 07:54):

gares pushed 2 commits to branch coq-elpi-1.4.

view this post on Zulip HB Github Bot (May 19 2020 at 07:54):

gares updated PR #70 port to coq-elpi 1.4 from coq-elpi-1.4 to master:

to be merged when coq-elpi 1.4 is out

Fix #52

view this post on Zulip HB Github Bot (May 19 2020 at 08:27):

gares pushed 2 commits to branch coq-master.

view this post on Zulip HB Github Bot (May 19 2020 at 08:27):

CohenCyril pushed 3 commits to branch coq-elpi-1.4.

view this post on Zulip HB Github Bot (May 19 2020 at 08:27):

CohenCyril updated PR #70 port to coq-elpi 1.4 from coq-elpi-1.4 to master:

to be merged when coq-elpi 1.4 is out

Fix #52

view this post on Zulip HB Github Bot (May 19 2020 at 08:31):

CohenCyril pushed 1 commit to branch coq-elpi-1.4.

view this post on Zulip HB Github Bot (May 19 2020 at 08:31):

CohenCyril updated PR #70 port to coq-elpi 1.4 from coq-elpi-1.4 to master:

to be merged when coq-elpi 1.4 is out

Fix #52

view this post on Zulip HB Github Bot (May 19 2020 at 08:40):

CohenCyril pushed 1 commit to branch parameters. Commits by gares (1).

view this post on Zulip HB Github Bot (May 19 2020 at 08:40):

CohenCyril updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := { ... }.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

view this post on Zulip HB Github Bot (May 19 2020 at 08:42):

CohenCyril pushed 1 commit to branch parameters. Commits by gares (1).

view this post on Zulip HB Github Bot (May 19 2020 at 08:42):

CohenCyril updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := { ... }.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

view this post on Zulip HB Github Bot (May 19 2020 at 08:47):

gares pushed 1 commit to branch coq-elpi-1.4.

view this post on Zulip HB Github Bot (May 19 2020 at 08:47):

gares updated PR #70 port to coq-elpi 1.4 from coq-elpi-1.4 to master:

to be merged when coq-elpi 1.4 is out

Fix #52

view this post on Zulip HB Github Bot (May 19 2020 at 09:48):

gares pushed 1 commit to branch fix-make.

view this post on Zulip HB Github Bot (May 19 2020 at 09:48):

gares opened PR #71 simplify makefile from fix-make to master.

view this post on Zulip HB Github Bot (May 19 2020 at 10:07):

gares merged PR #71 simplify makefile.

view this post on Zulip HB Github Bot (May 19 2020 at 10:07):

gares pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (May 19 2020 at 10:07):

gares deleted the branch fix-make.

view this post on Zulip HB Github Bot (May 19 2020 at 10:09):

gares pushed 6 commits to branch coq-master.

view this post on Zulip HB Github Bot (May 19 2020 at 10:28):

CohenCyril pushed 1 commit to branch parameters. Commits by gares (1).

view this post on Zulip HB Github Bot (May 19 2020 at 10:28):

CohenCyril updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := { ... }.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

view this post on Zulip HB Github Bot (May 19 2020 at 10:30):

CohenCyril pushed 1 commit to branch parameters. Commits by gares (1).

view this post on Zulip HB Github Bot (May 19 2020 at 10:30):

CohenCyril updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := { ... }.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

view this post on Zulip HB Github Bot (May 19 2020 at 10:33):

gares pushed 4 commits to branch coq-elpi-1.4. Commits by CohenCyril (2) and gares (2).

view this post on Zulip HB Github Bot (May 19 2020 at 10:33):

gares updated PR #70 port to coq-elpi 1.4 from coq-elpi-1.4 to master:

to be merged when coq-elpi 1.4 is out

Fix #52

view this post on Zulip HB Github Bot (May 19 2020 at 10:37):

CohenCyril pushed 1 commit to branch parameters. Commits by gares (1).

view this post on Zulip HB Github Bot (May 19 2020 at 10:37):

CohenCyril updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := { ... }.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

view this post on Zulip HB Github Bot (May 19 2020 at 13:22):

gares pushed 1 commit to branch coq-elpi-1.4.

view this post on Zulip HB Github Bot (May 19 2020 at 13:22):

gares updated PR #70 port to coq-elpi 1.4 from coq-elpi-1.4 to master:

to be merged when coq-elpi 1.4 is out

Fix #52

view this post on Zulip HB Github Bot (May 19 2020 at 15:18):

gares pushed 1 commit to branch coq-elpi-1.4.

view this post on Zulip HB Github Bot (May 19 2020 at 15:18):

gares updated PR #70 port to coq-elpi 1.4 from coq-elpi-1.4 to master:

to be merged when coq-elpi 1.4 is out

Fix #52

view this post on Zulip HB Github Bot (May 19 2020 at 16:33):

gares pushed 7 commits to branch coq-master. Commits by gares (5) and CohenCyril (2).

view this post on Zulip HB Github Bot (May 19 2020 at 17:37):

CohenCyril pushed 1 commit to branch parameters.

view this post on Zulip HB Github Bot (May 19 2020 at 17:37):

CohenCyril updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := { ... }.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

view this post on Zulip HB Github Bot (May 19 2020 at 17:48):

CohenCyril pushed 2 commits to branch parameters. Commits by CohenCyril (1) and gares (1).

view this post on Zulip HB Github Bot (May 19 2020 at 17:48):

CohenCyril updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := { ... }.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

view this post on Zulip HB Github Bot (May 20 2020 at 13:49):

CohenCyril pushed 1 commit to branch coq-elpi-1.4.

view this post on Zulip HB Github Bot (May 20 2020 at 13:49):

CohenCyril updated PR #70 port to coq-elpi 1.4 from coq-elpi-1.4 to master:

to be merged when coq-elpi 1.4 is out

Fix #52

view this post on Zulip HB Github Bot (May 20 2020 at 13:57):

CohenCyril pushed 1 commit to branch coq-elpi-1.4.

view this post on Zulip HB Github Bot (May 20 2020 at 13:57):

CohenCyril updated PR #70 port to coq-elpi 1.4 from coq-elpi-1.4 to master:

to be merged when coq-elpi 1.4 is out

Fix #52

view this post on Zulip HB Github Bot (May 20 2020 at 14:17):

CohenCyril pushed 1 commit to branch coq-elpi-1.4.

view this post on Zulip HB Github Bot (May 20 2020 at 14:17):

CohenCyril updated PR #70 port to coq-elpi 1.4 from coq-elpi-1.4 to master:

to be merged when coq-elpi 1.4 is out

Fix #52

view this post on Zulip HB Github Bot (May 20 2020 at 14:23):

CohenCyril pushed 2 commits to branch parameters. Commits by CohenCyril (1) and gares (1).

view this post on Zulip HB Github Bot (May 20 2020 at 14:23):

CohenCyril updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := { ... }.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

view this post on Zulip HB Github Bot (May 20 2020 at 20:36):

CohenCyril closed Issue #52 HB.mixin should not rename the type variable (assigned to gares):

otherwise error messages are misleading (they talk about T, but the user wrote A)

view this post on Zulip HB Github Bot (May 20 2020 at 20:36):

CohenCyril merged PR #70 port to coq-elpi 1.4.

view this post on Zulip HB Github Bot (May 20 2020 at 20:36):

CohenCyril pushed 9 commits to branch master. Commits by CohenCyril (5) and gares (4).

view this post on Zulip HB Github Bot (May 20 2020 at 20:39):

CohenCyril deleted the branch coq-elpi-1.4.

view this post on Zulip HB Github Bot (May 22 2020 at 09:34):

Janno opened Issue #72 A brief report on trying to port the Iris hierarchy to HB:

Hey everyone,

I was very happy to see the hierarchy builder being announced and I wanted to see what would happen if I used it to define the hierarchy in Iris. This was really just for fun since I do not expect the result to be usable given Iris's reliance on type classes. I also wanted to learn from the resulting definitions since I still don't really understand how one is supposed to set up canonical structures.

But my experiment ended before I got to actually trying out the result. I pushed the experiment to https://gitlab.mpi-sws.org/janno/iris-coq/-/tree/janno/try-HB (the branch name is janno/try-HB). The only file that changed is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v. It contains both old an new definitions, which are confined to lines 150-178. The original file without my new stuff is here: https://gitlab.mpi-sws.org/iris/iris/-/blob/962637df10a879ac4b1b9d523854d6fa4c9e8fb4/theories/bi/interface.v

Of particular interest is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L242 where I cannot get HB to accept the definition of an SBI (an extension of the BI definition in https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L156). The error HB reports is this (when using the right printing settings):

The term "@Some" of type "∀ A : Type, A → option A"
cannot be applied to the terms
 "?e5" : "Type"
 "("is not canonically a", bi.type)" : "(string * Type)%type"

I suppose the underlying error is a mistake on my side but I don't know what it would be.

To get to this point I also had to work around an unexpected shortcoming regarding implicit type class arguments. As you can see in the definition of the BI structure, I had to manually spell out all type class instances since HB would not accept the terms otherwise. (This is veeeeery annoying since it also means that notation such as that for equiv needs to be unfolded.)

Finally, there's something that I wouldn't count as a bug but more of a feature request: in the original Iris hierarchy, the bi_mixin Section (at the top of the file) creates local notation for the operators that make the axioms look very natural. I couldn't find a way to replicate this setup. Maybe HB.mixin could accept where clauses for (local) syntax?

Building the branch
My opam switch reports the following packages:

coq-elpi                1.3.1                     Elpi extension language for Coq
coq-hierarchy-builder   0.9.0                     Hierarchy Builder
coq-stdpp               dev.2019-12-06.0.1ef53c55 pinned to version dev.2019-12-06.0.1ef53c55 at git+https://gitlab.mpi-sws.org/iris/stdpp.git

If you want to avoid pinning coq-stdpp to the git hash (the suffix of that weird dev version) you can

opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

and then opam should be able to find that exact version.

Running make inside a clone of my iris-coq branch should eventually compile interfaces.v and report the errors.

view this post on Zulip HB Github Bot (May 22 2020 at 18:08):

gares pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (May 23 2020 at 02:16):

CohenCyril pushed 1 commit to branch parameters.

view this post on Zulip HB Github Bot (May 23 2020 at 02:16):

CohenCyril updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := { ... }.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

view this post on Zulip HB Github Bot (May 29 2020 at 17:06):

gares pushed 1 commit to branch instance-def.

view this post on Zulip HB Github Bot (May 29 2020 at 17:07):

gares opened PR #73 syntax HB.instance Definition := ... from instance-def to master:

Fix #53

view this post on Zulip HB Github Bot (Jun 01 2020 at 18:33):

gares pushed 1 commit to branch instance-def.

view this post on Zulip HB Github Bot (Jun 01 2020 at 18:33):

gares updated PR #73 syntax HB.instance Definition := ... from instance-def to master:

Fix #53

view this post on Zulip HB Github Bot (Jun 01 2020 at 18:34):

gares pushed 1 commit to branch instance-def.

view this post on Zulip HB Github Bot (Jun 01 2020 at 18:34):

gares updated PR #73 syntax HB.instance Definition := ... from instance-def to master:

Fix #53

view this post on Zulip HB Github Bot (Jun 02 2020 at 08:12):

gares closed Issue #53 HB.instance Definition bla := Foo.Build T .... syntax (assigned to gares):

Kind of looks nice

view this post on Zulip HB Github Bot (Jun 02 2020 at 08:12):

gares merged PR #73 syntax HB.instance Definition := ...

view this post on Zulip HB Github Bot (Jun 02 2020 at 08:12):

gares pushed 4 commits to branch master.

view this post on Zulip HB Github Bot (Jun 02 2020 at 08:12):

gares deleted the branch instance-def.

view this post on Zulip HB Github Bot (Jun 02 2020 at 08:24):

gares pushed 3 commits to branch parameters. Commits by CohenCyril (2) and gares (1).

view this post on Zulip HB Github Bot (Jun 02 2020 at 08:24):

gares updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := { ... }.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

view this post on Zulip HB Github Bot (Jun 02 2020 at 08:44):

gares pushed 1 commit to branch parameters.

view this post on Zulip HB Github Bot (Jun 02 2020 at 08:44):

gares updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := { ... }.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

view this post on Zulip HB Github Bot (Jun 02 2020 at 08:48):

gares opened Issue #74 HB.instance Definition f Params := ... (outside a section)

As of today we can only write

Section Foo.
Variable A : Type.
HB.instance Definition list_m1 := m1.Build (option A) (list nat) (cons 7 nil) None.
End Foo.

If we abstract list_m1 over A we get an assertion in

pred mixin-srcs i:term, i:term, o:list prop.
mixin-srcs T X MSL :- std.do! [
  std.assert-ok! (coq.typecheck X XTy) "mixin-src: X illtyped",
  if (not (safe-dest-app XTy (global _) _))
     (coq.error "Term:\n" {coq.term->string X}
                "\nhas type:\n" {coq.term->string XTy}
                "\nwhich is not a record")

Instead we should record the abstractions before the record and put them in front of S

pred declare-instances i:term, i:list class.
declare-instances T [class Class Struct MLwP|Rest] :-
  params->holes MLwP Params,
  get-class-constructor Class Params KC,
  list-w-params_list MLwP ML,
  mterm->term (mterm [/*Params already applied to KC*/] T ML KC) KCApp, % we can build it
  not (local-cs? T Struct), % not already built
  !,
  term->gref T TGR,
  coq.gref->id TGR TID,
  Name is TID ^ "_is_a_" ^ {term->modname Struct},

  if-verbose (coq.say "HB: declare canonical instance" Name),

  get-structure-constructor Struct Params KS,
  S = app[KS, T, KCApp],

view this post on Zulip HB Github Bot (Jun 02 2020 at 12:14):

CohenCyril created PR Review Comment on #65 [feature] parameters in structures:

I'd rather have this example in a different file/directory than demo4, unless I missed something?

view this post on Zulip HB Github Bot (Jun 02 2020 at 12:14):

CohenCyril submitted PR Review for #65 [feature] parameters in structures.

view this post on Zulip HB Github Bot (Jun 02 2020 at 12:20):

gares submitted PR Review for #65 [feature] parameters in structures.

view this post on Zulip HB Github Bot (Jun 02 2020 at 12:20):

gares created PR Review Comment on #65 [feature] parameters in structures:

You are right. We rebased on top of master after the merge of #73, we were just trying to see what needs fixing, see #74

view this post on Zulip HB Github Bot (Jun 02 2020 at 12:22):

gares edited PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := {
  ...
}.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

view this post on Zulip HB Github Bot (Jun 02 2020 at 12:23):

gares edited PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := {
  ...
}.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.
The code base has a new data type list-w-params A and w-params A to represent it.

view this post on Zulip HB Github Bot (Jun 02 2020 at 12:23):

gares milestoned Issue #65 [feature] parameters in structures:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := {
  ...
}.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.
The code base has a new data type list-w-params A and w-params A to represent it.

view this post on Zulip HB Github Bot (Jun 02 2020 at 16:03):

gares pushed 1 commit to branch instance-def-params.

view this post on Zulip HB Github Bot (Jun 02 2020 at 16:03):

gares opened PR #75 HB.instance Definition f A := .... A .... from instance-def-params to master.

view this post on Zulip HB Github Bot (Jun 02 2020 at 16:06):

gares edited PR #75 HB.instance Definition f A := .... A .... from instance-def-params to parameters.

view this post on Zulip HB Github Bot (Jun 02 2020 at 16:09):

gares pushed 1 commit to branch instance-def-params.

view this post on Zulip HB Github Bot (Jun 02 2020 at 16:09):

gares updated PR #75 HB.instance Definition f A := .... A .... from instance-def-params to parameters.

view this post on Zulip HB Github Bot (Jun 02 2020 at 16:18):

gares merged PR #75 HB.instance Definition f A := .... A ....

view this post on Zulip HB Github Bot (Jun 02 2020 at 16:18):

gares pushed 1 commit to branch parameters.

view this post on Zulip HB Github Bot (Jun 02 2020 at 16:18):

gares updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := {
  ...
}.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.
The code base has a new data type list-w-params A and w-params A to represent it.

view this post on Zulip HB Github Bot (Jun 02 2020 at 16:18):

gares deleted the branch instance-def-params.

view this post on Zulip HB Github Bot (Jun 02 2020 at 17:45):

gares edited PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := {
  ...
}.

The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.
The code base has a new data type list-w-params A and w-params A to represent it.

Fix #75

view this post on Zulip HB Github Bot (Jun 03 2020 at 08:45):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Jun 03 2020 at 08:47):

CohenCyril created release Hierarchy Builder 0.9.1 for tag v0.9.1.

view this post on Zulip HB Github Bot (Jun 03 2020 at 08:47):

CohenCyril released release Hierarchy Builder 0.9.1 for tag v0.9.1.

view this post on Zulip HB Github Bot (Jun 03 2020 at 08:47):

CohenCyril published release Hierarchy Builder 0.9.1 for tag v0.9.1.

view this post on Zulip HB Github Bot (Jun 03 2020 at 08:47):

CohenCyril pushed tag v0.9.1.

view this post on Zulip HB Github Bot (Jun 03 2020 at 08:48):

gares pushed 1 commit to branch coq-master-0.9.1.

view this post on Zulip HB Github Bot (Jun 03 2020 at 08:48):

gares opened PR #76 Coq master 0.9.1 from coq-master-0.9.1 to coq-master.

view this post on Zulip HB Github Bot (Jun 03 2020 at 08:54):

gares pushed 1 commit to branch coq-master-0.9.1.

view this post on Zulip HB Github Bot (Jun 03 2020 at 08:54):

gares updated PR #76 Coq master 0.9.1 from coq-master-0.9.1 to coq-master.

view this post on Zulip HB Github Bot (Jun 03 2020 at 08:55):

CohenCyril merged PR #65 [feature] parameters in structures.

view this post on Zulip HB Github Bot (Jun 03 2020 at 08:55):

CohenCyril pushed 6 commits to branch master. Commits by CohenCyril (3) and gares (3).

view this post on Zulip HB Github Bot (Jun 03 2020 at 08:57):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Jun 03 2020 at 10:11):

CohenCyril pushed 1 commit to branch more_tests.

view this post on Zulip HB Github Bot (Jun 03 2020 at 10:13):

CohenCyril opened PR #77 Creating Left module on a Ring from more_tests to master.

view this post on Zulip HB Github Bot (Jun 03 2020 at 10:14):

CohenCyril pushed 1 commit to branch more_tests.

view this post on Zulip HB Github Bot (Jun 03 2020 at 10:14):

CohenCyril updated PR #77 Creating Left module on a Ring from more_tests to master.

view this post on Zulip HB Github Bot (Jun 03 2020 at 13:15):

gares deleted the branch parameters.

view this post on Zulip HB Github Bot (Jun 03 2020 at 13:25):

gares pushed 1 commit to branch coq-master-0.9.1.

view this post on Zulip HB Github Bot (Jun 03 2020 at 13:25):

gares updated PR #76 Coq master 0.9.1 from coq-master-0.9.1 to coq-master.

view this post on Zulip HB Github Bot (Jun 03 2020 at 13:39):

gares merged PR #76 Coq master 0.9.1.

view this post on Zulip HB Github Bot (Jun 03 2020 at 13:39):

gares pushed 13 commits to branch coq-master. Commits by gares (9) and CohenCyril (4).

view this post on Zulip HB Github Bot (Jun 03 2020 at 13:39):

gares deleted the branch coq-master-0.9.1.

view this post on Zulip HB Github Bot (Jun 10 2020 at 08:32):

gares pushed 1 commit to branch more_tests.

view this post on Zulip HB Github Bot (Jun 10 2020 at 08:32):

gares updated PR #77 Creating Left module on a Ring from more_tests to master.

view this post on Zulip HB Github Bot (Jun 10 2020 at 08:56):

CohenCyril pushed 1 commit to branch more_tests.

view this post on Zulip HB Github Bot (Jun 10 2020 at 08:56):

CohenCyril updated PR #77 Creating Left module on a Ring from more_tests to master.

view this post on Zulip HB Github Bot (Jun 10 2020 at 09:05):

CohenCyril pushed 1 commit to branch more_tests.

view this post on Zulip HB Github Bot (Jun 10 2020 at 09:05):

CohenCyril updated PR #77 Creating Left module on a Ring from more_tests to master.

view this post on Zulip HB Github Bot (Jun 10 2020 at 09:06):

CohenCyril has marked PR #77 as ready for review.

view this post on Zulip HB Github Bot (Jun 10 2020 at 09:07):

CohenCyril merged PR #77 Creating Left module on a Ring.

view this post on Zulip HB Github Bot (Jun 10 2020 at 09:07):

CohenCyril pushed 5 commits to branch master. Commits by CohenCyril (4) and gares (1).

view this post on Zulip HB Github Bot (Jun 10 2020 at 09:08):

CohenCyril deleted the branch more_tests.

view this post on Zulip HB Github Bot (Jun 10 2020 at 09:10):

gares closed Issue #74 HB.instance Definition f Params := ... (outside a section)

As of today we can only write

Section Foo.
Variable A : Type.
HB.instance Definition list_m1 := m1.Build (option A) (list nat) (cons 7 nil) None.
End Foo.

If we abstract list_m1 over A we get an assertion in

pred mixin-srcs i:term, i:term, o:list prop.
mixin-srcs T X MSL :- std.do! [
  std.assert-ok! (coq.typecheck X XTy) "mixin-src: X illtyped",
  if (not (safe-dest-app XTy (global _) _))
     (coq.error "Term:\n" {coq.term->string X}
                "\nhas type:\n" {coq.term->string XTy}
                "\nwhich is not a record")

Instead we should record the abstractions before the record and put them in front of S

pred declare-instances i:term, i:list class.
declare-instances T [class Class Struct MLwP|Rest] :-
  params->holes MLwP Params,
  get-class-constructor Class Params KC,
  list-w-params_list MLwP ML,
  mterm->term (mterm [/*Params already applied to KC*/] T ML KC) KCApp, % we can build it
  not (local-cs? T Struct), % not already built
  !,
  term->gref T TGR,
  coq.gref->id TGR TID,
  Name is TID ^ "_is_a_" ^ {term->modname Struct},

  if-verbose (coq.say "HB: declare canonical instance" Name),

  get-structure-constructor Struct Params KS,
  S = app[KS, T, KCApp],

view this post on Zulip HB Github Bot (Jun 10 2020 at 09:11):

gares closed Issue #68 HB.builders should give access to names shadowed by the factory (assigned to CohenCyril):

Idea:

HB.builders Context T (f : F T).
  Module Super.
    Definition foo := foo.
  End Super.
  Section.
  Variable T.
  Variable f.
  Definition foo := foo f.

  ... user code can access both foo  and Super.foo ..

view this post on Zulip HB Github Bot (Jun 10 2020 at 09:14):

CohenCyril pushed 1 commit to branch factory-name-or-alias.

view this post on Zulip HB Github Bot (Jun 10 2020 at 09:14):

CohenCyril opened PR #78 renaming factory-name from factory-name-or-alias to master:

fixes #64

view this post on Zulip HB Github Bot (Jun 10 2020 at 10:13):

CohenCyril pushed 1 commit to branch fix-abbrev.

view this post on Zulip HB Github Bot (Jun 10 2020 at 10:14):

CohenCyril opened PR #79 fixing missing typeabbrev from coq-elpi from fix-abbrev to master.

view this post on Zulip HB Github Bot (Jun 10 2020 at 12:23):

gares pushed 1 commit to branch coq-elpi-1.4.1.

view this post on Zulip HB Github Bot (Jun 10 2020 at 12:24):

gares opened PR #80 coq-elpi 1.4.1 from coq-elpi-1.4.1 to master:

Waiting for https://github.com/coq/opam-coq-archive/pull/1283

view this post on Zulip HB Github Bot (Jun 10 2020 at 14:32):

CohenCyril closed without merge PR #79 fixing missing typeabbrev from coq-elpi.

view this post on Zulip HB Github Bot (Jun 10 2020 at 21:16):

gares deleted the branch fix-abbrev.

view this post on Zulip HB Github Bot (Jun 10 2020 at 22:12):

CohenCyril closed Issue #64 factoryname and factory-name types are too similar:

The latter could be renamed to factoryname-or-alias, or something like that.

view this post on Zulip HB Github Bot (Jun 10 2020 at 22:12):

CohenCyril merged PR #78 renaming factory-name.

view this post on Zulip HB Github Bot (Jun 10 2020 at 22:12):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Jun 17 2020 at 13:29):

CohenCyril closed without merge PR #80 coq-elpi 1.4.1.

view this post on Zulip HB Github Bot (Jun 17 2020 at 13:29):

CohenCyril reopened PR #80 coq-elpi 1.4.1 from coq-elpi-1.4.1 to master:

Waiting for https://github.com/coq/opam-coq-archive/pull/1283

view this post on Zulip HB Github Bot (Jun 19 2020 at 21:01):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Jun 19 2020 at 22:41):

CohenCyril pushed 2 commits to branch master. Commits by cyrilcohen (2).

view this post on Zulip HB Github Bot (Jun 20 2020 at 09:51):

gares merged PR #80 coq-elpi 1.4.1.

view this post on Zulip HB Github Bot (Jun 20 2020 at 09:51):

gares pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Jun 20 2020 at 09:51):

gares deleted the branch coq-elpi-1.4.1.

view this post on Zulip HB Github Bot (Jun 25 2020 at 23:02):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Jun 30 2020 at 15:24):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Jun 30 2020 at 23:59):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Jul 01 2020 at 11:18):

gares pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Jul 02 2020 at 14:10):

gares pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Jul 02 2020 at 19:18):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Jul 05 2020 at 08:51):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Jul 06 2020 at 16:10):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Jul 06 2020 at 16:23):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Jul 09 2020 at 17:54):

CohenCyril pushed 1 commit to branch new-phant-abbrev.

view this post on Zulip HB Github Bot (Jul 09 2020 at 17:55):

CohenCyril opened PR #81 refactoring/fixin phant-term build from new-phant-abbrev to master.

view this post on Zulip HB Github Bot (Jul 09 2020 at 17:57):

CohenCyril edited PR #81 refactoring/fixing phant-term build from new-phant-abbrev to master.

view this post on Zulip HB Github Bot (Jul 09 2020 at 18:13):

CohenCyril pushed 1 commit to branch new-phant-abbrev.

view this post on Zulip HB Github Bot (Jul 09 2020 at 18:13):

CohenCyril updated PR #81 refactoring/fixing phant-term build from new-phant-abbrev to master.

view this post on Zulip HB Github Bot (Jul 15 2020 at 12:33):

CohenCyril pushed 1 commit to branch new-phant-abbrev.

view this post on Zulip HB Github Bot (Jul 15 2020 at 12:33):

CohenCyril updated PR #81 refactoring/fixing phant-term build from new-phant-abbrev to master.

view this post on Zulip HB Github Bot (Jul 15 2020 at 20:32):

CohenCyril pushed 1 commit to branch new-phant-abbrev.

view this post on Zulip HB Github Bot (Jul 15 2020 at 20:32):

CohenCyril updated PR #81 refactoring/fixing phant-term build from new-phant-abbrev to master.

view this post on Zulip HB Github Bot (Jul 15 2020 at 20:49):

CohenCyril pushed 1 commit to branch new-phant-abbrev.

view this post on Zulip HB Github Bot (Jul 15 2020 at 20:49):

CohenCyril updated PR #81 refactoring/fixing phant-term build from new-phant-abbrev to master.

view this post on Zulip HB Github Bot (Jul 16 2020 at 01:47):

CohenCyril pushed 1 commit to branch new-phant-abbrev.

view this post on Zulip HB Github Bot (Jul 16 2020 at 01:47):

CohenCyril updated PR #81 refactoring/fixing phant-term build from new-phant-abbrev to master.

view this post on Zulip HB Github Bot (Jul 16 2020 at 01:56):

CohenCyril pushed 6 commits to branch new-phant-abbrev.

view this post on Zulip HB Github Bot (Jul 16 2020 at 01:56):

CohenCyril updated PR #81 refactoring/fixing phant-term build from new-phant-abbrev to master.

view this post on Zulip HB Github Bot (Jul 16 2020 at 08:06):

CohenCyril merged PR #81 refactoring/fixing phant-term build.

view this post on Zulip HB Github Bot (Jul 16 2020 at 08:06):

CohenCyril pushed 7 commits to branch master.

view this post on Zulip HB Github Bot (Jul 16 2020 at 08:07):

CohenCyril pushed 1 commit to branch is-structure.

view this post on Zulip HB Github Bot (Jul 16 2020 at 08:07):

CohenCyril opened PR #82 adding is-structure from is-structure to master.

view this post on Zulip HB Github Bot (Jul 16 2020 at 08:24):

CohenCyril merged PR #82 adding is-structure.

view this post on Zulip HB Github Bot (Jul 16 2020 at 08:24):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Jul 16 2020 at 09:17):

pi8027 pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Jul 16 2020 at 09:39):

gares opened Issue #83 HB.instance Definition foo : T := Build bar should read the number of parameters from T (when given)

view this post on Zulip HB Github Bot (Jul 16 2020 at 09:39):

gares edited Issue #83 HB.instance Definition foo : T := Build bar should read the number of parameters from T (when given)

view this post on Zulip HB Github Bot (Jul 16 2020 at 09:43):

gares opened Issue #84 HB.instance ty term should accept just the head symbol of ty:

Today you are force to write stuff like HB.instance { x : T &.... } t but actually only sigT is really needed

view this post on Zulip HB Github Bot (Jul 16 2020 at 09:44):

gares edited Issue #83 HB.instance Definition foo : T := Build bar should read the number of parameters from T (when given)

view this post on Zulip HB Github Bot (Jul 16 2020 at 09:44):

CohenCyril opened Issue #85 Add an HB mode to generate mathcomp compat boilerplate:

cf e.g. https://github.com/gares/math-comp/blob/hierarchy-builder/mathcomp/ssreflect/eqtype.v#L125-L146

view this post on Zulip HB Github Bot (Jul 16 2020 at 09:44):

gares edited Issue #83 HB.instance Definition foo : is_s T := Build bar should read the number of parameters from is_s T (when given)

view this post on Zulip HB Github Bot (Jul 16 2020 at 09:46):

CohenCyril pushed 1 commit to branch fix-get-canonical-mixin.

view this post on Zulip HB Github Bot (Jul 16 2020 at 09:46):

CohenCyril opened PR #86 fix from fix-get-canonical-mixin to master.

view this post on Zulip HB Github Bot (Jul 16 2020 at 10:43):

gares opened Issue #87 demo1 has still a dummy root structure with no properties.

view this post on Zulip HB Github Bot (Jul 16 2020 at 12:51):

gares opened Issue #88 in Coq 8.12 support #[local] HB.instance:

In 8.12 you can write #[local] Canonical foo

view this post on Zulip HB Github Bot (Jul 16 2020 at 15:18):

gares opened Issue #89 outdated doc about builders:

https://github.com/math-comp/hierarchy-builder/blob/22cc857bda3d9e696d49e827417af8e681e1e1bd/structures.v#L383

There is no _f anymore

view this post on Zulip HB Github Bot (Jul 16 2020 at 18:12):

CohenCyril edited PR #86 In HB.instance force unification to extract the class instead of the second argument. from fix-get-canonical-mixin to master.

view this post on Zulip HB Github Bot (Jul 16 2020 at 18:12):

CohenCyril edited PR #86 In HB.instance force unification to extract the class instead of the second argument. from fix-get-canonical-mixin to master:

E.g. in Definition t a b := K (T a b) (C a b). if you unify t x y = _ _ c you don't necessarily force the unfolding of t and c could get y, while with t x y = K _ c you do, since the RHS is a rigid HNF hence the LHS must be reduces to expose K and c gets C x y

view this post on Zulip HB Github Bot (Jul 16 2020 at 18:13):

CohenCyril merged PR #86 In HB.instance force unification to extract the class instead of the second argument.

view this post on Zulip HB Github Bot (Jul 16 2020 at 18:13):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Jul 16 2020 at 20:18):

gares deleted the branch fix-get-canonical-mixin.

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:05):

CohenCyril opened Issue #90 Reexport shadows the original notation for the relation/operation.

As noted by @chdoc on zulip.
C.f. https://gist.github.com/chdoc/f50c3a15c41e92ec0ac89112f1e18fbe

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:06):

CohenCyril milestoned Issue #90 Reexport shadows the original notation for the relation/operation.

As noted by @chdoc on zulip.
C.f. https://gist.github.com/chdoc/f50c3a15c41e92ec0ac89112f1e18fbe

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:06):

CohenCyril milestoned Issue #89 outdated doc about builders:

https://github.com/math-comp/hierarchy-builder/blob/22cc857bda3d9e696d49e827417af8e681e1e1bd/structures.v#L383

There is no _f anymore

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:06):

CohenCyril milestoned Issue #87 demo1 has still a dummy root structure with no properties.

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:06):

CohenCyril milestoned Issue #85 Add an HB mode to generate mathcomp compat boilerplate:

cf e.g. https://github.com/gares/math-comp/blob/hierarchy-builder/mathcomp/ssreflect/eqtype.v#L125-L146

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:07):

CohenCyril milestoned Issue #84 HB.instance ty term should accept just the head symbol of ty:

Today you are force to write stuff like HB.instance { x : T &.... } t but actually only sigT is really needed

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:07):

CohenCyril milestoned Issue #83 HB.instance Definition foo : is_s T := Build bar should read the number of parameters from is_s T (when given)

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:07):

CohenCyril milestoned Issue #72 A brief report on trying to port the Iris hierarchy to HB:

Hey everyone,

I was very happy to see the hierarchy builder being announced and I wanted to see what would happen if I used it to define the hierarchy in Iris. This was really just for fun since I do not expect the result to be usable given Iris's reliance on type classes. I also wanted to learn from the resulting definitions since I still don't really understand how one is supposed to set up canonical structures.

But my experiment ended before I got to actually trying out the result. I pushed the experiment to https://gitlab.mpi-sws.org/janno/iris-coq/-/tree/janno/try-HB (the branch name is janno/try-HB). The only file that changed is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v. It contains both old an new definitions, which are confined to lines 150-178. The original file without my new stuff is here: https://gitlab.mpi-sws.org/iris/iris/-/blob/962637df10a879ac4b1b9d523854d6fa4c9e8fb4/theories/bi/interface.v

Of particular interest is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L242 where I cannot get HB to accept the definition of an SBI (an extension of the BI definition in https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L156). The error HB reports is this (when using the right printing settings):

The term "@Some" of type "∀ A : Type, A → option A"
cannot be applied to the terms
 "?e5" : "Type"
 "("is not canonically a", bi.type)" : "(string * Type)%type"

I suppose the underlying error is a mistake on my side but I don't know what it would be.

To get to this point I also had to work around an unexpected shortcoming regarding implicit type class arguments. As you can see in the definition of the BI structure, I had to manually spell out all type class instances since HB would not accept the terms otherwise. (This is veeeeery annoying since it also means that notation such as that for equiv needs to be unfolded.)

Finally, there's something that I wouldn't count as a bug but more of a feature request: in the original Iris hierarchy, the bi_mixin Section (at the top of the file) creates local notation for the operators that make the axioms look very natural. I couldn't find a way to replicate this setup. Maybe HB.mixin could accept where clauses for (local) syntax?

Building the branch
My opam switch reports the following packages:

coq-elpi                1.3.1                     Elpi extension language for Coq
coq-hierarchy-builder   0.9.0                     Hierarchy Builder
coq-stdpp               dev.2019-12-06.0.1ef53c55 pinned to version dev.2019-12-06.0.1ef53c55 at git+https://gitlab.mpi-sws.org/iris/stdpp.git

If you want to avoid pinning coq-stdpp to the git hash (the suffix of that weird dev version) you can

opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

and then opam should be able to find that exact version.

Running make inside a clone of my iris-coq branch should eventually compile interfaces.v and report the errors.

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:08):

CohenCyril milestoned Issue #49 HB.instance should check for duplicate mixins (assigned to CohenCyril):

if the same mixin can be built in two different ways, both from the factories provided or from the existing instances, they must be convertible.

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:08):

CohenCyril demilestoned Issue #49 HB.instance should check for duplicate mixins (assigned to CohenCyril):

if the same mixin can be built in two different ways, both from the factories provided or from the existing instances, they must be convertible.

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:08):

CohenCyril milestoned Issue #36 HB.instance should no rely on std.findall order:

do not rely on std.findall order

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:09):

CohenCyril milestoned Issue #35 [hack] coercions in arg->term:

This is what we discussed this morning.
It is a hack since coq-elpi does not even distribute the elaborator since I believe it is not ready.
But of course we can change that...

I guess CI will fail since I've hardcoded the path of elaborator.elpi, but here it works...

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:09):

CohenCyril demilestoned Issue #35 [hack] coercions in arg->term:

This is what we discussed this morning.
It is a hack since coq-elpi does not even distribute the elaborator since I believe it is not ready.
But of course we can change that...

I guess CI will fail since I've hardcoded the path of elaborator.elpi, but here it works...

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:10):

CohenCyril milestoned Issue #34 HB.instance Ty Term should insert coercions in Ty when necessary:

@gares how do I replace
https://github.com/math-comp/hierarchy-builder/blob/854fc09f590752ff77a59f93bfc11c41fbbd722b/demo2/stage11.v#L172-L173
by

Elpi hb.canonical (T1 * T2)%type prod_topology.

?
(making coq-elpi insert the coercion TopologicalSpace.sort)

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:11):

CohenCyril milestoned Issue #27 HB.structure should not declare the class projection as canonical (assigned to gares):

We should either let this projection be anonymous and redeclare it by pattern matching later, or make Coq not register it when 8.11 is out.

https://github.com/math-comp/hierarchy-builder/blob/e118e77defa75c5cff9115eae91493a4997fb536/hb.elpi#L711

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:12):

CohenCyril demilestoned Issue #49 HB.instance should check for duplicate mixins (assigned to CohenCyril):

if the same mixin can be built in two different ways, both from the factories provided or from the existing instances, they must be convertible.

view this post on Zulip HB Github Bot (Jul 17 2020 at 20:12):

CohenCyril milestoned Issue #49 HB.instance should check for duplicate mixins (assigned to CohenCyril):

if the same mixin can be built in two different ways, both from the factories provided or from the existing instances, they must be convertible.

view this post on Zulip HB Github Bot (Jul 20 2020 at 09:19):

gares opened Issue #91 Error message "you must declare X before Y" is bogus since parameters were introduced:

Code
https://github.com/math-comp/hierarchy-builder/blob/01c24925f08ca39844a8e26e8eae085bfd6088e7/hb.elpi#L501-L506
prints stuff like:

You must declare
class (indt «axioms») (global (indt «type»))
 (w-params.nil `A` (sort (typ «bug.9333»)) c0 \
   [triple (indt «Ops_of_Type.axioms_») [] c0,
    triple (indt «Setoid_of_Type.axioms_») [] c0,
    triple (indt «Ptt_of_Ops.axioms_») [] c0]) before
indt «Pttdom.axioms»

The "class" must be printed better

view this post on Zulip HB Github Bot (Jul 20 2020 at 09:22):

gares milestoned Issue #91 Error message "you must declare X before Y" is bogus since parameters were introduced:

Code
https://github.com/math-comp/hierarchy-builder/blob/01c24925f08ca39844a8e26e8eae085bfd6088e7/hb.elpi#L501-L506
prints stuff like:

You must declare
class (indt «axioms») (global (indt «type»))
 (w-params.nil `A` (sort (typ «bug.9333»)) c0 \
   [triple (indt «Ops_of_Type.axioms_») [] c0,
    triple (indt «Setoid_of_Type.axioms_») [] c0,
    triple (indt «Ptt_of_Ops.axioms_») [] c0]) before
indt «Pttdom.axioms»

The "class" must be printed better

view this post on Zulip HB Github Bot (Jul 20 2020 at 09:23):

gares edited Issue #91 Error message "you must declare X before Y" is bogus since parameters were introduced:

Code
https://github.com/math-comp/hierarchy-builder/blob/01c24925f08ca39844a8e26e8eae085bfd6088e7/hb.elpi#L501-L506
prints stuff like:

You must declare
class (indt «axioms») (global (indt «type»))
 (w-params.nil `A` (sort (typ «bug.9333»)) c0 \
   [triple (indt «Ops_of_Type.axioms_») [] c0,
    triple (indt «Setoid_of_Type.axioms_») [] c0,
    triple (indt «Ptt_of_Ops.axioms_») [] c0]) before
indt «Pttdom.axioms»

The "class" must be printed better, also we should try to print only structure names (classes are sort of internal)

view this post on Zulip HB Github Bot (Jul 20 2020 at 13:48):

gares pushed 1 commit to branch HOAS+holes.

view this post on Zulip HB Github Bot (Jul 20 2020 at 13:49):

gares opened PR #92 Use the new HOAS:holes option of coq-elpi from HOAS+holes to master:

See https://github.com/LPCIC/coq-elpi/pull/160

view this post on Zulip HB Github Bot (Jul 20 2020 at 17:26):

gares opened Issue #93 Error message "BUG: ty-deps ..." should suggest to put indexed around the type.

view this post on Zulip HB Github Bot (Jul 27 2020 at 16:10):

gares pushed 2 commits to branch HOAS+holes.

view this post on Zulip HB Github Bot (Jul 27 2020 at 16:10):

gares updated PR #92 Use the new HOAS:holes option of coq-elpi from HOAS+holes to master:

See https://github.com/LPCIC/coq-elpi/pull/160

view this post on Zulip HB Github Bot (Jul 27 2020 at 16:13):

gares edited PR #92 coq-elpi 1.5 from HOAS+holes to master:

See https://github.com/LPCIC/coq-elpi/pull/160

view this post on Zulip HB Github Bot (Jul 28 2020 at 10:48):

gares pushed 1 commit to branch ty-ty.

view this post on Zulip HB Github Bot (Jul 28 2020 at 10:52):

gares opened PR #94 [instance] typecheck the type first from ty-ty to master:

This seems like a big bug even if I don't undestand yet how it was working.
If you don't typecheck the type first, and pass it as the expected type of coq.typecheck, you get a unification problem like this one:

(monoid_of_semigroup.axioms_ M is_monoid_semigroup)   =?1=
(monoid_of_semigroup.phant_axioms M ?e24 ?e26 (@id_phant ?e28 ?e30)
   ?e32 (@id_phant ?e34 ?e36) ?e38 (@id_phant ?e40 ?e42)
   (@id_phant ?e44 ?e46))

Coq is able to solve it (in 8.11) without assigning the arguments of id_phant (only ?e24/26 IIRC). In 8.12 as well, but later on the system "realizes that".

I'm hesitating, coq.typecheck could typecheck the expect type if given before unifying it with the inferred one...
This fix makes sense anyway.

view this post on Zulip HB Github Bot (Jul 28 2020 at 11:33):

gares merged PR #94 [instance] typecheck the type first.

view this post on Zulip HB Github Bot (Jul 28 2020 at 11:33):

gares pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Jul 28 2020 at 11:33):

gares deleted the branch ty-ty.

view this post on Zulip HB Github Bot (Jul 28 2020 at 11:45):

gares pushed 1 commit to branch ghactions.

view this post on Zulip HB Github Bot (Jul 28 2020 at 11:45):

gares opened PR #95 Create main.yml from ghactions to master.

view this post on Zulip HB Github Bot (Jul 28 2020 at 11:50):

gares edited PR #95 Create main.yml from ghactions to master:

TODO:

view this post on Zulip HB Github Bot (Jul 28 2020 at 12:07):

gares pushed 2 commits to branch ghactions.

view this post on Zulip HB Github Bot (Jul 28 2020 at 12:07):

gares updated PR #95 Create main.yml from ghactions to master:

TODO:

view this post on Zulip HB Github Bot (Jul 28 2020 at 12:07):

gares edited PR #95 Create main.yml from ghactions to master:

TODO:

view this post on Zulip HB Github Bot (Jul 28 2020 at 12:07):

gares edited PR #95 Create main.yml from ghactions to master:

TODO:

view this post on Zulip HB Github Bot (Jul 28 2020 at 14:17):

gares merged PR #95 Create main.yml.

view this post on Zulip HB Github Bot (Jul 28 2020 at 14:17):

gares pushed 4 commits to branch master.

view this post on Zulip HB Github Bot (Jul 28 2020 at 14:17):

gares deleted the branch ghactions.

view this post on Zulip HB Github Bot (Jul 28 2020 at 14:18):

gares pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Jul 29 2020 at 10:15):

gares pushed 4 commits to branch HOAS+holes.

view this post on Zulip HB Github Bot (Jul 29 2020 at 10:15):

gares updated PR #92 coq-elpi 1.5 from HOAS+holes to master:

See https://github.com/LPCIC/coq-elpi/pull/160

view this post on Zulip HB Github Bot (Jul 29 2020 at 10:16):

gares pushed 1 commit to branch HOAS+holes.

view this post on Zulip HB Github Bot (Jul 29 2020 at 10:16):

gares updated PR #92 coq-elpi 1.5 from HOAS+holes to master:

See https://github.com/LPCIC/coq-elpi/pull/160

view this post on Zulip HB Github Bot (Jul 29 2020 at 11:46):

gares edited PR #92 coq-elpi 1.5 from HOAS+holes to master:

Take advantage of Coq-Elpi 1.5.x

view this post on Zulip HB Github Bot (Jul 29 2020 at 14:26):

gares pushed 2 commits to branch elpi-1.5.

view this post on Zulip HB Github Bot (Jul 29 2020 at 14:27):

gares opened PR #96 Elpi 1.5 from elpi-1.5 to coq-master.

view this post on Zulip HB Github Bot (Jul 29 2020 at 14:27):

gares edited PR #96 Elpi 1.5 from elpi-1.5 to coq-master:

update the branch used by Coq CI

view this post on Zulip HB Github Bot (Jul 29 2020 at 14:27):

gares edited PR #96 [coq-ci] update to Coq-Elpi 1.5 from elpi-1.5 to coq-master:

update the branch used by Coq CI

view this post on Zulip HB Github Bot (Jul 29 2020 at 14:28):

gares pushed 1 commit to branch elpi-1.5.

view this post on Zulip HB Github Bot (Jul 29 2020 at 14:28):

gares updated PR #96 [coq-ci] update to Coq-Elpi 1.5 from elpi-1.5 to coq-master:

update the branch used by Coq CI

view this post on Zulip HB Github Bot (Jul 29 2020 at 14:30):

gares pushed 1 commit to branch elpi-1.5.

view this post on Zulip HB Github Bot (Jul 29 2020 at 14:30):

gares updated PR #96 [coq-ci] update to Coq-Elpi 1.5 from elpi-1.5 to coq-master:

update the branch used by Coq CI

view this post on Zulip HB Github Bot (Jul 29 2020 at 14:37):

gares merged PR #96 [coq-ci] update to Coq-Elpi 1.5.

view this post on Zulip HB Github Bot (Jul 29 2020 at 14:37):

gares pushed 58 commits to branch coq-master. Commits by CohenCyril (31), gares (26) and pi8027 (1).

view this post on Zulip HB Github Bot (Jul 29 2020 at 14:37):

gares deleted the branch elpi-1.5.

view this post on Zulip HB Github Bot (Jul 29 2020 at 16:13):

gares pushed 4 commits to branch elpi-elaborator.

view this post on Zulip HB Github Bot (Jul 29 2020 at 16:14):

gares opened PR #97 [hack] use Coq-Elpi elaborator from elpi-elaborator to master:

Since Coq-Elpi 1.5 the elaborator written in Elpi can be used, but is has some problems.

view this post on Zulip HB Github Bot (Jul 29 2020 at 16:16):

gares pushed 2 commits to branch elpi-elaborator.

view this post on Zulip HB Github Bot (Jul 29 2020 at 16:16):

gares updated PR #97 [hack] use Coq-Elpi elaborator from elpi-elaborator to master:

Since Coq-Elpi 1.5 the elaborator written in Elpi can be used, but is has some problems.

view this post on Zulip HB Github Bot (Jul 29 2020 at 16:17):

gares edited PR #97 [hack] use Coq-Elpi elaborator from elpi-elaborator to master:

Since Coq-Elpi 1.5 the elaborator written in Elpi can be used, but is has some problems.

Depends on: #92

view this post on Zulip HB Github Bot (Jul 29 2020 at 16:17):

gares submitted PR Review for #97 [hack] use Coq-Elpi elaborator.

view this post on Zulip HB Github Bot (Jul 29 2020 at 16:17):

gares created PR Review Comment on #97 [hack] use Coq-Elpi elaborator:

Here it works and inserts coercions

view this post on Zulip HB Github Bot (Jul 29 2020 at 16:18):

gares submitted PR Review for #97 [hack] use Coq-Elpi elaborator.

view this post on Zulip HB Github Bot (Jul 29 2020 at 16:18):

gares created PR Review Comment on #97 [hack] use Coq-Elpi elaborator:

This predicate is very incomplete

view this post on Zulip HB Github Bot (Jul 29 2020 at 16:18):

gares submitted PR Review for #97 [hack] use Coq-Elpi elaborator.

view this post on Zulip HB Github Bot (Jul 29 2020 at 16:18):

gares created PR Review Comment on #97 [hack] use Coq-Elpi elaborator:

This is even switched off

view this post on Zulip HB Github Bot (Jul 29 2020 at 16:20):

gares submitted PR Review for #97 [hack] use Coq-Elpi elaborator.

view this post on Zulip HB Github Bot (Jul 29 2020 at 16:20):

gares created PR Review Comment on #97 [hack] use Coq-Elpi elaborator:

This is a know bug I did not have time to investigate. The elaborator is likely to miss some universe constraints.

view this post on Zulip HB Github Bot (Jul 29 2020 at 16:20):

gares edited PR #97 [hack] use Coq-Elpi elaborator to infer coercions from elpi-elaborator to master:

Since Coq-Elpi 1.5 the elaborator written in Elpi can be used, but is has some problems.

Depends on: #92

view this post on Zulip HB Github Bot (Jul 29 2020 at 16:26):

gares milestoned Issue #88 in Coq 8.12 support #[local] HB.instance:

In 8.12 you can write #[local] Canonical foo

view this post on Zulip HB Github Bot (Jul 30 2020 at 12:06):

gares pushed 1 commit to branch HOAS+holes.

view this post on Zulip HB Github Bot (Jul 30 2020 at 12:06):

gares updated PR #92 coq-elpi 1.5 from HOAS+holes to master:

Take advantage of Coq-Elpi 1.5.x

view this post on Zulip HB Github Bot (Jul 31 2020 at 14:58):

gares merged PR #92 coq-elpi 1.5.

view this post on Zulip HB Github Bot (Jul 31 2020 at 14:58):

gares pushed 7 commits to branch master.

view this post on Zulip HB Github Bot (Jul 31 2020 at 14:58):

gares deleted the branch HOAS+holes.

view this post on Zulip HB Github Bot (Aug 03 2020 at 16:33):

dmitromikh opened Issue #98 A bug with insertion of coercions:

In the definition of mixin like the next one:

HB.mixin Record foo T := {
  bar : T -> true;
}.

there is an error without any meaningful explanation. However, after the insertion of coercion manually, it works fine:

HB.mixin Record foo T := {
  bar : T -> (is_true true);
}.

So, it would be great if the coercion insertion was automatic.

view this post on Zulip HB Github Bot (Aug 03 2020 at 17:04):

CohenCyril edited Issue #34 HB. commands should insert coercions when necessary:

@gares how do I replace
https://github.com/math-comp/hierarchy-builder/blob/854fc09f590752ff77a59f93bfc11c41fbbd722b/demo2/stage11.v#L172-L173
by

Elpi hb.canonical (T1 * T2)%type prod_topology.

?
(making coq-elpi insert the coercion TopologicalSpace.sort)

view this post on Zulip HB Github Bot (Aug 04 2020 at 14:41):

volodeyka opened Issue #99 HB forgets about Canonical Instance :

HB.mixin Record eqType_of_Type T := {
  op  : rel T;
  eqP : Equality.axiom op;
}.

HB.structure Definition eq := { T of eqType_of_Type T }.


Canonical hb_eqMixin {T : eq.type} := @EqMixin T _ eqP.
Canonical hb_eqType {T : eq.type} := Eval hnf in EqType T hb_eqMixin.
Definition foo {T : eq.type} (e : T) := e == e.

HB.mixin Record my_class_of_eqType T of eq T := {
  foo: T -> T;
}.

HB.structure Definition my := { T of eq T & my_class_of_eqType T }.

Fail Definition foo1 {T : my.type} (e : T) := e == e.
Fail Canonical porder_eqMixin {T : my.type} := @EqMixin T _ eqP.

I want to make my structure with decidable equality via HB. Then it could be an instance of mathcomp's eqType. I make my.type that inherits eq.type, so my.type is coercible to eq.type which is coercible to eqType. But if you look at foo1 definition you can see that Coq can't solve such a unification problem. Also, I can't make a new Canonical instance for my.type because it conflicts with hb_eqMixin.

view this post on Zulip HB Github Bot (Aug 04 2020 at 14:55):

volodeyka opened Issue #100 Inheritance of mathcomp's structures:

Can you provide the best way to inherit mathcomp's structures? I want to make something like this:

Section foo.
Variable (T : eqType).

HB.mixin my_class_of_eqType T := { ... }. (*or something like that*)

Is there any way to inherit mathcomp's eqType?

view this post on Zulip HB Github Bot (Aug 05 2020 at 09:59):

CohenCyril pushed 1 commit to branch class-to-mixin-coercions.

view this post on Zulip HB Github Bot (Aug 05 2020 at 09:59):

CohenCyril opened PR #101 Adding coercions from classes to mixins from class-to-mixin-coercions to master.

view this post on Zulip HB Github Bot (Aug 07 2020 at 14:40):

CohenCyril merged PR #101 Adding coercions from classes to mixins.

view this post on Zulip HB Github Bot (Aug 07 2020 at 14:40):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Aug 07 2020 at 14:40):

CohenCyril deleted the branch class-to-mixin-coercions.

view this post on Zulip HB Github Bot (Aug 07 2020 at 14:47):

CohenCyril pushed 1 commit to branch fix_89.

view this post on Zulip HB Github Bot (Aug 07 2020 at 14:48):

CohenCyril opened PR #102 fixes #89 from fix_89 to master.

view this post on Zulip HB Github Bot (Aug 07 2020 at 14:48):

CohenCyril edited PR #102 fixes #89 from fix_89 to master:

fixes #89

view this post on Zulip HB Github Bot (Aug 07 2020 at 20:11):

CohenCyril closed Issue #89 outdated doc about builders:

https://github.com/math-comp/hierarchy-builder/blob/22cc857bda3d9e696d49e827417af8e681e1e1bd/structures.v#L383

There is no _f anymore

view this post on Zulip HB Github Bot (Aug 07 2020 at 20:11):

CohenCyril merged PR #102 fixes #89.

view this post on Zulip HB Github Bot (Aug 07 2020 at 20:11):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Aug 07 2020 at 20:11):

CohenCyril milestoned Issue #102 fixes #89:

fixes #89

view this post on Zulip HB Github Bot (Aug 07 2020 at 20:55):

CohenCyril pushed 1 commit to branch fix_90.

view this post on Zulip HB Github Bot (Aug 07 2020 at 20:56):

CohenCyril opened PR #103 Remove reexports of notations from fix_90 to master:

fixes #90

view this post on Zulip HB Github Bot (Aug 07 2020 at 20:59):

CohenCyril pushed 1 commit to branch fix_91.

view this post on Zulip HB Github Bot (Aug 07 2020 at 20:59):

CohenCyril opened PR #104 Better error message in case of wrong structure definition order from fix_91 to master:

fixes #91

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:03):

CohenCyril demilestoned Issue #88 in Coq 8.12 support #[local] HB.instance:

In 8.12 you can write #[local] Canonical foo

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:03):

CohenCyril milestoned Issue #88 in Coq 8.12 support #[local] HB.instance:

In 8.12 you can write #[local] Canonical foo

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:03):

CohenCyril pushed 1 commit to branch fix_87.

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:04):

CohenCyril pushed 1 commit to branch fix_87.

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:05):

CohenCyril opened PR #105 removing spurious empty TYPE structure from fix_87 to master:

fixes #87

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:05):

CohenCyril closed Issue #90 Reexport shadows the original notation for the relation/operation.

As noted by @chdoc on zulip.
C.f. https://gist.github.com/chdoc/f50c3a15c41e92ec0ac89112f1e18fbe

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:05):

CohenCyril merged PR #103 Remove reexports of notations.

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:05):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:06):

CohenCyril milestoned Issue #103 Remove reexports of notations:

fixes #90

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:08):

CohenCyril milestoned Issue #104 Better error message in case of wrong structure definition order:

fixes #91

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:08):

CohenCyril closed Issue #91 Error message "you must declare X before Y" is bogus since parameters were introduced:

Code
https://github.com/math-comp/hierarchy-builder/blob/01c24925f08ca39844a8e26e8eae085bfd6088e7/hb.elpi#L501-L506
prints stuff like:

You must declare
class (indt «axioms») (global (indt «type»))
 (w-params.nil `A` (sort (typ «bug.9333»)) c0 \
   [triple (indt «Ops_of_Type.axioms_») [] c0,
    triple (indt «Setoid_of_Type.axioms_») [] c0,
    triple (indt «Ptt_of_Ops.axioms_») [] c0]) before
indt «Pttdom.axioms»

The "class" must be printed better, also we should try to print only structure names (classes are sort of internal)

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:08):

CohenCyril merged PR #104 Better error message in case of wrong structure definition order.

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:08):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:08):

CohenCyril deleted the branch fix_91.

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:08):

CohenCyril milestoned Issue #105 removing spurious empty TYPE structure:

fixes #87

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:13):

CohenCyril closed Issue #87 demo1 has still a dummy root structure with no properties.

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:13):

CohenCyril merged PR #105 removing spurious empty TYPE structure.

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:13):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:52):

CohenCyril pushed 2 commits to branch fix-join-with-params.

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:53):

CohenCyril opened PR #106 Fix the join of structures with parameters + changelog from fix-join-with-params to master:

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:53):

CohenCyril demilestoned Issue #72 A brief report on trying to port the Iris hierarchy to HB:

Hey everyone,

I was very happy to see the hierarchy builder being announced and I wanted to see what would happen if I used it to define the hierarchy in Iris. This was really just for fun since I do not expect the result to be usable given Iris's reliance on type classes. I also wanted to learn from the resulting definitions since I still don't really understand how one is supposed to set up canonical structures.

But my experiment ended before I got to actually trying out the result. I pushed the experiment to https://gitlab.mpi-sws.org/janno/iris-coq/-/tree/janno/try-HB (the branch name is janno/try-HB). The only file that changed is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v. It contains both old an new definitions, which are confined to lines 150-178. The original file without my new stuff is here: https://gitlab.mpi-sws.org/iris/iris/-/blob/962637df10a879ac4b1b9d523854d6fa4c9e8fb4/theories/bi/interface.v

Of particular interest is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L242 where I cannot get HB to accept the definition of an SBI (an extension of the BI definition in https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L156). The error HB reports is this (when using the right printing settings):

The term "@Some" of type "∀ A : Type, A → option A"
cannot be applied to the terms
 "?e5" : "Type"
 "("is not canonically a", bi.type)" : "(string * Type)%type"

I suppose the underlying error is a mistake on my side but I don't know what it would be.

To get to this point I also had to work around an unexpected shortcoming regarding implicit type class arguments. As you can see in the definition of the BI structure, I had to manually spell out all type class instances since HB would not accept the terms otherwise. (This is veeeeery annoying since it also means that notation such as that for equiv needs to be unfolded.)

Finally, there's something that I wouldn't count as a bug but more of a feature request: in the original Iris hierarchy, the bi_mixin Section (at the top of the file) creates local notation for the operators that make the axioms look very natural. I couldn't find a way to replicate this setup. Maybe HB.mixin could accept where clauses for (local) syntax?

Building the branch
My opam switch reports the following packages:

coq-elpi                1.3.1                     Elpi extension language for Coq
coq-hierarchy-builder   0.9.0                     Hierarchy Builder
coq-stdpp               dev.2019-12-06.0.1ef53c55 pinned to version dev.2019-12-06.0.1ef53c55 at git+https://gitlab.mpi-sws.org/iris/stdpp.git

If you want to avoid pinning coq-stdpp to the git hash (the suffix of that weird dev version) you can

opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

and then opam should be able to find that exact version.

Running make inside a clone of my iris-coq branch should eventually compile interfaces.v and report the errors.

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:53):

CohenCyril milestoned Issue #72 A brief report on trying to port the Iris hierarchy to HB:

Hey everyone,

I was very happy to see the hierarchy builder being announced and I wanted to see what would happen if I used it to define the hierarchy in Iris. This was really just for fun since I do not expect the result to be usable given Iris's reliance on type classes. I also wanted to learn from the resulting definitions since I still don't really understand how one is supposed to set up canonical structures.

But my experiment ended before I got to actually trying out the result. I pushed the experiment to https://gitlab.mpi-sws.org/janno/iris-coq/-/tree/janno/try-HB (the branch name is janno/try-HB). The only file that changed is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v. It contains both old an new definitions, which are confined to lines 150-178. The original file without my new stuff is here: https://gitlab.mpi-sws.org/iris/iris/-/blob/962637df10a879ac4b1b9d523854d6fa4c9e8fb4/theories/bi/interface.v

Of particular interest is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L242 where I cannot get HB to accept the definition of an SBI (an extension of the BI definition in https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L156). The error HB reports is this (when using the right printing settings):

The term "@Some" of type "∀ A : Type, A → option A"
cannot be applied to the terms
 "?e5" : "Type"
 "("is not canonically a", bi.type)" : "(string * Type)%type"

I suppose the underlying error is a mistake on my side but I don't know what it would be.

To get to this point I also had to work around an unexpected shortcoming regarding implicit type class arguments. As you can see in the definition of the BI structure, I had to manually spell out all type class instances since HB would not accept the terms otherwise. (This is veeeeery annoying since it also means that notation such as that for equiv needs to be unfolded.)

Finally, there's something that I wouldn't count as a bug but more of a feature request: in the original Iris hierarchy, the bi_mixin Section (at the top of the file) creates local notation for the operators that make the axioms look very natural. I couldn't find a way to replicate this setup. Maybe HB.mixin could accept where clauses for (local) syntax?

Building the branch
My opam switch reports the following packages:

coq-elpi                1.3.1                     Elpi extension language for Coq
coq-hierarchy-builder   0.9.0                     Hierarchy Builder
coq-stdpp               dev.2019-12-06.0.1ef53c55 pinned to version dev.2019-12-06.0.1ef53c55 at git+https://gitlab.mpi-sws.org/iris/stdpp.git

If you want to avoid pinning coq-stdpp to the git hash (the suffix of that weird dev version) you can

opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

and then opam should be able to find that exact version.

Running make inside a clone of my iris-coq branch should eventually compile interfaces.v and report the errors.

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:54):

CohenCyril demilestoned Issue #72 A brief report on trying to port the Iris hierarchy to HB:

Hey everyone,

I was very happy to see the hierarchy builder being announced and I wanted to see what would happen if I used it to define the hierarchy in Iris. This was really just for fun since I do not expect the result to be usable given Iris's reliance on type classes. I also wanted to learn from the resulting definitions since I still don't really understand how one is supposed to set up canonical structures.

But my experiment ended before I got to actually trying out the result. I pushed the experiment to https://gitlab.mpi-sws.org/janno/iris-coq/-/tree/janno/try-HB (the branch name is janno/try-HB). The only file that changed is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v. It contains both old an new definitions, which are confined to lines 150-178. The original file without my new stuff is here: https://gitlab.mpi-sws.org/iris/iris/-/blob/962637df10a879ac4b1b9d523854d6fa4c9e8fb4/theories/bi/interface.v

Of particular interest is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L242 where I cannot get HB to accept the definition of an SBI (an extension of the BI definition in https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L156). The error HB reports is this (when using the right printing settings):

The term "@Some" of type "∀ A : Type, A → option A"
cannot be applied to the terms
 "?e5" : "Type"
 "("is not canonically a", bi.type)" : "(string * Type)%type"

I suppose the underlying error is a mistake on my side but I don't know what it would be.

To get to this point I also had to work around an unexpected shortcoming regarding implicit type class arguments. As you can see in the definition of the BI structure, I had to manually spell out all type class instances since HB would not accept the terms otherwise. (This is veeeeery annoying since it also means that notation such as that for equiv needs to be unfolded.)

Finally, there's something that I wouldn't count as a bug but more of a feature request: in the original Iris hierarchy, the bi_mixin Section (at the top of the file) creates local notation for the operators that make the axioms look very natural. I couldn't find a way to replicate this setup. Maybe HB.mixin could accept where clauses for (local) syntax?

Building the branch
My opam switch reports the following packages:

coq-elpi                1.3.1                     Elpi extension language for Coq
coq-hierarchy-builder   0.9.0                     Hierarchy Builder
coq-stdpp               dev.2019-12-06.0.1ef53c55 pinned to version dev.2019-12-06.0.1ef53c55 at git+https://gitlab.mpi-sws.org/iris/stdpp.git

If you want to avoid pinning coq-stdpp to the git hash (the suffix of that weird dev version) you can

opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

and then opam should be able to find that exact version.

Running make inside a clone of my iris-coq branch should eventually compile interfaces.v and report the errors.

view this post on Zulip HB Github Bot (Aug 07 2020 at 21:54):

CohenCyril milestoned Issue #72 A brief report on trying to port the Iris hierarchy to HB:

Hey everyone,

I was very happy to see the hierarchy builder being announced and I wanted to see what would happen if I used it to define the hierarchy in Iris. This was really just for fun since I do not expect the result to be usable given Iris's reliance on type classes. I also wanted to learn from the resulting definitions since I still don't really understand how one is supposed to set up canonical structures.

But my experiment ended before I got to actually trying out the result. I pushed the experiment to https://gitlab.mpi-sws.org/janno/iris-coq/-/tree/janno/try-HB (the branch name is janno/try-HB). The only file that changed is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v. It contains both old an new definitions, which are confined to lines 150-178. The original file without my new stuff is here: https://gitlab.mpi-sws.org/iris/iris/-/blob/962637df10a879ac4b1b9d523854d6fa4c9e8fb4/theories/bi/interface.v

Of particular interest is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L242 where I cannot get HB to accept the definition of an SBI (an extension of the BI definition in https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L156). The error HB reports is this (when using the right printing settings):

The term "@Some" of type "∀ A : Type, A → option A"
cannot be applied to the terms
 "?e5" : "Type"
 "("is not canonically a", bi.type)" : "(string * Type)%type"

I suppose the underlying error is a mistake on my side but I don't know what it would be.

To get to this point I also had to work around an unexpected shortcoming regarding implicit type class arguments. As you can see in the definition of the BI structure, I had to manually spell out all type class instances since HB would not accept the terms otherwise. (This is veeeeery annoying since it also means that notation such as that for equiv needs to be unfolded.)

Finally, there's something that I wouldn't count as a bug but more of a feature request: in the original Iris hierarchy, the bi_mixin Section (at the top of the file) creates local notation for the operators that make the axioms look very natural. I couldn't find a way to replicate this setup. Maybe HB.mixin could accept where clauses for (local) syntax?

Building the branch
My opam switch reports the following packages:

coq-elpi                1.3.1                     Elpi extension language for Coq
coq-hierarchy-builder   0.9.0                     Hierarchy Builder
coq-stdpp               dev.2019-12-06.0.1ef53c55 pinned to version dev.2019-12-06.0.1ef53c55 at git+https://gitlab.mpi-sws.org/iris/stdpp.git

If you want to avoid pinning coq-stdpp to the git hash (the suffix of that weird dev version) you can

opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

and then opam should be able to find that exact version.

Running make inside a clone of my iris-coq branch should eventually compile interfaces.v and report the errors.

view this post on Zulip HB Github Bot (Aug 07 2020 at 22:26):

CohenCyril merged PR #106 Fix the join of structures with parameters + changelog.

view this post on Zulip HB Github Bot (Aug 07 2020 at 22:26):

CohenCyril pushed 3 commits to branch master.

view this post on Zulip HB Github Bot (Aug 07 2020 at 22:26):

CohenCyril milestoned Issue #106 Fix the join of structures with parameters + changelog:

view this post on Zulip HB Github Bot (Aug 07 2020 at 22:26):

CohenCyril deleted the branch fix-join-with-params.

view this post on Zulip HB Github Bot (Aug 07 2020 at 22:28):

CohenCyril created release Hierarchy Builder 0.10.0 for tag 0.10.0.

view this post on Zulip HB Github Bot (Aug 07 2020 at 22:29):

CohenCyril edited release Hierarchy Builder 0.10.0 for tag 0.10.0.

view this post on Zulip HB Github Bot (Aug 07 2020 at 22:29):

CohenCyril released release Hierarchy Builder 0.10.0 for tag 0.10.0.

view this post on Zulip HB Github Bot (Aug 07 2020 at 22:29):

CohenCyril published release Hierarchy Builder 0.10.0 for tag 0.10.0.

view this post on Zulip HB Github Bot (Aug 07 2020 at 22:29):

CohenCyril pushed tag 0.10.0.

view this post on Zulip HB Github Bot (Aug 07 2020 at 22:29):

CohenCyril edited release Hierarchy Builder 0.10.0 for tag 0.10.0.

view this post on Zulip HB Github Bot (Aug 07 2020 at 22:30):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Aug 07 2020 at 22:32):

CohenCyril edited release Hierarchy Builder 0.10.0 for tag v0.10.0.

view this post on Zulip HB Github Bot (Aug 07 2020 at 22:32):

CohenCyril pushed tag v0.10.0.

view this post on Zulip HB Github Bot (Aug 07 2020 at 22:32):

CohenCyril removed tag 0.10.0.

view this post on Zulip HB Github Bot (Aug 08 2020 at 05:33):

gares pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Aug 08 2020 at 05:34):

gares opened Issue #107 update readme wrt 0.10.

view this post on Zulip HB Github Bot (Aug 13 2020 at 13:11):

gares pushed 2 commits to branch mathcomp-compat.

view this post on Zulip HB Github Bot (Aug 13 2020 at 13:11):

gares opened PR #108 Mathcomp compat from mathcomp-compat to master.

view this post on Zulip HB Github Bot (Aug 14 2020 at 12:08):

gares pushed 1 commit to branch coq-elaborator-elpi-1.6.

view this post on Zulip HB Github Bot (Aug 14 2020 at 12:09):

gares opened PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

Depends on https://github.com/LPCIC/coq-elpi/pull/170
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 14 2020 at 12:11):

gares edited PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

That's it. It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing coq-elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170)

Depends on LPCIC/coq-elpi#170
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 14 2020 at 12:12):

gares edited PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

That's it. It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing Coq-Elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170).

Depends on LPCIC/coq-elpi#170
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 14 2020 at 12:15):

gares edited PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

That's it. It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing Coq-Elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170).

Depends on LPCIC/coq-elpi#170 it was tested locally and works, here CI does not pick up the needed Coq-Elpi branch.
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 14 2020 at 15:14):

gares pushed 2 commits to branch coq-elaborator-elpi-1.6.

view this post on Zulip HB Github Bot (Aug 14 2020 at 15:14):

gares updated PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

That's it. It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing Coq-Elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170).

Depends on LPCIC/coq-elpi#170 it was tested locally and works, here CI does not pick up the needed Coq-Elpi branch.
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 14 2020 at 17:57):

gares closed without merge PR #97 [hack] use Coq-Elpi elaborator to infer coercions.

view this post on Zulip HB Github Bot (Aug 20 2020 at 08:27):

gares pushed 1 commit to branch coq-elaborator-elpi-1.6.

view this post on Zulip HB Github Bot (Aug 20 2020 at 08:27):

gares updated PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

That's it. It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing Coq-Elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170).

Depends on LPCIC/coq-elpi#170 it was tested locally and works, here CI does not pick up the needed Coq-Elpi branch.
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 20 2020 at 08:30):

gares pushed 1 commit to branch coq-elaborator-elpi-1.6.

view this post on Zulip HB Github Bot (Aug 20 2020 at 08:30):

gares updated PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

That's it. It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing Coq-Elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170).

Depends on LPCIC/coq-elpi#170 it was tested locally and works, here CI does not pick up the needed Coq-Elpi branch.
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 20 2020 at 08:47):

gares pushed 1 commit to branch coq-elaborator-elpi-1.6.

view this post on Zulip HB Github Bot (Aug 20 2020 at 08:47):

gares updated PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

That's it. It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing Coq-Elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170).

Depends on LPCIC/coq-elpi#170 it was tested locally and works, here CI does not pick up the needed Coq-Elpi branch.
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 20 2020 at 09:18):

gares pushed 3 commits to branch coq-elaborator-elpi-1.6.

view this post on Zulip HB Github Bot (Aug 20 2020 at 09:18):

gares updated PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

That's it. It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing Coq-Elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170).

Depends on LPCIC/coq-elpi#170 it was tested locally and works, here CI does not pick up the needed Coq-Elpi branch.
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 21 2020 at 12:21):

gares pushed 1 commit to branch coq-elaborator-elpi-1.6.

view this post on Zulip HB Github Bot (Aug 21 2020 at 12:21):

gares updated PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

That's it. It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing Coq-Elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170).

Depends on LPCIC/coq-elpi#170 it was tested locally and works, here CI does not pick up the needed Coq-Elpi branch.
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 21 2020 at 12:22):

gares edited PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

That's it. It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing Coq-Elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170).

Depends on LPCIC/coq-elpi#170 it was tested locally and works, here CI does not pick up the needed Coq-Elpi branch.
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 21 2020 at 12:22):

gares edited PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

That's it.
It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing Coq-Elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170).

Depends on LPCIC/coq-elpi#170 it was tested locally and works, here CI does not pick up the needed Coq-Elpi branch.
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 21 2020 at 12:33):

gares pushed 12 commits to branch coq-elaborator-elpi-1.6.

view this post on Zulip HB Github Bot (Aug 21 2020 at 12:33):

gares updated PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

That's it.
It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing Coq-Elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170).

Depends on LPCIC/coq-elpi#170 it was tested locally and works, here CI does not pick up the needed Coq-Elpi branch.
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 21 2020 at 13:49):

gares pushed 1 commit to branch coq-elaborator-elpi-1.6.

view this post on Zulip HB Github Bot (Aug 21 2020 at 13:50):

gares updated PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

That's it.
It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing Coq-Elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170).

Depends on LPCIC/coq-elpi#170 it was tested locally and works, here CI does not pick up the needed Coq-Elpi branch.
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 25 2020 at 15:13):

gares pushed 1 commit to branch coq-master.

view this post on Zulip HB Github Bot (Aug 25 2020 at 15:17):

gares pushed the branch coq-elaborator-elpi-1.6.

view this post on Zulip HB Github Bot (Aug 25 2020 at 15:17):

gares updated PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

That's it.
It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing Coq-Elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170).

Depends on LPCIC/coq-elpi#170 it was tested locally and works, here CI does not pick up the needed Coq-Elpi branch.
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 25 2020 at 16:55):

gares pushed 1 commit to branch coq-elaborator-elpi-1.6.

view this post on Zulip HB Github Bot (Aug 25 2020 at 16:55):

gares updated PR #109 use Coq's elaborator for factories and instances from coq-elaborator-elpi-1.6 to master:

That's it.
It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing Coq-Elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170).

Depends on LPCIC/coq-elpi#170 it was tested locally and works, here CI does not pick up the needed Coq-Elpi branch.
Fix #98 #34

view this post on Zulip HB Github Bot (Aug 26 2020 at 08:10):

gares closed Issue #98 A bug with insertion of coercions:

In the definition of mixin like the next one:

HB.mixin Record foo T := {
  bar : T -> true;
}.

there is an error without any meaningful explanation. However, after the insertion of coercion manually, it works fine:

HB.mixin Record foo T := {
  bar : T -> (is_true true);
}.

So, it would be great if the coercion insertion was automatic.

view this post on Zulip HB Github Bot (Aug 26 2020 at 08:10):

gares merged PR #109 use Coq's elaborator for factories and instances.

view this post on Zulip HB Github Bot (Aug 26 2020 at 08:10):

gares pushed 14 commits to branch master.

view this post on Zulip HB Github Bot (Aug 26 2020 at 08:10):

gares deleted the branch coq-elaborator-elpi-1.6.

view this post on Zulip HB Github Bot (Aug 26 2020 at 08:12):

pi8027 closed Issue #34 HB. commands should insert coercions when necessary:

@gares how do I replace
https://github.com/math-comp/hierarchy-builder/blob/854fc09f590752ff77a59f93bfc11c41fbbd722b/demo2/stage11.v#L172-L173
by

Elpi hb.canonical (T1 * T2)%type prod_topology.

?
(making coq-elpi insert the coercion TopologicalSpace.sort)

view this post on Zulip HB Github Bot (Aug 26 2020 at 08:26):

gares opened Issue #110 when postulating section variables, assume type is Type if not given.

view this post on Zulip HB Github Bot (Aug 26 2020 at 08:28):

gares opened Issue #111 HB.structure Definition s forgot-params := { T of mixin_w_params T }

error message is about split-at but should talk about missing parameters

view this post on Zulip HB Github Bot (Aug 26 2020 at 09:10):

CohenCyril opened Issue #112 HB.structure should generate a pack notation:

Generate pack in order to build a structure from a single mixin.

view this post on Zulip HB Github Bot (Aug 26 2020 at 10:01):

CohenCyril opened Issue #113 HB interacts badly with "Set Implicit Arguments"

As of now we assume that the constant added by coq.env.add-const have explicit arguments, we should not assume such a thing because it is not true with option Set Implicit Arguments

view this post on Zulip HB Github Bot (Aug 26 2020 at 10:01):

gares pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Aug 26 2020 at 10:10):

gares opened Issue #114 get-canonical-mixin-of and type checking:

to play safe and avoid the bug fixed in 82ee5b9558e6f7c235e74fac208184eb42b9771a we could (should?)
typecheck the terms before calling the unifier. That would have detected the missing parameters.

view this post on Zulip HB Github Bot (Aug 26 2020 at 11:55):

gares pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Aug 26 2020 at 11:55):

gares closed Issue #111 HB.structure Definition s forgot-params := { T of mixin_w_params T }

error message is about split-at but should talk about missing parameters

view this post on Zulip HB Github Bot (Aug 26 2020 at 11:56):

gares closed Issue #110 when postulating section variables, assume type is Type if not given.

view this post on Zulip HB Github Bot (Aug 26 2020 at 11:56):

gares reopened Issue #111 HB.structure Definition s forgot-params := { T of mixin_w_params T }

error message is about split-at but should talk about missing parameters

view this post on Zulip HB Github Bot (Aug 26 2020 at 12:00):

gares closed Issue #83 HB.instance Definition foo : is_s T := Build bar should read the number of parameters from is_s T (when given)

view this post on Zulip HB Github Bot (Aug 26 2020 at 12:05):

gares pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Aug 26 2020 at 12:05):

gares closed Issue #107 update readme wrt 0.10.

view this post on Zulip HB Github Bot (Aug 26 2020 at 12:28):

gares pushed 1 commit to branch local-instances.

view this post on Zulip HB Github Bot (Aug 26 2020 at 12:28):

gares opened PR #115 HB.instance understands #[local] (fix #88) from local-instances to master.

view this post on Zulip HB Github Bot (Aug 26 2020 at 12:29):

gares pushed 1 commit to branch local-instances.

view this post on Zulip HB Github Bot (Aug 26 2020 at 12:29):

gares updated PR #115 HB.instance understands #[local] (fix #88) from local-instances to master.

view this post on Zulip HB Github Bot (Aug 26 2020 at 12:30):

gares submitted PR Review for #115 HB.instance understands #[local] (fix #88)

view this post on Zulip HB Github Bot (Aug 26 2020 at 12:30):

gares created PR Review Comment on #115 HB.instance understands #[local] (fix #88)

@CohenCyril @pi8027 : the comment here seems to suggest we want local-by-default.
If so, the attribute should be #[global] instead...

view this post on Zulip HB Github Bot (Aug 26 2020 at 12:31):

gares edited PR #115 HB.instance understands #[local] (fix #88) from local-instances to master:

This pr:

view this post on Zulip HB Github Bot (Aug 26 2020 at 12:32):

gares closed without merge PR #108 Mathcomp compat.

view this post on Zulip HB Github Bot (Sep 02 2020 at 08:27):

CohenCyril opened Issue #116 HB.instance without Definition should take head symbol rather than fully applied term:

E.g.

Definition stuff  T  : mixin (f T) :=  ...
HB.instance f stuff.

instead of

Section stuff.
Variable T.
Definition stuff  : mixin (f T) :=  ...
HB.instance (f T) stuff.
End stuff.

view this post on Zulip HB Github Bot (Sep 02 2020 at 08:29):

CohenCyril opened Issue #117 Mixins arguments scope should be settable:

e.g.

HB.mixin Record bla (T : Type) := ....
HB.arguments bla T%scope
Check (bla (_ * _)).

view this post on Zulip HB Github Bot (Sep 02 2020 at 09:54):

CohenCyril pushed 2 commits to branch pack_notation.

view this post on Zulip HB Github Bot (Sep 02 2020 at 16:43):

gares opened PR #118 Pack notation from pack_notation to master.

view this post on Zulip HB Github Bot (Sep 10 2020 at 09:17):

gares pushed 2 commits to branch pack_notation.

view this post on Zulip HB Github Bot (Sep 10 2020 at 09:17):

gares updated PR #118 Pack notation from pack_notation to master.

view this post on Zulip HB Github Bot (Sep 10 2020 at 09:45):

gares pushed 1 commit to branch pack_notation.

view this post on Zulip HB Github Bot (Sep 10 2020 at 09:45):

gares updated PR #118 Pack notation from pack_notation to master.

view this post on Zulip HB Github Bot (Sep 10 2020 at 11:26):

gares has marked PR #118 as ready for review.

view this post on Zulip HB Github Bot (Sep 16 2020 at 08:32):

gares closed without merge PR #118 Pack notation.

view this post on Zulip HB Github Bot (Sep 16 2020 at 08:32):

CohenCyril pushed 4 commits to branch master. Commits by CohenCyril (2) and gares (2).

view this post on Zulip HB Github Bot (Sep 16 2020 at 08:33):

gares deleted the branch pack_notation.

view this post on Zulip HB Github Bot (Sep 16 2020 at 10:01):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Sep 24 2020 at 09:44):

gares pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Sep 24 2020 at 09:45):

gares pushed 1 commit to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Sep 24 2020 at 09:45):

gares opened PR #119 wip from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Sep 24 2020 at 09:45):

gares edited PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 01 2020 at 10:02):

CohenCyril pushed 1 commit to branch section-discharge-fight-ko.

view this post on Zulip HB Github Bot (Oct 01 2020 at 10:21):

gares pushed 1 commit to branch section-discharge-fight-ko.

view this post on Zulip HB Github Bot (Oct 01 2020 at 10:21):

gares pushed 2 commits to branch section-discharge-fight. Commits by CohenCyril (1) and gares (1).

view this post on Zulip HB Github Bot (Oct 01 2020 at 10:21):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 01 2020 at 10:35):

CohenCyril commented on abbdc32:

:crying_cat_face:

view this post on Zulip HB Github Bot (Oct 01 2020 at 10:52):

gares commented on abbdc32:

Ooops

view this post on Zulip HB Github Bot (Oct 01 2020 at 11:16):

gares pushed 3 commits to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Oct 01 2020 at 11:16):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 01 2020 at 13:46):

gares pushed 2 commits to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Oct 01 2020 at 13:46):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 01 2020 at 14:01):

gares pushed 1 commit to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Oct 01 2020 at 14:01):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 06 2020 at 08:29):

gares pushed 1 commit to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Oct 06 2020 at 08:29):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 06 2020 at 08:40):

gares submitted PR Review for #119 [hack] section discharge unused.

view this post on Zulip HB Github Bot (Oct 06 2020 at 08:40):

gares created PR Review Comment on #119 [hack] section discharge unused:

Does this make sense? Or should we check something?

view this post on Zulip HB Github Bot (Oct 06 2020 at 08:45):

gares submitted PR Review for #119 [hack] section discharge unused.

view this post on Zulip HB Github Bot (Oct 06 2020 at 08:45):

gares created PR Review Comment on #119 [hack] section discharge unused:

We change the approach: hb.instance names all the mixin inhabitants and hb.end declares a from for them after section discharge.

view this post on Zulip HB Github Bot (Oct 08 2020 at 07:28):

gares pushed 1 commit to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Oct 08 2020 at 07:28):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 08 2020 at 09:07):

CohenCyril pushed 1 commit to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Oct 08 2020 at 09:07):

CohenCyril updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 08 2020 at 14:59):

gares pushed 6 commits to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Oct 08 2020 at 14:59):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 09 2020 at 08:08):

gares pushed 5 commits to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Oct 09 2020 at 08:08):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 09 2020 at 08:17):

gares requested CohenCyril for a review on PR #119 [hack] section discharge unused.

view this post on Zulip HB Github Bot (Oct 09 2020 at 15:33):

gares submitted PR Review for #119 [hack] section discharge unused.

view this post on Zulip HB Github Bot (Oct 09 2020 at 15:33):

gares created PR Review Comment on #119 [hack] section discharge unused:

@CohenCyril can you write a line of doc for this thing?

view this post on Zulip HB Github Bot (Oct 13 2020 at 15:08):

gares pushed 1 commit to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Oct 13 2020 at 15:08):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 13 2020 at 15:19):

gares pushed 1 commit to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Oct 13 2020 at 15:19):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 13 2020 at 18:10):

gares edited Issue #112 [wish] HB.pack Definition packager args : structure.

Generate pack in order to build a structure from a single mixin.

view this post on Zulip HB Github Bot (Oct 14 2020 at 07:41):

gares closed Issue #111 HB.structure Definition s forgot-params := { T of mixin_w_params T }

error message is about split-at but should talk about missing parameters

view this post on Zulip HB Github Bot (Oct 14 2020 at 07:42):

gares closed Issue #85 Add an HB mode to generate mathcomp compat boilerplate:

cf e.g. https://github.com/gares/math-comp/blob/hierarchy-builder/mathcomp/ssreflect/eqtype.v#L125-L146

view this post on Zulip HB Github Bot (Oct 14 2020 at 07:42):

gares closed Issue #84 HB.instance ty term should accept just the head symbol of ty:

Today you are force to write stuff like HB.instance { x : T &.... } t but actually only sigT is really needed

view this post on Zulip HB Github Bot (Oct 14 2020 at 08:28):

gares pushed 1 commit to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Oct 14 2020 at 08:28):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 14 2020 at 08:50):

gares pushed 1 commit to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Oct 14 2020 at 08:50):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 14 2020 at 09:16):

gares pushed 1 commit to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Oct 14 2020 at 09:16):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 16 2020 at 13:44):

gares pushed 1 commit to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Oct 16 2020 at 13:44):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Oct 21 2020 at 10:57):

gares pushed 2 commits to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Oct 21 2020 at 10:57):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Nov 02 2020 at 17:55):

gares opened Issue #120 under-canonical-mixins should filter the CS db better:

See: https://coq.zulipchat.com/#narrow/stream/237868-Hierarchy-Builder.20devs.20.26.20users/topic/instance.20family.20bug.3F

Test case:

From HB Require Import structures.

HB.mixin Record base_m T := { A : T }.
HB.structure Definition base := { T of base_m T }.

HB.mixin Record child1_m T := { C1 : T }.
HB.structure Definition child1 := { T of base T & child1_m T }.

HB.mixin Record child2_m T := { C2 : T }.
HB.structure Definition child2 := { T of base T & child2_m T }.

Axiom ix : Type.
Definition vec T := ix -> T.

Section b.
Variable T : base.type.
HB.instance Definition v_base_m : base_m (vec T) :=
  base_m.Build _ (fun _ => A).
End b.

Section c1.
Variable T : child1.type.
HB.instance Definition v_child1_m : child1_m (vec T) :=
    child1_m.Build _ (fun _ => C1).
End c1.

Section c2.
Variable T : child2.type.

  (* CS lookup for `vec` says yes... but the instance is for a paramter T of different type, kaboom *)
  HB.instance Definition v_child2_m : child2_m (vec T) :=
  child2_m.Build _ (fun _ => C2).

End c2.

view this post on Zulip HB Github Bot (Nov 02 2020 at 17:59):

gares pushed 1 commit to branch fix-120.

view this post on Zulip HB Github Bot (Nov 02 2020 at 17:59):

gares opened PR #121 filter CS db in a more precise way (fix#120) from fix-120 to master.

view this post on Zulip HB Github Bot (Nov 02 2020 at 18:01):

gares pushed 1 commit to branch fix-120.

view this post on Zulip HB Github Bot (Nov 02 2020 at 18:01):

gares updated PR #121 filter CS db in a more precise way (fix#120) from fix-120 to master.

view this post on Zulip HB Github Bot (Nov 02 2020 at 18:02):

gares requested CohenCyril for a review on PR #121 filter CS db in a more precise way (fix#120).

view this post on Zulip HB Github Bot (Nov 02 2020 at 20:29):

CohenCyril submitted PR Review for #121 filter CS db in a more precise way (fix#120)

view this post on Zulip HB Github Bot (Nov 02 2020 at 20:29):

CohenCyril merged PR #121 filter CS db in a more precise way (fix#120)

view this post on Zulip HB Github Bot (Nov 02 2020 at 20:29):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and gares (1).

view this post on Zulip HB Github Bot (Nov 02 2020 at 20:29):

CohenCyril closed Issue #120 under-canonical-mixins should filter the CS db better:

See: https://coq.zulipchat.com/#narrow/stream/237868-Hierarchy-Builder.20devs.20.26.20users/topic/instance.20family.20bug.3F

Test case:

From HB Require Import structures.

HB.mixin Record base_m T := { A : T }.
HB.structure Definition base := { T of base_m T }.

HB.mixin Record child1_m T := { C1 : T }.
HB.structure Definition child1 := { T of base T & child1_m T }.

HB.mixin Record child2_m T := { C2 : T }.
HB.structure Definition child2 := { T of base T & child2_m T }.

Axiom ix : Type.
Definition vec T := ix -> T.

Section b.
Variable T : base.type.
HB.instance Definition v_base_m : base_m (vec T) :=
  base_m.Build _ (fun _ => A).
End b.

Section c1.
Variable T : child1.type.
HB.instance Definition v_child1_m : child1_m (vec T) :=
    child1_m.Build _ (fun _ => C1).
End c1.

Section c2.
Variable T : child2.type.

  (* CS lookup for `vec` says yes... but the instance is for a paramter T of different type, kaboom *)
  HB.instance Definition v_child2_m : child2_m (vec T) :=
  child2_m.Build _ (fun _ => C2).

End c2.

view this post on Zulip HB Github Bot (Nov 02 2020 at 21:50):

gares deleted the branch fix-120.

view this post on Zulip HB Github Bot (Nov 03 2020 at 08:18):

gares pushed 13 commits to branch section-discharge-fight.

view this post on Zulip HB Github Bot (Nov 03 2020 at 08:18):

gares updated PR #119 [hack] section discharge unused from section-discharge-fight to master.

view this post on Zulip HB Github Bot (Nov 03 2020 at 13:58):

CohenCyril submitted PR Review for #119 [hack] section discharge unused.

view this post on Zulip HB Github Bot (Nov 03 2020 at 14:07):

gares merged PR #119 [hack] section discharge unused.

view this post on Zulip HB Github Bot (Nov 03 2020 at 14:07):

gares pushed 14 commits to branch master.

view this post on Zulip HB Github Bot (Nov 03 2020 at 14:07):

gares closed Issue #116 HB.instance without Definition should take head symbol rather than fully applied term:

E.g.

Definition stuff  T  : mixin (f T) :=  ...
HB.instance f stuff.

instead of

Section stuff.
Variable T.
Definition stuff  : mixin (f T) :=  ...
HB.instance (f T) stuff.
End stuff.

view this post on Zulip HB Github Bot (Nov 03 2020 at 14:07):

gares closed Issue #113 HB interacts badly with "Set Implicit Arguments"

As of now we assume that the constant added by coq.env.add-const have explicit arguments, we should not assume such a thing because it is not true with option Set Implicit Arguments

view this post on Zulip HB Github Bot (Nov 03 2020 at 14:07):

gares deleted the branch section-discharge-fight.

view this post on Zulip HB Github Bot (Nov 03 2020 at 17:44):

gares pushed 1 commit to branch univ-poly.

view this post on Zulip HB Github Bot (Nov 03 2020 at 17:45):

gares opened PR #122 [wip] universe polymorphism from univ-poly to master:

Depends on LPCIC/coq-elpi#190

view this post on Zulip HB Github Bot (Nov 05 2020 at 16:05):

gares pushed 3 commits to branch univ-poly.

view this post on Zulip HB Github Bot (Nov 05 2020 at 16:05):

gares updated PR #122 [wip] universe polymorphism from univ-poly to master:

Depends on LPCIC/coq-elpi#190

view this post on Zulip HB Github Bot (Nov 06 2020 at 09:43):

gares pushed 1 commit to branch cleanup.

view this post on Zulip HB Github Bot (Nov 06 2020 at 09:45):

gares opened PR #123 cleanup structure and sub-class from cleanup to master:

This is an extract from the branch about universe polymorphism.

view this post on Zulip HB Github Bot (Nov 24 2020 at 08:36):

gares opened Issue #124 Please create a tag for the upcoming release of Coq 8.13:

The Coq team is planning to release Coq 8.13-beta1 on December 7, 2020
and Coq 8.13.0 on January 7, 2020.

Your project is currently scheduled for being bundled in the Windows installer.

We are currently testing commit 6089de41147dc4909e8c452eb4b8a10885b62cf2
on branch https://github.com/math-comp/hierarchy-builder/tree/coq-master
but we would like to ship a released version instead (a tag in git's slang).

Could you please tag that commit, or communicate us any other tag
that works with the Coq branch v8.13 at the latest 15 days before the
date of the final release?

Thanks!
CC: https://github.com/coq/coq/issues/12334

view this post on Zulip HB Github Bot (Nov 24 2020 at 13:24):

gares pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Nov 26 2020 at 08:56):

gares pushed 1 commit to branch bump-elpi.

view this post on Zulip HB Github Bot (Nov 26 2020 at 08:57):

gares opened PR #125 Elpi 1.12 + Coq-Elpi 1.7.0 from bump-elpi to master:

Waiting for https://github.com/coq/opam-coq-archive/pull/1480

view this post on Zulip HB Github Bot (Nov 26 2020 at 08:58):

gares pushed 1 commit to branch coq-master+coq-elpi-1.7.0+elpi-1.12.

view this post on Zulip HB Github Bot (Nov 26 2020 at 08:59):

gares opened PR #126 Coq master+coq elpi 1.7.0+elpi 1.12 from coq-master+coq-elpi-1.7.0+elpi-1.12 to coq-master:

overlay for Coq

view this post on Zulip HB Github Bot (Nov 26 2020 at 11:00):

gares merged PR #126 Coq master+coq elpi 1.7.0+elpi 1.12.

view this post on Zulip HB Github Bot (Nov 26 2020 at 11:00):

gares pushed 43 commits to branch coq-master. Commits by gares (39) and CohenCyril (4).

view this post on Zulip HB Github Bot (Nov 26 2020 at 11:00):

gares deleted the branch coq-master+coq-elpi-1.7.0+elpi-1.12.

view this post on Zulip HB Github Bot (Dec 10 2020 at 14:14):

gares pushed 1 commit to branch bump-elpi.

view this post on Zulip HB Github Bot (Dec 10 2020 at 14:14):

gares updated PR #125 Elpi 1.12 + Coq-Elpi 1.7.0 from bump-elpi to master:

Waiting for https://github.com/coq/opam-coq-archive/pull/1480

view this post on Zulip HB Github Bot (Dec 14 2020 at 13:29):

CohenCyril opened Issue #127 Using indexed is too fragile:

We should replace by another kind of meta information.

view this post on Zulip HB Github Bot (Dec 15 2020 at 15:32):

gares edited PR #125 Elpi 1.12 + Coq-Elpi 1.8.0 from bump-elpi to master:

Waiting for https://github.com/coq/opam-coq-archive/pull/1480

view this post on Zulip HB Github Bot (Dec 15 2020 at 15:34):

gares milestoned Issue #127 Using indexed is too fragile:

We should replace by another kind of meta information.

view this post on Zulip HB Github Bot (Dec 15 2020 at 15:45):

gares pushed 1 commit to branch bump-elpi.

view this post on Zulip HB Github Bot (Dec 15 2020 at 15:45):

gares updated PR #125 Elpi 1.12 + Coq-Elpi 1.8.0 from bump-elpi to master:

Waiting for https://github.com/coq/opam-coq-archive/pull/1480

view this post on Zulip HB Github Bot (Dec 15 2020 at 15:45):

gares merged PR #125 Elpi 1.12 + Coq-Elpi 1.8.0.

view this post on Zulip HB Github Bot (Dec 15 2020 at 15:45):

gares pushed 4 commits to branch master.

view this post on Zulip HB Github Bot (Dec 15 2020 at 15:45):

gares deleted the branch bump-elpi.

view this post on Zulip HB Github Bot (Dec 15 2020 at 15:48):

gares pushed 1 commit to branch cleanup.

view this post on Zulip HB Github Bot (Dec 15 2020 at 15:48):

gares updated PR #123 cleanup structure and sub-class from cleanup to master:

This is an extract from the branch about universe polymorphism.

view this post on Zulip HB Github Bot (Dec 15 2020 at 15:50):

CohenCyril pushed 1 commit to branch nix-elpi-1.8.

view this post on Zulip HB Github Bot (Dec 15 2020 at 15:50):

CohenCyril opened PR #128 Compile with coq 8.12 & coq elpi 1.8 from nix-elpi-1.8 to master.

view this post on Zulip HB Github Bot (Dec 15 2020 at 15:51):

CohenCyril pushed 1 commit to branch nix-elpi-1.8.

view this post on Zulip HB Github Bot (Dec 15 2020 at 15:52):

CohenCyril updated PR #128 Compile with coq 8.12 & coq elpi 1.8 from nix-elpi-1.8 to master.

view this post on Zulip HB Github Bot (Dec 15 2020 at 15:55):

CohenCyril pushed 1 commit to branch nix-elpi-1.8.

view this post on Zulip HB Github Bot (Dec 15 2020 at 15:55):

CohenCyril updated PR #128 Compile with coq 8.12 & coq elpi 1.8 from nix-elpi-1.8 to master.

view this post on Zulip HB Github Bot (Dec 15 2020 at 16:04):

CohenCyril pushed 1 commit to branch nix-elpi-1.8.

view this post on Zulip HB Github Bot (Dec 15 2020 at 16:04):

CohenCyril updated PR #128 Compile with coq 8.12 & coq elpi 1.8 from nix-elpi-1.8 to master.

view this post on Zulip HB Github Bot (Dec 15 2020 at 16:12):

CohenCyril pushed 1 commit to branch nix-elpi-1.8.

view this post on Zulip HB Github Bot (Dec 15 2020 at 16:12):

CohenCyril updated PR #128 Compile with coq 8.12 & coq elpi 1.8 from nix-elpi-1.8 to master.

view this post on Zulip HB Github Bot (Dec 15 2020 at 16:25):

CohenCyril merged PR #128 Compile with coq 8.12 & coq elpi 1.8.

view this post on Zulip HB Github Bot (Dec 15 2020 at 16:25):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Dec 15 2020 at 16:25):

CohenCyril deleted the branch nix-elpi-1.8.

view this post on Zulip HB Github Bot (Dec 15 2020 at 16:26):

gares merged PR #123 cleanup structure and sub-class.

view this post on Zulip HB Github Bot (Dec 15 2020 at 16:26):

gares pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Dec 15 2020 at 16:26):

gares deleted the branch cleanup.

view this post on Zulip HB Github Bot (Dec 16 2020 at 10:28):

gares pushed 1 commit to branch release-1.0.0.

view this post on Zulip HB Github Bot (Dec 16 2020 at 10:29):

gares opened PR #129 Close changelog for 1.0.0 from release-1.0.0 to master:

speak now or ...

view this post on Zulip HB Github Bot (Dec 16 2020 at 10:30):

gares milestoned Issue #27 HB.structure should not declare the class projection as canonical (assigned to gares):

We should either let this projection be anonymous and redeclare it by pattern matching later, or make Coq not register it when 8.11 is out.

https://github.com/math-comp/hierarchy-builder/blob/e118e77defa75c5cff9115eae91493a4997fb536/hb.elpi#L711

view this post on Zulip HB Github Bot (Dec 16 2020 at 10:30):

gares demilestoned Issue #27 HB.structure should not declare the class projection as canonical (assigned to gares):

We should either let this projection be anonymous and redeclare it by pattern matching later, or make Coq not register it when 8.11 is out.

https://github.com/math-comp/hierarchy-builder/blob/e118e77defa75c5cff9115eae91493a4997fb536/hb.elpi#L711

view this post on Zulip HB Github Bot (Dec 16 2020 at 10:30):

gares demilestoned Issue #36 HB.instance should no rely on std.findall order:

do not rely on std.findall order

view this post on Zulip HB Github Bot (Dec 16 2020 at 10:30):

gares milestoned Issue #36 HB.instance should no rely on std.findall order:

do not rely on std.findall order

view this post on Zulip HB Github Bot (Dec 16 2020 at 10:30):

gares demilestoned Issue #49 HB.instance should check for duplicate mixins (assigned to CohenCyril):

if the same mixin can be built in two different ways, both from the factories provided or from the existing instances, they must be convertible.

view this post on Zulip HB Github Bot (Dec 16 2020 at 10:30):

gares milestoned Issue #49 HB.instance should check for duplicate mixins (assigned to CohenCyril):

if the same mixin can be built in two different ways, both from the factories provided or from the existing instances, they must be convertible.

view this post on Zulip HB Github Bot (Dec 16 2020 at 10:30):

gares demilestoned Issue #88 in Coq 8.12 support #[local] HB.instance:

In 8.12 you can write #[local] Canonical foo

view this post on Zulip HB Github Bot (Dec 16 2020 at 10:30):

gares milestoned Issue #88 in Coq 8.12 support #[local] HB.instance:

In 8.12 you can write #[local] Canonical foo

view this post on Zulip HB Github Bot (Dec 16 2020 at 10:30):

gares demilestoned Issue #127 Using indexed is too fragile:

We should replace by another kind of meta information.

view this post on Zulip HB Github Bot (Dec 16 2020 at 10:30):

gares milestoned Issue #127 Using indexed is too fragile:

We should replace by another kind of meta information.

view this post on Zulip HB Github Bot (Dec 16 2020 at 10:38):

gares edited PR #129 Close changelog for 1.0.0 from release-1.0.0 to master:

speak now or ...

Fix #124

view this post on Zulip HB Github Bot (Dec 16 2020 at 14:10):

gares closed Issue #124 Please create a tag for the upcoming release of Coq 8.13:

The Coq team is planning to release Coq 8.13-beta1 on December 7, 2020
and Coq 8.13.0 on January 7, 2020.

Your project is currently scheduled for being bundled in the Windows installer.

We are currently testing commit 6089de41147dc4909e8c452eb4b8a10885b62cf2
on branch https://github.com/math-comp/hierarchy-builder/tree/coq-master
but we would like to ship a released version instead (a tag in git's slang).

Could you please tag that commit, or communicate us any other tag
that works with the Coq branch v8.13 at the latest 15 days before the
date of the final release?

Thanks!
CC: https://github.com/coq/coq/issues/12334

view this post on Zulip HB Github Bot (Dec 16 2020 at 14:10):

gares merged PR #129 Close changelog for 1.0.0.

view this post on Zulip HB Github Bot (Dec 16 2020 at 14:10):

gares pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Dec 16 2020 at 14:10):

gares deleted the branch release-1.0.0.

view this post on Zulip HB Github Bot (Dec 16 2020 at 14:13):

gares created release Hierarchy Builder 1.0.0 for tag v1.0.0.

view this post on Zulip HB Github Bot (Dec 16 2020 at 14:13):

gares released release Hierarchy Builder 1.0.0 for tag v1.0.0.

view this post on Zulip HB Github Bot (Dec 16 2020 at 14:13):

gares published release Hierarchy Builder 1.0.0 for tag v1.0.0.

view this post on Zulip HB Github Bot (Dec 16 2020 at 14:13):

gares pushed tag v1.0.0.

view this post on Zulip HB Github Bot (Dec 30 2020 at 18:49):

MSoegtropIMC opened Issue #130 Example files don't run without changes with opam installed HB:

If hierachy builder is installed via opam, the examples are

This because they use require statements like From HB.demo2 Require Import classical. which assume that demo2 is installed with HB, but this is not the case. I see a few possible solutions:

1.) Install the examples required as prerequisites including .vo files
2.) Remove the From HB.demo2 so that files can be compiled locally one by one and run (e.g. in CoqIDE with compile buffer)
3.) Install the examples with a _CoqProject file which sets proper -Q options, so that this does work

view this post on Zulip Enrico Tassi (Dec 30 2020 at 22:04):

I guess I like 3, I'll see what I can do next week

view this post on Zulip HB Github Bot (Jan 12 2021 at 11:55):

gares pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Jan 29 2021 at 17:43):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Jan 29 2021 at 17:46):

gares opened PR #131 HB prints its effect in term of vernac commands from logging-vernac to master:

Based on elpi#master (bug in open_append) and coq-elpi#pp
This is still a huge hack, see readme2.v for something intelligible.

Notes:

view this post on Zulip HB Github Bot (Feb 05 2021 at 20:15):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 05 2021 at 20:15):

gares updated PR #131 HB prints its effect in term of vernac commands from logging-vernac to master:

Based on elpi#master (bug in open_append) and coq-elpi#pp
This is still a huge hack, see readme2.v for something intelligible.

Notes:

view this post on Zulip HB Github Bot (Feb 06 2021 at 17:55):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 06 2021 at 17:55):

gares updated PR #131 HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 06 2021 at 17:59):

gares edited PR #131 HB prints its effect in term of vernac commands from logging-vernac to master:

Based on elpi#master (bug in open_append) and coq-elpi#pp
This is still a huge hack, see readme2.v for something intelligible.

Notes:

Status:

view this post on Zulip HB Github Bot (Feb 06 2021 at 18:26):

gares edited PR #131 HB prints its effect in term of vernac commands from logging-vernac to master:

Based on elpi#master (bug in open_append) and coq-elpi#pp

Notes:

Status:

view this post on Zulip HB Github Bot (Feb 06 2021 at 18:30):

gares edited PR #131 HB prints its effect in term of vernac commands from logging-vernac to master:

Based on elpi#master (bug in open_append) and coq-elpi#pp

Bugs:

Status:

view this post on Zulip HB Github Bot (Feb 06 2021 at 18:31):

gares edited PR #131 HB prints its effect in term of vernac commands from logging-vernac to master:

Based on elpi#master (bug in open_append) and coq-elpi#pp

Bugs:

TODO:

Status:

view this post on Zulip HB Github Bot (Feb 06 2021 at 18:49):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 06 2021 at 18:49):

gares updated PR #131 HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 09 2021 at 17:49):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 09 2021 at 17:49):

gares updated PR #131 HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 09 2021 at 17:55):

gares edited PR #131 HB prints its effect in term of vernac commands from logging-vernac to master:

Based on elpi#master (bug in open_append) and coq-elpi#pp

Bugs:

TODO:

Status:

view this post on Zulip HB Github Bot (Feb 09 2021 at 19:22):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 09 2021 at 19:22):

gares updated PR #131 HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 09 2021 at 19:24):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 09 2021 at 19:24):

gares updated PR #131 HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 10 2021 at 14:10):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 10 2021 at 14:10):

gares updated PR #131 HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 10 2021 at 14:12):

gares edited PR #131 HB prints its effect in term of vernac commands from logging-vernac to master:

Based on elpi#master (bug in open_append) and coq-elpi#pp

Bugs:

TODO:

Status:

view this post on Zulip HB Github Bot (Feb 10 2021 at 14:14):

gares edited PR #131 HB prints its effect in term of vernac commands from logging-vernac to master:

Based on elpi#master (bug in open_append) and coq-elpi#pp

Bugs:

TODO:

Status:

view this post on Zulip HB Github Bot (Feb 10 2021 at 14:14):

gares edited PR #131 HB prints its effect in term of vernac commands from logging-vernac to master:

Based on elpi#master (bug in open_append) and coq-elpi#pp

Bugs:

TODO:

Status:

view this post on Zulip HB Github Bot (Feb 10 2021 at 14:15):

gares edited PR #131 HB prints its effect in term of vernac commands from logging-vernac to master:

Based on elpi#master (bug in open_append) and coq-elpi#pp

Bugs:

TODO:

Status:

view this post on Zulip HB Github Bot (Feb 10 2021 at 14:15):

gares edited PR #131 HB prints its effect in term of vernac commands from logging-vernac to master:

Based on elpi#master (bug in open_append) and coq-elpi#pp

Bugs:

TODO:

Status:

view this post on Zulip HB Github Bot (Feb 10 2021 at 17:56):

CohenCyril pushed 1 commit to branch cat.

view this post on Zulip HB Github Bot (Feb 10 2021 at 18:01):

CohenCyril deleted the branch cat.

view this post on Zulip HB Github Bot (Feb 11 2021 at 09:12):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 11 2021 at 09:12):

gares updated PR #131 HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 11 2021 at 09:12):

gares edited PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 11 2021 at 09:13):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 11 2021 at 09:13):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 11 2021 at 09:14):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 11 2021 at 09:14):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 11 2021 at 09:48):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 11 2021 at 09:48):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 11 2021 at 10:19):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 11 2021 at 10:19):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 11 2021 at 10:29):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 11 2021 at 10:29):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 11 2021 at 10:42):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 11 2021 at 10:42):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 11 2021 at 10:54):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 11 2021 at 10:54):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 11 2021 at 11:36):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 11 2021 at 11:36):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 11 2021 at 11:43):

gares edited PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master:

Require coq-elpi 1.9.0 (Coq 8.13)

Todo:

Status:

view this post on Zulip HB Github Bot (Feb 11 2021 at 11:46):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 11 2021 at 11:46):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 11 2021 at 11:47):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 11 2021 at 11:47):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 11 2021 at 13:13):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 11 2021 at 13:13):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 11 2021 at 14:09):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 11 2021 at 14:09):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 11 2021 at 16:05):

gares has marked PR #131 as ready for review.

view this post on Zulip HB Github Bot (Feb 12 2021 at 09:05):

gares opened Issue #132 Remove arguments that are there just to force discharging:

Blocked by https://github.com/LPCIC/coq-elpi/issues/210

view this post on Zulip HB Github Bot (Feb 12 2021 at 09:40):

CohenCyril opened Issue #133 HB commands telescope inferrence is dumb:

When using HB commands requiring a telescope.
E.g.

HB.builders Context (V : zmodType) .... of stuff V

where stuff requires a zmodType, should make the explicit typing of v optional.

view this post on Zulip HB Github Bot (Feb 12 2021 at 11:03):

CohenCyril opened Issue #134 HB.structure does not always insert coercions.

Cf mathcomp port subLmodule structure definition.

view this post on Zulip HB Github Bot (Feb 12 2021 at 16:50):

gares pushed 1 commit to branch fix-elab-params.

view this post on Zulip HB Github Bot (Feb 12 2021 at 16:50):

gares opened PR #135 fix elaboration of parameters in HB.structure from fix-elab-params to master:

Fix #134

view this post on Zulip HB Github Bot (Feb 12 2021 at 16:50):

gares edited PR #135 fix elaboration of parameters in HB.structure from fix-elab-params to master:

We were bluntly ignoring the parameters of the definition.

Fix #134

view this post on Zulip HB Github Bot (Feb 12 2021 at 17:16):

gares submitted PR Review for #135 fix elaboration of parameters in HB.structure.

view this post on Zulip HB Github Bot (Feb 12 2021 at 17:16):

gares created PR Review Comment on #135 fix elaboration of parameters in HB.structure:

elaborate-params-skeleton.aux _ _ _ _ :- coq.error "You cannot give a type to this definition".

view this post on Zulip HB Github Bot (Feb 12 2021 at 17:16):

gares pushed 1 commit to branch fix-elab-params.

view this post on Zulip HB Github Bot (Feb 12 2021 at 17:16):

gares updated PR #135 fix elaboration of parameters in HB.structure from fix-elab-params to master.

view this post on Zulip HB Github Bot (Feb 12 2021 at 17:53):

gares pushed 1 commit to branch smart-elab-context.

view this post on Zulip HB Github Bot (Feb 12 2021 at 17:54):

gares opened PR #136 Smart elab context from smart-elab-context to master:

HB.factory Record pred_subZmodule V (S : {pred V})
    (subS : zmodPred S)
    (kS : keyed_pred subS)
    (U : indexed Type) of subChoice V S U := {}.

HB.builders Context V S subS kS U of pred_subZmodule V S subS kS U.

this now works, but I guess we could do the same for factory and mixin

view this post on Zulip HB Github Bot (Feb 12 2021 at 18:41):

gares edited PR #136 Smart elab context from smart-elab-context to master:

HB.factory Record pred_subZmodule V (S : {pred V})
    (subS : zmodPred S)
    (kS : keyed_pred subS)
    (U : indexed Type) of subChoice V S U := {}.

HB.builders Context V S subS kS U of pred_subZmodule V S subS kS U.

this now works, but I guess we could do the same for factory and mixin

Fix #133

view this post on Zulip HB Github Bot (Feb 12 2021 at 18:41):

gares edited PR #136 Smart elab context from smart-elab-context to master:

HB.factory Record pred_subZmodule V (S : {pred V})
    (subS : zmodPred S)
    (kS : keyed_pred subS)
    (U : indexed Type) of subChoice V S U := {}.

HB.builders Context V S subS kS U of pred_subZmodule V S subS kS U.

this now works, but I guess we could do the same for factory and mixin

Fix #133 (piled on #136 to ease testing)

view this post on Zulip HB Github Bot (Feb 12 2021 at 18:41):

gares edited PR #136 Smart elab context from smart-elab-context to master:

HB.factory Record pred_subZmodule V (S : {pred V})
    (subS : zmodPred S)
    (kS : keyed_pred subS)
    (U : indexed Type) of subChoice V S U := {}.

HB.builders Context V S subS kS U of pred_subZmodule V S subS kS U.

this now works, but I guess we could do the same for factory and mixin

Fix #133 (piled on #135 to ease testing)

view this post on Zulip HB Github Bot (Feb 12 2021 at 19:06):

gares pushed 1 commit to branch rm-hack-discharge.

view this post on Zulip HB Github Bot (Feb 12 2021 at 19:07):

gares opened PR #137 Removed hack for discharging on 8.13 from rm-hack-discharge to master:

It is still broken and I don't why

Fix #132

view this post on Zulip HB Github Bot (Feb 12 2021 at 19:07):

gares edited PR #137 Removed hack for discharging on 8.13 from rm-hack-discharge to master:

It is still broken and I don't get why

Fix #132

view this post on Zulip HB Github Bot (Feb 13 2021 at 16:24):

gares pushed 4 commits to branch fix-elab-params.

view this post on Zulip HB Github Bot (Feb 13 2021 at 16:24):

gares updated PR #135 fix elaboration of parameters in HB.structure from fix-elab-params to master.

view this post on Zulip HB Github Bot (Feb 13 2021 at 16:24):

gares edited PR #135 fix elaboration of parameters in HB.structure from fix-elab-params to master:

We were bluntly ignoring the parameters of the definition.

Fix #134 #133

view this post on Zulip HB Github Bot (Feb 13 2021 at 16:25):

gares edited PR #135 fix elaboration of parameters in HB.structure from fix-elab-params to master:

We were bluntly ignoring the parameters of the definition.

Fix #134
Fix #133

view this post on Zulip HB Github Bot (Feb 13 2021 at 16:25):

gares closed without merge PR #136 Smart elab context.

view this post on Zulip HB Github Bot (Feb 13 2021 at 16:38):

gares edited PR #135 Elaboration of parameters in HB.structure and HB.builders from fix-elab-params to master.

view this post on Zulip HB Github Bot (Feb 13 2021 at 16:43):

gares edited PR #135 Elaboration of parameters in HB.structure and HB.builders from fix-elab-params to master:

We now run type inference but we first turn all id_phant into _. The problem is that if you don't do that the term does not type check, e.g. the factory requires are not postulated (yet). Similarly in structures, before we were ignoring (no type inference for the parameters) parameters and then we were postulating all requires.

IMO this PR makes things a bit more predictable (and similar to the usual way Coq works), but this is a sharp weapon since inference goes left to right, so you should put the most demanding (on parameters) factory piece first in a structure.

Fix #134
Fix #133

view this post on Zulip HB Github Bot (Feb 13 2021 at 16:45):

gares edited PR #135 Elaboration of parameters in HB.structure and HB.builders from fix-elab-params to master:

We now run type inference but we first turn all id_phant into _. The problem is that if you don't do that the term does not type check, e.g. the factory requires are not postulated (yet). Similarly in structures, before we were ignoring (no type inference for the parameters) parameters and then we were postulating all requires.

IMO this PR makes things a bit more predictable (and similar to the usual way Coq works), but this is a sharp weapon since inference goes left to right, so you should put the most demanding factory (on parameters) first (in a structure declaration).

There is also another subtle problem with indexed that stays there in some terms and type inference can put it in the type of a parameter breaking things (see the commit in the test suite).

Fix #134
Fix #133

view this post on Zulip HB Github Bot (Feb 13 2021 at 16:45):

gares requested CohenCyril for a review on PR #135 Elaboration of parameters in HB.structure and HB.builders.

view this post on Zulip HB Github Bot (Feb 13 2021 at 17:10):

gares pushed 2 commits to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 13 2021 at 17:10):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 13 2021 at 18:51):

CohenCyril submitted PR Review for #135 Elaboration of parameters in HB.structure and HB.builders.

view this post on Zulip HB Github Bot (Feb 13 2021 at 18:51):

CohenCyril created PR Review Comment on #135 Elaboration of parameters in HB.structure and HB.builders:

Amazing!

view this post on Zulip HB Github Bot (Feb 13 2021 at 18:55):

CohenCyril submitted PR Review for #135 Elaboration of parameters in HB.structure and HB.builders.

view this post on Zulip HB Github Bot (Feb 13 2021 at 20:32):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 13 2021 at 20:32):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 14 2021 at 18:22):

CohenCyril pushed 1 commit to branch fixfactoryfields.

view this post on Zulip HB Github Bot (Feb 14 2021 at 18:23):

CohenCyril opened PR #138 Bugfix: forgotten parameters from fixfactoryfields to master:

view this post on Zulip HB Github Bot (Feb 14 2021 at 18:32):

gares submitted PR Review for #138 Bugfix: forgotten parameters.

view this post on Zulip HB Github Bot (Feb 14 2021 at 18:44):

CohenCyril closed Issue #134 HB.structure does not always insert coercions.

Cf mathcomp port subLmodule structure definition.

view this post on Zulip HB Github Bot (Feb 14 2021 at 18:44):

CohenCyril closed Issue #133 HB commands telescope inferrence is dumb:

When using HB commands requiring a telescope.
E.g.

HB.builders Context (V : zmodType) .... of stuff V

where stuff requires a zmodType, should make the explicit typing of v optional.

view this post on Zulip HB Github Bot (Feb 14 2021 at 18:44):

CohenCyril merged PR #135 Elaboration of parameters in HB.structure and HB.builders.

view this post on Zulip HB Github Bot (Feb 14 2021 at 18:44):

CohenCyril pushed 5 commits to branch master. Commits by gares (4) and CohenCyril (1).

view this post on Zulip HB Github Bot (Feb 14 2021 at 18:48):

CohenCyril pushed 1 commit to branch fixfactoryfields.

view this post on Zulip HB Github Bot (Feb 14 2021 at 18:48):

CohenCyril updated PR #138 Bugfix: forgotten parameters from fixfactoryfields to master.

view this post on Zulip HB Github Bot (Feb 14 2021 at 19:04):

CohenCyril merged PR #138 Bugfix: forgotten parameters.

view this post on Zulip HB Github Bot (Feb 14 2021 at 19:04):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Feb 14 2021 at 19:04):

CohenCyril deleted the branch fixfactoryfields.

view this post on Zulip HB Github Bot (Feb 14 2021 at 21:52):

gares deleted the branch fix-elab-params.

view this post on Zulip HB Github Bot (Feb 15 2021 at 08:37):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 15 2021 at 08:37):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 09:55):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 15 2021 at 09:55):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 10:00):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 15 2021 at 10:00):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 10:09):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 15 2021 at 10:09):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 10:46):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 15 2021 at 10:46):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 10:49):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 15 2021 at 10:49):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 11:08):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 15 2021 at 11:08):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 12:06):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 15 2021 at 12:06):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 12:37):

gares opened Issue #139 #[index="R"]

view this post on Zulip HB Github Bot (Feb 15 2021 at 12:38):

gares labeled Issue #139 #[index="R"]

view this post on Zulip HB Github Bot (Feb 15 2021 at 12:40):

gares opened Issue #140 #[infer(R="Type")]

view this post on Zulip HB Github Bot (Feb 15 2021 at 12:40):

gares labeled Issue #140 #[infer(R="Type")]

view this post on Zulip HB Github Bot (Feb 15 2021 at 12:45):

gares edited Issue #140 #[infer(var = "R", from ="Type")]

view this post on Zulip HB Github Bot (Feb 15 2021 at 13:41):

gares opened Issue #141 redesign factory-alias + builders:

Avoid

HB.factory Definition alias R1 := real (proj R1).
HB.builders R1 of alias R1.
  HB.instance Definition : more := more.Build.
..
HB.instance Definition _ := real.Build ...
HB.instance Definition _ := alias.Build ...

and rather have

HB.builders R1 of real (proj R1).
...
HB.instance Definition _ R1 : real (proj R1) * more R1 := real.Build ...

view this post on Zulip HB Github Bot (Feb 15 2021 at 13:41):

gares edited Issue #141 redesign factory-alias + builders:

Avoid (where R1 is richer than R)

HB.factory Definition alias R1 := real (proj R1).
HB.builders R1 of alias R1.
  HB.instance Definition : more := more.Build.
..
HB.instance Definition _ := real.Build ...
HB.instance Definition _ := alias.Build ...

and rather have

HB.builders R1 of real (proj R1).
...
HB.instance Definition _ R1 : real (proj R1) * more R1 := real.Build ...

view this post on Zulip HB Github Bot (Feb 15 2021 at 13:41):

gares edited Issue #141 redesign factory-alias + builders:

Avoid (where R1 is richer than R)

HB.factory Definition alias R1 := real (proj R1).
HB.builders R1 of alias R1.
  HB.instance Definition : more := more.Build.
..
HB.instance Definition _ R := real.Build ...
HB.instance Definition _ R1 := alias.Build ...

and rather have

HB.builders R1 of real (proj R1).
...
HB.instance Definition _ R1 : real (proj R1) * more R1 := real.Build ...

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:18):

CohenCyril pushed 1 commit to branch new_nix.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:20):

CohenCyril pushed 1 commit to branch new_nix.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:21):

CohenCyril opened PR #142 Bugfix: forgotten parameters from new_nix to master:

Conflicts:

hb.elpi

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:21):

CohenCyril edited PR #142 Bugfix: forgotten parameters from new_nix to master:

New nix config

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:23):

CohenCyril pushed 1 commit to branch new_nix.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:23):

CohenCyril updated PR #142 Bugfix: forgotten parameters from new_nix to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:24):

CohenCyril edited PR #142 New nix config from new_nix to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:27):

CohenCyril pushed 1 commit to branch new_nix.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:27):

CohenCyril updated PR #142 New nix config from new_nix to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:29):

gares pushed 1 commit to branch rm-hack-discharge.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:29):

gares updated PR #137 Removed hack for discharging on 8.13 from rm-hack-discharge to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:29):

gares edited PR #137 Removed hack for discharging from rm-hack-discharge to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:30):

gares pushed 1 commit to branch rm-hack-discharge.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:30):

gares updated PR #137 Removed hack for discharging from rm-hack-discharge to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:31):

gares requested CohenCyril for a review on PR #137 Removed hack for discharging.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:32):

gares edited PR #137 Removed hack for discharging from rm-hack-discharge to master:

Fix #132

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:33):

gares submitted PR Review for #142 New nix config.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:33):

gares created PR Review Comment on #142 New nix config:

Did you forget to commit meta.yml?

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:34):

CohenCyril merged PR #142 New nix config.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:34):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:35):

gares submitted PR Review for #142 New nix config.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:35):

gares created PR Review Comment on #142 New nix config:

Yes, because =, :=, and <- would be too standard for (optional?) assignment ;-)
Don't tell me Larry Wall is behind nix

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:35):

CohenCyril submitted PR Review for #142 New nix config.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:35):

CohenCyril created PR Review Comment on #142 New nix config:

No...

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:37):

CohenCyril pushed 1 commit to branch nocomment.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:38):

CohenCyril submitted PR Review for #142 New nix config.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:38):

CohenCyril created PR Review Comment on #142 New nix config:

I really don't like some parts of the syntax, the arguments and abstraction syntax are part of it...
(seriously x: y !)

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:39):

CohenCyril opened PR #143 removing comment from nocomment to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:42):

gares pushed 1 commit to branch rm-hack-discharge.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:42):

gares updated PR #137 Removed hack for discharging from rm-hack-discharge to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:43):

CohenCyril pushed 1 commit to branch withNES.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:43):

CohenCyril opened PR #144 NES in HB from withNES to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:44):

gares pushed 2 commits to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:44):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:45):

gares edited PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master:

Require coq-elpi 1.9.0 (Coq 8.13)

Todo:

Status:

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:49):

gares merged PR #143 removing comment.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:49):

gares pushed 2 commits to branch master. Commits by CohenCyril (1) and gares (1).

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:49):

gares deleted the branch nocomment.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:51):

gares pushed 1 commit to branch rm-hack-discharge.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:51):

gares updated PR #137 Removed hack for discharging from rm-hack-discharge to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:57):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 15 2021 at 17:57):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 18:20):

CohenCyril pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 15 2021 at 18:20):

CohenCyril updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 19:37):

CohenCyril pushed 1 commit to branch withNES.

view this post on Zulip HB Github Bot (Feb 15 2021 at 19:37):

CohenCyril updated PR #144 NES in HB from withNES to master.

view this post on Zulip HB Github Bot (Feb 15 2021 at 20:46):

gares deleted the branch new_nix.

view this post on Zulip HB Github Bot (Feb 16 2021 at 11:13):

gares opened Issue #145 CI job for mathcomp (assigned to CohenCyril):

As soon as ssralg passes we should add a job compiling up to that file

view this post on Zulip HB Github Bot (Feb 16 2021 at 11:13):

gares assigned Issue #145 CI job for mathcomp (assigned to CohenCyril):

As soon as ssralg passes we should add a job compiling up to that file

view this post on Zulip HB Github Bot (Feb 16 2021 at 14:34):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 16 2021 at 14:34):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 16 2021 at 14:36):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 16 2021 at 14:36):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 16 2021 at 14:37):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 16 2021 at 14:37):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 16 2021 at 14:38):

gares assigned Issue #140 #[infer(var = "R", from ="Type")] (assigned to gares).

view this post on Zulip HB Github Bot (Feb 16 2021 at 17:52):

gares pushed 2 commits to branch phant-params.

view this post on Zulip HB Github Bot (Feb 16 2021 at 17:53):

gares opened PR #146 Phant params from phant-params to master:

Fix #140

view this post on Zulip HB Github Bot (Feb 16 2021 at 17:53):

gares edited PR #146 inference of structures on paramters from phant-params to master.

view this post on Zulip HB Github Bot (Feb 16 2021 at 18:01):

gares pushed 1 commit to branch phant-params.

view this post on Zulip HB Github Bot (Feb 16 2021 at 18:01):

gares updated PR #146 inference of structures on paramters from phant-params to master.

view this post on Zulip HB Github Bot (Feb 16 2021 at 18:08):

gares pushed 1 commit to branch phant-params.

view this post on Zulip HB Github Bot (Feb 16 2021 at 18:08):

gares updated PR #146 inference of structures on paramters from phant-params to master.

view this post on Zulip HB Github Bot (Feb 16 2021 at 18:10):

gares requested CohenCyril for a review on PR #146 inference of structures on paramters.

view this post on Zulip HB Github Bot (Feb 16 2021 at 18:11):

gares edited PR #146 inference of structures on paramters from phant-params to master:

The syntax if #[infer(P = "something")] and #[infer(P)] is also supported and works as P = "Type".

Fix #140

view this post on Zulip HB Github Bot (Feb 16 2021 at 18:11):

gares edited PR #146 inference of structures on paramters from phant-params to master:

The syntax is #[infer(P = "something")] and #[infer(P)] is also supported and works as P = "Type".

Fix #140

view this post on Zulip HB Github Bot (Feb 16 2021 at 18:16):

gares pushed 1 commit to branch phant-params.

view this post on Zulip HB Github Bot (Feb 16 2021 at 18:16):

gares updated PR #146 inference of structures on paramters from phant-params to master.

view this post on Zulip HB Github Bot (Feb 16 2021 at 18:24):

gares pushed 1 commit to branch phant-params.

view this post on Zulip HB Github Bot (Feb 16 2021 at 18:24):

gares updated PR #146 inference of structures on paramters from phant-params to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 08:00):

gares pushed 3 commits to branch master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 08:00):

gares closed Issue #132 Remove arguments that are there just to force discharging:

Blocked by https://github.com/LPCIC/coq-elpi/issues/210

view this post on Zulip HB Github Bot (Feb 17 2021 at 08:00):

gares merged PR #137 Removed hack for discharging.

view this post on Zulip HB Github Bot (Feb 17 2021 at 08:00):

gares deleted the branch rm-hack-discharge.

view this post on Zulip HB Github Bot (Feb 17 2021 at 08:06):

gares pushed 2 commits to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 17 2021 at 08:06):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 08:15):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 17 2021 at 08:15):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 08:35):

CohenCyril pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 17 2021 at 08:35):

CohenCyril updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 08:50):

CohenCyril pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 17 2021 at 08:50):

CohenCyril updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 09:04):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 17 2021 at 09:04):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

You can pass extra flags to make install here

view this post on Zulip HB Github Bot (Feb 17 2021 at 09:05):

gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 17 2021 at 09:05):

gares created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

with this PR this flag is not needed anymore

view this post on Zulip HB Github Bot (Feb 17 2021 at 09:07):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 17 2021 at 09:07):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

ok great, but I was thinking of a destdir for the binary hb

view this post on Zulip HB Github Bot (Feb 17 2021 at 10:26):

gares submitted PR Review for #146 inference of structures on paramters.

view this post on Zulip HB Github Bot (Feb 17 2021 at 10:26):

gares created PR Review Comment on #146 inference of structures on paramters:

  pi x\ mk-phant-abbrev.term K {mk-app F [_,{{ lib:hb.Phant lp:x }}]} AL K' (AbbrevFx x),

view this post on Zulip HB Github Bot (Feb 17 2021 at 10:26):

gares pushed 1 commit to branch phant-params.

view this post on Zulip HB Github Bot (Feb 17 2021 at 10:26):

gares updated PR #146 inference of structures on paramters from phant-params to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 10:34):

gares pushed 6 commits to branch phant-params.

view this post on Zulip HB Github Bot (Feb 17 2021 at 10:34):

gares updated PR #146 inference of structures on paramters from phant-params to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:24):

CohenCyril pushed 1 commit to branch exports.

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:25):

CohenCyril opened PR #147 Managing Exports from exports to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:27):

gares submitted PR Review for #147 Managing Exports.

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:27):

gares created PR Review Comment on #147 Managing Exports:

(** [HB.export Modname] does the work of [Export Modname] but also schedules [Modname]
   to be exported later on, when [HB.reexport] is called. *)

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:29):

gares created PR Review Comment on #147 Managing Exports:

(** [HB.reexport] Exports all modules that were previously exported via [HB.export].
   It is useful to create one big module with all exports at the end of a file. *)

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:29):

gares submitted PR Review for #147 Managing Exports.

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:31):

gares pushed 1 commit to branch exports.

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:31):

gares updated PR #147 Managing Exports from exports to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:31):

gares pushed 1 commit to branch exports.

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:31):

gares updated PR #147 Managing Exports from exports to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:37):

gares submitted PR Review for #147 Managing Exports.

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:37):

gares created PR Review Comment on #147 Managing Exports:

   to be exported later on, when [HB.reexport] is called.
   Note that the list of modules to be exported is store in the current module,
   hence the recommended way to do is
   <<<
   Module Algebra.
     HB.mixin .... HB.structure ...
     Module MoreExports. ... End MoreExports. HB.export MoreExports.
     ...
     Module Export. HB.reexport. End Exports.
   End Algebra.
   Export Algebra.Exports.
   >>> *)

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:37):

gares pushed 1 commit to branch exports.

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:37):

gares updated PR #147 Managing Exports from exports to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:49):

gares opened Issue #148 #[export] HB.instance:

Elaborates to

Module Exports$rand.
HB.instance ...
End Exports$rand.
HB.export Exports$rand.

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:59):

CohenCyril pushed 1 commit to branch exports.

view this post on Zulip HB Github Bot (Feb 17 2021 at 11:59):

CohenCyril updated PR #147 Managing Exports from exports to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 14:02):

gares submitted PR Review for #147 Managing Exports.

view this post on Zulip HB Github Bot (Feb 17 2021 at 14:02):

gares created PR Review Comment on #147 Managing Exports:

   Note that the list of modules to be exported is stored in the current module,

view this post on Zulip HB Github Bot (Feb 17 2021 at 14:03):

gares pushed 1 commit to branch exports.

view this post on Zulip HB Github Bot (Feb 17 2021 at 14:03):

gares updated PR #147 Managing Exports from exports to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 16:22):

CohenCyril merged PR #147 Managing Exports.

view this post on Zulip HB Github Bot (Feb 17 2021 at 16:22):

CohenCyril pushed 7 commits to branch master. Commits by gares (4) and CohenCyril (3).

view this post on Zulip HB Github Bot (Feb 17 2021 at 16:22):

CohenCyril deleted the branch exports.

view this post on Zulip HB Github Bot (Feb 17 2021 at 16:42):

CohenCyril pushed 1 commit to branch phant-params.

view this post on Zulip HB Github Bot (Feb 17 2021 at 16:42):

CohenCyril updated PR #146 inference of structures on paramters from phant-params to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 17:20):

CohenCyril pushed 7 commits to branch phant-params. Commits by gares (6) and CohenCyril (1).

view this post on Zulip HB Github Bot (Feb 17 2021 at 17:20):

CohenCyril updated PR #146 inference of structures on paramters from phant-params to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 17:25):

gares pushed 1 commit to branch ci-ssralg.

view this post on Zulip HB Github Bot (Feb 17 2021 at 17:26):

gares opened PR #149 ci job to test ssralg from ci-ssralg to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 17:30):

CohenCyril closed Issue #140 #[infer(var = "R", from ="Type")] (assigned to gares).

view this post on Zulip HB Github Bot (Feb 17 2021 at 17:30):

CohenCyril merged PR #146 inference of structures on paramters.

view this post on Zulip HB Github Bot (Feb 17 2021 at 17:30):

CohenCyril pushed 8 commits to branch master. Commits by gares (6) and CohenCyril (2).

view this post on Zulip HB Github Bot (Feb 17 2021 at 17:30):

CohenCyril deleted the branch phant-params.

view this post on Zulip HB Github Bot (Feb 17 2021 at 17:33):

gares pushed 1 commit to branch ci-ssralg.

view this post on Zulip HB Github Bot (Feb 17 2021 at 17:33):

gares updated PR #149 ci job to test ssralg from ci-ssralg to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 17:41):

gares pushed 1 commit to branch ci-ssralg.

view this post on Zulip HB Github Bot (Feb 17 2021 at 17:41):

gares updated PR #149 ci job to test ssralg from ci-ssralg to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 17:58):

gares opened Issue #150 performance problem of instance declaration.

view this post on Zulip HB Github Bot (Feb 17 2021 at 18:01):

CohenCyril pushed 1 commit to branch nixci.

view this post on Zulip HB Github Bot (Feb 17 2021 at 18:01):

CohenCyril opened PR #151 experimenting with nix ci from nixci to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 18:03):

CohenCyril pushed 1 commit to branch nixci.

view this post on Zulip HB Github Bot (Feb 17 2021 at 18:03):

CohenCyril updated PR #151 experimenting with nix ci from nixci to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 18:05):

CohenCyril pushed 1 commit to branch nixci.

view this post on Zulip HB Github Bot (Feb 17 2021 at 18:05):

CohenCyril updated PR #151 experimenting with nix ci from nixci to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 18:09):

CohenCyril pushed 1 commit to branch nixci.

view this post on Zulip HB Github Bot (Feb 17 2021 at 18:09):

CohenCyril updated PR #151 experimenting with nix ci from nixci to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 18:09):

gares edited Issue #150 performance problem of instance declaration:

From the very last instances in ssralg.v

HB: declare has_mul_inverse_to_has_mul_inverse__122
HB: declare canonical mixin instance
«has_mul_inverse_to_has_mul_inverse__122»
1613585046.099228 HB: we try to build a indt «SUB.type»
HB: skipping alreay existing Equality instance on (A1 * A2)%type
HB: skipping alreay existing Choice instance on (A1 * A2)%type
HB: skipping alreay existing Zmodule instance on (A1 * A2)%type
HB: skipping alreay existing Lmodule instance on (A1 * A2)%type
HB: skipping alreay existing Ring instance on (A1 * A2)%type
HB: skipping alreay existing UnitRing instance on (A1 * A2)%type
HB: skipping alreay existing ComRing instance on (A1 * A2)%type
HB: skipping alreay existing ComUnitRing instance on (A1 * A2)%type
1613585046.171108 HB: we try to build a indt «IntegralDomain.type»
1613585046.184017 HB: we try to build a indt «Field.type»
1613585046.199054 HB: we try to build a indt «ClosedField.type»
1613585046.213381 HB: we try to build a indt «DecidableField.type»
HB: skipping alreay existing Lalgebra instance on (A1 * A2)%type
HB: skipping alreay existing Algebra instance on (A1 * A2)%type
1613585046.251127 HB: we try to build a indt «UnitAlgebra.type»
1613585047.896515 HB: we can build a UnitAlgebra on (A1 * A2)%type
1613585047.932029 HB: begin typechecking
{|
  UnitAlgebra.sort := A1 * A2;
  UnitAlgebra.class :=
    {|
      UnitAlgebra.is_Zmodule_mixin :=
        ZmodMixin (A1 * A2)%type (pair_addA (M2:=A2)) (pair_addC (M2:=A2))
          (pair_add0 (M2:=A2)) (pair_addN (M2:=A2));
      UnitAlgebra.is_eqType_mixin := prod_eqMixin A1 A2;
      UnitAlgebra.has_choice_mixin := prod_choiceMixin A1 A2;
      UnitAlgebra.is_Lmodule_of_Zmodule_mixin :=
        LmodMixin (pair_scaleA (V2:=A2)) (pair_scale1 (V2:=A2))
          (pair_scaleDr (V2:=A2)) (pair_scaleDl (V2:=A2));
      UnitAlgebra.is_Ring_of_Zmodule_mixin :=
        RingMixin (A1 * A2)%type (pair_mulA (R2:=A2)) (pair_mul1l (R2:=A2))
          (pair_mul1r (R2:=A2)) (pair_mulDl (R2:=A2)) (pair_mulDr (R2:=A2))
          (pair_one_neq0 A1 A2);
      UnitAlgebra.is_Lalgebra_of_Lmodule_mixin :=
        LalgMixin (pair_scaleAl (A2:=A2));
      UnitAlgebra.is_Algebra_of_Lalgebra_mixin :=
        Algebra.Mixin (pair_scaleAr (A2:=A2));
      UnitAlgebra.has_mul_inverse_mixin := XXX A1 A2
    |}
|}
1613585052.874924 HB: end typechecking
{|
  UnitAlgebra.sort := A1 * A2;
  UnitAlgebra.class :=
    {|
      UnitAlgebra.is_Zmodule_mixin :=
        ZmodMixin (A1 * A2)%type (pair_addA (M2:=A2)) (pair_addC (M2:=A2))
          (pair_add0 (M2:=A2)) (pair_addN (M2:=A2));
      UnitAlgebra.is_eqType_mixin := prod_eqMixin A1 A2;
      UnitAlgebra.has_choice_mixin := prod_choiceMixin A1 A2;
      UnitAlgebra.is_Lmodule_of_Zmodule_mixin :=
        LmodMixin (pair_scaleA (V2:=A2)) (pair_scale1 (V2:=A2))
          (pair_scaleDr (V2:=A2)) (pair_scaleDl (V2:=A2));
      UnitAlgebra.is_Ring_of_Zmodule_mixin :=
        RingMixin (A1 * A2)%type (pair_mulA (R2:=A2)) (pair_mul1l (R2:=A2))
          (pair_mul1r (R2:=A2)) (pair_mulDl (R2:=A2)) (pair_mulDr (R2:=A2))
          (pair_one_neq0 A1 A2);
      UnitAlgebra.is_Lalgebra_of_Lmodule_mixin :=
        LalgMixin (pair_scaleAl (A2:=A2));
      UnitAlgebra.is_Algebra_of_Lalgebra_mixin :=
        Algebra.Mixin (pair_scaleAr (A2:=A2));
      UnitAlgebra.has_mul_inverse_mixin := XXX A1 A2
    |}
|}
1613585056.908798 HB: begin CS decl
1613585056.914190 HB: declare canonical structure instance
prod_is_a_UnitAlgebra
1613585056.923026 HB: we try to build a indt «ComAlgebra.type»
1613585056.944423 HB: we try to build a indt «ComUnitAlgebra.type»
HB: skipping alreay existing Countable instance on (A1 * A2)%type
HB: skipping alreay existing Finite instance on (A1 * A2)%type
1613585056.980981 HB: we try to build a indt «subEquality.type»
1613585056.989645 HB: we try to build a indt «subChoice.type»
1613585056.999233 HB: we try to build a indt «SubZmodule.type»
1613585057.007633 HB: we try to build a indt «SubLmodule.type»
1613585057.016103 HB: we try to build a indt «SubRing.type»
1613585057.024662 HB: we try to build a indt «SubUnitRing.type»
1613585057.033086 HB: we try to build a indt «SubCountable.type»
1613585057.041577 HB: we try to build a indt «subFinite.type»
Finished transaction in 13.601 secs (13.554u,0.043s) (successful)

The type checking step is 5 seconds! the problem is that the term is huge due to implicit arguments. In set printing all

$ wc -cl log
 112640 6717143 log
$ cat log | gzip | wc -cl
    655  132437

For example this term occurs many times

                               (@Lalgebra_to_Lmodule
                                 (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                 (@Algebra_to_Lalgebra
                                    (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                    (@UnitAlgebra_to_Algebra
                                       (ComRing_to_Ring
                                          (ComUnitRing_to_ComRing R)) A1)))

view this post on Zulip HB Github Bot (Feb 17 2021 at 18:22):

CohenCyril pushed 1 commit to branch nixci.

view this post on Zulip HB Github Bot (Feb 17 2021 at 18:22):

CohenCyril updated PR #151 experimenting with nix ci from nixci to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 18:22):

gares edited Issue #150 performance problem of instance declaration:

From the very last instances in ssralg.v

HB: declare has_mul_inverse_to_has_mul_inverse__122
HB: declare canonical mixin instance
«has_mul_inverse_to_has_mul_inverse__122»
1613585046.099228 HB: we try to build a indt «SUB.type»
HB: skipping alreay existing Equality instance on (A1 * A2)%type
HB: skipping alreay existing Choice instance on (A1 * A2)%type
HB: skipping alreay existing Zmodule instance on (A1 * A2)%type
HB: skipping alreay existing Lmodule instance on (A1 * A2)%type
HB: skipping alreay existing Ring instance on (A1 * A2)%type
HB: skipping alreay existing UnitRing instance on (A1 * A2)%type
HB: skipping alreay existing ComRing instance on (A1 * A2)%type
HB: skipping alreay existing ComUnitRing instance on (A1 * A2)%type
1613585046.171108 HB: we try to build a indt «IntegralDomain.type»
1613585046.184017 HB: we try to build a indt «Field.type»
1613585046.199054 HB: we try to build a indt «ClosedField.type»
1613585046.213381 HB: we try to build a indt «DecidableField.type»
HB: skipping alreay existing Lalgebra instance on (A1 * A2)%type
HB: skipping alreay existing Algebra instance on (A1 * A2)%type
1613585046.251127 HB: we try to build a indt «UnitAlgebra.type»
1613585047.896515 HB: we can build a UnitAlgebra on (A1 * A2)%type
1613585047.932029 HB: begin typechecking
{|
  UnitAlgebra.sort := A1 * A2;
  UnitAlgebra.class :=
    {|
      UnitAlgebra.is_Zmodule_mixin :=
        ZmodMixin (A1 * A2)%type (pair_addA (M2:=A2)) (pair_addC (M2:=A2))
          (pair_add0 (M2:=A2)) (pair_addN (M2:=A2));
      UnitAlgebra.is_eqType_mixin := prod_eqMixin A1 A2;
      UnitAlgebra.has_choice_mixin := prod_choiceMixin A1 A2;
      UnitAlgebra.is_Lmodule_of_Zmodule_mixin :=
        LmodMixin (pair_scaleA (V2:=A2)) (pair_scale1 (V2:=A2))
          (pair_scaleDr (V2:=A2)) (pair_scaleDl (V2:=A2));
      UnitAlgebra.is_Ring_of_Zmodule_mixin :=
        RingMixin (A1 * A2)%type (pair_mulA (R2:=A2)) (pair_mul1l (R2:=A2))
          (pair_mul1r (R2:=A2)) (pair_mulDl (R2:=A2)) (pair_mulDr (R2:=A2))
          (pair_one_neq0 A1 A2);
      UnitAlgebra.is_Lalgebra_of_Lmodule_mixin :=
        LalgMixin (pair_scaleAl (A2:=A2));
      UnitAlgebra.is_Algebra_of_Lalgebra_mixin :=
        Algebra.Mixin (pair_scaleAr (A2:=A2));
      UnitAlgebra.has_mul_inverse_mixin := XXX A1 A2
    |}
|}
1613585052.874924 HB: end typechecking
{|
  UnitAlgebra.sort := A1 * A2;
  UnitAlgebra.class :=
    {|
      UnitAlgebra.is_Zmodule_mixin :=
        ZmodMixin (A1 * A2)%type (pair_addA (M2:=A2)) (pair_addC (M2:=A2))
          (pair_add0 (M2:=A2)) (pair_addN (M2:=A2));
      UnitAlgebra.is_eqType_mixin := prod_eqMixin A1 A2;
      UnitAlgebra.has_choice_mixin := prod_choiceMixin A1 A2;
      UnitAlgebra.is_Lmodule_of_Zmodule_mixin :=
        LmodMixin (pair_scaleA (V2:=A2)) (pair_scale1 (V2:=A2))
          (pair_scaleDr (V2:=A2)) (pair_scaleDl (V2:=A2));
      UnitAlgebra.is_Ring_of_Zmodule_mixin :=
        RingMixin (A1 * A2)%type (pair_mulA (R2:=A2)) (pair_mul1l (R2:=A2))
          (pair_mul1r (R2:=A2)) (pair_mulDl (R2:=A2)) (pair_mulDr (R2:=A2))
          (pair_one_neq0 A1 A2);
      UnitAlgebra.is_Lalgebra_of_Lmodule_mixin :=
        LalgMixin (pair_scaleAl (A2:=A2));
      UnitAlgebra.is_Algebra_of_Lalgebra_mixin :=
        Algebra.Mixin (pair_scaleAr (A2:=A2));
      UnitAlgebra.has_mul_inverse_mixin := XXX A1 A2
    |}
|}
1613585056.908798 HB: begin CS decl
1613585056.914190 HB: declare canonical structure instance
prod_is_a_UnitAlgebra
1613585056.923026 HB: we try to build a indt «ComAlgebra.type»
1613585056.944423 HB: we try to build a indt «ComUnitAlgebra.type»
HB: skipping alreay existing Countable instance on (A1 * A2)%type
HB: skipping alreay existing Finite instance on (A1 * A2)%type
1613585056.980981 HB: we try to build a indt «subEquality.type»
1613585056.989645 HB: we try to build a indt «subChoice.type»
1613585056.999233 HB: we try to build a indt «SubZmodule.type»
1613585057.007633 HB: we try to build a indt «SubLmodule.type»
1613585057.016103 HB: we try to build a indt «SubRing.type»
1613585057.024662 HB: we try to build a indt «SubUnitRing.type»
1613585057.033086 HB: we try to build a indt «SubCountable.type»
1613585057.041577 HB: we try to build a indt «subFinite.type»
Finished transaction in 13.601 secs (13.554u,0.043s) (successful)

Deciding if the structure can be built is not super fast, but it is not the main problem

1613585046.251127 HB: we try to build a indt «UnitAlgebra.type»
1613585047.896515 HB: we can build a UnitAlgebra on (A1 * A2)%type

The type checking step is 5 seconds! the problem is that the term is huge due to implicit arguments. In set printing all

$ wc -cl log
 112640 6717143 log
$ cat log | gzip | wc -cl
    655  132437

For example this term occurs many times

                               (@Lalgebra_to_Lmodule
                                 (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                 (@Algebra_to_Lalgebra
                                    (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                    (@UnitAlgebra_to_Algebra
                                       (ComRing_to_Ring
                                          (ComUnitRing_to_ComRing R)) A1)))

A Check .. of that term takes 8s (in that case Coq has to do a little more) so it does not seem that passing the monster to Coq (from elpi) is the main problem here.

So we have to figure out if "flattening" makes the implicit argument /type parameter problem worse.. This is the unitAlgebra Class:

Variant axioms (R : Ring.type) (V : Type) : Type :=
    Class : forall (is_Zmodule_mixin : is_Zmodule.axioms_ V)
              (is_eqType_mixin : is_eqType.axioms_ V)
              (has_choice_mixin : has_choice.axioms_ V)
              (is_Lmodule_of_Zmodule_mixin : is_Lmodule_of_Zmodule.axioms_ R
                                               V is_eqType_mixin
                                               has_choice_mixin
                                               is_Zmodule_mixin)
              (is_Ring_of_Zmodule_mixin : is_Ring_of_Zmodule.axioms_ V
                                            is_eqType_mixin has_choice_mixin
                                            is_Zmodule_mixin)
              (is_Lalgebra_of_Lmodule_mixin : is_Lalgebra_of_Lmodule.axioms_
                                                R V is_eqType_mixin
                                                has_choice_mixin
                                                is_Zmodule_mixin
                                                is_Ring_of_Zmodule_mixin
                                                is_Lmodule_of_Zmodule_mixin)
              (_ : is_Algebra_of_Lalgebra.axioms_ R V is_eqType_mixin
                     has_choice_mixin is_Zmodule_mixin
                     is_Ring_of_Zmodule_mixin is_Lmodule_of_Zmodule_mixin
                     is_Lalgebra_of_Lmodule_mixin)
              (_ : has_mul_inverse.axioms_ V is_Zmodule_mixin is_eqType_mixin
                     has_choice_mixin is_Ring_of_Zmodule_mixin),
            UnitAlgebra.axioms R V

view this post on Zulip HB Github Bot (Feb 17 2021 at 18:24):

gares edited Issue #150 performance problem of instance declaration:

From the very last instances in ssralg.v

HB: declare has_mul_inverse_to_has_mul_inverse__122
HB: declare canonical mixin instance
«has_mul_inverse_to_has_mul_inverse__122»
1613585046.099228 HB: we try to build a indt «SUB.type»
HB: skipping alreay existing Equality instance on (A1 * A2)%type
HB: skipping alreay existing Choice instance on (A1 * A2)%type
HB: skipping alreay existing Zmodule instance on (A1 * A2)%type
HB: skipping alreay existing Lmodule instance on (A1 * A2)%type
HB: skipping alreay existing Ring instance on (A1 * A2)%type
HB: skipping alreay existing UnitRing instance on (A1 * A2)%type
HB: skipping alreay existing ComRing instance on (A1 * A2)%type
HB: skipping alreay existing ComUnitRing instance on (A1 * A2)%type
1613585046.171108 HB: we try to build a indt «IntegralDomain.type»
1613585046.184017 HB: we try to build a indt «Field.type»
1613585046.199054 HB: we try to build a indt «ClosedField.type»
1613585046.213381 HB: we try to build a indt «DecidableField.type»
HB: skipping alreay existing Lalgebra instance on (A1 * A2)%type
HB: skipping alreay existing Algebra instance on (A1 * A2)%type
1613585046.251127 HB: we try to build a indt «UnitAlgebra.type»
1613585047.896515 HB: we can build a UnitAlgebra on (A1 * A2)%type
1613585047.932029 HB: begin typechecking
{|
  UnitAlgebra.sort := A1 * A2;
  UnitAlgebra.class :=
    {|
      UnitAlgebra.is_Zmodule_mixin :=
        ZmodMixin (A1 * A2)%type (pair_addA (M2:=A2)) (pair_addC (M2:=A2))
          (pair_add0 (M2:=A2)) (pair_addN (M2:=A2));
      UnitAlgebra.is_eqType_mixin := prod_eqMixin A1 A2;
      UnitAlgebra.has_choice_mixin := prod_choiceMixin A1 A2;
      UnitAlgebra.is_Lmodule_of_Zmodule_mixin :=
        LmodMixin (pair_scaleA (V2:=A2)) (pair_scale1 (V2:=A2))
          (pair_scaleDr (V2:=A2)) (pair_scaleDl (V2:=A2));
      UnitAlgebra.is_Ring_of_Zmodule_mixin :=
        RingMixin (A1 * A2)%type (pair_mulA (R2:=A2)) (pair_mul1l (R2:=A2))
          (pair_mul1r (R2:=A2)) (pair_mulDl (R2:=A2)) (pair_mulDr (R2:=A2))
          (pair_one_neq0 A1 A2);
      UnitAlgebra.is_Lalgebra_of_Lmodule_mixin :=
        LalgMixin (pair_scaleAl (A2:=A2));
      UnitAlgebra.is_Algebra_of_Lalgebra_mixin :=
        Algebra.Mixin (pair_scaleAr (A2:=A2));
      UnitAlgebra.has_mul_inverse_mixin := XXX A1 A2
    |}
|}
1613585052.874924 HB: end typechecking
{|
  UnitAlgebra.sort := A1 * A2;
  UnitAlgebra.class :=
    {|
      UnitAlgebra.is_Zmodule_mixin :=
        ZmodMixin (A1 * A2)%type (pair_addA (M2:=A2)) (pair_addC (M2:=A2))
          (pair_add0 (M2:=A2)) (pair_addN (M2:=A2));
      UnitAlgebra.is_eqType_mixin := prod_eqMixin A1 A2;
      UnitAlgebra.has_choice_mixin := prod_choiceMixin A1 A2;
      UnitAlgebra.is_Lmodule_of_Zmodule_mixin :=
        LmodMixin (pair_scaleA (V2:=A2)) (pair_scale1 (V2:=A2))
          (pair_scaleDr (V2:=A2)) (pair_scaleDl (V2:=A2));
      UnitAlgebra.is_Ring_of_Zmodule_mixin :=
        RingMixin (A1 * A2)%type (pair_mulA (R2:=A2)) (pair_mul1l (R2:=A2))
          (pair_mul1r (R2:=A2)) (pair_mulDl (R2:=A2)) (pair_mulDr (R2:=A2))
          (pair_one_neq0 A1 A2);
      UnitAlgebra.is_Lalgebra_of_Lmodule_mixin :=
        LalgMixin (pair_scaleAl (A2:=A2));
      UnitAlgebra.is_Algebra_of_Lalgebra_mixin :=
        Algebra.Mixin (pair_scaleAr (A2:=A2));
      UnitAlgebra.has_mul_inverse_mixin := XXX A1 A2
    |}
|}
1613585056.908798 HB: begin CS decl
1613585056.914190 HB: declare canonical structure instance
prod_is_a_UnitAlgebra
1613585056.923026 HB: we try to build a indt «ComAlgebra.type»
1613585056.944423 HB: we try to build a indt «ComUnitAlgebra.type»
HB: skipping alreay existing Countable instance on (A1 * A2)%type
HB: skipping alreay existing Finite instance on (A1 * A2)%type
1613585056.980981 HB: we try to build a indt «subEquality.type»
1613585056.989645 HB: we try to build a indt «subChoice.type»
1613585056.999233 HB: we try to build a indt «SubZmodule.type»
1613585057.007633 HB: we try to build a indt «SubLmodule.type»
1613585057.016103 HB: we try to build a indt «SubRing.type»
1613585057.024662 HB: we try to build a indt «SubUnitRing.type»
1613585057.033086 HB: we try to build a indt «SubCountable.type»
1613585057.041577 HB: we try to build a indt «subFinite.type»
Finished transaction in 13.601 secs (13.554u,0.043s) (successful)

Deciding if the structure can be built is not super fast, but it is not the main problem

1613585046.251127 HB: we try to build a indt «UnitAlgebra.type»
1613585047.896515 HB: we can build a UnitAlgebra on (A1 * A2)%type

The type checking step is 5 seconds! the problem is that the term is huge due to implicit arguments. In set printing all

$ wc -cl log
 112640 6717143 log
$ cat log | gzip | wc -cl
    655  132437

For example this term occurs many times

                               (@Lalgebra_to_Lmodule
                                 (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                 (@Algebra_to_Lalgebra
                                    (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                    (@UnitAlgebra_to_Algebra
                                       (ComRing_to_Ring
                                          (ComUnitRing_to_ComRing R)) A1)))

A Check .. of that term takes 8s (in that case Coq has to do a little more) so it does not seem that passing the monster to Coq (from elpi) is the main problem here. The kernel (just before declaring the CS instance) takes 4s to typecheck, so it is not an inefficiency of the "elaborator" alone.

So we have to figure out if "flattening" makes the implicit argument /type parameter problem worse.. This is the unitAlgebra Class:

Variant axioms (R : Ring.type) (V : Type) : Type :=
    Class : forall (is_Zmodule_mixin : is_Zmodule.axioms_ V)
              (is_eqType_mixin : is_eqType.axioms_ V)
              (has_choice_mixin : has_choice.axioms_ V)
              (is_Lmodule_of_Zmodule_mixin : is_Lmodule_of_Zmodule.axioms_ R
                                               V is_eqType_mixin
                                               has_choice_mixin
                                               is_Zmodule_mixin)
              (is_Ring_of_Zmodule_mixin : is_Ring_of_Zmodule.axioms_ V
                                            is_eqType_mixin has_choice_mixin
                                            is_Zmodule_mixin)
              (is_Lalgebra_of_Lmodule_mixin : is_Lalgebra_of_Lmodule.axioms_
                                                R V is_eqType_mixin
                                                has_choice_mixin
                                                is_Zmodule_mixin
                                                is_Ring_of_Zmodule_mixin
                                                is_Lmodule_of_Zmodule_mixin)
              (_ : is_Algebra_of_Lalgebra.axioms_ R V is_eqType_mixin
                     has_choice_mixin is_Zmodule_mixin
                     is_Ring_of_Zmodule_mixin is_Lmodule_of_Zmodule_mixin
                     is_Lalgebra_of_Lmodule_mixin)
              (_ : has_mul_inverse.axioms_ V is_Zmodule_mixin is_eqType_mixin
                     has_choice_mixin is_Ring_of_Zmodule_mixin),
            UnitAlgebra.axioms R V

view this post on Zulip HB Github Bot (Feb 17 2021 at 18:26):

gares edited Issue #150 performance problem of instance declaration:

From the very last instances in ssralg.v

HB: declare has_mul_inverse_to_has_mul_inverse__122
HB: declare canonical mixin instance
«has_mul_inverse_to_has_mul_inverse__122»
1613585046.099228 HB: we try to build a indt «SUB.type»
HB: skipping alreay existing Equality instance on (A1 * A2)%type
HB: skipping alreay existing Choice instance on (A1 * A2)%type
HB: skipping alreay existing Zmodule instance on (A1 * A2)%type
HB: skipping alreay existing Lmodule instance on (A1 * A2)%type
HB: skipping alreay existing Ring instance on (A1 * A2)%type
HB: skipping alreay existing UnitRing instance on (A1 * A2)%type
HB: skipping alreay existing ComRing instance on (A1 * A2)%type
HB: skipping alreay existing ComUnitRing instance on (A1 * A2)%type
1613585046.171108 HB: we try to build a indt «IntegralDomain.type»
1613585046.184017 HB: we try to build a indt «Field.type»
1613585046.199054 HB: we try to build a indt «ClosedField.type»
1613585046.213381 HB: we try to build a indt «DecidableField.type»
HB: skipping alreay existing Lalgebra instance on (A1 * A2)%type
HB: skipping alreay existing Algebra instance on (A1 * A2)%type
1613585046.251127 HB: we try to build a indt «UnitAlgebra.type»
1613585047.896515 HB: we can build a UnitAlgebra on (A1 * A2)%type
1613585047.932029 HB: begin typechecking
{|
  UnitAlgebra.sort := A1 * A2;
  UnitAlgebra.class :=
    {|
      UnitAlgebra.is_Zmodule_mixin :=
        ZmodMixin (A1 * A2)%type (pair_addA (M2:=A2)) (pair_addC (M2:=A2))
          (pair_add0 (M2:=A2)) (pair_addN (M2:=A2));
      UnitAlgebra.is_eqType_mixin := prod_eqMixin A1 A2;
      UnitAlgebra.has_choice_mixin := prod_choiceMixin A1 A2;
      UnitAlgebra.is_Lmodule_of_Zmodule_mixin :=
        LmodMixin (pair_scaleA (V2:=A2)) (pair_scale1 (V2:=A2))
          (pair_scaleDr (V2:=A2)) (pair_scaleDl (V2:=A2));
      UnitAlgebra.is_Ring_of_Zmodule_mixin :=
        RingMixin (A1 * A2)%type (pair_mulA (R2:=A2)) (pair_mul1l (R2:=A2))
          (pair_mul1r (R2:=A2)) (pair_mulDl (R2:=A2)) (pair_mulDr (R2:=A2))
          (pair_one_neq0 A1 A2);
      UnitAlgebra.is_Lalgebra_of_Lmodule_mixin :=
        LalgMixin (pair_scaleAl (A2:=A2));
      UnitAlgebra.is_Algebra_of_Lalgebra_mixin :=
        Algebra.Mixin (pair_scaleAr (A2:=A2));
      UnitAlgebra.has_mul_inverse_mixin := XXX A1 A2
    |}
|}
1613585052.874924 HB: end typechecking
{|
  UnitAlgebra.sort := A1 * A2;
  UnitAlgebra.class :=
    {|
      UnitAlgebra.is_Zmodule_mixin :=
        ZmodMixin (A1 * A2)%type (pair_addA (M2:=A2)) (pair_addC (M2:=A2))
          (pair_add0 (M2:=A2)) (pair_addN (M2:=A2));
      UnitAlgebra.is_eqType_mixin := prod_eqMixin A1 A2;
      UnitAlgebra.has_choice_mixin := prod_choiceMixin A1 A2;
      UnitAlgebra.is_Lmodule_of_Zmodule_mixin :=
        LmodMixin (pair_scaleA (V2:=A2)) (pair_scale1 (V2:=A2))
          (pair_scaleDr (V2:=A2)) (pair_scaleDl (V2:=A2));
      UnitAlgebra.is_Ring_of_Zmodule_mixin :=
        RingMixin (A1 * A2)%type (pair_mulA (R2:=A2)) (pair_mul1l (R2:=A2))
          (pair_mul1r (R2:=A2)) (pair_mulDl (R2:=A2)) (pair_mulDr (R2:=A2))
          (pair_one_neq0 A1 A2);
      UnitAlgebra.is_Lalgebra_of_Lmodule_mixin :=
        LalgMixin (pair_scaleAl (A2:=A2));
      UnitAlgebra.is_Algebra_of_Lalgebra_mixin :=
        Algebra.Mixin (pair_scaleAr (A2:=A2));
      UnitAlgebra.has_mul_inverse_mixin := XXX A1 A2
    |}
|}
1613585056.908798 HB: begin CS decl
1613585056.914190 HB: declare canonical structure instance
prod_is_a_UnitAlgebra
1613585056.923026 HB: we try to build a indt «ComAlgebra.type»
1613585056.944423 HB: we try to build a indt «ComUnitAlgebra.type»
HB: skipping alreay existing Countable instance on (A1 * A2)%type
HB: skipping alreay existing Finite instance on (A1 * A2)%type
1613585056.980981 HB: we try to build a indt «subEquality.type»
1613585056.989645 HB: we try to build a indt «subChoice.type»
1613585056.999233 HB: we try to build a indt «SubZmodule.type»
1613585057.007633 HB: we try to build a indt «SubLmodule.type»
1613585057.016103 HB: we try to build a indt «SubRing.type»
1613585057.024662 HB: we try to build a indt «SubUnitRing.type»
1613585057.033086 HB: we try to build a indt «SubCountable.type»
1613585057.041577 HB: we try to build a indt «subFinite.type»
Finished transaction in 13.601 secs (13.554u,0.043s) (successful)

Deciding if the structure can be built is not super fast, but it is not the main problem

1613585046.251127 HB: we try to build a indt «UnitAlgebra.type»
1613585047.896515 HB: we can build a UnitAlgebra on (A1 * A2)%type

The type checking step is 5 seconds! the problem is that the term is huge due to implicit arguments. In set printing all

$ wc -cl log
 112640 6717143 log
$ cat log | gzip | wc -cl
    655  132437

For example this term occurs many times

                               (@Lalgebra_to_Lmodule
                                 (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                 (@Algebra_to_Lalgebra
                                    (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                    (@UnitAlgebra_to_Algebra
                                       (ComRing_to_Ring
                                          (ComUnitRing_to_ComRing R)) A1)))

A Check .. of that term takes 8s (in that case Coq has to do a little more) so it does not seem that passing the monster to Coq (from elpi) is the main problem here. The kernel (just before declaring the CS instance) takes 4s to typecheck, so it is not an inefficiency of the "elaborator" alone.

So we have to figure out if "flattening" makes the implicit argument /type parameter problem worse, and/or how to compress the term (either in the logic, via let, or in caml/elpi, or both).

This is the unitAlgebra Class, it does not seem to bad.

Variant axioms (R : Ring.type) (V : Type) : Type :=
    Class : forall (is_Zmodule_mixin : is_Zmodule.axioms_ V)
              (is_eqType_mixin : is_eqType.axioms_ V)
              (has_choice_mixin : has_choice.axioms_ V)
              (is_Lmodule_of_Zmodule_mixin : is_Lmodule_of_Zmodule.axioms_ R
                                               V is_eqType_mixin
                                               has_choice_mixin
                                               is_Zmodule_mixin)
              (is_Ring_of_Zmodule_mixin : is_Ring_of_Zmodule.axioms_ V
                                            is_eqType_mixin has_choice_mixin
                                            is_Zmodule_mixin)
              (is_Lalgebra_of_Lmodule_mixin : is_Lalgebra_of_Lmodule.axioms_
                                                R V is_eqType_mixin
                                                has_choice_mixin
                                                is_Zmodule_mixin
                                                is_Ring_of_Zmodule_mixin
                                                is_Lmodule_of_Zmodule_mixin)
              (_ : is_Algebra_of_Lalgebra.axioms_ R V is_eqType_mixin
                     has_choice_mixin is_Zmodule_mixin
                     is_Ring_of_Zmodule_mixin is_Lmodule_of_Zmodule_mixin
                     is_Lalgebra_of_Lmodule_mixin)
              (_ : has_mul_inverse.axioms_ V is_Zmodule_mixin is_eqType_mixin
                     has_choice_mixin is_Ring_of_Zmodule_mixin),
            UnitAlgebra.axioms R V

view this post on Zulip HB Github Bot (Feb 17 2021 at 20:22):

CohenCyril merged PR #151 experimenting with nix ci.

view this post on Zulip HB Github Bot (Feb 17 2021 at 20:22):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 21:17):

gares edited Issue #150 performance problem of instance declaration:

From the very last instances in ssralg.v

HB: declare has_mul_inverse_to_has_mul_inverse__122
HB: declare canonical mixin instance
«has_mul_inverse_to_has_mul_inverse__122»
1613585046.099228 HB: we try to build a indt «SUB.type»
HB: skipping alreay existing Equality instance on (A1 * A2)%type
HB: skipping alreay existing Choice instance on (A1 * A2)%type
HB: skipping alreay existing Zmodule instance on (A1 * A2)%type
HB: skipping alreay existing Lmodule instance on (A1 * A2)%type
HB: skipping alreay existing Ring instance on (A1 * A2)%type
HB: skipping alreay existing UnitRing instance on (A1 * A2)%type
HB: skipping alreay existing ComRing instance on (A1 * A2)%type
HB: skipping alreay existing ComUnitRing instance on (A1 * A2)%type
1613585046.171108 HB: we try to build a indt «IntegralDomain.type»
1613585046.184017 HB: we try to build a indt «Field.type»
1613585046.199054 HB: we try to build a indt «ClosedField.type»
1613585046.213381 HB: we try to build a indt «DecidableField.type»
HB: skipping alreay existing Lalgebra instance on (A1 * A2)%type
HB: skipping alreay existing Algebra instance on (A1 * A2)%type
1613585046.251127 HB: we try to build a indt «UnitAlgebra.type»
1613585047.896515 HB: we can build a UnitAlgebra on (A1 * A2)%type
1613585047.932029 HB: begin typechecking
{|
  UnitAlgebra.sort := A1 * A2;
  UnitAlgebra.class :=
    {|
      UnitAlgebra.is_Zmodule_mixin :=
        ZmodMixin (A1 * A2)%type (pair_addA (M2:=A2)) (pair_addC (M2:=A2))
          (pair_add0 (M2:=A2)) (pair_addN (M2:=A2));
      UnitAlgebra.is_eqType_mixin := prod_eqMixin A1 A2;
      UnitAlgebra.has_choice_mixin := prod_choiceMixin A1 A2;
      UnitAlgebra.is_Lmodule_of_Zmodule_mixin :=
        LmodMixin (pair_scaleA (V2:=A2)) (pair_scale1 (V2:=A2))
          (pair_scaleDr (V2:=A2)) (pair_scaleDl (V2:=A2));
      UnitAlgebra.is_Ring_of_Zmodule_mixin :=
        RingMixin (A1 * A2)%type (pair_mulA (R2:=A2)) (pair_mul1l (R2:=A2))
          (pair_mul1r (R2:=A2)) (pair_mulDl (R2:=A2)) (pair_mulDr (R2:=A2))
          (pair_one_neq0 A1 A2);
      UnitAlgebra.is_Lalgebra_of_Lmodule_mixin :=
        LalgMixin (pair_scaleAl (A2:=A2));
      UnitAlgebra.is_Algebra_of_Lalgebra_mixin :=
        Algebra.Mixin (pair_scaleAr (A2:=A2));
      UnitAlgebra.has_mul_inverse_mixin := XXX A1 A2
    |}
|}
1613585052.874924 HB: end typechecking
{|
  UnitAlgebra.sort := A1 * A2;
  UnitAlgebra.class :=
    {|
      UnitAlgebra.is_Zmodule_mixin :=
        ZmodMixin (A1 * A2)%type (pair_addA (M2:=A2)) (pair_addC (M2:=A2))
          (pair_add0 (M2:=A2)) (pair_addN (M2:=A2));
      UnitAlgebra.is_eqType_mixin := prod_eqMixin A1 A2;
      UnitAlgebra.has_choice_mixin := prod_choiceMixin A1 A2;
      UnitAlgebra.is_Lmodule_of_Zmodule_mixin :=
        LmodMixin (pair_scaleA (V2:=A2)) (pair_scale1 (V2:=A2))
          (pair_scaleDr (V2:=A2)) (pair_scaleDl (V2:=A2));
      UnitAlgebra.is_Ring_of_Zmodule_mixin :=
        RingMixin (A1 * A2)%type (pair_mulA (R2:=A2)) (pair_mul1l (R2:=A2))
          (pair_mul1r (R2:=A2)) (pair_mulDl (R2:=A2)) (pair_mulDr (R2:=A2))
          (pair_one_neq0 A1 A2);
      UnitAlgebra.is_Lalgebra_of_Lmodule_mixin :=
        LalgMixin (pair_scaleAl (A2:=A2));
      UnitAlgebra.is_Algebra_of_Lalgebra_mixin :=
        Algebra.Mixin (pair_scaleAr (A2:=A2));
      UnitAlgebra.has_mul_inverse_mixin := XXX A1 A2
    |}
|}
1613585056.908798 HB: begin CS decl
1613585056.914190 HB: declare canonical structure instance
prod_is_a_UnitAlgebra
1613585056.923026 HB: we try to build a indt «ComAlgebra.type»
1613585056.944423 HB: we try to build a indt «ComUnitAlgebra.type»
HB: skipping alreay existing Countable instance on (A1 * A2)%type
HB: skipping alreay existing Finite instance on (A1 * A2)%type
1613585056.980981 HB: we try to build a indt «subEquality.type»
1613585056.989645 HB: we try to build a indt «subChoice.type»
1613585056.999233 HB: we try to build a indt «SubZmodule.type»
1613585057.007633 HB: we try to build a indt «SubLmodule.type»
1613585057.016103 HB: we try to build a indt «SubRing.type»
1613585057.024662 HB: we try to build a indt «SubUnitRing.type»
1613585057.033086 HB: we try to build a indt «SubCountable.type»
1613585057.041577 HB: we try to build a indt «subFinite.type»
Finished transaction in 13.601 secs (13.554u,0.043s) (successful)

Deciding if the structure can be built is not super fast, but it is not the main problem

1613585046.251127 HB: we try to build a indt «UnitAlgebra.type»
1613585047.896515 HB: we can build a UnitAlgebra on (A1 * A2)%type

The type checking step is 5 seconds! the problem is that the term is huge due to implicit arguments. In set printing all

$ wc -cl log
 112640 6717143 log
$ cat log | gzip | wc -cl
    655  132437

For example this term occurs many times

                               (@Lalgebra_to_Lmodule         (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                 (@Algebra_to_Lalgebra       (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                    (@UnitAlgebra_to_Algebra (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                       A1)))

A Check .. of that term takes 8s (in that case Coq has to do a little more) so it does not seem that passing the monster to Coq (from elpi) is the main problem here. The kernel (just before declaring the CS instance) takes 4s to typecheck, so it is not an inefficiency of the "elaborator" alone.

So we have to figure out if "flattening" makes the implicit argument /type parameter problem worse, and/or how to compress the term (either in the logic, via let, or in caml/elpi, or both).

This is the unitAlgebra Class, it does not seem to bad.

Variant axioms (R : Ring.type) (V : Type) : Type :=
    Class : forall (is_Zmodule_mixin : is_Zmodule.axioms_ V)
              (is_eqType_mixin : is_eqType.axioms_ V)
              (has_choice_mixin : has_choice.axioms_ V)
              (is_Lmodule_of_Zmodule_mixin : is_Lmodule_of_Zmodule.axioms_ R
                                               V is_eqType_mixin
                                               has_choice_mixin
                                               is_Zmodule_mixin)
              (is_Ring_of_Zmodule_mixin : is_Ring_of_Zmodule.axioms_ V
                                            is_eqType_mixin has_choice_mixin
                                            is_Zmodule_mixin)
              (is_Lalgebra_of_Lmodule_mixin : is_Lalgebra_of_Lmodule.axioms_
                                                R V is_eqType_mixin
                                                has_choice_mixin
                                                is_Zmodule_mixin
                                                is_Ring_of_Zmodule_mixin
                                                is_Lmodule_of_Zmodule_mixin)
              (_ : is_Algebra_of_Lalgebra.axioms_ R V is_eqType_mixin
                     has_choice_mixin is_Zmodule_mixin
                     is_Ring_of_Zmodule_mixin is_Lmodule_of_Zmodule_mixin
                     is_Lalgebra_of_Lmodule_mixin)
              (_ : has_mul_inverse.axioms_ V is_Zmodule_mixin is_eqType_mixin
                     has_choice_mixin is_Ring_of_Zmodule_mixin),
            UnitAlgebra.axioms R V

view this post on Zulip HB Github Bot (Feb 17 2021 at 21:20):

gares closed without merge PR #149 ci job to test ssralg.

view this post on Zulip HB Github Bot (Feb 17 2021 at 21:21):

gares edited Issue #150 performance problem of instance declaration:

From the very last instance in ssralg.v

HB: declare has_mul_inverse_to_has_mul_inverse__122
HB: declare canonical mixin instance
«has_mul_inverse_to_has_mul_inverse__122»
1613585046.099228 HB: we try to build a indt «SUB.type»
HB: skipping alreay existing Equality instance on (A1 * A2)%type
HB: skipping alreay existing Choice instance on (A1 * A2)%type
HB: skipping alreay existing Zmodule instance on (A1 * A2)%type
HB: skipping alreay existing Lmodule instance on (A1 * A2)%type
HB: skipping alreay existing Ring instance on (A1 * A2)%type
HB: skipping alreay existing UnitRing instance on (A1 * A2)%type
HB: skipping alreay existing ComRing instance on (A1 * A2)%type
HB: skipping alreay existing ComUnitRing instance on (A1 * A2)%type
1613585046.171108 HB: we try to build a indt «IntegralDomain.type»
1613585046.184017 HB: we try to build a indt «Field.type»
1613585046.199054 HB: we try to build a indt «ClosedField.type»
1613585046.213381 HB: we try to build a indt «DecidableField.type»
HB: skipping alreay existing Lalgebra instance on (A1 * A2)%type
HB: skipping alreay existing Algebra instance on (A1 * A2)%type
1613585046.251127 HB: we try to build a indt «UnitAlgebra.type»
1613585047.896515 HB: we can build a UnitAlgebra on (A1 * A2)%type
1613585047.932029 HB: begin typechecking
{|
  UnitAlgebra.sort := A1 * A2;
  UnitAlgebra.class :=
    {|
      UnitAlgebra.is_Zmodule_mixin :=
        ZmodMixin (A1 * A2)%type (pair_addA (M2:=A2)) (pair_addC (M2:=A2))
          (pair_add0 (M2:=A2)) (pair_addN (M2:=A2));
      UnitAlgebra.is_eqType_mixin := prod_eqMixin A1 A2;
      UnitAlgebra.has_choice_mixin := prod_choiceMixin A1 A2;
      UnitAlgebra.is_Lmodule_of_Zmodule_mixin :=
        LmodMixin (pair_scaleA (V2:=A2)) (pair_scale1 (V2:=A2))
          (pair_scaleDr (V2:=A2)) (pair_scaleDl (V2:=A2));
      UnitAlgebra.is_Ring_of_Zmodule_mixin :=
        RingMixin (A1 * A2)%type (pair_mulA (R2:=A2)) (pair_mul1l (R2:=A2))
          (pair_mul1r (R2:=A2)) (pair_mulDl (R2:=A2)) (pair_mulDr (R2:=A2))
          (pair_one_neq0 A1 A2);
      UnitAlgebra.is_Lalgebra_of_Lmodule_mixin :=
        LalgMixin (pair_scaleAl (A2:=A2));
      UnitAlgebra.is_Algebra_of_Lalgebra_mixin :=
        Algebra.Mixin (pair_scaleAr (A2:=A2));
      UnitAlgebra.has_mul_inverse_mixin := XXX A1 A2
    |}
|}
1613585052.874924 HB: end typechecking
{|
  UnitAlgebra.sort := A1 * A2;
  UnitAlgebra.class :=
    {|
      UnitAlgebra.is_Zmodule_mixin :=
        ZmodMixin (A1 * A2)%type (pair_addA (M2:=A2)) (pair_addC (M2:=A2))
          (pair_add0 (M2:=A2)) (pair_addN (M2:=A2));
      UnitAlgebra.is_eqType_mixin := prod_eqMixin A1 A2;
      UnitAlgebra.has_choice_mixin := prod_choiceMixin A1 A2;
      UnitAlgebra.is_Lmodule_of_Zmodule_mixin :=
        LmodMixin (pair_scaleA (V2:=A2)) (pair_scale1 (V2:=A2))
          (pair_scaleDr (V2:=A2)) (pair_scaleDl (V2:=A2));
      UnitAlgebra.is_Ring_of_Zmodule_mixin :=
        RingMixin (A1 * A2)%type (pair_mulA (R2:=A2)) (pair_mul1l (R2:=A2))
          (pair_mul1r (R2:=A2)) (pair_mulDl (R2:=A2)) (pair_mulDr (R2:=A2))
          (pair_one_neq0 A1 A2);
      UnitAlgebra.is_Lalgebra_of_Lmodule_mixin :=
        LalgMixin (pair_scaleAl (A2:=A2));
      UnitAlgebra.is_Algebra_of_Lalgebra_mixin :=
        Algebra.Mixin (pair_scaleAr (A2:=A2));
      UnitAlgebra.has_mul_inverse_mixin := XXX A1 A2
    |}
|}
1613585056.908798 HB: begin CS decl
1613585056.914190 HB: declare canonical structure instance
prod_is_a_UnitAlgebra
1613585056.923026 HB: we try to build a indt «ComAlgebra.type»
1613585056.944423 HB: we try to build a indt «ComUnitAlgebra.type»
HB: skipping alreay existing Countable instance on (A1 * A2)%type
HB: skipping alreay existing Finite instance on (A1 * A2)%type
1613585056.980981 HB: we try to build a indt «subEquality.type»
1613585056.989645 HB: we try to build a indt «subChoice.type»
1613585056.999233 HB: we try to build a indt «SubZmodule.type»
1613585057.007633 HB: we try to build a indt «SubLmodule.type»
1613585057.016103 HB: we try to build a indt «SubRing.type»
1613585057.024662 HB: we try to build a indt «SubUnitRing.type»
1613585057.033086 HB: we try to build a indt «SubCountable.type»
1613585057.041577 HB: we try to build a indt «subFinite.type»
Finished transaction in 13.601 secs (13.554u,0.043s) (successful)

Deciding if the structure can be built is not super fast, but it is not the main problem

1613585046.251127 HB: we try to build a indt «UnitAlgebra.type»
1613585047.896515 HB: we can build a UnitAlgebra on (A1 * A2)%type

The type checking step is 5 seconds! the problem is that the term is huge due to implicit arguments. In set printing all

$ wc -cl log
 112640 6717143 log
$ cat log | gzip | wc -cl
    655  132437

For example this term occurs many times

                               (@Lalgebra_to_Lmodule         (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                 (@Algebra_to_Lalgebra       (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                    (@UnitAlgebra_to_Algebra (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                       A1)))

A Check .. of that term takes 8s (in that case Coq has to do a little more) so it does not seem that passing the monster to Coq (from elpi) is the main problem here. The kernel (just before declaring the CS instance) takes 4s to typecheck, so it is not an inefficiency of the "elaborator" alone.

So we have to figure out if "flattening" makes the implicit argument /type parameter problem worse, and/or how to compress the term (either in the logic, via let, or in caml/elpi, or both).

This is the unitAlgebra Class, it does not seem to bad.

Variant axioms (R : Ring.type) (V : Type) : Type :=
    Class : forall (is_Zmodule_mixin : is_Zmodule.axioms_ V)
              (is_eqType_mixin : is_eqType.axioms_ V)
              (has_choice_mixin : has_choice.axioms_ V)
              (is_Lmodule_of_Zmodule_mixin : is_Lmodule_of_Zmodule.axioms_ R
                                               V is_eqType_mixin
                                               has_choice_mixin
                                               is_Zmodule_mixin)
              (is_Ring_of_Zmodule_mixin : is_Ring_of_Zmodule.axioms_ V
                                            is_eqType_mixin has_choice_mixin
                                            is_Zmodule_mixin)
              (is_Lalgebra_of_Lmodule_mixin : is_Lalgebra_of_Lmodule.axioms_
                                                R V is_eqType_mixin
                                                has_choice_mixin
                                                is_Zmodule_mixin
                                                is_Ring_of_Zmodule_mixin
                                                is_Lmodule_of_Zmodule_mixin)
              (_ : is_Algebra_of_Lalgebra.axioms_ R V is_eqType_mixin
                     has_choice_mixin is_Zmodule_mixin
                     is_Ring_of_Zmodule_mixin is_Lmodule_of_Zmodule_mixin
                     is_Lalgebra_of_Lmodule_mixin)
              (_ : has_mul_inverse.axioms_ V is_Zmodule_mixin is_eqType_mixin
                     has_choice_mixin is_Ring_of_Zmodule_mixin),
            UnitAlgebra.axioms R V

view this post on Zulip HB Github Bot (Feb 17 2021 at 21:21):

gares edited Issue #150 performance problem of instance declaration:

From the very last instance in ssralg.v, sprinkling {gettimeofday} in coq.say we get:

HB: declare has_mul_inverse_to_has_mul_inverse__122
HB: declare canonical mixin instance
«has_mul_inverse_to_has_mul_inverse__122»
1613585046.099228 HB: we try to build a indt «SUB.type»
HB: skipping alreay existing Equality instance on (A1 * A2)%type
HB: skipping alreay existing Choice instance on (A1 * A2)%type
HB: skipping alreay existing Zmodule instance on (A1 * A2)%type
HB: skipping alreay existing Lmodule instance on (A1 * A2)%type
HB: skipping alreay existing Ring instance on (A1 * A2)%type
HB: skipping alreay existing UnitRing instance on (A1 * A2)%type
HB: skipping alreay existing ComRing instance on (A1 * A2)%type
HB: skipping alreay existing ComUnitRing instance on (A1 * A2)%type
1613585046.171108 HB: we try to build a indt «IntegralDomain.type»
1613585046.184017 HB: we try to build a indt «Field.type»
1613585046.199054 HB: we try to build a indt «ClosedField.type»
1613585046.213381 HB: we try to build a indt «DecidableField.type»
HB: skipping alreay existing Lalgebra instance on (A1 * A2)%type
HB: skipping alreay existing Algebra instance on (A1 * A2)%type
1613585046.251127 HB: we try to build a indt «UnitAlgebra.type»
1613585047.896515 HB: we can build a UnitAlgebra on (A1 * A2)%type
1613585047.932029 HB: begin typechecking
{|
  UnitAlgebra.sort := A1 * A2;
  UnitAlgebra.class :=
    {|
      UnitAlgebra.is_Zmodule_mixin :=
        ZmodMixin (A1 * A2)%type (pair_addA (M2:=A2)) (pair_addC (M2:=A2))
          (pair_add0 (M2:=A2)) (pair_addN (M2:=A2));
      UnitAlgebra.is_eqType_mixin := prod_eqMixin A1 A2;
      UnitAlgebra.has_choice_mixin := prod_choiceMixin A1 A2;
      UnitAlgebra.is_Lmodule_of_Zmodule_mixin :=
        LmodMixin (pair_scaleA (V2:=A2)) (pair_scale1 (V2:=A2))
          (pair_scaleDr (V2:=A2)) (pair_scaleDl (V2:=A2));
      UnitAlgebra.is_Ring_of_Zmodule_mixin :=
        RingMixin (A1 * A2)%type (pair_mulA (R2:=A2)) (pair_mul1l (R2:=A2))
          (pair_mul1r (R2:=A2)) (pair_mulDl (R2:=A2)) (pair_mulDr (R2:=A2))
          (pair_one_neq0 A1 A2);
      UnitAlgebra.is_Lalgebra_of_Lmodule_mixin :=
        LalgMixin (pair_scaleAl (A2:=A2));
      UnitAlgebra.is_Algebra_of_Lalgebra_mixin :=
        Algebra.Mixin (pair_scaleAr (A2:=A2));
      UnitAlgebra.has_mul_inverse_mixin := XXX A1 A2
    |}
|}
1613585052.874924 HB: end typechecking
{|
  UnitAlgebra.sort := A1 * A2;
  UnitAlgebra.class :=
    {|
      UnitAlgebra.is_Zmodule_mixin :=
        ZmodMixin (A1 * A2)%type (pair_addA (M2:=A2)) (pair_addC (M2:=A2))
          (pair_add0 (M2:=A2)) (pair_addN (M2:=A2));
      UnitAlgebra.is_eqType_mixin := prod_eqMixin A1 A2;
      UnitAlgebra.has_choice_mixin := prod_choiceMixin A1 A2;
      UnitAlgebra.is_Lmodule_of_Zmodule_mixin :=
        LmodMixin (pair_scaleA (V2:=A2)) (pair_scale1 (V2:=A2))
          (pair_scaleDr (V2:=A2)) (pair_scaleDl (V2:=A2));
      UnitAlgebra.is_Ring_of_Zmodule_mixin :=
        RingMixin (A1 * A2)%type (pair_mulA (R2:=A2)) (pair_mul1l (R2:=A2))
          (pair_mul1r (R2:=A2)) (pair_mulDl (R2:=A2)) (pair_mulDr (R2:=A2))
          (pair_one_neq0 A1 A2);
      UnitAlgebra.is_Lalgebra_of_Lmodule_mixin :=
        LalgMixin (pair_scaleAl (A2:=A2));
      UnitAlgebra.is_Algebra_of_Lalgebra_mixin :=
        Algebra.Mixin (pair_scaleAr (A2:=A2));
      UnitAlgebra.has_mul_inverse_mixin := XXX A1 A2
    |}
|}
1613585056.908798 HB: begin CS decl
1613585056.914190 HB: declare canonical structure instance
prod_is_a_UnitAlgebra
1613585056.923026 HB: we try to build a indt «ComAlgebra.type»
1613585056.944423 HB: we try to build a indt «ComUnitAlgebra.type»
HB: skipping alreay existing Countable instance on (A1 * A2)%type
HB: skipping alreay existing Finite instance on (A1 * A2)%type
1613585056.980981 HB: we try to build a indt «subEquality.type»
1613585056.989645 HB: we try to build a indt «subChoice.type»
1613585056.999233 HB: we try to build a indt «SubZmodule.type»
1613585057.007633 HB: we try to build a indt «SubLmodule.type»
1613585057.016103 HB: we try to build a indt «SubRing.type»
1613585057.024662 HB: we try to build a indt «SubUnitRing.type»
1613585057.033086 HB: we try to build a indt «SubCountable.type»
1613585057.041577 HB: we try to build a indt «subFinite.type»
Finished transaction in 13.601 secs (13.554u,0.043s) (successful)

Deciding if the structure can be built is not super fast, but it is not the main problem

1613585046.251127 HB: we try to build a indt «UnitAlgebra.type»
1613585047.896515 HB: we can build a UnitAlgebra on (A1 * A2)%type

The type checking step is 5 seconds! the problem is that the term is huge due to implicit arguments. In set printing all

$ wc -cl log
 112640 6717143 log
$ cat log | gzip | wc -cl
    655  132437

For example this term occurs many times

                               (@Lalgebra_to_Lmodule         (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                 (@Algebra_to_Lalgebra       (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                    (@UnitAlgebra_to_Algebra (ComRing_to_Ring (ComUnitRing_to_ComRing R))
                                       A1)))

A Check .. of that term takes 8s (in that case Coq has to do a little more) so it does not seem that passing the monster to Coq (from elpi) is the main problem here. The kernel (just before declaring the CS instance) takes 4s to typecheck, so it is not an inefficiency of the "elaborator" alone.

So we have to figure out if "flattening" makes the implicit argument /type parameter problem worse, and/or how to compress the term (either in the logic, via let, or in caml/elpi, or both).

This is the unitAlgebra Class, it does not seem to bad.

Variant axioms (R : Ring.type) (V : Type) : Type :=
    Class : forall (is_Zmodule_mixin : is_Zmodule.axioms_ V)
              (is_eqType_mixin : is_eqType.axioms_ V)
              (has_choice_mixin : has_choice.axioms_ V)
              (is_Lmodule_of_Zmodule_mixin : is_Lmodule_of_Zmodule.axioms_ R
                                               V is_eqType_mixin
                                               has_choice_mixin
                                               is_Zmodule_mixin)
              (is_Ring_of_Zmodule_mixin : is_Ring_of_Zmodule.axioms_ V
                                            is_eqType_mixin has_choice_mixin
                                            is_Zmodule_mixin)
              (is_Lalgebra_of_Lmodule_mixin : is_Lalgebra_of_Lmodule.axioms_
                                                R V is_eqType_mixin
                                                has_choice_mixin
                                                is_Zmodule_mixin
                                                is_Ring_of_Zmodule_mixin
                                                is_Lmodule_of_Zmodule_mixin)
              (_ : is_Algebra_of_Lalgebra.axioms_ R V is_eqType_mixin
                     has_choice_mixin is_Zmodule_mixin
                     is_Ring_of_Zmodule_mixin is_Lmodule_of_Zmodule_mixin
                     is_Lalgebra_of_Lmodule_mixin)
              (_ : has_mul_inverse.axioms_ V is_Zmodule_mixin is_eqType_mixin
                     has_choice_mixin is_Ring_of_Zmodule_mixin),
            UnitAlgebra.axioms R V

view this post on Zulip HB Github Bot (Feb 17 2021 at 22:30):

CohenCyril deleted the branch nixci.

view this post on Zulip HB Github Bot (Feb 17 2021 at 22:50):

CohenCyril pushed 6 commits to branch nixci.

view this post on Zulip HB Github Bot (Feb 17 2021 at 22:53):

CohenCyril pushed 1 commit to branch nixci.

view this post on Zulip HB Github Bot (Feb 17 2021 at 22:54):

CohenCyril opened PR #152 local cache from nixci to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 22:59):

CohenCyril pushed 1 commit to branch nixci.

view this post on Zulip HB Github Bot (Feb 17 2021 at 22:59):

CohenCyril updated PR #152 local cache from nixci to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 23:10):

CohenCyril pushed 1 commit to branch nixci.

view this post on Zulip HB Github Bot (Feb 17 2021 at 23:10):

CohenCyril updated PR #152 local cache from nixci to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 23:14):

CohenCyril pushed 1 commit to branch nixci.

view this post on Zulip HB Github Bot (Feb 17 2021 at 23:14):

CohenCyril updated PR #152 local cache from nixci to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 23:19):

CohenCyril pushed 1 commit to branch nixci.

view this post on Zulip HB Github Bot (Feb 17 2021 at 23:19):

CohenCyril updated PR #152 local cache from nixci to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 23:24):

CohenCyril pushed 1 commit to branch nixci.

view this post on Zulip HB Github Bot (Feb 17 2021 at 23:24):

CohenCyril updated PR #152 local cache from nixci to master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 23:35):

CohenCyril merged PR #152 local cache.

view this post on Zulip HB Github Bot (Feb 17 2021 at 23:35):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Feb 17 2021 at 23:35):

CohenCyril deleted the branch nixci.

view this post on Zulip HB Github Bot (Feb 18 2021 at 12:12):

gares pushed 2 commits to branch dont-be-silly.

view this post on Zulip HB Github Bot (Feb 18 2021 at 12:15):

gares opened PR #153 optimizations from dont-be-silly to master:

the first one brings down the last instance in ssralg to 0.4s, slow but tolerable.
the second one is just to avoid being silly and store s.phant_Build crap instead of s.Build less crap, it does not impact performances too much for not.

I believe the root problem is still there:

Set Printing All. Print prod_is_a_Ring.
(*
prod_is_a_Ring =
@Ring.Pack (prod (Ring.sort R1) (Ring.sort R2))
  (@Ring.Class (prod (Ring.sort R1) (Ring.sort R2))
     (HB_unnamed_factory_105 (Ring_to_Zmodule R1) (Ring_to_Zmodule R2))
     (prod_eqMixin
        (Choice_to_Equality (Zmodule_to_Choice (Ring_to_Zmodule R1)))
        (Choice_to_Equality (Zmodule_to_Choice (Ring_to_Zmodule R2))))
     (prod_choiceMixin (Zmodule_to_Choice (Ring_to_Zmodule R1))
        (Zmodule_to_Choice (Ring_to_Zmodule R2))) HB_unnamed_factory_107)
     : Ring.type
*)

This instance is where the "coercion chain problem" pops up and is still manageable, hence were we can debug it.

CC @CohenCyril @pi8027

view this post on Zulip HB Github Bot (Feb 18 2021 at 12:17):

gares edited PR #153 optimizations from dont-be-silly to master:

the first one brings down the last instance in ssralg to 0.4s, slow but tolerable.
the second one is just to avoid being silly and store s.phant_Build crap instead of s.Build less crap, it does not impact performances too much for not.

I believe the root problem is still there:

Set Printing All. Print prod_is_a_Ring.
(*
prod_is_a_Ring =
@Ring.Pack (prod (Ring.sort R1) (Ring.sort R2))
  (@Ring.Class (prod (Ring.sort R1) (Ring.sort R2))
     (HB_unnamed_factory_105 (Ring_to_Zmodule R1) (Ring_to_Zmodule R2))
     (prod_eqMixin
        (Choice_to_Equality (Zmodule_to_Choice (Ring_to_Zmodule R1)))
        (Choice_to_Equality (Zmodule_to_Choice (Ring_to_Zmodule R2))))
     (prod_choiceMixin (Zmodule_to_Choice (Ring_to_Zmodule R1))
        (Zmodule_to_Choice (Ring_to_Zmodule R2))) HB_unnamed_factory_107)
     : Ring.type
*)

This instance is where the "coercion chain problem" pops up and is still manageable, hence were we can debug it.
(FTR: before this PR this term was already gigantic and contained phant_Build crap)

CC @CohenCyril @pi8027

view this post on Zulip HB Github Bot (Feb 18 2021 at 18:00):

CohenCyril pushed 1 commit to branch metanix.

view this post on Zulip HB Github Bot (Feb 18 2021 at 18:00):

CohenCyril opened PR #154 Trying out meta.yml with nix action from metanix to master.

view this post on Zulip HB Github Bot (Feb 18 2021 at 18:05):

CohenCyril pushed 1 commit to branch metanix.

view this post on Zulip HB Github Bot (Feb 18 2021 at 18:05):

CohenCyril updated PR #154 Trying out meta.yml with nix action from metanix to master.

view this post on Zulip HB Github Bot (Feb 18 2021 at 18:09):

CohenCyril pushed 1 commit to branch metanix.

view this post on Zulip HB Github Bot (Feb 18 2021 at 18:09):

CohenCyril updated PR #154 Trying out meta.yml with nix action from metanix to master.

view this post on Zulip HB Github Bot (Feb 18 2021 at 18:13):

CohenCyril pushed 1 commit to branch metanix.

view this post on Zulip HB Github Bot (Feb 18 2021 at 18:13):

CohenCyril updated PR #154 Trying out meta.yml with nix action from metanix to master.

view this post on Zulip HB Github Bot (Feb 18 2021 at 18:20):

CohenCyril pushed 1 commit to branch metanix.

view this post on Zulip HB Github Bot (Feb 18 2021 at 18:20):

CohenCyril updated PR #154 Trying out meta.yml with nix action from metanix to master.

view this post on Zulip HB Github Bot (Feb 18 2021 at 18:23):

CohenCyril pushed 1 commit to branch metanix.

view this post on Zulip HB Github Bot (Feb 18 2021 at 18:23):

CohenCyril updated PR #154 Trying out meta.yml with nix action from metanix to master.

view this post on Zulip HB Github Bot (Feb 18 2021 at 18:25):

CohenCyril pushed 1 commit to branch metanix.

view this post on Zulip HB Github Bot (Feb 18 2021 at 18:25):

CohenCyril updated PR #154 Trying out meta.yml with nix action from metanix to master.

view this post on Zulip HB Github Bot (Feb 18 2021 at 20:24):

CohenCyril submitted PR Review for #153 optimizations.

view this post on Zulip HB Github Bot (Feb 18 2021 at 20:28):

gares merged PR #153 optimizations.

view this post on Zulip HB Github Bot (Feb 18 2021 at 20:28):

gares pushed 3 commits to branch master.

view this post on Zulip HB Github Bot (Feb 18 2021 at 20:28):

gares deleted the branch dont-be-silly.

view this post on Zulip HB Github Bot (Feb 18 2021 at 21:22):

gares pushed 2 commits to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 18 2021 at 21:22):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 18 2021 at 21:24):

gares pushed 2 commits to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 18 2021 at 21:24):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 00:34):

CohenCyril pushed 1 commit to branch new_nixpkgs.

view this post on Zulip HB Github Bot (Feb 19 2021 at 00:34):

CohenCyril opened PR #155 update nixpkgs from new_nixpkgs to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 00:35):

CohenCyril pushed 1 commit to branch nixupdate.

view this post on Zulip HB Github Bot (Feb 19 2021 at 00:42):

CohenCyril pushed 1 commit to branch metanix.

view this post on Zulip HB Github Bot (Feb 19 2021 at 00:42):

CohenCyril updated PR #154 Trying out meta.yml with nix action from metanix to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 00:42):

CohenCyril deleted the branch nixupdate.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:07):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:07):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:08):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:08):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:16):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:16):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:24):

CohenCyril pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:24):

CohenCyril updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:36):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:36):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:37):

CohenCyril pushed 1 commit to branch new_nixpkgs.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:37):

CohenCyril updated PR #155 update nixpkgs from new_nixpkgs to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:42):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:42):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:46):

CohenCyril merged PR #155 update nixpkgs.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:46):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:46):

CohenCyril deleted the branch new_nixpkgs.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:48):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:48):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

  extraInstallFlags = [ "DESTDIR=$(out)" ];

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:48):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:48):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:50):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:50):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:56):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 08:56):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 12:49):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 12:49):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:19):

gares pushed 1 commit to branch fix-discharge.

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:19):

gares opened PR #156 discharge by hand both mixins and factories from fix-discharge to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:23):

gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:23):

gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:23):

gares created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

this is why it should work, something else is buggy

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:28):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:28):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

Why didn't I have this in my local checkout, is it recent??

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:29):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:29):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

ahah it works!

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:29):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:29):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

But then I cannot use both the variables COQMF_COQLIB and $DESTDIR :-/

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:30):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:30):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

I will hack around this...

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:39):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:39):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

The behaviour of DESTDIR is superweird... why does it concatenate it with coq's full path...

$ make DESTDIR=$(mktemp -d) install
/nix/store/kvhw9snhf3hxnlfmqbkq88yf2bqk19iy-coq-8.13.0/bin/coq_makefile  -f _CoqProject -o Makefile.coq
make -f Makefile.coq  install
make[1] : on entre dans le répertoire « /home/cyril/git/hierarchy-builder/logging-vernac »
INSTALL structures.vo /run/user/1000/tmp.RVRxOFEV2d//nix/store/kvhw9snhf3hxnlfmqbkq88yf2bqk19iy-coq-8.13.0/lib/coq//user-contrib/HB/
INSTALL structures.v /run/user/1000/tmp.RVRxOFEV2d//nix/store/kvhw9snhf3hxnlfmqbkq88yf2bqk19iy-coq-8.13.0/lib/coq//user-contrib/HB/
INSTALL structures.glob /run/user/1000/tmp.RVRxOFEV2d//nix/store/kvhw9snhf3hxnlfmqbkq88yf2bqk19iy-coq-8.13.0/lib/coq//user-contrib/HB/
make[2] : on entre dans le répertoire « /home/cyril/git/hierarchy-builder/logging-vernac »
install hb /run/user/1000/tmp.RVRxOFEV2d/bin
make[2] : on quitte le répertoire « /home/cyril/git/hierarchy-builder/logging-vernac »
make[1] : on quitte le répertoire « /home/cyril/git/hierarchy-builder/logging-vernac »

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:41):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:41):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

ah I think I figured it out!

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:43):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:43):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

The right command is a combination of both DESTDIR and COQMF_COQLIB!!

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:44):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:44):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

installFlags = [ "DESTDIR=$(out)" "COQMF_COQLIB=lib/coq/${coq.coq-version}" ];

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:44):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:44):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

Can I rebase and push?

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:48):

gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 13:48):

gares created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

please do.

It is not weird, it is the layout chose in nix which is not standard. $PREFIX/lib/coq/$VERSION/stuff if something made up by nix to have multiple coq versions coexist. Shall I repeat: PUSH THESE CHANGE UPSTREAM you nixer

view this post on Zulip HB Github Bot (Feb 19 2021 at 14:26):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 14:26):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

I will!

view this post on Zulip HB Github Bot (Feb 19 2021 at 14:26):

CohenCyril pushed 11 commits to branch logging-vernac. Commits by gares (9) and CohenCyril (2).

view this post on Zulip HB Github Bot (Feb 19 2021 at 14:26):

CohenCyril updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 14:28):

CohenCyril pushed 1 commit to branch logging-vernac. Commits by gares (1).

view this post on Zulip HB Github Bot (Feb 19 2021 at 14:28):

CohenCyril updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 14:30):

gares pushed 1 commit to branch nicer-error-messages.

view this post on Zulip HB Github Bot (Feb 19 2021 at 14:31):

gares opened PR #157 nicer error messages for non ground terms from nicer-error-messages to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 14:50):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 14:50):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

$PREFIX/lib/coq/$VERSION/stuff I agree this is weird, it looks unnecessary to me... (none should ever install two versions of coq at the same time anyway...) I git blame and ask why.

view this post on Zulip HB Github Bot (Feb 19 2021 at 14:50):

CohenCyril edited PR Review Comment on #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 15:22):

gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 15:22):

gares created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

it may make sense, I don't know, but if it does it should not be done by hacking an internal coq_makefile variable

view this post on Zulip HB Github Bot (Feb 19 2021 at 15:34):

gares pushed 1 commit to branch update-doc.

view this post on Zulip HB Github Bot (Feb 19 2021 at 15:34):

gares opened PR #158 update the doc from update-doc to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 15:35):

gares pushed 1 commit to branch update-doc.

view this post on Zulip HB Github Bot (Feb 19 2021 at 15:35):

gares updated PR #158 update the doc from update-doc to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 15:39):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 15:39):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

you mean COQMF_COQLIB is supposed to be internal?

view this post on Zulip HB Github Bot (Feb 19 2021 at 15:58):

gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 15:58):

gares created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

Internal.... it is given by coq, it is not supposed to be overridden on the command line (it is not in the doc for example).

IMO, if you want to have coq populate lib/coq-$VERSION/ you can add a configure time option to it and have all coq projects get from coq the right path, a bit like -prefix.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:00):

gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:00):

gares created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

I think it may make sense to have this feature. I'm complaining because it is "simulated" via little hacks.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:01):

gares created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

Actually, you can already do it, there is a -libdir

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:01):

gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:01):

gares edited PR Review Comment on #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:02):

gares merged PR #158 update the doc.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:02):

gares pushed 3 commits to branch master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:02):

gares deleted the branch update-doc.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:03):

gares merged PR #157 nicer error messages for non ground terms.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:03):

gares pushed 2 commits to branch master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:03):

gares deleted the branch nicer-error-messages.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:19):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:19):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

Nice!

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:21):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:21):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

Mmmh, are you sure though...

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:21):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:21):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

where did you find this?

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:22):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:22):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

is it a configureflag?

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:23):

CohenCyril edited PR Review Comment on #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:24):

CohenCyril edited PR Review Comment on #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:43):

gares pushed 2 commits to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:43):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:45):

gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:45):

gares created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

it is a flag in coq's configure

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:46):

gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:46):

gares created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

I guess you can configure coq to use /usr/lib/coq-8.13/ and as a consequence coq_makefile will install things there without hacking COQMF_COQLIB (which contains the value at configure time for -coqlib) I guess.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:56):

CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 19 2021 at 16:56):

CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:

I don't thing it is a good idea, COQLIB should keep pointing to coq's main /lib/ directory, which we cannot overwrite...

view this post on Zulip HB Github Bot (Feb 19 2021 at 17:26):

gares pushed 2 commits to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 17:26):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 17:41):

gares pushed 2 commits to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 17:41):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 17:54):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 17:54):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 18:22):

gares pushed 2 commits to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 18:23):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 19 2021 at 18:40):

gares pushed 3 commits to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 19 2021 at 18:40):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 20 2021 at 16:48):

gares edited PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master:

Require coq-elpi 1.9.0 (Coq 8.13)

Todo:

Status:

view this post on Zulip HB Github Bot (Feb 22 2021 at 16:00):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 22 2021 at 16:00):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 22 2021 at 16:07):

gares pushed 1 commit to branch fix-discharge.

view this post on Zulip HB Github Bot (Feb 22 2021 at 16:07):

gares updated PR #156 discharge by hand both mixins and factories from fix-discharge to master.

view this post on Zulip HB Github Bot (Feb 22 2021 at 16:16):

gares merged PR #156 discharge by hand both mixins and factories.

view this post on Zulip HB Github Bot (Feb 22 2021 at 16:16):

gares pushed 3 commits to branch master.

view this post on Zulip HB Github Bot (Feb 22 2021 at 16:16):

gares deleted the branch fix-discharge.

view this post on Zulip HB Github Bot (Feb 22 2021 at 16:16):

gares assigned Issue #139 #[index="R"] (assigned to gares).

view this post on Zulip HB Github Bot (Feb 22 2021 at 16:16):

gares assigned Issue #127 Using indexed is too fragile (assigned to gares):

We should replace by another kind of meta information.

view this post on Zulip HB Github Bot (Feb 23 2021 at 12:35):

gares pushed 1 commit to branch kill-ty-deps.

view this post on Zulip HB Github Bot (Feb 23 2021 at 12:35):

gares opened PR #159 kill ty-deps: add gref-deps for each factory and operation from kill-ty-deps to master:

I plan to push here another commit about killing indexed, but first I want to see if this one is OK

view this post on Zulip HB Github Bot (Feb 23 2021 at 12:40):

gares pushed 1 commit to branch kill-ty-deps.

view this post on Zulip HB Github Bot (Feb 23 2021 at 12:40):

gares updated PR #159 kill ty-deps: add gref-deps for each factory and operation from kill-ty-deps to master.

view this post on Zulip HB Github Bot (Feb 23 2021 at 12:40):

gares pushed 1 commit to branch kill-ty-deps.

view this post on Zulip HB Github Bot (Feb 23 2021 at 12:40):

gares updated PR #159 kill ty-deps: add gref-deps for each factory and operation from kill-ty-deps to master.

view this post on Zulip HB Github Bot (Feb 23 2021 at 12:42):

gares pushed 1 commit to branch kill-ty-deps.

view this post on Zulip HB Github Bot (Feb 23 2021 at 12:42):

gares updated PR #159 kill ty-deps: add gref-deps for each factory and operation from kill-ty-deps to master.

view this post on Zulip HB Github Bot (Feb 23 2021 at 12:47):

gares edited PR #159 kill ty-deps, long live #[key="T"] from kill-ty-deps to master.

view this post on Zulip HB Github Bot (Feb 23 2021 at 12:54):

gares pushed 2 commits to branch kill-ty-deps.

view this post on Zulip HB Github Bot (Feb 23 2021 at 12:54):

gares updated PR #159 kill ty-deps, long live #[key="T"] from kill-ty-deps to master.

view this post on Zulip HB Github Bot (Feb 23 2021 at 13:07):

gares pushed 1 commit to branch kill-ty-deps.

view this post on Zulip HB Github Bot (Feb 23 2021 at 13:07):

gares updated PR #159 kill ty-deps, long live #[key="T"] from kill-ty-deps to master.

view this post on Zulip HB Github Bot (Feb 23 2021 at 13:07):

gares edited PR #159 kill ty-deps, long live #[key="T"] from kill-ty-deps to master:

I tested it locally and it work on MC!

view this post on Zulip HB Github Bot (Feb 23 2021 at 13:10):

gares edited PR #159 kill ty-deps, long live #[key="T"] from kill-ty-deps to master:

I tested it locally and it work on MC!

Fix #139
Fix #127

view this post on Zulip HB Github Bot (Feb 23 2021 at 13:16):

gares pushed 1 commit to branch kill-ty-deps.

view this post on Zulip HB Github Bot (Feb 23 2021 at 13:16):

gares updated PR #159 kill ty-deps, long live #[key="T"] from kill-ty-deps to master.

view this post on Zulip HB Github Bot (Feb 23 2021 at 13:35):

gares pushed 1 commit to branch kill-ty-deps.

view this post on Zulip HB Github Bot (Feb 23 2021 at 13:35):

gares updated PR #159 kill ty-deps, long live #[key="T"] from kill-ty-deps to master.

view this post on Zulip HB Github Bot (Feb 23 2021 at 14:31):

gares pushed 1 commit to branch xdot.

view this post on Zulip HB Github Bot (Feb 23 2021 at 14:32):

gares opened PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot to master:

Because we can... and because I'm in procrastination mode.

CC @affeldt-aist

view this post on Zulip HB Github Bot (Feb 23 2021 at 14:41):

gares pushed 1 commit to branch xdot.

view this post on Zulip HB Github Bot (Feb 23 2021 at 14:41):

gares updated PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot to master.

view this post on Zulip HB Github Bot (Feb 23 2021 at 14:52):

gares pushed 1 commit to branch xdot.

view this post on Zulip HB Github Bot (Feb 23 2021 at 14:52):

gares updated PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot to master.

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:06):

gares pushed 1 commit to branch xdot.

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:06):

gares updated PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot to master.

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:08):

gares edited PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot to master:

![Screenshot from 2021-02-23 16-07-40](https://user-images.githubusercontent.com/1013846/108863249-47f8fc00-75f1-11eb-807b-1d89fece1fed.png)

Because we can... and because I'm in procrastination mode.

CC @affeldt-aist

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:15):

gares submitted PR Review for #160 HB.status handles the #[dot] and #[dot(file=..)] attributes.

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:15):

gares created PR Review Comment on #160 HB.status handles the #[dot] and #[dot(file=..)] attributes:

The attribute #[dot] prints the hierarchy in dot format and opens
a suitable viewer (eg xdot).

The attribute #[dot(file="name")] prints the hierarchy in dot format in the

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:15):

gares pushed 1 commit to branch xdot.

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:15):

gares updated PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot to master.

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:24):

gares closed Issue #145 CI job for mathcomp (assigned to CohenCyril):

As soon as ssralg passes we should add a job compiling up to that file

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:26):

gares edited PR #159 kill ty-deps, long live #[key="T"] from kill-ty-deps to master:

I tested it locally and it work on MC!

Fix #139
Fix #127
Fix #93

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:31):

gares submitted PR Review for #159 kill ty-deps, long live #[key="T"]

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:31):

gares created PR Review Comment on #159 kill ty-deps, long live #[key="T"]

  ClassName = indt ClassInd, coq.env.indt ClassInd _ _ _ _ [ClassK] _,
  GRDepsClauses = [gref-deps (indt ClassInd) MLwP, gref-deps (indc ClassK) MLwP],

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:32):

gares submitted PR Review for #159 kill ty-deps, long live #[key="T"]

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:32):

gares created PR Review Comment on #159 kill ty-deps, long live #[key="T"]

  std.forall GRDepsClauses (c\ acc current (clause _ _ c)),
  % std.map {gr-deps GRK} (_\ r\ r = maximal) Implicits,

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:33):

gares pushed 1 commit to branch kill-ty-deps.

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:33):

gares updated PR #159 kill ty-deps, long live #[key="T"] from kill-ty-deps to master.

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:34):

gares milestoned Issue #159 kill ty-deps, long live #[key="T"]

I tested it locally and it work on MC!

Fix #139
Fix #127
Fix #93

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:34):

gares milestoned Issue #160 HB.status handles the #[dot] and #[dot(file=..)] attributes:

![Screenshot from 2021-02-23 16-07-40](https://user-images.githubusercontent.com/1013846/108863249-47f8fc00-75f1-11eb-807b-1d89fece1fed.png)

Because we can... and because I'm in procrastination mode.

CC @affeldt-aist

view this post on Zulip HB Github Bot (Feb 23 2021 at 15:49):

gares pushed 1 commit to branch master.

view this post on Zulip HB Github Bot (Feb 23 2021 at 18:39):

gares pushed 1 commit to branch xdot.

view this post on Zulip HB Github Bot (Feb 23 2021 at 18:39):

gares updated PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot to master.

view this post on Zulip HB Github Bot (Feb 23 2021 at 21:22):

gares pushed 1 commit to branch xdot.

view this post on Zulip HB Github Bot (Feb 23 2021 at 21:22):

gares updated PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot to master.

view this post on Zulip HB Github Bot (Feb 24 2021 at 07:35):

gares edited PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot to master:

![Screenshot from 2021-02-24 08-35-27](https://user-images.githubusercontent.com/1013846/108964061-483dd980-767b-11eb-93c6-895b5a69546b.png)

Because we can... and because I'm in procrastination mode.

CC @affeldt-aist

view this post on Zulip HB Github Bot (Feb 24 2021 at 10:01):

CohenCyril edited PR Review Comment on #131 logging: HB prints its effect in term of vernac commands.

view this post on Zulip HB Github Bot (Feb 24 2021 at 10:35):

CohenCyril closed Issue #139 #[index="R"] (assigned to gares).

view this post on Zulip HB Github Bot (Feb 24 2021 at 10:35):

CohenCyril closed Issue #127 Using indexed is too fragile (assigned to gares):

We should replace by another kind of meta information.

view this post on Zulip HB Github Bot (Feb 24 2021 at 10:35):

CohenCyril closed Issue #93 Error message "BUG: ty-deps ..." should suggest to put indexed around the type.

view this post on Zulip HB Github Bot (Feb 24 2021 at 10:35):

CohenCyril merged PR #159 kill ty-deps, long live #[key="T"]

view this post on Zulip HB Github Bot (Feb 24 2021 at 10:35):

CohenCyril pushed 8 commits to branch master. Commits by gares (7) and CohenCyril (1).

view this post on Zulip HB Github Bot (Feb 24 2021 at 10:36):

coqbot-app[bot] milestoned Issue #139 #[index="R"] (assigned to gares).

view this post on Zulip HB Github Bot (Feb 24 2021 at 10:36):

coqbot-app[bot] milestoned Issue #93 Error message "BUG: ty-deps ..." should suggest to put indexed around the type.

view this post on Zulip HB Github Bot (Feb 24 2021 at 11:30):

gares pushed 2 commits to branch cleanup.

view this post on Zulip HB Github Bot (Feb 24 2021 at 11:30):

gares opened PR #161 Cleanup from cleanup to master.

view this post on Zulip HB Github Bot (Feb 24 2021 at 11:38):

gares merged PR #161 Cleanup.

view this post on Zulip HB Github Bot (Feb 24 2021 at 11:38):

gares pushed 3 commits to branch master.

view this post on Zulip HB Github Bot (Feb 24 2021 at 11:38):

gares deleted the branch cleanup.

view this post on Zulip HB Github Bot (Feb 24 2021 at 13:42):

gares pushed 1 commit to branch xdot.

view this post on Zulip HB Github Bot (Feb 24 2021 at 13:42):

gares updated PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot to master.

view this post on Zulip HB Github Bot (Feb 24 2021 at 13:43):

gares edited PR #160 HB.graph "file.dot". from xdot to master.

view this post on Zulip HB Github Bot (Feb 24 2021 at 18:01):

gares pushed 1 commit to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 24 2021 at 18:01):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 24 2021 at 18:23):

gares pushed 3 commits to branch logging-vernac.

view this post on Zulip HB Github Bot (Feb 24 2021 at 18:23):

gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac to master.

view this post on Zulip HB Github Bot (Feb 24 2021 at 18:23):

gares pushed the branch cleanup2.

view this post on Zulip HB Github Bot (Feb 24 2021 at 18:23):

gares opened PR #162 Cleanup from logging vernac from cleanup2 to master.

view this post on Zulip HB Github Bot (Feb 24 2021 at 18:25):

gares pushed 1 commit to branch cleanup2.

view this post on Zulip HB Github Bot (Feb 24 2021 at 18:25):

gares updated PR #162 Cleanup from logging vernac from cleanup2 to master.

view this post on Zulip HB Github Bot (Feb 24 2021 at 18:36):

gares pushed 1 commit to branch cleanup2.

view this post on Zulip HB Github Bot (Feb 24 2021 at 18:36):

gares updated PR #162 Cleanup from logging vernac from cleanup2 to master.

view this post on Zulip HB Github Bot (Feb 24 2021 at 18:36):

gares requested CohenCyril for a review on PR #162 Cleanup from logging vernac.

view this post on Zulip HB Github Bot (Feb 24 2021 at 18:47):

CohenCyril pushed 1 commit to branch intermediate_sort.

view this post on Zulip HB Github Bot (Feb 24 2021 at 18:49):

CohenCyril pushed 1 commit to branch intermediate_sort.

view this post on Zulip HB Github Bot (Feb 24 2021 at 18:49):

CohenCyril opened PR #163 attributes "nocoercion" and "arg_sort" from intermediate_sort to master:

view this post on Zulip HB Github Bot (Feb 24 2021 at 22:14):

CohenCyril edited PR #163 attributes "nocoercion" and "arg_sort" from intermediate_sort to master:

cf https://github.com/math-comp/math-comp/pull/new/hierarchy-builder-fingroup

view this post on Zulip HB Github Bot (Feb 24 2021 at 22:14):

CohenCyril edited PR #163 attributes "nocoercion" and "arg_sort" from intermediate_sort to master:

cf https://github.com/math-comp/math-comp/tree/46efb5c7e224b367b24e776d682118ddb623bec3

view this post on Zulip HB Github Bot (Feb 24 2021 at 22:14):

CohenCyril edited PR #163 attributes "nocoercion" and "arg_sort" from intermediate_sort to master:

cf https://github.com/math-comp/math-comp/tree/hierarchy-builder-fingroup/mathcomp

view this post on Zulip HB Github Bot (Feb 24 2021 at 22:15):

CohenCyril merged PR #162 Cleanup from logging vernac.

view this post on Zulip HB Github Bot (Feb 24 2021 at 22:15):

CohenCyril pushed 4 commits to branch master. Commits by gares (3) and CohenCyril (1).

view this post on Zulip HB Github Bot (Feb 24 2021 at 22:18):

CohenCyril pushed 1 commit to branch intermediate_sort.

view this post on Zulip HB Github Bot (Feb 24 2021 at 22:18):

CohenCyril updated PR #163 attributes "nocoercion" and "arg_sort" from intermediate_sort to master.

view this post on Zulip HB Github Bot (Feb 24 2021 at 22:19):

CohenCyril pushed 1 commit to branch intermediate_sort.

view this post on Zulip HB Github Bot (Feb 24 2021 at 22:19):

CohenCyril updated PR #163 attributes "nocoercion" and "arg_sort" from intermediate_sort to master.

view this post on Zulip HB Github Bot (Feb 25 2021 at 12:31):

gares pushed 8 commits to branch cleanup3.

view this post on Zulip HB Github Bot (Feb 25 2021 at 12:32):

gares opened PR #164 small cleanup from cleanup3 to master:

the next one in the pipeline is more ambitious, so I'd rather have the two separated.

view this post on Zulip HB Github Bot (Feb 25 2021 at 14:23):

gares pushed 4 commits to branch cleanup3.

view this post on Zulip HB Github Bot (Feb 25 2021 at 14:23):

gares updated PR #164 small cleanup from cleanup3 to master.

view this post on Zulip HB Github Bot (Feb 25 2021 at 14:33):

CohenCyril pushed 1 commit to branch intermediate_sort.

view this post on Zulip HB Github Bot (Feb 25 2021 at 14:33):

CohenCyril updated PR #163 attributes "nocoercion" and "arg_sort" from intermediate_sort to master.

view this post on Zulip HB Github Bot (Feb 25 2021 at 14:33):

CohenCyril edited PR #163 Attribute "arg_sort" from intermediate_sort to master.

view this post on Zulip HB Github Bot (Feb 25 2021 at 14:34):

CohenCyril edited PR #163 Attribute "arg_sort" from intermediate_sort to master:

view this post on Zulip HB Github Bot (Feb 25 2021 at 15:56):

gares submitted PR Review for #163 Attribute "arg_sort"

view this post on Zulip HB Github Bot (Feb 25 2021 at 15:57):

CohenCyril pushed 1 commit to branch intermediate_sort.

view this post on Zulip HB Github Bot (Feb 25 2021 at 15:57):

CohenCyril updated PR #163 Attribute "arg_sort" from intermediate_sort to master.

view this post on Zulip HB Github Bot (Feb 25 2021 at 16:01):

CohenCyril pushed 1 commit to branch intermediate_sort.

view this post on Zulip HB Github Bot (Feb 25 2021 at 16:01):

CohenCyril updated PR #163 Attribute "arg_sort" from intermediate_sort to master.

view this post on Zulip HB Github Bot (Feb 25 2021 at 16:11):

gares pushed 6 commits to branch separate-commands.

view this post on Zulip HB Github Bot (Feb 25 2021 at 16:16):

gares pushed 1 commit to branch separate-commands.

view this post on Zulip HB Github Bot (Feb 25 2021 at 16:17):

gares opened PR #165 Separate commands from separate-commands to master:

This is a monster PR based on #164 which does:

$ ls -R HB
HB:
builders.elpi  common  context.elpi  export.elpi  factory.elpi  instance.elpi  status.elpi  structure.elpi

HB/common:
coq-vernac.elpi  database.elpi  phant-abbreviation.elpi  synthesis.elpi  utils.elpi

view this post on Zulip HB Github Bot (Feb 25 2021 at 16:20):

gares pushed 1 commit to branch separate-commands.

view this post on Zulip HB Github Bot (Feb 25 2021 at 16:20):

gares updated PR #165 Separate commands from separate-commands to master.

view this post on Zulip HB Github Bot (Feb 25 2021 at 16:24):

gares edited PR #165 Separate commands from separate-commands to master:

This is a monster PR based on #164 which does:

$ ls -R HB
HB:
builders.elpi  common  context.elpi  export.elpi  factory.elpi  instance.elpi  status.elpi  structure.elpi

HB/common:
coq-vernac.elpi  database.elpi  phant-abbreviation.elpi  synthesis.elpi  utils.elpi

$ wc -l ...
    199 HB/builders.elpi