Zulip Chat Archive

Stream: general

Topic: import all files


view this post on Zulip 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?

view this post on Zulip Simon Hudon (Jul 29 2019 at 19:15):

What do you need that for?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Floris van Doorn (Jul 29 2019 at 19:25):

that is reasonable.

view this post on Zulip Simon Hudon (Jul 29 2019 at 19:27):

I would also like a command to cleanup those files please

view this post on Zulip Johan Commelin (Jul 29 2019 at 19:44):

ls -R | grep all.*lean | xargs rm

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Simon Hudon (Jul 29 2019 at 21:23):

Yes, Lean has a file interface that you can use

view this post on Zulip Scott Morrison (Jul 29 2019 at 21:53):

Is there actually anything wrong with having a permanent all.lean?

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 29 2019 at 21:59):

Ok! :-) Somehow I hadn't thought about the need to constantly update...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Floris van Doorn (Jul 29 2019 at 22:17):

I'm fine with that.


Last updated: May 08 2021 at 04:14 UTC