Namespace

Stream: CSLib

[Fabrizio Montesi]

Is CSLib just a project name or is it gonna use the 'Cslib' namespace, as we're doing at https://github.com/cs-lean/cslib ?

We (contributors) are in the middle of implementing a governance model for the lib, and some of us are using or planning to use it downstream for work. So if name clashes are likely, it'd be great to consider/discuss this.

[Swarat Chaudhuri]

Thanks for flagging this! We were planning to use the Cslib namespace. We would love to understand the scope of your project and ideally join forces. We can discuss further over email.

[Eric Wieser]

As a reminder, there's both the namespace and the name of the module at play here. If two projects use the same module names they can't be imported at the same time ever. If they use the same namespace, you can still perhaps mix and match subcomponents as long as no declaration names clash.

[Eric Wieser]

(and Mathlib the module very rarely uses Mathlib the namespace)

[Fabrizio Montesi]

Swarat Chaudhuri said:

Thanks for flagging this! We were planning to use the Cslib namespace. We would love to understand the scope of your project and ideally join forces. We can discuss further over email.

Thanks Swarat, it'd make good sense to discuss scopes. I'll reach out.