Dots in outputs + documentation

Stream: general

[Jasmin Blanchette]

I've upgraded to Lean 3.16.5 and suddenly I get lots of n.succ in the output. This is terrible for teaching, and there are very good reasons to dislike this overloaded notation (n could be a namespace or an object, two very different entities). I've heard rumors there's an option to disable this, but I can't find a comprehensive list of options anywhere.

Concerning documentation. Searching on the community web site was fruitless (I tried the search of mathlib on the community web set). It's a common issue with proof assistants that even when there is documentation, it's hard to figure out where. Lean has bits of documentation that appear when you hover over things, other bits in mathlib and now increasingly the community site. But I just don't know, as a user, how to find the list of options, a list of tactics, etc., even if some of them do exist. Isabelle is just like that too, because the documentation is organized by ownership (Makarius's domain, Alex Krauss's domain, etc.), not logically.

Back at Trolltech, we had systematic documentation. From

https://doc.qt.io/archives/4.3/

you could find all classes, all functions, all overviews, all modules, etc., all auto-generated by my qdoc ($\approx$ doxygen). With Lean, one can sense that this goal is within reach. I unfortunately don't have any time to help you guys make it happen (if you agree this is a desirable goal), but I can continue complaining if you feel this is useful.

[Gabriel Ebner]

The option you're looking for is called @[pp_nodot]. The documentation you're looking for is maybe Rob's baby here: https://leanprover-community.github.io/mathlib_docs/

[Gabriel Ebner]

And yes, pp_nodot is so undocumented that google only finds it on some shady mirrors.

[Jasmin Blanchette]

Rob's documentation is the closest, and when I wrote that I tried the search of mathlib, that's what I meant. It doesn't help me with some core Lean things like pp.beta, not to mention @[pp_nodot].

[Jasmin Blanchette]

I also don't see a list of tactic, with simp, dsimp, etc., in there. That's what I'm complaining about. There is no single entry point to all documentation to all Lean.

[Jasmin Blanchette]

And please tell me how to use @[pp_nodot]. set_option @[pp_nodot] true certainly doesn't work. :S

[Kevin Buzzard]

Robs docs have got a link for tactics in the top right I think

[Jasmin Blanchette]

You're right. That's good. :)

[Jasmin Blanchette]

Oh, and now Lean is being "helpful" again. I mistyped set_option pp.gamma true and it says

unknown option 'pp.gamma', type 'help options.' for list of available options

but it can't seem to be able to parse help options.. This seems to be outdated or something. :S

[Jasmin Blanchette]

Kevin, do your mathematician friends like the dot notation? I see it can shoten notations.

[Jasmin Blanchette]

But it also works backwards w.r.t. the rest of the lambda-calculus and requires a bidirectional parser in one's head.

[Alex J. Best]

I think a lot of people weren't too keen on it for mathematical functions like ker. And nodot is enabled for thins like sin  etc in mathlib:

