namespacing

Stream: CSLib

[Kim Morrison]

Can I suggest/recommend that CSLib puts everything in the CSLib namespace?

(Mathlib conspicuously doesn't do this, but this is not an example to emulate.)

[Chris Henson]

Yes, I can do this. We unfortunately picked up the bad habit of not consistently using a top level CSLib namespace.

[Kim Morrison]

It would be nice to have a linter for this, but I'm not sure exactly what the condition should be.

[Chris Henson]

Something like every new declaration is either in the CSLib namespace, or extending something upstream? If that's possible metaprogramming-wise, seems like it would be something you run periodically.

[Ching-Tsun Chou]

#CSLib > Strange "lake build" error msg @ 💬

Does cslib require that all theory files have their paths be included in the top-level Cslib.lean?

[Snir Broshi]

Is it possible to make _root_ point to CSLib? Prefixing names with _root.CSLib. when you're in a namespace and want to define something outside of it is a bit verbose. Or maybe there's some syntax for the parent namespace?

[Fabrizio Montesi]

Ah, I wasn't aware of this. I took Mathlib's example, unaware that it was not a good one.

Yes, let's put everything under a namespace. But with what casing? I've been going with Cslib so far, while other people with CSLib and recently in the steering committee we've adopted CSlib. :face_with_spiral_eyes:

[Ching-Tsun Chou]

I think Cslib is better. After all, that's the name already used by file and directory names at the top of the repo (like Cslib.lean, etc). Having CSlib as a namespace just creates confusion.

[Chris Henson]

Yeah, the casing constantly trips me up. We should decide on a standard usage. I tend to prefer Cslib in code for the same reasons as @Ching-Tsun Chou. It'd be confusing for it not to match the imports. It's okay(ish) if in informal usage another casing is used.

[Fabrizio Montesi]

Glad to read this.
I find casing of cslib a nightmare both to figure out and to type, so I settled on no casing early on (cslib), and just capitalise the first letter when a first capital letter is expected (like in Lean).
So, I like Cslib for the namespace.

[Ching-Tsun Chou]

I just noticed that Cslib/Foundations/Data/OmegaSequence missed the Cslib namespacing patch. So I made a PR (cslib#112) to fix it. @Fabrizio Montesi , could you take a look and merge it into "main"? Thanks!

[Mario Carneiro]

I think CSLib is the most sensible casing (and the one that follows lean + mathlib casing guidelines re: acronyms in names), but it should be used uniformly (on the root package name and the namespace alike)

[Fabrizio Montesi]

Is Mathlib not following the convention then? (Shouldn't it be MathLib?)

[Mario Carneiro]

mathlib is one word for branding purposes

[Shreyas Srinivas]

I think Cslib can be a similar brand name

[Shreyas Srinivas]

I agree with the others that Cslib is easier to type that CSLib

[Mario Carneiro]

I believe there was an initial confusion on this matter because two projects started around the same time with different casings

[Mario Carneiro]

see e.g. this zulip channel name

[Shreyas Srinivas]

I think this hasn't been mentioned in this thread, but for context I just namespaced everything in Cslib yesterday

[Mario Carneiro]

I think it's harder to pronounce Cslib as a word though

[Shreyas Srinivas]

There are some 50 odd files to modify if you wish to change that

[Chris Henson]

It is mildly annoying to have another big PR, but it's just a search and replace. (Not arguing for it per se, I just don't find that reasoning compelling)

[Shreyas Srinivas]

how do you get a list of all declarations that were declared in the current file (as opposed to imported)? Maybe we could write a linter that just checks that all these declarations have a namespace matching the project name or specified in the lakefile.

[Chris Henson]

We still want to allow extending existing namespaces though, say for instance to add something for List or Nat. Here is my reasoning so far:

What needs to be checked is that every new declaration falls under either CsLib or an upstream top level namespace. If I can write it so the latter isn't recalculated each time (or otherwise fast), it can be a usual linter. Otherwise, it could be a library-wide check run in CI.

[Ching-Tsun Chou]

Alas, isn't it a bit too late to make such disruptive name changes now? It is not just a matter of a global name change in the main branch of the upstream repo. There are other branches and some of us are working on multiple patches locally. I would hate to spend the time fixing all the patches I'm working on.

And this is not to mention that CSLib is harder to read and to type than Cslib. You have to look at it twice to make sure that the "L" is in uppercase.

[Damiano Testa]

In case it is helpful, docs#Lean.Environment.getNamespaceSet returns all available namespaces. In fact, every namespaces is added to the docs#Lean.namespacesExt environment extension. However, a command like

theorem A.B.C : True := trivial

does extend the environment extension with A and A.B, so checking after-the-fact whether a namespace already existed is a little tricky. You may have to preemptively scan the environment for declarations that are "imported" and extract their namespace, before you check if the initial segment of a new name matches Cslib or one of the others.

Here is a sample usage of namespaceExt:

import Lean

open Lean

/--
info: #[Acc, Add, Alternative, AndOp, AndThen, Append, Applicative, Array, BEq, Bind, BitVec, Bool,
ByteArray, Char, Classical, Coe, CoeDep, CoeFun, CoeHTC, CoeHTCT, CoeHead, CoeOTC, CoeOut, CoeSort,
CoeT, CoeTC, CoeTail, Complement, Decidable, DecidableLE, Div, DoResultBC, DoResultPR, DoResultPRBC,
DoResultSBC, Dvd, Dyadic, EStateM, EmptyCollection, Except, ExceptT, Fin, Float, Float32,
FloatArray, FloatSpec, ForIn, ForIn', ForInStep, ForM, Function, Functor, GetElem, GetElem?, HAdd,
HAnd, HAndThen, HAppend, HDiv, HMod, HMul, HOr, HOrElse, HPow, HSMul, HShiftLeft, HShiftRight, HSub,
HXor, HasEquiv, HasSSubset, HasSubset, Hashable, HomogeneousPow, IO, ISize, ImportCompletion,
Inhabited, Insert, Int, Int16, Int32, Int64, Int8, IntCast, Inter, Inv, LE, LLVM, LT, Lean, List,
MProd, Max, Membership, MessageActionItem, MessageType, Min, Mod, Monad, MonadControl,
MonadControlT, MonadEval, MonadEvalT, MonadExcept, MonadExceptOf, MonadFinally, MonadFunctor,
MonadFunctorT, MonadLift, MonadLiftT, MonadReader, MonadReaderOf, MonadShareCommon, MonadState,
MonadStateOf, MonadWithReader, MonadWithReaderOf, Mul, Nat, NatCast, NatPow, Neg, NonScalar, OfNat,
OfScientific, One, Option, OrElse, OrOp, Ord, Ordering, PEmpty, PLift, PNonScalar, PProd, PSigma,
PSum, PULift, PUnit, Pow, Prod, Pure, Quotient, RandomGen, Rat, Relation, Repr, ReprTuple, SDiff,
SMul, ST, Sep, Seq, SeqLeft, SeqRight, Setoid, ShareCommon, ShiftLeft, ShiftRight,
ShowMessageParams, ShowMessageRequestParams, Sigma, Singleton, SizeOf, StateCpsT, StateT, Std,
StdGen, Stream, String, Sub, Substring, Subtype, Sum, System, Task, Thunk, ToBool, ToStream,
ToString, Trans, UInt16, UInt32, UInt64, UInt8, ULift, USize, Union, Vector, WellFoundedRelation,
XorOp, Zero, default, instDecidableEqDyadic, instDecidableEqRat, instDecidableEqSum]
-/
#guard_msgs in
run_cmd
  let namespaces := (← getEnv).getNamespaceSet.fold (init := (∅ : NameSet)) fun tot n =>
    match n.components with
    | r::_::_ => tot.insert r
    | _ => tot
  let sorted := namespaces.toArray.qsort (·.toString < ·.toString)
  dbg_trace sorted

[Shreyas Srinivas]

I think concretely an API function that returns the namespaces of a declaration in an array will be useful. The idea is that in any file there shouldn’t be any unnamespaced local declaration.

[Chris Henson]

@Damiano Testa This "preemptive scan" is what I had in mind, though thanks for pointing out that function to make it easier!

To avoid having to query for the namespaces every time in a linter, I was thinking I would have this as a constant, and have a test that it is equal.

[Damiano Testa]

If you want to write a syntax linter, then I agree that probably storing the available namespaces in a constant is a viable option. If you are writing an environment linter, though, the computation of the available namespaces is (probably) only performed once and it is not an especially slow computation, so you may not need to hard-code it.

[Chris Henson]

Ah this probably does make better sense as an environment linter, I overlooked that possibility. If it performs fine, I'll do that, thanks!

[Chris Henson]

This seems to work reasonably fast, ~20 seconds to check Cslib. The only offending declarations it found were unscoped notations from LTS and ReductionSystem. Once I figure out how to fix those I'll make a PR.

[Chris Henson]

PR: cslib#123

[Kim Morrison]

Ching-Tsun Chou said:

Alas, isn't it a bit too late to make such disruptive name changes now?

Just as a general principle, no, it is never too late to do anything. :-) At least, this is the approach that Mathlib takes, that all refactors are fair game, and that PR branches just need to merge master, and that this is an acceptable cost.

