Zulip Chat Archive

Stream: general

Topic: mathlib directories

Reid Barton (Dec 20 2018 at 21:27):

Not sure whether joke suggestion: one top-level directory per arXiv primary category.

Mario Carneiro (Dec 20 2018 at 21:28):

lol they are all physics

Patrick Massot (Dec 20 2018 at 21:28):

https://arxiv.org/archive/math

Reid Barton (Dec 20 2018 at 21:28):

I had in mind https://arxiv.org/archive/math, though one could include at least the CS ones as well

Mario Carneiro (Dec 20 2018 at 21:29):

which one is data?

Reid Barton (Dec 20 2018 at 21:31):

there's always math.GM - General Mathematics, though it's not totally clear to me that data should exist in the first place

Reid Barton (Dec 20 2018 at 21:31):

though it's indeed unclear where many of the contents of data would be categorized

Kenny Lau (Dec 20 2018 at 21:33):

one has to ask the question: why is [insert file name] not included in data/?

Mario Carneiro (Dec 20 2018 at 21:42):

I would broadly categorize it as "stuff useful for programming, but not meta"

Scott Morrison (Dec 21 2018 at 01:30):

I think we should reserve the /math.GM/ folder for crank contributions to mathlib, keeping with tradition. Maybe we could hardcode leanpkg to not compile math.GM unless you are a "contributor" to that folder?

Last updated: Dec 20 2023 at 11:08 UTC