Still struggling with CI

Stream: mathlib4

[Dominic Steinitz]

I have

/-
Copyright (c) 2026 Dominic Steinitz. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Dominic Steinitz
-/
module

public import Mathlib.Init
public import Mathlib.Analysis.InnerProductSpace.PiL2
public import Mathlib.Geometry.Manifold.Sheaf.Basic
public import Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
public import Mathlib.Geometry.Manifold.VectorField.Pullback

open scoped Manifold

and lint(?) complains: "The module doc-string for a file should be the first command after the imports.
Please, add a module doc-string before open scoped Manifold."

But what is a module doc-string?

public import Mathlib.Geometry.Manifold.VectorField.Pullback
/-- A module doc-string -/

Still gives me a lint error.

Also at some point on my CI journey, CI wanted me to have this public import Mathlib.Init but I have no idea why.

As Schiller might have put it: Gegen CI kämpfen selbst die Götter vergebens.

[Dominic Steinitz]

/-! # Ehresmann Connections This file defines Ehresmann connections on fiber bundles and establishes basic properties.## Main definitions * verticalSubspace: The vertical subspace at a point in the total space * EhresmannConnection: A smooth distribution of horizontal subspaces complementary to the vertical ## References * [Kobayashi and Nomizu, Foundations of Differential Geometry][kobayashi1963] -/

Apparently I needed a !

[Michael Rothgang]

Yes, a module doc-string starts with /-!; a /-- starts a doc comment.

[Michael Rothgang]

If you have imported other mathlib files, you shouldn't need public import Mathlib.Init any more.

[Michael Rothgang]

If CI still requires it, feel free to DM me and I'll investigate: that would sound like a bug.

[Dominic Steinitz]

All good now thanks :-)