Zulip Chat Archive

Stream: general

Topic: List categories def'd in lib?

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.

Daniel Donnelly (Aug 28 2019 at 19:02):

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

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

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.

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)?

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

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

Johan Commelin (Aug 28 2019 at 19:22):

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

Daniel Donnelly (Aug 28 2019 at 19:25):

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

Simon Hudon (Aug 28 2019 at 19:29):

Have a look at:

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

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

Daniel Donnelly (Aug 28 2019 at 19:31):

@Simon Hudon thx. I will bookmark this.

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?

Daniel Donnelly (Aug 28 2019 at 19:50):

Does sh come with every install of VSCode by default?

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.

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

Johan Commelin (Aug 28 2019 at 20:23):

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

Scott Morrison (Aug 28 2019 at 23:30):

Or add some more. :-)

Last updated: Dec 20 2023 at 11:08 UTC