Zulip Chat Archive

Stream: new members

Topic: Making a contribution to mathlib - lattice ordered groups

Christopher Hoskin (Aug 13 2021 at 19:46):

Hello, I'd like to offer a contribution to mathlib - a basic theory of lattice ordered groups: https://github.com/leanprover-community/mathlib/pull/8663

If this is of interest, please could I have write access to non-master branches of the mathlib repository? My GitHub username is mans0954.

Thank you,

Christopher Hoskin

Johan Commelin (Aug 13 2021 at 20:01):


Alex J. Best (Aug 13 2021 at 20:35):

@Christopher Hoskin once you've accepted the invite you can open a new version of that PR from a branch on mathlib and the CI will run on it.

Yury G. Kudryashov (Aug 13 2021 at 20:39):

Note that we have docs#covariant_class and docs#contravariant_class.

Alex J. Best (Aug 13 2021 at 20:53):

Some random thoughts from looking over the code, it looks pretty good overall!:

  • You use simp in some places where it doesn't close the goal (pos_meet_neg_eq_zero), this is called a non-terminal simp and is generally discouraged as if the set of simp lemmas later changes (someone adds a new simplification perhaps) it can break your proof, its better in such situations to change simp to squeeze_simp which will output a call to simp only [...] instead that will be more robust.
  • In lemmas like join_eq_add_pos_sub the proof is a pure calc block, so doesn't need to be in a begin... end just := calc ... will do.
  • Some of your very short proofs in tactic more are term mode one-liners, like lemma pos_sub_neg' (a : α) : a⁺ - a⁻ = a := (pos_sub_neg _).symm getting more experience with writing direct lean terms like this is always helpful to get rid of small goals faster.
  • if you have multiple rewrites in a row they can be combined like rw a, rw b, is equivalent to rw [a, b]
  • are you aware of tactic#library_search? in abs_pos_eq where you write -- I feel there ought to be a simpler way of finishing from here? putting instead library_search tells me the proof can be finished with exact nsmul_nonneg h 2, instead.

Patrick Massot (Aug 13 2021 at 21:04):

You should also read https://leanprover-community.github.io/contribute/style.html, especially the part about braces.

Christopher Hoskin (Aug 14 2021 at 07:59):

Thanks, I've created a branch within mathlib, but the CI is failing with the message "Error: ERR_RNT: Reserved notation outside tactic.reserved_notation" https://github.com/leanprover-community/mathlib/runs/3328082790

Having looked in reserved_notation it's not obvious to me what I've done wrong. Is there a way of seeing which line it's failing at?


Julian Berman (Aug 14 2021 at 08:03):

CI is hiding that for some reason (I have vague recollection there's desire to make that integrate better with the GitHub UI which is why that happened). Running it locally (by running ./scripts/lint-style.sh) it shows me:

:error file=src/algebra/lattice_ordered_group.lean,line=214,code=ERR_RNT::ERR_RNT: Reserved notation outside tactic.reserved_notation
::error file=src/algebra/lattice_ordered_group.lean,line=222,code=ERR_RNT::ERR_RNT: Reserved notation outside tactic.reserved_notation

Eric Wieser (Aug 14 2021 at 08:04):

The error message is also visible at https://github.com/leanprover-community/mathlib/compare/lattice_ordered_group

Eric Wieser (Aug 14 2021 at 08:04):

Where it is attached to the correct line number

Last updated: Dec 20 2023 at 11:08 UTC