src/data/complex/basic.lean:@[pp_nodot] def norm_sq (z : ℂ) : ℝ := z.re * z.re + z.im * z.im
src/data/complex/basic.lean:@[pp_nodot] noncomputable def abs (z : ℂ) : ℝ := (norm_sq z).sqrt
src/data/complex/exponential.lean:@[pp_nodot] def exp' (z : ℂ) :
src/data/complex/exponential.lean:@[pp_nodot] def exp (z : ℂ) : ℂ := lim (exp' z)
src/data/complex/exponential.lean:@[pp_nodot] def sin (z : ℂ) : ℂ := ((exp (-z * I) - exp (z * I)) * I) / 2
src/data/complex/exponential.lean:@[pp_nodot] def cos (z : ℂ) : ℂ := (exp (z * I) + exp (-z * I)) / 2
src/data/complex/exponential.lean:@[pp_nodot] def tan (z : ℂ) : ℂ := sin z / cos z
src/data/complex/exponential.lean:@[pp_nodot] def sinh (z : ℂ) : ℂ := (exp z - exp (-z)) / 2
src/data/complex/exponential.lean:@[pp_nodot] def cosh (z : ℂ) : ℂ := (exp z + exp (-z)) / 2
src/data/complex/exponential.lean:@[pp_nodot] def tanh (z : ℂ) : ℂ := sinh z / cosh z
src/data/complex/exponential.lean:@[pp_nodot] def exp (x : ℝ) : ℝ := (exp x).re
src/data/complex/exponential.lean:@[pp_nodot] def sin (x : ℝ) : ℝ := (sin x).re
src/data/complex/exponential.lean:@[pp_nodot] def cos (x : ℝ) : ℝ := (cos x).re
src/data/complex/exponential.lean:@[pp_nodot] def tan (x : ℝ) : ℝ := (tan x).re
src/data/complex/exponential.lean:@[pp_nodot] def sinh (x : ℝ) : ℝ := (sinh x).re
src/data/complex/exponential.lean:@[pp_nodot] def cosh (x : ℝ) : ℝ := (cosh x).re
src/data/complex/exponential.lean:@[pp_nodot] def tanh (x : ℝ) : ℝ := (tanh x).re

[Alex J. Best]

It looks to be definition by definition so each definition you don't want dot notation for is marked nodot, either at declaration time or later with local attribute [pp_nodot] foo.x

[Jasmin Blanchette]

So I have to set this manually for every single symbol? This is absolutely awful.

[Sebastien Gouezel]

In general, most of us find that dot notation is absolutely great, except for a few particular cases like sin and friends. That's why it is the default behavior. I don't know if there is a pretty printer option that disables it completely.

[Johan Commelin]

@Jasmin Blanchette I think it also automatically kicks in if you open the namespace. So open nat should solve your issue.

[Gabriel Ebner]

set_option pp.generalized_field_notation false

[Johan Commelin]

I agree with Jasmin that we should have an auto-generated set_option help page.

[Jasmin Blanchette]

Thanks Johan for the hint, but I don't want to open nat. When I teach, I open nothing. Opening stuff is just another way to confuse students. (Some are still confused by the f x y syntax five lectures into the course, so I have to keep things syntactically simple if I want to actually teach something of value.)

[Jasmin Blanchette]

Gabriel, you're my hero. :)

[Johan Commelin]

Not only your hero...

[Jasmin Blanchette]

Right. He's also my idol. :)

[Kyle Miller]

Gabriel Ebner said:

set_option pp.generalized_field_notation false

I just found where in the source the effect of this is applied. It's bool pretty_fn<T>::is_field_notation_candidate(expr const & e) in src/frontends/lean/pp.cpp. (The pp_nodot check is there, too.)

[Johan Commelin]

@Jasmin Blanchette I meant, not only your hero... as in he's also my hero (-;

[Kyle Miller]

It seems like field notation in the pretty printer should be opt-in rather than opt-out. Maybe with structure fields automatically marked to pretty print.

[Jasmin Blanchette]

I certainly wouldn't be against Kyle's proposal. But Sébastien pointed out that mathematicians seem to generally like the dot notation, so I don't know. Maybe I'm just a dinosaur.

[Johan Commelin]

I guess it can be confusing for students that have heard of the concepts "namespace" and "object" before... but for uneducated mathematicians... we just dive in and take whatever the system feeds us.

[Jasmin Blanchette]

I don't know how confusing it is or not, because we don't go that route. All I know is that despite my best attempt to refresh my MSc-level, mostly C.S. students' memory of the lambda calculus, parsing f a (g b c) isn't automatic and takes some time. Then I keep the cognitive load low by avoiding avoidable variants (and the dot notation, which doesn't exist AFAIK in any other proof assistant, is the first victim of my Occam's razor).

[Jasmin Blanchette]

Moreover, in Isabelle/ML, we have a |> operator which can be used like this to apply functions: x |> f |> g |> h means h (g (f x)). It's reminiscent of . in terms of directionality. It's very addictive, and I've written tens of thousands of lines of code using it, but in the end I'm not so pleased with the result. There's an unhealthy mixture of f x and x |> f, often in the same file and with no rhyme or reason, and if I could go back I'd use |> only where there's a clear benefit (like applying several functions in sequence, my first example). I would definitely not make |> the default in the output. The fact that it's so addictive should have been a red flag.

[Kevin Buzzard]

@Jasmin Blanchette I find the dot notation everywhere quite disorientating. Chris Hughes suggested that it could be disabled for open namespaces, which I thought was an interesting idea.

[Jasmin Blanchette]

Yes, that would be a good start, since in that case, it brings no real benefit.

[Johan Commelin]

The massive benefit is of course with things like de : dense_embedding f, and write de.continuous instead of dense_embedding.continuous de to obtain a proof of continuous f.

[Johan Commelin]

Or hf : continuous f and hg : continuous g, and then write hf.add hg for a proof of continuous (f + g), instead of writing continuous.add hf hg.

[Jasmin Blanchette]

Sure, it's just unfortunate that that substantial benefit was obtained at the cost of an operator that swings the wrong way and that doesn't mesh well generally with functional programming notations.

[Patrick Massot]

The dot notation is absolutely great in general. It makes Lean look more like a real programming language. But we should have more [pp_nodot]. I don't mind n.succ (in the sense that it's not worse than nat.succ n but both of them should be avoided as soon as the basic nat API is in place), but f.ker or x.sin are of course absurd.

