Broken file references

Stream: mathlib4

[Kim Morrison]

find Mathlib -type f -exec grep -l "Mathlib/[^Ä {} \; | while read f; do grep -n "Mathlib/[^Ä "$f" | while IFS=: read n p; do p=$(echo "$p" | grep -o "Mathlib/[^Ä [ ! -f "$p" ] && echo "$f:$n: $p does not exist"; done; done

prints out something close to

Mathlib/Analysis/Convex/Cone/Basic.lean:25: Mathlib/Analysis/Convex/Cone/Dual.lean does not exist
Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean:328: Mathlib/Analysis/SpecialFunctions/Gaussian.lean does not exist
Mathlib/Analysis/Normed/Group/Uniform.lean:56: Mathlib/Analysis/NormedSpace/OperatorNorm.lean does not exist
Mathlib/Analysis/Normed/Group/Uniform.lean:59: Mathlib/Analysis/NormedSpace/OperatorNorm.lean does not exist
Mathlib/Probability/Kernel/IntegralCompProd.lean:26: Mathlib/MeasureTheory/Constructions/Prod/Basic.lean does not exist
Mathlib/CategoryTheory/Functor/Basic.lean:56: Mathlib/Tactic/Reassoc.lean does not exist
Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean:42: Mathlib/GroupTheory/Subgroup/Basic.lean does not exist
Mathlib/AlgebraicTopology/SimplicialSet/KanComplex.lean:13: Mathlib/AlgebraicTopology/Quasicategory.lean does not exist
Mathlib/AlgebraicTopology/SimplicialSet/Quasicategory.lean:16: Mathlib/AlgebraicTopology/Nerve.lean does not exist
Mathlib/AlgebraicTopology/SimplicialSet/Quasicategory.lean:22: Mathlib/AlgebraicTopology/KanComplex.lean does not exist
Mathlib/Condensed/Explicit.lean:22: Mathlib/CategoryTheory/Sites/RegularSheaves.lean does not exist
Mathlib/Condensed/Light/Explicit.lean:17: Mathlib/CategoryTheory/Sites/RegularExtensive.lean does not exist
Mathlib/RingTheory/Coalgebra/Equiv.lean:12: Mathlib/Algebra/Module/Equiv.lean does not exist
Mathlib/RingTheory/Congruence/Basic.lean:86: Mathlib/GroupTheory/Congruence.lean does not exist
Mathlib/SetTheory/Cardinal/Basic.lean:62: Mathlib/SetTheory/Cardinal/Ordinal.lean does not exist
Mathlib/Data/Complex/Order.lean:20: Mathlib/Data/RCLike/Basic.lean does not exist
Mathlib/Data/Set/Finite.lean:433: Mathlib/Order/LocallyFinite.lean does not exist
Mathlib/Algebra/Quotient.lean:15: Mathlib/GroupTheory/QuotientGroup.lean does not exist
Mathlib/Algebra/Quotient.lean:16: Mathlib/LinearAlgebra/Quotient.lean does not exist
Mathlib/Algebra/Quotient.lean:17: Mathlib/RingTheory/Ideal/Quotient.lean does not exist

Would anyone be interested in any of:

1. finding out what these references should now point to?
2. turning this a linter?
3. generalizing this to also capture `Mathlib.X.Y.Z` references?

[Damiano Testa]

Is reading comments/docstrings something that Verso would do?

[Daniel Weber]

related

[Kim Morrison]

Yes. But not yet, and in any case we'll need to fix these problems even once/if Verso is catching them. Verso is likely going to need to manual mark-up to tell it how to interpret backticks, in any case.

[Damiano Testa]

Would having a #assert_imported/#assert_not_imported be something useful? There would probably still have to be a linter checking that what looks like a file path/module name in comments has a corresponding command, but the machinery for the #assert_xxx already has its API.

[Kim Morrison]

Why not just a linter that directly reads the module docs?

[Damiano Testa]

And comments/module docs, I guess.

[Eric Wieser]

Should we standardize on the path spelling to refer to modules in docstrings?

[Damiano Testa]

Note that, e.g., Mathlib/Algebra/Algebra/Basic.lean contains

/-! TODO: The following lemmas no longer involve `Algebra` at all, and could be moved closer
to `Algebra/Module/Submodule.lean`. Currently this is tricky because `ker`, `range`, `⊤`, and `⊥`
are all defined in `LinearAlgebra/Basic.lean`. -/

that refers to a file path without Mathlib.

[Damiano Testa]

Maybe we should search also for "[^ ]*\.lean".

[Kim Morrison]

We'd have to detect the missing Mathlib/ and add it, however!

[Kim Morrison]

But I think better to just disallow that, even if the file exists.

[Damiano Testa]

Ok, I am still trying to see how much we have to rely on string-parsing (this was the motivation for the #assert_xxx proposal, to try to move away from shell tools as quickly as possible).

[Damiano Testa]

Anyway, having a tool (linter or otherwise) that extracts all doc-strings, module docs and comments seems like it would be useful generally anyway.

[Damiano Testa]

And the output of that could then be scanned for regexes.

[Johan Commelin]

I think that for now we should just strive to have Kim's command return 0 results. And hopefully we'll have better tooling in the near future once we start using Verso.
So I would not invest a lot of time in writing Lean tooling for this. We just want to get our docs in a better state to prepare for when Verso arrives.

[Yaël Dillies]

Eric Wieser said:

Should we standardize on the path spelling to refer to modules in docstrings?

That would be great, because the reason I introduce inconstencies when renaming files is that I only look for the module name, not the file name

[Yaël Dillies]

measure theory.constructions.prod.basic is now measurehtoery.measurablespace.prod and measuretheory.measure.prod, sorry for bad spelling

[Ruben Van de Velde]

Is it still the case that module names are only linked in the documentation if you're importing the file in question?