## Stream: general

### Topic: Dots in outputs + documentation

#### Jasmin Blanchette (Jul 08 2020 at 07:26):

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 (Jul 08 2020 at 07:37):

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 (Jul 08 2020 at 07:39):

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

#### Jasmin Blanchette (Jul 08 2020 at 07:43):

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 (Jul 08 2020 at 07:44):

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 (Jul 08 2020 at 07:44):

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

#### Kevin Buzzard (Jul 08 2020 at 07:46):

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

#### Jasmin Blanchette (Jul 08 2020 at 07:46):

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

#### Jasmin Blanchette (Jul 08 2020 at 07:48):

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 (Jul 08 2020 at 07:49):

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

#### Jasmin Blanchette (Jul 08 2020 at 07:50):

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 (Jul 08 2020 at 07:51):

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 (Jul 08 2020 at 07:52):

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 (Jul 08 2020 at 07:54):

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

#### Sebastien Gouezel (Jul 08 2020 at 07:56):

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 (Jul 08 2020 at 07:56):

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

#### Gabriel Ebner (Jul 08 2020 at 07:56):

set_option pp.generalized_field_notation false


#### Johan Commelin (Jul 08 2020 at 07:56):

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

#### Jasmin Blanchette (Jul 08 2020 at 07:57):

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 (Jul 08 2020 at 07:57):

Gabriel, you're my hero. :)

#### Jasmin Blanchette (Jul 08 2020 at 07:59):

Right. He's also my idol. :)

#### Kyle Miller (Jul 08 2020 at 07:59):

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 (Jul 08 2020 at 08:00):

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

#### Kyle Miller (Jul 08 2020 at 08:01):

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 (Jul 08 2020 at 08:14):

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 (Jul 08 2020 at 08:18):

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 (Jul 08 2020 at 08:21):

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 (Jul 08 2020 at 08:27):

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 (Jul 08 2020 at 08:30):

@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 (Jul 08 2020 at 08:32):

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

#### Johan Commelin (Jul 08 2020 at 08:35):

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 (Jul 08 2020 at 08:35):

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 (Jul 08 2020 at 08:38):

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 (Jul 08 2020 at 08:43):

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 (Jul 08 2020 at 08:43):

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

#### Patrick Massot (Jul 08 2020 at 08:44):

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 (Jul 08 2020 at 08:44):

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 (Jul 08 2020 at 08:45):

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 (Jul 08 2020 at 08:46):

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 (Jul 08 2020 at 08:49):

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

#### Rob Lewis (Jul 08 2020 at 10:30):

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 (Jul 08 2020 at 10:32):

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 (Jul 08 2020 at 10:38):

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 (Jul 08 2020 at 10:44):

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 (Jul 08 2020 at 10:47):

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 (Jul 08 2020 at 10:48):

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 (Jul 08 2020 at 10:48):

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.

I see.

#### Rob Lewis (Jul 08 2020 at 10:49):

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

#### Jasmin Blanchette (Jul 08 2020 at 10:49):

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

#### Jasmin Blanchette (Jul 08 2020 at 10:50):

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 (Jul 08 2020 at 10:51):

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

#### Johan Commelin (Jul 08 2020 at 10:53):

That certainly is an if in NL

#### Jasmin Blanchette (Jul 08 2020 at 10:56):

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

(deleted)

#### Johan Commelin (Jul 08 2020 at 10:58):

Good luck! That was pretty horrible news.

#### Jasmin Blanchette (Jul 08 2020 at 15:08):

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.

Last updated: May 14 2021 at 13:24 UTC