Name clashes

[gebner]

We currently have two top-level definitions with the name embedding: one for cardinals, and another one for topological spaces. This causes problems if you want to import both, or use lean --recursive --export=mathlib.txt for the reference type checkers.

I put the cardinal embedding into the cardinal namespace. The topological embedding should probably also be namespaced, but I don't see an obvious candidate.

[digama0]

Do you know a way to work this into the Travis testing? That is, importing everything into the same file and seeing if it compiles?

[gebner]

That would work, but requires maintenance. We could also use lean --recursive --export=mathlib.txt, but that will break on sorry.

[Kha]

You could --make that single file, then check whether that created all .olean files. The only thing missing is leanpkg clean... :)

[digama0]

I'm okay with "break on sorry", I keep mathlib sorry-free anyway.

[digama0]

Does lean --recursive --export do the same as find -name *.lean? I don't want to maintain a file with the list, but it should not be difficult to just scan the whole folder for lean files - there are no files we need to avoid.

[gebner]

Yes, lean --recursive --export=mathlib.txt recursively traverses the directory. It uses the same code as lean --make.