meaning of `section end`

Stream: new members

[David Chanin]

I'm confused by the keyword section end in https://github.com/leanprover-community/mathlib/blob/master/src/algebraic_geometry/pullbacks.lean#L113. I would have thought this meant a new section is being created called end but there's no equivalent end end. What does this line of code do?

[Junyan Xu]

I think it's an unnamed section that immediately ends; seems to serve no purpose.

The section end line was already there when the file was added in #11450.

[David Chanin]

interesting, I'll just ignore it then!

[David Chanin]

If you open a section and never close it, that's allowed? Does it auto-close at the end of the file? e.g. https://github.com/leanprover-community/mathlib/blob/96d3f9505666502b67d73ebd0dd0cc360c3418a7/analysis/topology/topological_groups.lean#L52 this section is never ended

[Kyle Miller]

Sections need to be closed. That file (from 2018) starts with #exit so none of the rest is processed.

[David Chanin]

So #exit means to not parse the rest of the file?

[Kyle Miller]

Yes, the #exit command causes Lean to stop processing the file immediately.

[David Chanin]

I'm also confused by this namespace nat.partrec' in https://github.com/leanprover-community/mathlib/blob/bdd54acda358f535b42951b784757135213dcf52/data/computability/halting.lean#L194. It's never closed, but another namespace named nat.primrec' does get closed even though it's never opened. Are these the same namespace somehow?

[Kyle Miller]

It might be a Lean bug that it's not checking the names match beyond the first dot. (By the way, why are you looking at mathlib from 2018?)

[Kyle Miller]

When you close a namespace or section with end, Lean already knows what it's closing, and it's only using the text you supply as a check.

[David Chanin]

I'm working on getting better namespace parsing working for https://mathlib-changelog.vercel.app/, which requires manually keeping track of which namespace/sections are open/closed. But the script I wrote is erroring on some of these examples, so just trying to understand what's going on

[Kyle Miller]

As far as I can tell, that data/computability/halting.lean would always have been an error, at least as far back as the last official Microsoft release of Lean 3.

On github, there's a red X saying the Travis CI failed for that commit. Indeed, in the next commit it was fixed: https://github.com/leanprover-community/mathlib/commit/b37526407ed1846f29dcdfb976554daf7f8a983e#diff-b5b02b57165dd41df0a1154c6d87b6ac2e174c4e2f7ba7b4ae51d0294e375297R318

[David Chanin]

aah good catch! Yeah seems like it's safe to ignore the error there then