Zulip Chat Archive

Stream: general

Topic: import hierarchy


Kenny Lau (Oct 17 2020 at 11:27):

Suppose I want to state the lemma that if A is nonempty and R is a ring of char p then A -> R is a ring of char p.

Kenny Lau (Oct 17 2020 at 11:27):

The "char p" involves the file algebra.char_p and the A -> R involves the file algebra.ring.pi

Kenny Lau (Oct 17 2020 at 11:28):

currently I believe the two files do not import each other

Kenny Lau (Oct 17 2020 at 11:28):

so is there a way to put this lemma in mathlib without messing up the import hierarchy? or does this not matter at all?

Kevin Buzzard (Oct 17 2020 at 11:51):

My impression is that the way this sort of thing is handled is you just make a new file and import them both, or dump it in a file which imports both.

Johan Commelin (Oct 17 2020 at 13:36):

@Kenny Lau I think in this case it's ok to import alg.ring.pi in alg.char_p

Kenny Lau (Oct 17 2020 at 13:40):

@Johan Commelin then we're making alg.char_p depend on more files

Kenny Lau (Oct 17 2020 at 13:44):

I think this is a bigger problem than we think, in the sense that we might need an entirely new approach to dealing with hierarchy

Kenny Lau (Oct 17 2020 at 13:44):

I'm sure issues like this is hidden everywhere in mathlib

Kenny Lau (Oct 17 2020 at 13:45):

Maybe more segmentation (dividing files into multiple files) is the solution

Johan Commelin (Oct 17 2020 at 13:45):

content addressable declarations

Kenny Lau (Oct 17 2020 at 13:49):

For example, ring_theory.principal_ideal_domain imports ring_theory.noetherian and ring_theory.unique_factorization_domain

Kenny Lau (Oct 17 2020 at 13:49):

I'm pretty sure you don't need those imports to define PID

Adam Topaz (Oct 17 2020 at 13:59):

what about smaller files, more directories, and more default.lean files?

Kenny Lau (Oct 17 2020 at 14:12):

Sounds like a good idea to me

Adam Topaz (Oct 17 2020 at 14:15):

This way you could have the option to import giant things (by importing the default file), or little things by importing individual files

Johan Commelin (Oct 17 2020 at 14:19):

I would still love to see a version of Lean that is similar to unisonweb.org
Every declaration is hashed, and the hash is its stable name. (Before hashing, you also replace all names in the declaration by the hashes that they point to.)

Johan Commelin (Oct 17 2020 at 14:20):

You dump everything into a database, and you no longer really have directories or files.

Adam Topaz (Oct 17 2020 at 14:20):

Says the nixos user :wink:

Johan Commelin (Oct 17 2020 at 14:20):

But they do have tooling to "extract files" that you can then edit, and push back to the db

Johan Commelin (Oct 17 2020 at 14:21):

The reason this might be tricky for Lean / mathlib is that we have proof search going on. If all simp and tidy proofs would be replaced by the stable output of squeeze_simp and tidy?, then we might be a lot closer to making this work.

Johan Commelin (Oct 17 2020 at 14:22):

But then we would get really long and ugly proofs (e.g. in category theory). So I feel like maybe you would need to store multiple layers of proofs.

Johan Commelin (Oct 17 2020 at 14:22):

And then you quickly go down a rabbit hole of open problems and cute dreams. But nothing that we can actually realise in a short amount of time.

Johan Commelin (Oct 17 2020 at 14:23):

So probably the more pragmatic solution is what Adam said above: more dirs, more files, more default.lean

Johan Commelin (Oct 17 2020 at 14:29):

The other pragmatic solution is to ask Mario to make us a Lean layer on top of MM0 so that we have an ITP that compiles mathlib in < 5s, and then we can just dump everything into one file, like set.mm.

Adam Topaz (Oct 17 2020 at 14:44):

Unison sounds really cool BTW

Adam Topaz (Oct 17 2020 at 14:54):

Just thinking out loud.... How would this hashing AST a la unison work with typeclasses? E.g. how would I define two different category instances on the same type? Right now I would make an alias, and define a new instance on the alias.

Johan Commelin (Oct 17 2020 at 14:58):

I think you can make that work, if you have some special type_alias constructor in the language


Last updated: Dec 20 2023 at 11:08 UTC