CohenCyril pushed 1 commit to branch parameters.
CohenCyril pushed 1 commit to branch parameters.
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
gares pushed 1 commit to branch master.
gares pushed 1 commit to branch coq-elpi-1.4.
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
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
gares pushed 3 commits to branch coq-master.
gares pushed 1 commit to branch coq-elpi-1.4.
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
gares pushed 1 commit to branch coq-master.
gares pushed 1 commit to branch master.
gares pushed 1 commit to branch coq-elpi-1.4.
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
gares pushed 2 commits to branch coq-elpi-1.4.
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
gares pushed 2 commits to branch coq-master.
CohenCyril pushed 3 commits to branch coq-elpi-1.4.
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
CohenCyril pushed 1 commit to branch coq-elpi-1.4.
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
CohenCyril pushed 1 commit to branch parameters. Commits by gares (1).
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
CohenCyril pushed 1 commit to branch parameters. Commits by gares (1).
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
gares pushed 1 commit to branch coq-elpi-1.4.
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
gares pushed 1 commit to branch fix-make.
gares opened PR #71 simplify makefile from fix-make
to master
.
gares merged PR #71 simplify makefile.
gares pushed 2 commits to branch master.
gares deleted the branch fix-make.
gares pushed 6 commits to branch coq-master.
CohenCyril pushed 1 commit to branch parameters. Commits by gares (1).
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
CohenCyril pushed 1 commit to branch parameters. Commits by gares (1).
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
gares pushed 4 commits to branch coq-elpi-1.4. Commits by CohenCyril (2) and gares (2).
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
CohenCyril pushed 1 commit to branch parameters. Commits by gares (1).
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
gares pushed 1 commit to branch coq-elpi-1.4.
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
gares pushed 1 commit to branch coq-elpi-1.4.
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
gares pushed 7 commits to branch coq-master. Commits by gares (5) and CohenCyril (2).
CohenCyril pushed 1 commit to branch parameters.
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
CohenCyril pushed 2 commits to branch parameters. Commits by CohenCyril (1) and gares (1).
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
CohenCyril pushed 1 commit to branch coq-elpi-1.4.
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
CohenCyril pushed 1 commit to branch coq-elpi-1.4.
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
CohenCyril pushed 1 commit to branch coq-elpi-1.4.
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
CohenCyril pushed 2 commits to branch parameters. Commits by CohenCyril (1) and gares (1).
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
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)
CohenCyril merged PR #70 port to coq-elpi 1.4.
CohenCyril pushed 9 commits to branch master. Commits by CohenCyril (5) and gares (4).
CohenCyril deleted the branch coq-elpi-1.4.
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.vOf 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 acceptwhere
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.
gares pushed 1 commit to branch master.
CohenCyril pushed 1 commit to branch parameters.
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
gares pushed 1 commit to branch instance-def.
gares opened PR #73 syntax HB.instance Definition := ... from instance-def
to master
:
Fix #53
gares pushed 1 commit to branch instance-def.
gares updated PR #73 syntax HB.instance Definition := ... from instance-def
to master
:
Fix #53
gares pushed 1 commit to branch instance-def.
gares updated PR #73 syntax HB.instance Definition := ... from instance-def
to master
:
Fix #53
gares closed Issue #53 HB.instance Definition bla := Foo.Build T .... syntax (assigned to gares):
Kind of looks nice
gares merged PR #73 syntax HB.instance Definition := ...
gares pushed 4 commits to branch master.
gares deleted the branch instance-def.
gares pushed 3 commits to branch parameters. Commits by CohenCyril (2) and gares (1).
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
gares pushed 1 commit to branch parameters.
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
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
overA
we get an assertion inpred 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],
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?
CohenCyril submitted PR Review for #65 [feature] parameters in structures.
gares submitted PR Review for #65 [feature] parameters in structures.
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
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
The code base has a new data typelist-w-params A
andw-params A
to represent it.
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
The code base has a new data typelist-w-params A
andw-params A
to represent it.
gares pushed 1 commit to branch instance-def-params.
gares opened PR #75 HB.instance Definition f A := .... A .... from instance-def-params
to master
.
gares edited PR #75 HB.instance Definition f A := .... A .... from instance-def-params
to parameters
.
gares pushed 1 commit to branch instance-def-params.
gares updated PR #75 HB.instance Definition f A := .... A .... from instance-def-params
to parameters
.
gares merged PR #75 HB.instance Definition f A := .... A ....
gares pushed 1 commit to branch parameters.
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
The code base has a new data typelist-w-params A
andw-params A
to represent it.
gares deleted the branch instance-def-params.
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 herefoo P1 ..
passesP1
tof1
andP1
,P1 * P2
tof2
.
A dispatching is an arbitrary function from parameters to a list of parameters.
The code base has a new data typelist-w-params A
andw-params A
to represent it.Fix #75
CohenCyril pushed 1 commit to branch master.
CohenCyril created release Hierarchy Builder 0.9.1 for tag v0.9.1.
CohenCyril released release Hierarchy Builder 0.9.1 for tag v0.9.1.
CohenCyril published release Hierarchy Builder 0.9.1 for tag v0.9.1.
CohenCyril pushed tag v0.9.1.
gares pushed 1 commit to branch coq-master-0.9.1.
gares opened PR #76 Coq master 0.9.1 from coq-master-0.9.1
to coq-master
.
gares pushed 1 commit to branch coq-master-0.9.1.
gares updated PR #76 Coq master 0.9.1 from coq-master-0.9.1
to coq-master
.
CohenCyril merged PR #65 [feature] parameters in structures.
CohenCyril pushed 6 commits to branch master. Commits by CohenCyril (3) and gares (3).
CohenCyril pushed 1 commit to branch master.
CohenCyril pushed 1 commit to branch more_tests.
CohenCyril opened PR #77 Creating Left module on a Ring from more_tests
to master
.
CohenCyril pushed 1 commit to branch more_tests.
CohenCyril updated PR #77 Creating Left module on a Ring from more_tests
to master
.
gares deleted the branch parameters.
gares pushed 1 commit to branch coq-master-0.9.1.
gares updated PR #76 Coq master 0.9.1 from coq-master-0.9.1
to coq-master
.
gares merged PR #76 Coq master 0.9.1.
gares pushed 13 commits to branch coq-master. Commits by gares (9) and CohenCyril (4).
gares deleted the branch coq-master-0.9.1.
gares pushed 1 commit to branch more_tests.
gares updated PR #77 Creating Left module on a Ring from more_tests
to master
.
CohenCyril pushed 1 commit to branch more_tests.
CohenCyril updated PR #77 Creating Left module on a Ring from more_tests
to master
.
CohenCyril pushed 1 commit to branch more_tests.
CohenCyril updated PR #77 Creating Left module on a Ring from more_tests
to master
.
CohenCyril has marked PR #77 as ready for review.
CohenCyril merged PR #77 Creating Left module on a Ring.
CohenCyril pushed 5 commits to branch master. Commits by CohenCyril (4) and gares (1).
CohenCyril deleted the branch more_tests.
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
overA
we get an assertion inpred 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],
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 ..
CohenCyril pushed 1 commit to branch factory-name-or-alias.
CohenCyril opened PR #78 renaming factory-name from factory-name-or-alias
to master
:
fixes #64
CohenCyril pushed 1 commit to branch fix-abbrev.
CohenCyril opened PR #79 fixing missing typeabbrev from coq-elpi from fix-abbrev
to master
.
gares pushed 1 commit to branch coq-elpi-1.4.1.
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
CohenCyril closed without merge PR #79 fixing missing typeabbrev from coq-elpi.
gares deleted the branch fix-abbrev.
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.
CohenCyril merged PR #78 renaming factory-name.
CohenCyril pushed 2 commits to branch master.
CohenCyril closed without merge PR #80 coq-elpi 1.4.1.
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
CohenCyril pushed 1 commit to branch master.
CohenCyril pushed 2 commits to branch master. Commits by cyrilcohen (2).
gares merged PR #80 coq-elpi 1.4.1.
gares pushed 2 commits to branch master.
gares deleted the branch coq-elpi-1.4.1.
CohenCyril pushed 1 commit to branch master.
CohenCyril pushed 1 commit to branch master.
CohenCyril pushed 1 commit to branch master.
gares pushed 2 commits to branch master.
gares pushed 2 commits to branch master.
CohenCyril pushed 1 commit to branch master.
CohenCyril pushed 1 commit to branch master.
CohenCyril pushed 1 commit to branch master.
CohenCyril pushed 1 commit to branch master.
CohenCyril pushed 1 commit to branch new-phant-abbrev.
CohenCyril opened PR #81 refactoring/fixin phant-term build from new-phant-abbrev
to master
.
CohenCyril edited PR #81 refactoring/fixing phant-term build from new-phant-abbrev
to master
.
CohenCyril pushed 1 commit to branch new-phant-abbrev.
CohenCyril updated PR #81 refactoring/fixing phant-term build from new-phant-abbrev
to master
.
CohenCyril pushed 1 commit to branch new-phant-abbrev.
CohenCyril updated PR #81 refactoring/fixing phant-term build from new-phant-abbrev
to master
.
CohenCyril pushed 1 commit to branch new-phant-abbrev.
CohenCyril updated PR #81 refactoring/fixing phant-term build from new-phant-abbrev
to master
.
CohenCyril pushed 1 commit to branch new-phant-abbrev.
CohenCyril updated PR #81 refactoring/fixing phant-term build from new-phant-abbrev
to master
.
CohenCyril pushed 1 commit to branch new-phant-abbrev.
CohenCyril updated PR #81 refactoring/fixing phant-term build from new-phant-abbrev
to master
.
CohenCyril pushed 6 commits to branch new-phant-abbrev.
CohenCyril updated PR #81 refactoring/fixing phant-term build from new-phant-abbrev
to master
.
CohenCyril merged PR #81 refactoring/fixing phant-term build.
CohenCyril pushed 7 commits to branch master.
CohenCyril pushed 1 commit to branch is-structure.
CohenCyril opened PR #82 adding is-structure from is-structure
to master
.
CohenCyril merged PR #82 adding is-structure.
CohenCyril pushed 2 commits to branch master.
pi8027 pushed 1 commit to branch master.
gares opened Issue #83 HB.instance Definition foo : T := Build bar should read the number of parameters from T (when given)
gares edited Issue #83 HB.instance Definition foo : T := Build bar
should read the number of parameters from T (when given)
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 onlysigT
is really needed
gares edited Issue #83 HB.instance Definition foo : T := Build bar should read the number of parameters from T (when given)
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
CohenCyril pushed 1 commit to branch fix-get-canonical-mixin.
CohenCyril opened PR #86 fix from fix-get-canonical-mixin
to master
.
gares opened Issue #87 demo1 has still a dummy root structure with no properties.
gares opened Issue #88 in Coq 8.12 support #[local] HB.instance:
In 8.12 you can write
#[local] Canonical foo
gares opened Issue #89 outdated doc about builders:
There is no
_f
anymore
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
.
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 unifyt x y = _ _ c
you don't necessarily force the unfolding oft
andc
could gety
, while witht x y = K _ c
you do, since the RHS is a rigid HNF hence the LHS must be reduces to exposeK
andc
getsC x y
CohenCyril merged PR #86 In HB.instance
force unification to extract the class instead of the second argument.
CohenCyril pushed 2 commits to branch master.
gares deleted the branch fix-get-canonical-mixin.
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
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
CohenCyril milestoned Issue #89 outdated doc about builders:
There is no
_f
anymore
CohenCyril milestoned Issue #87 demo1 has still a dummy root structure with no properties.
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
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 onlysigT
is really needed
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)
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.vOf 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 acceptwhere
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.
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.
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.
CohenCyril milestoned Issue #36 HB.instance should no rely on std.findall
order:
do not rely on std.findall order
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...
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...
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
byElpi hb.canonical (T1 * T2)%type prod_topology.
?
(making coq-elpi insert the coercionTopologicalSpace.sort
)
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.
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.
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.
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
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
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)
gares pushed 1 commit to branch HOAS+holes.
gares opened PR #92 Use the new HOAS:holes option of coq-elpi from HOAS+holes
to master
:
gares opened Issue #93 Error message "BUG: ty-deps ..." should suggest to put indexed
around the type.
gares pushed 2 commits to branch HOAS+holes.
gares updated PR #92 Use the new HOAS:holes option of coq-elpi from HOAS+holes
to master
:
gares edited PR #92 coq-elpi 1.5 from HOAS+holes
to master
:
gares pushed 1 commit to branch ty-ty.
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.
gares merged PR #94 [instance] typecheck the type first.
gares pushed 2 commits to branch master.
gares deleted the branch ty-ty.
gares pushed 1 commit to branch ghactions.
gares opened PR #95 Create main.yml from ghactions
to master
.
gares edited PR #95 Create main.yml from ghactions
to master
:
TODO:
- [x] nix
- [ ] opam
- [ ] rm travis
gares pushed 2 commits to branch ghactions.
gares updated PR #95 Create main.yml from ghactions
to master
:
TODO:
- [x] nix
- [ ] opam
- [ ] rm travis
gares edited PR #95 Create main.yml from ghactions
to master
:
TODO:
- [x] nix
- [x] opam
- [ ] rm travis
gares edited PR #95 Create main.yml from ghactions
to master
:
TODO:
- [x] nix
- [x] opam
- [x] rm travis
gares merged PR #95 Create main.yml.
gares pushed 4 commits to branch master.
gares deleted the branch ghactions.
gares pushed 1 commit to branch master.
gares pushed 4 commits to branch HOAS+holes.
gares updated PR #92 coq-elpi 1.5 from HOAS+holes
to master
:
gares pushed 1 commit to branch HOAS+holes.
gares updated PR #92 coq-elpi 1.5 from HOAS+holes
to master
:
gares edited PR #92 coq-elpi 1.5 from HOAS+holes
to master
:
Take advantage of Coq-Elpi 1.5.x
gares pushed 2 commits to branch elpi-1.5.
gares opened PR #96 Elpi 1.5 from elpi-1.5
to coq-master
.
gares edited PR #96 Elpi 1.5 from elpi-1.5
to coq-master
:
update the branch used by Coq CI
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
gares pushed 1 commit to branch elpi-1.5.
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
gares pushed 1 commit to branch elpi-1.5.
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
gares merged PR #96 [coq-ci] update to Coq-Elpi 1.5.
gares pushed 58 commits to branch coq-master. Commits by CohenCyril (31), gares (26) and pi8027 (1).
gares deleted the branch elpi-1.5.
gares pushed 4 commits to branch elpi-elaborator.
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.
gares pushed 2 commits to branch elpi-elaborator.
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.
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
gares submitted PR Review for #97 [hack] use Coq-Elpi elaborator.
gares created PR Review Comment on #97 [hack] use Coq-Elpi elaborator:
Here it works and inserts coercions
gares submitted PR Review for #97 [hack] use Coq-Elpi elaborator.
gares created PR Review Comment on #97 [hack] use Coq-Elpi elaborator:
This predicate is very incomplete
gares submitted PR Review for #97 [hack] use Coq-Elpi elaborator.
gares created PR Review Comment on #97 [hack] use Coq-Elpi elaborator:
This is even switched off
gares submitted PR Review for #97 [hack] use Coq-Elpi elaborator.
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.
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
gares milestoned Issue #88 in Coq 8.12 support #[local] HB.instance:
In 8.12 you can write
#[local] Canonical foo
gares pushed 1 commit to branch HOAS+holes.
gares updated PR #92 coq-elpi 1.5 from HOAS+holes
to master
:
Take advantage of Coq-Elpi 1.5.x
gares merged PR #92 coq-elpi 1.5.
gares pushed 7 commits to branch master.
gares deleted the branch HOAS+holes.
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.
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
byElpi hb.canonical (T1 * T2)%type prod_topology.
?
(making coq-elpi insert the coercionTopologicalSpace.sort
)
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 makemy.type
that inheritseq.type
, somy.type
is coercible toeq.type
which is coercible toeqType
. But if you look atfoo1
definition you can see that Coq can't solve such a unification problem. Also, I can't make a new Canonical instance formy.type
because it conflicts withhb_eqMixin
.
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
?
CohenCyril pushed 1 commit to branch class-to-mixin-coercions.
CohenCyril opened PR #101 Adding coercions from classes to mixins from class-to-mixin-coercions
to master
.
CohenCyril merged PR #101 Adding coercions from classes to mixins.
CohenCyril pushed 2 commits to branch master.
CohenCyril deleted the branch class-to-mixin-coercions.
CohenCyril pushed 1 commit to branch fix_89.
CohenCyril opened PR #102 fixes #89 from fix_89
to master
.
CohenCyril edited PR #102 fixes #89 from fix_89
to master
:
fixes #89
CohenCyril closed Issue #89 outdated doc about builders:
There is no
_f
anymore
CohenCyril merged PR #102 fixes #89.
CohenCyril pushed 2 commits to branch master.
CohenCyril milestoned Issue #102 fixes #89:
fixes #89
CohenCyril pushed 1 commit to branch fix_90.
CohenCyril opened PR #103 Remove reexports of notations from fix_90
to master
:
fixes #90
CohenCyril pushed 1 commit to branch fix_91.
CohenCyril opened PR #104 Better error message in case of wrong structure definition order from fix_91
to master
:
fixes #91
CohenCyril demilestoned Issue #88 in Coq 8.12 support #[local] HB.instance:
In 8.12 you can write
#[local] Canonical foo
CohenCyril milestoned Issue #88 in Coq 8.12 support #[local] HB.instance:
In 8.12 you can write
#[local] Canonical foo
CohenCyril pushed 1 commit to branch fix_87.
CohenCyril pushed 1 commit to branch fix_87.
CohenCyril opened PR #105 removing spurious empty TYPE structure from fix_87
to master
:
fixes #87
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
CohenCyril merged PR #103 Remove reexports of notations.
CohenCyril pushed 2 commits to branch master.
CohenCyril milestoned Issue #103 Remove reexports of notations:
fixes #90
CohenCyril milestoned Issue #104 Better error message in case of wrong structure definition order:
fixes #91
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)
CohenCyril merged PR #104 Better error message in case of wrong structure definition order.
CohenCyril pushed 2 commits to branch master.
CohenCyril deleted the branch fix_91.
CohenCyril milestoned Issue #105 removing spurious empty TYPE structure:
fixes #87
CohenCyril closed Issue #87 demo1 has still a dummy root structure with no properties.
CohenCyril merged PR #105 removing spurious empty TYPE structure.
CohenCyril pushed 2 commits to branch master.
CohenCyril pushed 2 commits to branch fix-join-with-params.
CohenCyril opened PR #106 Fix the join of structures with parameters + changelog from fix-join-with-params
to master
:
- A non-obvious fix for an obvious bug
- Update changelog
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.vOf 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 acceptwhere
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.
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.vOf 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 acceptwhere
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.
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.vOf 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 acceptwhere
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.
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.vOf 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 acceptwhere
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.
CohenCyril merged PR #106 Fix the join of structures with parameters + changelog.
CohenCyril pushed 3 commits to branch master.
CohenCyril milestoned Issue #106 Fix the join of structures with parameters + changelog:
- A non-obvious fix for an obvious bug
- Update changelog
CohenCyril deleted the branch fix-join-with-params.
CohenCyril created release Hierarchy Builder 0.10.0 for tag 0.10.0.
CohenCyril edited release Hierarchy Builder 0.10.0 for tag 0.10.0.
CohenCyril released release Hierarchy Builder 0.10.0 for tag 0.10.0.
CohenCyril published release Hierarchy Builder 0.10.0 for tag 0.10.0.
CohenCyril pushed tag 0.10.0.
CohenCyril edited release Hierarchy Builder 0.10.0 for tag 0.10.0.
CohenCyril pushed 1 commit to branch master.
CohenCyril edited release Hierarchy Builder 0.10.0 for tag v0.10.0.
CohenCyril pushed tag v0.10.0.
CohenCyril removed tag 0.10.0.
gares pushed 1 commit to branch master.
gares opened Issue #107 update readme wrt 0.10.
gares pushed 2 commits to branch mathcomp-compat.
gares opened PR #108 Mathcomp compat from mathcomp-compat
to master
.
gares pushed 1 commit to branch coq-elaborator-elpi-1.6.
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
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
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
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
gares pushed 2 commits to branch coq-elaborator-elpi-1.6.
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
gares closed without merge PR #97 [hack] use Coq-Elpi elaborator to infer coercions.
gares pushed 1 commit to branch coq-elaborator-elpi-1.6.
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
gares pushed 1 commit to branch coq-elaborator-elpi-1.6.
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
gares pushed 1 commit to branch coq-elaborator-elpi-1.6.
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
gares pushed 3 commits to branch coq-elaborator-elpi-1.6.
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
gares pushed 1 commit to branch coq-elaborator-elpi-1.6.
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
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
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
gares pushed 12 commits to branch coq-elaborator-elpi-1.6.
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
gares pushed 1 commit to branch coq-elaborator-elpi-1.6.
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
gares pushed 1 commit to branch coq-master.
gares pushed the branch coq-elaborator-elpi-1.6.
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
gares pushed 1 commit to branch coq-elaborator-elpi-1.6.
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
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.
gares merged PR #109 use Coq's elaborator for factories and instances.
gares pushed 14 commits to branch master.
gares deleted the branch coq-elaborator-elpi-1.6.
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
byElpi hb.canonical (T1 * T2)%type prod_topology.
?
(making coq-elpi insert the coercionTopologicalSpace.sort
)
gares opened Issue #110 when postulating section variables, assume type is Type if not given.
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
CohenCyril opened Issue #112 HB.structure should generate a pack notation:
Generate
pack
in order to build a structure from a single mixin.
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 optionSet Implicit Arguments
gares pushed 1 commit to branch master.
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.
gares pushed 1 commit to branch master.
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
gares closed Issue #110 when postulating section variables, assume type is Type if not given.
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
gares pushed 1 commit to branch master.
gares closed Issue #107 update readme wrt 0.10.
gares pushed 1 commit to branch local-instances.
gares opened PR #115 HB.instance understands #[local] (fix #88) from local-instances
to master
.
gares pushed 1 commit to branch local-instances.
gares updated PR #115 HB.instance understands #[local] (fix #88) from local-instances
to master
.
gares submitted PR Review for #115 HB.instance understands #[local] (fix #88)
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...
gares edited PR #115 HB.instance understands #[local] (fix #88) from local-instances
to master
:
This pr:
- adds
#[local]
toHB.instance
- document which command supports which attribute. If you pass a non-supported attribute to a command you get an error.
gares closed without merge PR #108 Mathcomp compat.
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.
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 (_ * _)).
CohenCyril pushed 2 commits to branch pack_notation.
gares opened PR #118 Pack notation from pack_notation
to master
.
gares pushed 2 commits to branch pack_notation.
gares updated PR #118 Pack notation from pack_notation
to master
.
gares pushed 1 commit to branch pack_notation.
gares updated PR #118 Pack notation from pack_notation
to master
.
gares has marked PR #118 as ready for review.
gares closed without merge PR #118 Pack notation.
CohenCyril pushed 4 commits to branch master. Commits by CohenCyril (2) and gares (2).
gares deleted the branch pack_notation.
CohenCyril pushed 1 commit to branch master.
gares pushed 1 commit to branch master.
gares pushed 1 commit to branch section-discharge-fight.
gares opened PR #119 wip from section-discharge-fight
to master
.
gares edited PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
CohenCyril pushed 1 commit to branch section-discharge-fight-ko.
gares pushed 1 commit to branch section-discharge-fight-ko.
gares pushed 2 commits to branch section-discharge-fight. Commits by CohenCyril (1) and gares (1).
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
CohenCyril commented on abbdc32:
:crying_cat_face:
Ooops
gares pushed 3 commits to branch section-discharge-fight.
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
gares pushed 2 commits to branch section-discharge-fight.
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
gares pushed 1 commit to branch section-discharge-fight.
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
gares pushed 1 commit to branch section-discharge-fight.
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
gares submitted PR Review for #119 [hack] section discharge unused.
gares created PR Review Comment on #119 [hack] section discharge unused:
Does this make sense? Or should we check something?
gares submitted PR Review for #119 [hack] section discharge unused.
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.
gares pushed 1 commit to branch section-discharge-fight.
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
CohenCyril pushed 1 commit to branch section-discharge-fight.
CohenCyril updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
gares pushed 6 commits to branch section-discharge-fight.
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
gares pushed 5 commits to branch section-discharge-fight.
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
gares requested CohenCyril for a review on PR #119 [hack] section discharge unused.
gares submitted PR Review for #119 [hack] section discharge unused.
gares created PR Review Comment on #119 [hack] section discharge unused:
@CohenCyril can you write a line of doc for this thing?
gares pushed 1 commit to branch section-discharge-fight.
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
gares pushed 1 commit to branch section-discharge-fight.
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
gares edited Issue #112 [wish] HB.pack Definition packager args : structure.
Generate
pack
in order to build a structure from a single mixin.
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
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
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 onlysigT
is really needed
gares pushed 1 commit to branch section-discharge-fight.
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
gares pushed 1 commit to branch section-discharge-fight.
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
gares pushed 1 commit to branch section-discharge-fight.
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
gares pushed 1 commit to branch section-discharge-fight.
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
gares pushed 2 commits to branch section-discharge-fight.
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
gares opened Issue #120 under-canonical-mixins should filter the CS db better:
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.
gares pushed 1 commit to branch fix-120.
gares opened PR #121 filter CS db in a more precise way (fix#120) from fix-120
to master
.
gares pushed 1 commit to branch fix-120.
gares updated PR #121 filter CS db in a more precise way (fix#120) from fix-120
to master
.
gares requested CohenCyril for a review on PR #121 filter CS db in a more precise way (fix#120).
CohenCyril submitted PR Review for #121 filter CS db in a more precise way (fix#120)
CohenCyril merged PR #121 filter CS db in a more precise way (fix#120)
CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and gares (1).
CohenCyril closed Issue #120 under-canonical-mixins should filter the CS db better:
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.
gares deleted the branch fix-120.
gares pushed 13 commits to branch section-discharge-fight.
gares updated PR #119 [hack] section discharge unused from section-discharge-fight
to master
.
CohenCyril submitted PR Review for #119 [hack] section discharge unused.
gares merged PR #119 [hack] section discharge unused.
gares pushed 14 commits to branch master.
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.
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 optionSet Implicit Arguments
gares deleted the branch section-discharge-fight.
gares pushed 1 commit to branch univ-poly.
gares opened PR #122 [wip] universe polymorphism from univ-poly
to master
:
Depends on LPCIC/coq-elpi#190
gares pushed 3 commits to branch univ-poly.
gares updated PR #122 [wip] universe polymorphism from univ-poly
to master
:
Depends on LPCIC/coq-elpi#190
gares pushed 1 commit to branch cleanup.
gares opened PR #123 cleanup structure and sub-class from cleanup
to master
:
This is an extract from the branch about universe polymorphism.
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
gares pushed 1 commit to branch master.
gares pushed 1 commit to branch bump-elpi.
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
gares pushed 1 commit to branch coq-master+coq-elpi-1.7.0+elpi-1.12.
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
gares merged PR #126 Coq master+coq elpi 1.7.0+elpi 1.12.
gares pushed 43 commits to branch coq-master. Commits by gares (39) and CohenCyril (4).
gares deleted the branch coq-master+coq-elpi-1.7.0+elpi-1.12.
gares pushed 1 commit to branch bump-elpi.
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
CohenCyril opened Issue #127 Using indexed
is too fragile:
We should replace by another kind of meta information.
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
gares milestoned Issue #127 Using indexed
is too fragile:
We should replace by another kind of meta information.
gares pushed 1 commit to branch bump-elpi.
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
gares merged PR #125 Elpi 1.12 + Coq-Elpi 1.8.0.
gares pushed 4 commits to branch master.
gares deleted the branch bump-elpi.
gares pushed 1 commit to branch cleanup.
gares updated PR #123 cleanup structure and sub-class from cleanup
to master
:
This is an extract from the branch about universe polymorphism.
CohenCyril pushed 1 commit to branch nix-elpi-1.8.
CohenCyril opened PR #128 Compile with coq 8.12 & coq elpi 1.8 from nix-elpi-1.8
to master
.
CohenCyril pushed 1 commit to branch nix-elpi-1.8.
CohenCyril updated PR #128 Compile with coq 8.12 & coq elpi 1.8 from nix-elpi-1.8
to master
.
CohenCyril pushed 1 commit to branch nix-elpi-1.8.
CohenCyril updated PR #128 Compile with coq 8.12 & coq elpi 1.8 from nix-elpi-1.8
to master
.
CohenCyril pushed 1 commit to branch nix-elpi-1.8.
CohenCyril updated PR #128 Compile with coq 8.12 & coq elpi 1.8 from nix-elpi-1.8
to master
.
CohenCyril pushed 1 commit to branch nix-elpi-1.8.
CohenCyril updated PR #128 Compile with coq 8.12 & coq elpi 1.8 from nix-elpi-1.8
to master
.
CohenCyril merged PR #128 Compile with coq 8.12 & coq elpi 1.8.
CohenCyril pushed 2 commits to branch master.
CohenCyril deleted the branch nix-elpi-1.8.
gares merged PR #123 cleanup structure and sub-class.
gares pushed 2 commits to branch master.
gares deleted the branch cleanup.
gares pushed 1 commit to branch release-1.0.0.
gares opened PR #129 Close changelog for 1.0.0 from release-1.0.0
to master
:
speak now or ...
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.
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.
gares demilestoned Issue #36 HB.instance should no rely on std.findall
order:
do not rely on std.findall order
gares milestoned Issue #36 HB.instance should no rely on std.findall
order:
do not rely on std.findall order
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.
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.
gares demilestoned Issue #88 in Coq 8.12 support #[local] HB.instance:
In 8.12 you can write
#[local] Canonical foo
gares milestoned Issue #88 in Coq 8.12 support #[local] HB.instance:
In 8.12 you can write
#[local] Canonical foo
gares demilestoned Issue #127 Using indexed
is too fragile:
We should replace by another kind of meta information.
gares milestoned Issue #127 Using indexed
is too fragile:
We should replace by another kind of meta information.
gares edited PR #129 Close changelog for 1.0.0 from release-1.0.0
to master
:
speak now or ...
Fix #124
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
gares merged PR #129 Close changelog for 1.0.0.
gares pushed 2 commits to branch master.
gares deleted the branch release-1.0.0.
gares created release Hierarchy Builder 1.0.0 for tag v1.0.0.
gares released release Hierarchy Builder 1.0.0 for tag v1.0.0.
gares published release Hierarchy Builder 1.0.0 for tag v1.0.0.
gares pushed tag v1.0.0.
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
- not installed
- don't run if taken from somewhere else
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 theFrom 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
I guess I like 3, I'll see what I can do next week
gares pushed 1 commit to branch master.
gares pushed 1 commit to branch logging-vernac.
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:
- [ ]
indexed
,unify
,nomsg
end up in the final terms but are in HB.
gares pushed 1 commit to branch logging-vernac.
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:
- [ ]
indexed
,unify
,nomsg
end up in the final terms but are in HB.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 HB prints its effect in term of vernac commands from logging-vernac
to master
.
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:
- [ ]
indexed
,unify
,nomsg
end up in the final terms but are in HB.- [ ] strings are printed ungly, making phant terms even uglier
Status:
- it works (round trips)
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:
- [ ]
indexed
,unify
,nomsg
end up in the final terms but are in HB.- [ ] strings are printed ungly, making phant terms even uglier
Status:
- it works (round trips)
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:
- [ ]
indexed
,unify
,nomsg
end up in the final terms but are in HB.- [ ] strings are printed ungly, making phant terms even uglier
- [ ]
.hb
files are never removed, if you compile twice they get appended things twice and then the patch cannot be appliedStatus:
- it works (round trips)
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:
- [ ]
indexed
,unify
,nomsg
end up in the final terms but are in HB.- [ ] strings are printed ungly, making phant terms even uglier
- [ ]
.hb
files are never removed, if you compile twice they get appended things twice and then the patch cannot be appliedTODO:
- [ ] move in hb the vernacular printing code from coq-elpi, since is is too sketchy to be of general interest.
Status:
- it works (round trips)
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 HB prints its effect in term of vernac commands from logging-vernac
to master
.
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:
- [ ]
indexed
,unify
,nomsg
end up in the final terms but are in HB.- [ ] strings are printed ungly, making phant terms even uglier
- [ ]
.hb
files are never removed, if you compile twice they get appended things twice and then the patch cannot be appliedTODO:
- [ ] move in hb the vernacular printing code from coq-elpi, since is is too sketchy to be of general interest.
Status:
- it works (round trips)
- impacted by https://github.com/coq/coq/issues/13843 (I removed all empty structures)
- quality of the logged code is impacted by (the lack of in 8.13) https://github.com/coq/coq/pull/13840
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 HB prints its effect in term of vernac commands from logging-vernac
to master
.
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:
- [ ]
indexed
,unify
,nomsg
end up in the final terms but are in HB.- [ ] strings are printed ungly, making phant terms even uglier
- [ ]
.hb
files are never removed, if you compile twice they get appended things twice and then the patch cannot be appliedTODO:
- [ ] move in hb the vernacular printing code from coq-elpi, since is is too sketchy to be of general interest.
Status:
- it works (round trips)
- impacted by https://github.com/coq/coq/issues/13843 (I removed all empty structures)
- quality of the logged code is impacted by (the lack of in 8.13) https://github.com/coq/coq/pull/13840
- hack for command locations to be removed once https://github.com/coq/coq/pull/13844 is merged
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:
- [ ]
indexed
,unify
,nomsg
end up in the final terms but are in HB.- [ ] strings are printed ungly, making phant terms even uglier
- [x]
.hb
files are never removed, if you compile twice they get appended things twice and then the patch cannot be appliedTODO:
- [ ] move in hb the vernacular printing code from coq-elpi, since is is too sketchy to be of general interest.
Status:
- it works (round trips)
- impacted by https://github.com/coq/coq/issues/13843 (I removed all empty structures)
- quality of the logged code is impacted by (the lack of in 8.13) https://github.com/coq/coq/pull/13840
- hack for command locations to be removed once https://github.com/coq/coq/pull/13844 is merged
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:
- [ ]
indexed
,unify
,nomsg
end up in the final terms but are in HB.- [x] strings are printed ungly, making phant terms even uglier
- [x]
.hb
files are never removed, if you compile twice they get appended things twice and then the patch cannot be appliedTODO:
- [ ] move in hb the vernacular printing code from coq-elpi, since is is too sketchy to be of general interest.
Status:
- it works (round trips)
- impacted by https://github.com/coq/coq/issues/13843 (I removed all empty structures)
- quality of the logged code is impacted by (the lack of in 8.13) https://github.com/coq/coq/pull/13840
- hack for command locations to be removed once https://github.com/coq/coq/pull/13844 is merged
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:
- [ ]
indexed
,unify
,nomsg
end up in the final terms but are in HB.- [x] strings are printed ungly, making phant terms even uglier (fixed in https://github.com/coq/coq/pull/13840)
- [x]
.hb
files are never removed, if you compile twice they get appended things twice and then the patch cannot be applied (fixed, nowhb reset
moved the patches away)TODO:
- [ ] move in hb the vernacular printing code from coq-elpi, since is is too sketchy to be of general interest.
Status:
- it works (round trips)
- impacted by https://github.com/coq/coq/issues/13843 (I removed all empty structures)
- quality of the logged code is impacted by (the lack of in 8.13) https://github.com/coq/coq/pull/13840
- hack for command locations to be removed once https://github.com/coq/coq/pull/13844 is merged
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:
- [ ]
indexed
,unify
,nomsg
end up in the final terms but are in HB.- [x] strings are printed ungly, making phant terms even uglier (fixed in https://github.com/coq/coq/pull/13840)
- [x]
.hb
files are never removed, if you compile twice they get appended things twice and then the patch cannot be applied (fixed, nowhb reset
moved the patches away)TODO:
- [x] move in hb the vernacular printing code from coq-elpi, since is is too sketchy to be of general interest.
Status:
- it works (round trips)
- impacted by https://github.com/coq/coq/issues/13843 (I removed all empty structures)
- quality of the logged code is impacted by (the lack of in 8.13) https://github.com/coq/coq/pull/13840
- hack for command locations to be removed once https://github.com/coq/coq/pull/13844 is merged
CohenCyril pushed 1 commit to branch cat.
CohenCyril deleted the branch cat.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares edited PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
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:
- [ ]
indexed
,unify
,nomsg
end up in the final terms but are in HB/structures.v, where do we move these? Do we need these?Status:
- it works (round trips)
- impacted by https://github.com/coq/coq/issues/13843 (I removed all empty structures)
- quality of the logged code is impacted by (the lack of in 8.13) https://github.com/coq/coq/pull/13840
- hack for command locations to be removed once https://github.com/coq/coq/pull/13844 is merged
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares has marked PR #131 as ready for review.
gares opened Issue #132 Remove arguments that are there just to force discharging:
Blocked by https://github.com/LPCIC/coq-elpi/issues/210
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 azmodType
, should make the explicit typing ofv
optional.
CohenCyril opened Issue #134 HB.structure does not always insert coercions.
Cf mathcomp port subLmodule structure definition.
gares pushed 1 commit to branch fix-elab-params.
gares opened PR #135 fix elaboration of parameters in HB.structure from fix-elab-params
to master
:
Fix #134
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
gares submitted PR Review for #135 fix elaboration of parameters in HB.structure.
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".
gares pushed 1 commit to branch fix-elab-params.
gares updated PR #135 fix elaboration of parameters in HB.structure from fix-elab-params
to master
.
gares pushed 1 commit to branch smart-elab-context.
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
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
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)
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)
gares pushed 1 commit to branch rm-hack-discharge.
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
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
gares pushed 4 commits to branch fix-elab-params.
gares updated PR #135 fix elaboration of parameters in HB.structure from fix-elab-params
to master
.
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
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
gares closed without merge PR #136 Smart elab context.
gares edited PR #135 Elaboration of parameters in HB.structure and HB.builders from fix-elab-params
to master
.
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
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
gares requested CohenCyril for a review on PR #135 Elaboration of parameters in HB.structure and HB.builders.
gares pushed 2 commits to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
CohenCyril submitted PR Review for #135 Elaboration of parameters in HB.structure and HB.builders.
CohenCyril created PR Review Comment on #135 Elaboration of parameters in HB.structure and HB.builders:
Amazing!
CohenCyril submitted PR Review for #135 Elaboration of parameters in HB.structure and HB.builders.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
CohenCyril pushed 1 commit to branch fixfactoryfields.
CohenCyril opened PR #138 Bugfix: forgotten parameters from fixfactoryfields
to master
:
- factory local definitions were not taking parameters into account.
- making sure factory/mixin arguments are always explicit.
gares submitted PR Review for #138 Bugfix: forgotten parameters.
CohenCyril closed Issue #134 HB.structure does not always insert coercions.
Cf mathcomp port subLmodule structure definition.
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 azmodType
, should make the explicit typing ofv
optional.
CohenCyril merged PR #135 Elaboration of parameters in HB.structure and HB.builders.
CohenCyril pushed 5 commits to branch master. Commits by gares (4) and CohenCyril (1).
CohenCyril pushed 1 commit to branch fixfactoryfields.
CohenCyril updated PR #138 Bugfix: forgotten parameters from fixfactoryfields
to master
.
CohenCyril merged PR #138 Bugfix: forgotten parameters.
CohenCyril pushed 2 commits to branch master.
CohenCyril deleted the branch fixfactoryfields.
gares deleted the branch fix-elab-params.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares opened Issue #139 #[index="R"]
gares labeled Issue #139 #[index="R"]
gares opened Issue #140 #[infer(R="Type")]
gares labeled Issue #140 #[infer(R="Type")]
gares edited Issue #140 #[infer(var = "R", from ="Type")]
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 ...
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 ...
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 ...
CohenCyril pushed 1 commit to branch new_nix.
CohenCyril pushed 1 commit to branch new_nix.
CohenCyril opened PR #142 Bugfix: forgotten parameters from new_nix
to master
:
- factory local definitions were not taking parameters into account.
- making sure factory/mixin arguments are always explicit.
Conflicts:
hb.elpi
CohenCyril edited PR #142 Bugfix: forgotten parameters from new_nix
to master
:
New nix config
CohenCyril pushed 1 commit to branch new_nix.
CohenCyril updated PR #142 Bugfix: forgotten parameters from new_nix
to master
.
CohenCyril edited PR #142 New nix config from new_nix
to master
.
CohenCyril pushed 1 commit to branch new_nix.
CohenCyril updated PR #142 New nix config from new_nix
to master
.
gares pushed 1 commit to branch rm-hack-discharge.
gares updated PR #137 Removed hack for discharging on 8.13 from rm-hack-discharge
to master
.
gares edited PR #137 Removed hack for discharging from rm-hack-discharge
to master
.
gares pushed 1 commit to branch rm-hack-discharge.
gares updated PR #137 Removed hack for discharging from rm-hack-discharge
to master
.
gares requested CohenCyril for a review on PR #137 Removed hack for discharging.
gares edited PR #137 Removed hack for discharging from rm-hack-discharge
to master
:
Fix #132
gares submitted PR Review for #142 New nix config.
gares created PR Review Comment on #142 New nix config:
Did you forget to commit meta.yml?
CohenCyril merged PR #142 New nix config.
CohenCyril pushed 2 commits to branch master.
gares submitted PR Review for #142 New nix config.
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
CohenCyril submitted PR Review for #142 New nix config.
CohenCyril created PR Review Comment on #142 New nix config:
No...
CohenCyril pushed 1 commit to branch nocomment.
CohenCyril submitted PR Review for #142 New nix config.
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...
(seriouslyx: y
!)
CohenCyril opened PR #143 removing comment from nocomment
to master
.
gares pushed 1 commit to branch rm-hack-discharge.
gares updated PR #137 Removed hack for discharging from rm-hack-discharge
to master
.
CohenCyril pushed 1 commit to branch withNES.
CohenCyril opened PR #144 NES in HB from withNES
to master
.
gares pushed 2 commits to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
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:
- [x]
indexed
,unify
,nomsg
end up in the final terms but are in HB/structures.v, where do we move these? Do we need these?Status:
- it works (round trips)
- impacted by https://github.com/coq/coq/issues/13843 (I removed all empty structures)
- quality of the logged code is impacted by (the lack of in 8.13) https://github.com/coq/coq/pull/13840
- hack for command locations to be removed once https://github.com/coq/coq/pull/13844 is merged
gares merged PR #143 removing comment.
gares pushed 2 commits to branch master. Commits by CohenCyril (1) and gares (1).
gares deleted the branch nocomment.
gares pushed 1 commit to branch rm-hack-discharge.
gares updated PR #137 Removed hack for discharging from rm-hack-discharge
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
CohenCyril pushed 1 commit to branch logging-vernac.
CohenCyril updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
CohenCyril pushed 1 commit to branch withNES.
CohenCyril updated PR #144 NES in HB from withNES
to master
.
gares deleted the branch new_nix.
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
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
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares assigned Issue #140 #[infer(var = "R", from ="Type")] (assigned to gares).
gares pushed 2 commits to branch phant-params.
gares opened PR #146 Phant params from phant-params
to master
:
Fix #140
gares edited PR #146 inference of structures on paramters from phant-params
to master
.
gares pushed 1 commit to branch phant-params.
gares updated PR #146 inference of structures on paramters from phant-params
to master
.
gares pushed 1 commit to branch phant-params.
gares updated PR #146 inference of structures on paramters from phant-params
to master
.
gares requested CohenCyril for a review on PR #146 inference of structures on paramters.
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 asP = "Type"
.Fix #140
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 asP = "Type"
.Fix #140
gares pushed 1 commit to branch phant-params.
gares updated PR #146 inference of structures on paramters from phant-params
to master
.
gares pushed 1 commit to branch phant-params.
gares updated PR #146 inference of structures on paramters from phant-params
to master
.
gares pushed 3 commits to branch master.
gares closed Issue #132 Remove arguments that are there just to force discharging:
Blocked by https://github.com/LPCIC/coq-elpi/issues/210
gares merged PR #137 Removed hack for discharging.
gares deleted the branch rm-hack-discharge.
gares pushed 2 commits to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
CohenCyril pushed 1 commit to branch logging-vernac.
CohenCyril updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
CohenCyril pushed 1 commit to branch logging-vernac.
CohenCyril updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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
gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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
gares submitted PR Review for #146 inference of structures on paramters.
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),
gares pushed 1 commit to branch phant-params.
gares updated PR #146 inference of structures on paramters from phant-params
to master
.
gares pushed 6 commits to branch phant-params.
gares updated PR #146 inference of structures on paramters from phant-params
to master
.
CohenCyril pushed 1 commit to branch exports.
CohenCyril opened PR #147 Managing Exports from exports
to master
.
gares submitted PR Review for #147 Managing Exports.
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. *)
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. *)
gares submitted PR Review for #147 Managing Exports.
gares pushed 1 commit to branch exports.
gares updated PR #147 Managing Exports from exports
to master
.
gares pushed 1 commit to branch exports.
gares updated PR #147 Managing Exports from exports
to master
.
gares submitted PR Review for #147 Managing Exports.
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. >>> *)
gares pushed 1 commit to branch exports.
gares updated PR #147 Managing Exports from exports
to master
.
gares opened Issue #148 #[export] HB.instance:
Elaborates to
Module Exports$rand. HB.instance ... End Exports$rand. HB.export Exports$rand.
CohenCyril pushed 1 commit to branch exports.
CohenCyril updated PR #147 Managing Exports from exports
to master
.
gares submitted PR Review for #147 Managing Exports.
gares created PR Review Comment on #147 Managing Exports:
Note that the list of modules to be exported is stored in the current module,
gares pushed 1 commit to branch exports.
gares updated PR #147 Managing Exports from exports
to master
.
CohenCyril merged PR #147 Managing Exports.
CohenCyril pushed 7 commits to branch master. Commits by gares (4) and CohenCyril (3).
CohenCyril deleted the branch exports.
CohenCyril pushed 1 commit to branch phant-params.
CohenCyril updated PR #146 inference of structures on paramters from phant-params
to master
.
CohenCyril pushed 7 commits to branch phant-params. Commits by gares (6) and CohenCyril (1).
CohenCyril updated PR #146 inference of structures on paramters from phant-params
to master
.
gares pushed 1 commit to branch ci-ssralg.
gares opened PR #149 ci job to test ssralg from ci-ssralg
to master
.
CohenCyril closed Issue #140 #[infer(var = "R", from ="Type")] (assigned to gares).
CohenCyril merged PR #146 inference of structures on paramters.
CohenCyril pushed 8 commits to branch master. Commits by gares (6) and CohenCyril (2).
CohenCyril deleted the branch phant-params.
gares pushed 1 commit to branch ci-ssralg.
gares updated PR #149 ci job to test ssralg from ci-ssralg
to master
.
gares pushed 1 commit to branch ci-ssralg.
gares updated PR #149 ci job to test ssralg from ci-ssralg
to master
.
gares opened Issue #150 performance problem of instance declaration.
CohenCyril pushed 1 commit to branch nixci.
CohenCyril opened PR #151 experimenting with nix ci from nixci
to master
.
CohenCyril pushed 1 commit to branch nixci.
CohenCyril updated PR #151 experimenting with nix ci from nixci
to master
.
CohenCyril pushed 1 commit to branch nixci.
CohenCyril updated PR #151 experimenting with nix ci from nixci
to master
.
CohenCyril pushed 1 commit to branch nixci.
CohenCyril updated PR #151 experimenting with nix ci from nixci
to master
.
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)))
CohenCyril pushed 1 commit to branch nixci.
CohenCyril updated PR #151 experimenting with nix ci from nixci
to master
.
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
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
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
CohenCyril merged PR #151 experimenting with nix ci.
CohenCyril pushed 1 commit to branch master.
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
gares closed without merge PR #149 ci job to test ssralg.
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
gares edited Issue #150 performance problem of instance declaration:
From the very last instance in ssralg.v, sprinkling
{gettimeofday}
incoq.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
CohenCyril deleted the branch nixci.
CohenCyril pushed 6 commits to branch nixci.
CohenCyril pushed 1 commit to branch nixci.
CohenCyril opened PR #152 local cache from nixci
to master
.
CohenCyril pushed 1 commit to branch nixci.
CohenCyril updated PR #152 local cache from nixci
to master
.
CohenCyril pushed 1 commit to branch nixci.
CohenCyril updated PR #152 local cache from nixci
to master
.
CohenCyril pushed 1 commit to branch nixci.
CohenCyril updated PR #152 local cache from nixci
to master
.
CohenCyril pushed 1 commit to branch nixci.
CohenCyril updated PR #152 local cache from nixci
to master
.
CohenCyril pushed 1 commit to branch nixci.
CohenCyril updated PR #152 local cache from nixci
to master
.
CohenCyril merged PR #152 local cache.
CohenCyril pushed 1 commit to branch master.
CohenCyril deleted the branch nixci.
gares pushed 2 commits to branch dont-be-silly.
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 stores.phant_Build crap
instead ofs.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
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 stores.phant_Build crap
instead ofs.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 containedphant_Build crap
)CC @CohenCyril @pi8027
CohenCyril pushed 1 commit to branch metanix.
CohenCyril opened PR #154 Trying out meta.yml with nix action from metanix
to master
.
CohenCyril pushed 1 commit to branch metanix.
CohenCyril updated PR #154 Trying out meta.yml with nix action from metanix
to master
.
CohenCyril pushed 1 commit to branch metanix.
CohenCyril updated PR #154 Trying out meta.yml with nix action from metanix
to master
.
CohenCyril pushed 1 commit to branch metanix.
CohenCyril updated PR #154 Trying out meta.yml with nix action from metanix
to master
.
CohenCyril pushed 1 commit to branch metanix.
CohenCyril updated PR #154 Trying out meta.yml with nix action from metanix
to master
.
CohenCyril pushed 1 commit to branch metanix.
CohenCyril updated PR #154 Trying out meta.yml with nix action from metanix
to master
.
CohenCyril pushed 1 commit to branch metanix.
CohenCyril updated PR #154 Trying out meta.yml with nix action from metanix
to master
.
CohenCyril submitted PR Review for #153 optimizations.
gares merged PR #153 optimizations.
gares pushed 3 commits to branch master.
gares deleted the branch dont-be-silly.
gares pushed 2 commits to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 2 commits to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
CohenCyril pushed 1 commit to branch new_nixpkgs.
CohenCyril opened PR #155 update nixpkgs from new_nixpkgs
to master
.
CohenCyril pushed 1 commit to branch nixupdate.
CohenCyril pushed 1 commit to branch metanix.
CohenCyril updated PR #154 Trying out meta.yml with nix action from metanix
to master
.
CohenCyril deleted the branch nixupdate.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
CohenCyril pushed 1 commit to branch logging-vernac.
CohenCyril updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
CohenCyril pushed 1 commit to branch new_nixpkgs.
CohenCyril updated PR #155 update nixpkgs from new_nixpkgs
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
CohenCyril merged PR #155 update nixpkgs.
CohenCyril pushed 1 commit to branch master.
CohenCyril deleted the branch new_nixpkgs.
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:
extraInstallFlags = [ "DESTDIR=$(out)" ];
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch fix-discharge.
gares opened PR #156 discharge by hand both mixins and factories from fix-discharge
to master
.
gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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??
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:
ahah it works!
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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
:-/
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:
I will hack around this...
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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 »
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:
ah I think I figured it out!
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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
andCOQMF_COQLIB
!!
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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}" ];
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:
Can I rebase and push?
gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:
I will!
CohenCyril pushed 11 commits to branch logging-vernac. Commits by gares (9) and CohenCyril (2).
CohenCyril updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
CohenCyril pushed 1 commit to branch logging-vernac. Commits by gares (1).
CohenCyril updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch nicer-error-messages.
gares opened PR #157 nicer error messages for non ground terms from nicer-error-messages
to master
.
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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.
CohenCyril edited PR Review Comment on #131 logging: HB prints its effect in term of vernac commands.
gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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
gares pushed 1 commit to branch update-doc.
gares opened PR #158 update the doc from update-doc
to master
.
gares pushed 1 commit to branch update-doc.
gares updated PR #158 update the doc from update-doc
to master
.
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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?
gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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
.
gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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.
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
gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
gares edited PR Review Comment on #131 logging: HB prints its effect in term of vernac commands.
gares merged PR #158 update the doc.
gares pushed 3 commits to branch master.
gares deleted the branch update-doc.
gares merged PR #157 nicer error messages for non ground terms.
gares pushed 2 commits to branch master.
gares deleted the branch nicer-error-messages.
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:
Nice!
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:
Mmmh, are you sure though...
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:
where did you find this?
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
CohenCyril created PR Review Comment on #131 logging: HB prints its effect in term of vernac commands:
is it a configureflag?
CohenCyril edited PR Review Comment on #131 logging: HB prints its effect in term of vernac commands.
CohenCyril edited PR Review Comment on #131 logging: HB prints its effect in term of vernac commands.
gares pushed 2 commits to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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
gares submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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.
CohenCyril submitted PR Review for #131 logging: HB prints its effect in term of vernac commands.
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...
gares pushed 2 commits to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 2 commits to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 2 commits to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 3 commits to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
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:
- [x]
indexed
,unify
,nomsg
end up in the final terms but are in HB/structures.v, where do we move these? Do we need these?Status:
- it works (round trips)
- impacted by https://github.com/coq/coq/issues/13843 (I removed all empty structures)
- broken by https://github.com/coq/coq/issues/13875 (could not find a workaround)
- quality of the logged code is impacted by (the lack of in 8.13) https://github.com/coq/coq/pull/13840
- hack for command locations to be removed once https://github.com/coq/coq/pull/13844 is merged
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 1 commit to branch fix-discharge.
gares updated PR #156 discharge by hand both mixins and factories from fix-discharge
to master
.
gares merged PR #156 discharge by hand both mixins and factories.
gares pushed 3 commits to branch master.
gares deleted the branch fix-discharge.
gares assigned Issue #139 #[index="R"] (assigned to gares).
gares assigned Issue #127 Using indexed
is too fragile (assigned to gares):
We should replace by another kind of meta information.
gares pushed 1 commit to branch kill-ty-deps.
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
gares pushed 1 commit to branch kill-ty-deps.
gares updated PR #159 kill ty-deps: add gref-deps for each factory and operation from kill-ty-deps
to master
.
gares pushed 1 commit to branch kill-ty-deps.
gares updated PR #159 kill ty-deps: add gref-deps for each factory and operation from kill-ty-deps
to master
.
gares pushed 1 commit to branch kill-ty-deps.
gares updated PR #159 kill ty-deps: add gref-deps for each factory and operation from kill-ty-deps
to master
.
gares edited PR #159 kill ty-deps, long live #[key="T"] from kill-ty-deps
to master
.
gares pushed 2 commits to branch kill-ty-deps.
gares updated PR #159 kill ty-deps, long live #[key="T"] from kill-ty-deps
to master
.
gares pushed 1 commit to branch kill-ty-deps.
gares updated PR #159 kill ty-deps, long live #[key="T"] from kill-ty-deps
to master
.
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!
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
gares pushed 1 commit to branch kill-ty-deps.
gares updated PR #159 kill ty-deps, long live #[key="T"] from kill-ty-deps
to master
.
gares pushed 1 commit to branch kill-ty-deps.
gares updated PR #159 kill ty-deps, long live #[key="T"] from kill-ty-deps
to master
.
gares pushed 1 commit to branch xdot.
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
gares pushed 1 commit to branch xdot.
gares updated PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot
to master
.
gares pushed 1 commit to branch xdot.
gares updated PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot
to master
.
gares pushed 1 commit to branch xdot.
gares updated PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot
to master
.
gares edited 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
gares submitted PR Review for #160 HB.status handles the #[dot] and #[dot(file=..)] attributes.
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
gares pushed 1 commit to branch xdot.
gares updated PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot
to master
.
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
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
gares submitted PR Review for #159 kill ty-deps, long live #[key="T"]
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],
gares submitted PR Review for #159 kill ty-deps, long live #[key="T"]
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,
gares pushed 1 commit to branch kill-ty-deps.
gares updated PR #159 kill ty-deps, long live #[key="T"] from kill-ty-deps
to master
.
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
gares milestoned Issue #160 HB.status handles the #[dot] and #[dot(file=..)] attributes:

