Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC