Topic: import all files
Floris van Doorn (Jul 29 2019 at 19:12):
I want a file that imports all files in mathlib. I don't think that there is currently a good way to do that.
Shall I make a PR that for every folder in
src/ creates a file
all.lean which imports all files in that folder?
Simon Hudon (Jul 29 2019 at 19:15):
What do you need that for?
Floris van Doorn (Jul 29 2019 at 19:19):
I want to write some commands to clean up stuff in mathlib. For example, I have a command now that detects all declarations in all imported files with an argument that is unused. This is often by mistake.
Simon Hudon (Jul 29 2019 at 19:24):
I wouldn't want to commit those
all files in mathlib but you could write a command that generates them when you want to run that command. We can even get Travis to run it
Floris van Doorn (Jul 29 2019 at 19:25):
that is reasonable.
Simon Hudon (Jul 29 2019 at 19:27):
I would also like a command to cleanup those files please
Johan Commelin (Jul 29 2019 at 19:44):
ls -R | grep all.*lean | xargs rm
Simon Hudon (Jul 29 2019 at 20:06):
If we use a sh/bash script to do the automation, that makes sense (almost) but if it's scripted from within Lean, let's do the deletion in Lean too
Floris van Doorn (Jul 29 2019 at 21:18):
I'm currently writing an sh script to making these
all.lean files. Is there a way of doing it inside Lean? Using the io monad?
Simon Hudon (Jul 29 2019 at 21:23):
Yes, Lean has a file interface that you can use
Scott Morrison (Jul 29 2019 at 21:53):
Is there actually anything wrong with having a permanent
Simon Hudon (Jul 29 2019 at 21:56):
Yes, we need to update it routinely for it to be useful, that's not a useful maintenance burden to take on. Also, it doesn't go in the direction of minimizing dependencies. Finally, it's not a feature of mathlib, it's an implementation of a tool
Scott Morrison (Jul 29 2019 at 21:59):
Ok! :-) Somehow I hadn't thought about the need to constantly update...
Floris van Doorn (Jul 29 2019 at 22:02):
See PR #1281. If we ever decide to add the
all.lean files to mathlib, we can also use the
mk_all script to update.
Simon Hudon (Jul 29 2019 at 22:06):
Sorry, I feel like I'm being curt. It's just I think it's really not worth it. It's better to add
mk_all in the build system so that we can be sure that they are up to date when we need them
Floris van Doorn (Jul 29 2019 at 22:17):
I'm fine with that.
Last updated: May 08 2021 at 04:14 UTC