[Patrick Massot]

And of course the documentation improvement is an endless mission that we must always keep in mind.

[Patrick Massot]

But the way, Rob do you have any news from your student who was meant to work on this? Is it happening in the end?

[Rob Lewis]

Jasmin Blanchette said:

Oh, and now Lean is being "helpful" again. I mistyped set_option pp.gamma true and it says

unknown option 'pp.gamma', type 'help options.' for list of available options

but it can't seem to be able to parse help options.. This seems to be outdated or something. :S

Indeed, this is probably Lean 2 leftovers and should be #help options.

[Rob Lewis]

The options do come with descriptions, so we just need a hook to access them from meta-Lean, and generating a doc page will be easy.

[Rob Lewis]

Patrick Massot said:

But the way, Rob do you have any news from your student who was meant to work on this? Is it happening in the end?

It's still in progress.

[Patrick Massot]

What is in progress? Work on doc or work on figuring out whether work on doc will happen?

[Rob Lewis]

Jasmin Blanchette said:

I also don't see a list of tactic, with simp, dsimp, etc., in there. That's what I'm complaining about. There is no single entry point to all documentation to all Lean.

@Jasmin Blanchette Regarding the tactic documentation at https://leanprover-community.github.io/mathlib_docs/tactics.html, note that there's also issue #3088 which deserves attention. I guess you have descriptions of tactics in the Hitchhiker's Guide that may be more helpful or complete than the official ones in some cases. If you're interested in PRing updates to mathlib I'd be very happy to review and accept.

[Rob Lewis]

My longer-term goal there is to go the other way, to be able to embed tactic descriptions in other texts. Right now each description is a single blob of markdown. I'd like to split them more ("description", "syntax", "options", etc) so that e.g. the Hitchhiker's Guide could describe linarith in its own way and then import the official syntax documentation.

[Patrick Massot]

I agree with everything Rob wrote, but we also still need a tactic cheat-sheet which fits on one A4 page with only the essential ones.

[Jasmin Blanchette]

Yes, I resisted ranting about some of the less informative tactic descriptions. Short is better than nothing. ;) I can PR them. That much (little) I can do. Hopefully the people reviewing the PRs will have more of a clue than me and will spot any inaccuracies.

[Rob Lewis]

Thanks! The docs for core tactics are mostly (all?) found here: https://github.com/leanprover-community/mathlib/blob/master/src/tactic/lean_core_docs.lean
Mathlib tactics are documented right after they're defined. This arrangement is a little less convenient for mass updates, but it helps a lot to keep the docs from becoming outdated.

[Jasmin Blanchette]

Of course, putting the docs near to the code is a good idea. I remember the discussion. That's how qdoc/oxygen/javadoc etc. work. I'll find them.

[Rob Lewis]

An add_tactic_doc that has no description means its inheriting its body from the doc string of the relevant tactic. You can override this by just adding the description in the add_tactic_doc.

[Jasmin Blanchette]

I see.

[Rob Lewis]

Or you can update the tactic doc string, of course, if it seems appropriate!

[Jasmin Blanchette]

(We also had a manual for qdoc. But Lean has a chat. ;))

[Jasmin Blanchette]

I'll be in the office the next two weeks, so perhaps you can even look over my shoulder as I try to do it.

[Rob Lewis]

I'll be in if/when it stops raining :)

[Johan Commelin]

That certainly is an if in NL

[Jasmin Blanchette]

I'll be there if I don't get kidnapped and tortured. Another if in NL.

[Gabriel Ebner]

(deleted)

[Johan Commelin]

Good luck! That was pretty horrible news.

[Jasmin Blanchette]

Concerning Rob's last suggestion regarding "embed[ding] tactic descriptions in other texts": It could be useful for others, but I wouldn't import that. I want to show an idealized fragment of the syntax, not the whole thing. And I want to stick to my own naming conventions anyway. At the end of the day, although most of my readers are using it as a Lean tutorial, it was never my ambition to write one. At most, I would consider adding links to the official documentation, on a "for more information" basis. I'll add that to my TODO.