[Ching-Tsun Chou]

But you need to argue first that CSLib is a better name than Cslib to be worth the effort. Also, changing the names of namespaces is one thing, but changing the filenames and directories names is quite something else.

[Chris Henson]

I agree with Kim in general. It is not unacceptably difficult to merge even large changes, including filenames, given a sufficient benefit. That said, I think people are reasonably happy at the moment. I am not compelled to make any change.

[Kim Morrison]

Ching-Tsun Chou said:

But you need to argue first that CSLib is a better name than Cslib to be worth the effort.

Ah, I'd missed the context, and thought we were talking about adding CSLIB namespace in the first place, not changing the casing.

[Fabrizio Montesi]

@Chris Henson I've merged your lint-test-integration (nice!). Will people get that linting also while they edit files? Maybe we should add a check that Cslib.Init is imported somehow (albeit indirectly)?

[Chris Henson]

Because they are environment linters, which by their nature are a bit slower, they will not be run as you edit. You must either run lake test locally or wait for it to run in CI. The import requirements are:

• Syntax linters, such as the ones we use from Mathlib, need that Cslib.Init/Mathlib.Init are imported. When I add Cslib.Init, I will test for this.
• Environment linters require that everything is imported in Cslib.lean. I believe lint-style -action leaves on comment on PRs if we forget an import? I'd be more comfortable if there were an actual test though.

[Fabrizio Montesi]

Sounds good, thx!

[Damiano Testa]

I was thinking that, if you wanted to make a syntax linter for this check, what you could do is to create an IO.Ref that contains a precomputation of all the namespaces that are available before the current file, computed using the constants in (← getEnv).constants.map₁. After that, for each declaration you check whether its root namespace appears in the precomputed list.

This means that you pay the price for the precomputation once per file, but since the first time that you compute it, you store it in the IO.Ref, you only pay it once.

[Chris Henson]

As a practical matter I think you could get away with fewer precomputations (maybe one in our Init?) because the only time the top namespace is not Cslib is for upstream core/Mathlib. I felt the environment linter was simpler and sufficient because I don't anticipate people violating this rule often.

[Ching-Tsun Chou]

I noticed that import CslibTests.Lint has not been added to CslibTests.lean.

[Chris Henson]

Oops, my bad. I will add a test for this eventually. (Though compared to the library it is less crucial, because the tests are unlikely to be used as a library, and everything is still built by lake test because of the glob pattern)

[Ching-Tsun Chou]

I run the following:

lake exe mk_all && lake build

on everything I work on all the time.