Minutes December 14 2022
Participants: Cyril, Enrico, Pierre, Julien, Yves
Reference:
Pierre: Is this really used? Cyril: Not yet clear what to do. To take care of it.
port to HB #733
+++ algebra/finalg.v
+(* FIXME: add to HB or define directly type instead of type_ *)
+Identity Coercion lmodtype_id : Lmodule.type >-> Lmodule.type_.
Cyril Cohen 2021-05-10 15:26 Several fixes
~~> actual TODO? (x4 in that file)Cyril: isn't this functionality infer? Add just before HB.structure.
TODO: test
Cyril: No, actually the infer is already here...
Not a blocking issue.
Enrico: what happens if we declare twice the same identity coercion?
Not sure...
Pierre: actually, removing the Identity Coercion things are fine with HB 1.4.0.
+ (* FIXME: we would have expected GRing.DecidableField.axiom *)
+ Lemma decidable : GRing.decidable_field_axiom sat.
Pierre Roux 2021-04-08 Start porting finalg.v
~~> ?The same axiom has two names, replacing should be ok.
+++ algebra/ssralg.v
+(* TODO: HB.instance Definition _ : ComUnitRing_isIntegral R^o := alias R. *)
+HB.instance Definition regular_integral : ComUnitRing_isIntegral R^o :=
+ ComUnitRing_isIntegral.Build (R^o) mulf_eq0_subproof.
thery 2021-04-08 Rename Ring_IsIntegral by ComUnitRing_IsIntegral and UnitRing_IsDec by Field_IsDec
~~> ?Future request by Laurent?
Laurent: Coq was not recognizing R so we created an alias?
Enrico: does alias correspond to light factories?
Pierre: Try IntegralDomain.on R^o?
Cyril: Does not work, certainly because some structure has changed in between.
The problem might come from the order in which we declare the structures.
Guess: there is an instance before that is ill-defined. Problem fixed during
the meeting by Cyril. It was a matter to define xxx2 using .on
instead of doing it by hand (which breaks convertibility of mixins but that
is not the only problem).
+++ ssreflect/tuple.v
+(* TODO: try to factor this into a single instance *)
+HB.instance Definition tuple_hasChoice n (T : choiceType) :=
+ [hasChoice of n.-tuple T by <:].
+HB.instance Definition tuple_isCountable n (T : countType) :=
+ [isCountable of n.-tuple T by <:].
Enrico Tassi 2021-04-01 16:21 Partial port to HB
~~> not sure how this could be factored, the hypotheses (type of T) are not the same?Pierre: nothing we can do?
Cyril: this is a non-trivial extension of HB to do.
TODO: open an issue in HB
+++ test_suite/test_regular_conv.v
+(* TODO: commented out with HB port *)
+(*
Pierre Roux 2022-09-08 11:24 "Fix" test-suite
~~> ?Pierre: test that were commented out, equality between named structures and Pack/Class. Do we really want to keep these tests?
Cyril: we can recover these tests with their HB versions, we had these tests to test forgetful inheritance
TODO: restore tests
NB: Enrico has added a page on HB's wiki: https://github.com/math-comp/hierarchy-builder/wiki/Copy-of-instances-over-convertible-types
Laurent: should we get rid of .on and use systematically .copy?
Enrico: that would help for the documentation
Cyril: .on and .copy are really two different functionalities
Cyril: no all .on are no-ops but we might want to change HB so that
.on are not necessary anymore
Laurent: order.v:5634, why is there a .on on seq? this is because
it is a local alias
Cyril: coqdoc does not document constructs built by coq-elpi
Enrico: to create an issue
Cyril: could we use About instead of HB.About`?
Pierre: this is related to our older intent to have docstrings to document