Conversation
| (* Ring-like structures *) | ||
| (* *) | ||
| (* This file re-exports the contents of rings_modules_and_algebras.v, *) | ||
| (* divalg.v, decfield.v, countalg.v, finalg.v, and ring_quotient.v: *) |
There was a problem hiding this comment.
according to the above:
| (* divalg.v, decfield.v, countalg.v, finalg.v, and ring_quotient.v: *) | |
| (* divalg.v, decfield.v, countalg.v and finalg.v: *) |
but maybe it would be easier to say "the content of the algebraic_hierarchy directory". I observed that these header comments tend to become easily inaccurate with time.
There was a problem hiding this comment.
IMO, the idea is rather to use the header doc of algebra_hierarchy.v as the general description of the files in the directory (like order.v).
There was a problem hiding this comment.
(In addition, maybe we could have one line README.md in each directory saying something like "look at [order.v]")
There was a problem hiding this comment.
And indeed, I forgot to export ring_quotient here. Fixed.
Do we really want to do that? These are maybe not of such general use but adding them could make the
Still not a big fan of this mixing between file renaming and deprecations removal (it just makes the renaming harder for users). However, see my comments for mitigation recommendations. |
I suggest discussing this point in a meeting. Perhaps the general recommendation for users should be to import only what they need (most of the time only |
|
By the way, I don't think it's very useful to review this PR in detail before merging #1560. |
|
I was just reacting to
above (but maybe these are automatic, I never really mastered them). |
7b721cf to
870daf7
Compare
| From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq nmodule. | ||
| From mathcomp Require Import preorder. | ||
| From mathcomp Require Export ssralg. | ||
| From mathcomp Require Import rings_modules_and_algebras divalg. |
There was a problem hiding this comment.
@proux01 Do you know why ssralg was exported here and also in field_tactic.v? (It looks like we need to turn them into Import to fix some breakages in CI.)
There was a problem hiding this comment.
Or we need to export decfield here, even though it is not needed here. Otherwise Import GRing.Theory doesn't import the right GRing.Theory module.
There was a problem hiding this comment.
Ok, now I see that not exporting ssralg here breaks hmap_ops.v in the graph-theory library because it imports ring_tactic but not rings_modules_and_algebras, and it cannot find the semiring instance on nat. I think the right fix is to explicitly import rings_modules_and_algebras there.
There was a problem hiding this comment.
I agree, graph-theory should be fixed (overlay to merge before the current PR).
There was a problem hiding this comment.
I decided to revert the change and suppress the warning since I'm not going to write the overlay.
870daf7 to
dda0abf
Compare
b3062fa to
9f04928
Compare
…lg.v and ssrnum.v
9f04928 to
22b3107
Compare
|
CI green. This PR is ready. |
Motivation for this change
This is the remaining work from #1582.
Closes #1505
Closes #1557
The difference between
ssralg.vandalgebraic_hierarchy.v:countalg.v,finalg.v, andring_quotient.v(because this PR moves them toalgebraic_hierarchy/)nmodule.v(because it belongs to the boot package)ssralg.vThe difference between
ssrnum.vandnumeric_hierarchy.v:orderedzmod.v(because Moveorderedzmod.vfromalgebra/numeric_hierarchy/toorder/#1560 moves it to the order package)Num.ExtraDef.sqrtrDependency
orderedzmod.vfromalgebra/numeric_hierarchy/toorder/#1560Overlay
Minimal TODO list
doc/changelog/make-entry.shSee this Checklist for details.
Automatic note to reviewers
Read this Checklist.