Scott Morrison (Sep 25 2020 at 04:46):
I would like to slice
category_theory/limits/limits.lean into smaller files, as it has become unwieldy. @Johan Commelin, @Bhavik Mehta, @Markus Himmel, @Reid Barton
The first thing I would like to do is separate out the
is_limit stuff from the
has_limit stuff (presumably into files with those names). There's also a variety of rarely used API (e.g. equivalent formulations of limit conditions in terms of yoneda) that I might just break into their own files.
The change I'm not sure about is whether to split everything to two sets of parallel files, once for limits, once for colimits.
- better parallelism while compiling (or just faster if you only need one side)
- perhaps easier to keep thing in sync by opening the files side by side
- perhaps harder to keep things in sync by forgetting about the other file...
Happy to follow any expressed preferences here.
Johan Commelin (Sep 25 2020 at 05:16):
I don't have strong reasons, but I slightly favour the two-files version, I think.
Bhavik Mehta (Sep 25 2020 at 13:30):
I slightly prefer the one-file version, partially because the splitting might need to happen for special shapes and anything else which uses limits, so I think the maintainability problem could get tough. That said opening the files side by side seems like a good way round this; so I'd be happy with either decision. Obviously though it would be great if we could automatically dualise :)
Scott Morrison (Sep 26 2020 at 01:29):
I think I might try a compromise: I'll split
has_colimit.lean, but not plan to split the special shapes files into dual pairs.
Last updated: May 18 2021 at 06:15 UTC