Because we can... and because I'm in procrastination mode.
CC @affeldt-aist
gares pushed 1 commit to branch master.
gares pushed 1 commit to branch xdot.
gares updated PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot
to master
.
gares pushed 1 commit to branch xdot.
gares updated PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot
to master
.
gares edited 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
CohenCyril edited PR Review Comment on #131 logging: HB prints its effect in term of vernac commands.
CohenCyril closed Issue #139 #[index="R"] (assigned to gares).
CohenCyril closed Issue #127 Using indexed
is too fragile (assigned to gares):
We should replace by another kind of meta information.
CohenCyril closed Issue #93 Error message "BUG: ty-deps ..." should suggest to put indexed
around the type.
CohenCyril merged PR #159 kill ty-deps, long live #[key="T"]
CohenCyril pushed 8 commits to branch master. Commits by gares (7) and CohenCyril (1).
coqbot-app[bot] milestoned Issue #139 #[index="R"] (assigned to gares).
coqbot-app[bot] milestoned Issue #93 Error message "BUG: ty-deps ..." should suggest to put indexed
around the type.
gares pushed 2 commits to branch cleanup.
gares opened PR #161 Cleanup from cleanup
to master
.
gares merged PR #161 Cleanup.
gares pushed 3 commits to branch master.
gares deleted the branch cleanup.
gares pushed 1 commit to branch xdot.
gares updated PR #160 HB.status handles the #[dot] and #[dot(file=..)] attributes from xdot
to master
.
gares edited PR #160 HB.graph "file.dot". from xdot
to master
.
gares pushed 1 commit to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed 3 commits to branch logging-vernac.
gares updated PR #131 logging: HB prints its effect in term of vernac commands from logging-vernac
to master
.
gares pushed the branch cleanup2.
gares opened PR #162 Cleanup from logging vernac from cleanup2
to master
.
gares pushed 1 commit to branch cleanup2.
gares updated PR #162 Cleanup from logging vernac from cleanup2
to master
.
gares pushed 1 commit to branch cleanup2.
gares updated PR #162 Cleanup from logging vernac from cleanup2
to master
.
gares requested CohenCyril for a review on PR #162 Cleanup from logging vernac.
CohenCyril pushed 1 commit to branch intermediate_sort.
CohenCyril pushed 1 commit to branch intermediate_sort.
CohenCyril opened PR #163 attributes "nocoercion" and "arg_sort" from intermediate_sort
to master
:
- "nocoercion" to turn off the coercion on
sort
- "arg_sort" adds an intermediate coercion class
arg_sort
as documented in the header of fingroup.v
CohenCyril edited PR #163 attributes "nocoercion" and "arg_sort" from intermediate_sort
to master
:
- "nocoercion" to turn off the coercion on
sort
- "arg_sort" adds an intermediate coercion class
arg_sort
as documented in the header of fingroup.vcf https://github.com/math-comp/math-comp/pull/new/hierarchy-builder-fingroup
CohenCyril edited PR #163 attributes "nocoercion" and "arg_sort" from intermediate_sort
to master
:
- "nocoercion" to turn off the coercion on
sort
- "arg_sort" adds an intermediate coercion class
arg_sort
as documented in the header of fingroup.vcf https://github.com/math-comp/math-comp/tree/46efb5c7e224b367b24e776d682118ddb623bec3
CohenCyril edited PR #163 attributes "nocoercion" and "arg_sort" from intermediate_sort
to master
:
- "nocoercion" to turn off the coercion on
sort
- "arg_sort" adds an intermediate coercion class
arg_sort
as documented in the header of fingroup.vcf https://github.com/math-comp/math-comp/tree/hierarchy-builder-fingroup/mathcomp
CohenCyril merged PR #162 Cleanup from logging vernac.
CohenCyril pushed 4 commits to branch master. Commits by gares (3) and CohenCyril (1).
CohenCyril pushed 1 commit to branch intermediate_sort.
CohenCyril updated PR #163 attributes "nocoercion" and "arg_sort" from intermediate_sort
to master
.
CohenCyril pushed 1 commit to branch intermediate_sort.
CohenCyril updated PR #163 attributes "nocoercion" and "arg_sort" from intermediate_sort
to master
.
gares pushed 8 commits to branch cleanup3.
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.
gares pushed 4 commits to branch cleanup3.
gares updated PR #164 small cleanup from cleanup3
to master
.
CohenCyril pushed 1 commit to branch intermediate_sort.
CohenCyril updated PR #163 attributes "nocoercion" and "arg_sort" from intermediate_sort
to master
.
CohenCyril edited PR #163 Attribute "arg_sort" from intermediate_sort
to master
.
CohenCyril edited PR #163 Attribute "arg_sort" from intermediate_sort
to master
:
"arg_sort" adds an intermediate coercion class
arg_sort
as
documented in the header of fingroup.v
cf https://github.com/math-comp/math-comp/tree/hierarchy-builder-fingroup/mathcomptest against hierarchy-builder math-comp branch
gares submitted PR Review for #163 Attribute "arg_sort"
CohenCyril pushed 1 commit to branch intermediate_sort.
CohenCyril updated PR #163 Attribute "arg_sort" from intermediate_sort
to master
.
CohenCyril pushed 1 commit to branch intermediate_sort.
CohenCyril updated PR #163 Attribute "arg_sort" from intermediate_sort
to master
.
gares pushed 6 commits to branch separate-commands.
gares pushed 1 commit to branch separate-commands.
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
gares pushed 1 commit to branch separate-commands.
gares updated PR #165 Separate commands from separate-commands
to master
.
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 36 HB/context.elpi 22 HB/export.elpi 269 HB/factory.elpi 188 HB/instance.elpi 35 HB/README.md 50 HB/status.elpi 528 HB/structure.elpi 95 HB/common/coq-vernac.elpi 302 HB/common/database.elpi 235 HB/common/phant-abbreviation.elpi 147 HB/common/synthesis.elpi 404 HB/common/utils.elpi 2510 total
CohenCyril pushed 1 commit to branch intermediate_sort.
CohenCyril updated PR #163 Attribute "arg_sort" from intermediate_sort
to master
.