Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

update reenableeta #4009

Merged
merged 134 commits into from
May 15, 2023
Merged

update reenableeta #4009

merged 134 commits into from
May 15, 2023

Conversation

gebner
Copy link
Member

@gebner gebner commented May 15, 2023

Open in Gitpod

eric-wieser and others added 30 commits May 8, 2023 22:44
@eric-wieser
fix: make ConcreteCategory.Forget reducible (#3857)
9bac7ff 
This seems to help in downstream files, [See Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/typeclass.20inference.20not.20seeing.20through.20reducible.20definition/near/356130343)
@MonadMaverick @Komyyy
@ChrisHughes24 @Parcly-Taxel
feat: port MeasureTheory.Measure.MeasureSpace (#3324)
773a35f 
This PR also renames instances in `MeasureTheory.MeasurableSpace`.



Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@dwrensha
fix: remove unneeded LibrarySearch import (#3854)
a2eec64 
Removes from `Analysis/SpecificLimits/Normed.lean` an `import Mathlib.Tactic.LibrarySearch` that was accidentally included in #3419.
@mattrobball
feat: port Topology.Category.Top.Limits.Cofiltered (#3855)
57b4fe5
@mattrobball
feat: port CategoryTheory.Preadditive.Injective (#3859)
5d7b89a
@int-y1
feat: port Topology.PartitionOfUnity (#3863)
47189ba
@Ruben-VandeVelde
chore: tidy various files (#3848)
66cb7cc
@xroblot
feat port: LinearAlgebra.ProjectiveSpace.Subspace (#3832)
3e2a20e
@int-y1
feat: port MeasureTheory.Measure.Sub (#3866)
d4ad63c
@mattrobball
feat: port Topology.Category.Top.Limits.Konig (#3853)
0533f14 
Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
@mattrobball
feat: port CategoryTheory.Preadditive.InjectiveResolution (#3860)
98de133 
Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
@int-y1
feat: port Probability.ProbabilityMassFunction.Basic (#3865)
68b21e1
@MonadMaverick @Komyyy @Parcly-Taxel
feat: port MeasureTheory.Measure.AEMeasurable (#3819)
9042f7b 
Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@semorrison @kbuzzard
@Parcly-Taxel @YaelDillies
feat: port CategoryTheory.Functor.Flat (#3703)
ddeaa9d 


Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@loefflerd
feat: port Analysis.NormedSpace.CompactOperator (#3805)
bb9f362
@kmill
feat: pp_extended_field_notation command to pretty print with dot not…
c93011c 
…ation (#3811)

The projection notation delaborator that comes from core Lean has some limitations. We introduce a new projection notation delaborator that is able to collapse parent projection sequences, for example `x.toC.toB.toA.val` into `x.val`.

The other limitation of the delaborator is that it can only handle true projections that do not have any additional arguments. This commit adds a `pp_extended_field_notation` command to switch on projection notation for specific functions. This command defines app unexpanders that pretty print that function application using dot notation.

The app unexpander it produces has a small hack to completely collapse parent projection sequences. Since it is an app unexpander, we do not have access to the actual types, so we use a heuristic that, for example with `A.foo`, if we are looking at `A.foo x.toA y z ...` then we can pretty print this as `x.foo y z`. The projection delaborator is able to collapse parent projection sequences except for the vary last one, so this finishes it off. Note that this heuristic can lead to output that does not round trip if there is a `toA` function that is not a parent projection that happens to be pretty printed with dot notation.
@MonadMaverick @Komyyy @Parcly-Taxel
feat: port MeasureTheory.Measure.MutuallySingular (#3818)
672941e 
Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@Komyyy @MonadMaverick
feat: port MeasureTheory.Lattice (#3824)
13d7a9c 
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: MonadMaverick <MonadMaverick@pm.me>
@int-y1
feat: port Analysis.Convex.PartitionOfUnity (#3868)
92aa9de
@MonadMaverick @Komyyy @Parcly-Taxel
feat: port MeasureTheory.Measure.OpenPos (#3820)
68ec219 
Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@Komyyy @MonadMaverick
feat: port Dynamics.Ergodic.MeasurePreserving (#3821)
3ae4023 
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: MonadMaverick <MonadMaverick@pm.me>
@mattrobball
feat: port Algebra.Category.Group.EquivalenceGroupAddGroup (#3861)
70f423b
@int-y1
feat: port MeasureTheory.Covering.VitaliFamily (#3867)
c7a6fc0
@int-y1
feat: port Topology.ContinuousFunction.LocallyConstant (#3877)
dcf5342
@kbuzzard @kmill
feat: add some pp_extended_field_notations (#3592)
ae6decd 
Add some `pp_extended_field_notation`, for opt-in cases with additional arguments.



Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@int-y1
feat: port Analysis.Normed.Group.ControlledClosure (#3880)
ebf0b75
@semorrison @Parcly-Taxel
feat: rewrites, a tactic to suggest rewrites. (#3119)
f2c85c3 
Unlike the very slow `rw_hint` long ago proposed (but never merged) for mathlib3, this uses discrimination trees (with keys given by LHS and RHS of lemmas), and looks up all subexpressions of the target expression.

- [x] depends on: #2898
- [x] depends on: #3181 

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
@semorrison
feat: tactic frontend for slim_check (#3114)
0774576 
Adds a tactic front end for `slim_check`, and provides commands `#test` and `#sample`.
Updates all the mathlib3 tests, although many are broken.

There are still some missing parts of `Mathlib.Testing.SlimCheck.Sampleable`: in particular we can't currently sample from lists, and this explains most of the broken tests.





Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
@int-y1
feat: port CategoryTheory.Abelian.Pseudoelements (#3843)
8ac1301 
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
@mattrobball @mo271
feat: port Topology.Category.Top.Limits.Products (#3709)
c2a84a8 
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
@gebner
Copy link
Member Author

gebner commented May 15, 2023

@mattrobball There's still a couple of "-e" files here.

@mattrobball
Copy link
Collaborator

@mattrobball There's still a couple of "-e" files here.

Thanks. I removed lean-e previously. This should remove the remainder.

@mattrobball
Copy link
Collaborator

mattrobball commented May 15, 2023 •
edited
Loading

Is the removable of the instance as in leanprover-community/mathlib#18986 still necessary? Everything seems to build fine unless I am missing something.

@semorrison
Copy link
Contributor

If it's not necessary to remove, I vote we revert the change, so we don't need to diagnose leanprover-community/mathlib#18986.

@gebner gebner merged commit a048b8c into reenableeta May 15, 2023
9 of 10 checks passed
@bors bors bot deleted the reenableeta_20230515 branch May 15, 2023 23:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet