Zulip Chat Archive

Stream: general

Topic: List categories def'd in lib?


view this post on Zulip Daniel Donnelly (Aug 28 2019 at 19:01):

For my app, I would like to list common categories like Set, etc. using Lean. Is there a simple script that can loop through a list of imports and do that? Find all definitions of type category (or something) within a namespace.

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 19:02):

If not that, then at least some of the commonly used categories

view this post on Zulip Simon Hudon (Aug 28 2019 at 19:09):

I don't know any such script so you might have to write one that generates a Lean file that imports all the category theory modules and list the instances of category

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 19:16):

@Simon Hudon that is a brilliant idea. I will do that right now in order to learn some more Lean coding.

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 19:17):

Is there a way to find out what all libs have category theory stuff in them or is that another scripting question (scriping in python)?

view this post on Zulip Simon Hudon (Aug 28 2019 at 19:18):

I believe @Floris van Doorn did something similar recently for his sanity check tool. His solution was to simply generate a file that imports everything in mathlib. That might be good enough for you as well

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 19:21):

I will do that right now. I'll learn more about importing from mathlib and the list feature

view this post on Zulip Johan Commelin (Aug 28 2019 at 19:22):

Isn't Floris's script now in the scripts/ subfolder?

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 19:25):

@Johan Commelin I didn't see anything with sanity check in it ;)

view this post on Zulip Simon Hudon (Aug 28 2019 at 19:29):

Have a look at:

https://github.com/leanprover-community/mathlib/commit/2e76f36444942e98d2fa59bbbbe03ed739bd9e68

view this post on Zulip Simon Hudon (Aug 28 2019 at 19:30):

This is where it is introduced. But the scripts that imports everything is scripts/mk_all.sh

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 19:31):

@Simon Hudon thx. I will bookmark this.

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 19:49):

One more thing about this. Should include mk_all.sh into bananacats or just simply have a Lean template .txt file that lists the output as I have just generated it using sh mk_all.sh?

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 19:50):

Does sh come with every install of VSCode by default?

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 19:59):

Surely I can just use the .sh file one way or another, so that's my aim.

view this post on Zulip Simon Hudon (Aug 28 2019 at 20:20):

I recommend you have your program call mk_all.sh when it needs information because the all.lean file will be obsolete fast

view this post on Zulip Johan Commelin (Aug 28 2019 at 20:23):

Otoh, for now you could just hardcode the 5 examples that we have: Type, Top, CommRing...

view this post on Zulip Scott Morrison (Aug 28 2019 at 23:30):

Or add some more. :-)


Last updated: May 17 2021 at 21:12 UTC