## Stream: general

### 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 all.lean?

#### 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