noncomputable in the docs

Stream: general

[Eric Wieser]

Currently I've gone for

image.png

Which is a bit more mathematician-friendly than repeating-linear-gradient( 45deg, #FFFFE0, #FFFFE0 10px, #E0E0E0 10px, #E0E0E0 20px):

image.png

[Yaël Dillies]

Too bad, this looked funky.

[Eric Wieser]

There could be an "I'm a computer scientist" preference checkbox, and a similar one for mathematicians that makes meta look scary

[Yaël Dillies]

What about applying the construction zone layout to only the left bar?

[Eric Wieser]

Feel free to play around with styles at https://leanprover-community.github.io/mathlib_docs_demo/data/real/ereal.html

[Eric Wieser]

You can adjust the style for .noncomputable in the chrome inspector

[Yaël Dillies]

I'm afraid I don't know how to CSS.

[Eric Wieser]

Here's the result of

    border-image-source: repeating-linear-gradient(
45deg, #FFFF80, #FFFF80 10px, #808080 10px, #808080 20px);
    border-image-slice: 10;

image.png

[Yaël Dillies]

Okay the top looks terrible, but I like the left!

[Reid Barton]

noncomputable isn't really the right thing to be flagging anyways, it should be whether the definition depends on arbitrary choices, but we don't have a way to track that yet

[Eric Wieser]

I don't understand what you mean by that

[Eric Wieser]

Can you give an example of something that makes an "arbitrary choice" but is computable?

[Reid Barton]

No but I can give examples of things that don't make arbitrary choices yet are noncomputable

[Reid Barton]

I think just the word "noncomputable" is plenty

[Eric Wieser]

My thinking was that the word noncomputable might be too noisy, so we could use color or something to indicate it instead without making it take longer to find the lemma name in the decl header

[Eric Wieser]

Writing it as

@[simp] noncomputable
def some_def

might also be the way to go, which I think someone suggested earlier; it just would be a little odd to use a different convention to the mathlib source code in that regard

[Reid Barton]

I was thinking that noncomputable could go on the previous line too. I guess it costs an extra line when there weren't any other attributes, but that seems pretty minor.

[Reid Barton]

Eric Wieser said:

My thinking was that the word noncomputable might be too noisy, so we could use color or something to indicate it instead without making it take longer to find the lemma name in the decl header

For me any kind of visual distinction (like the dashed bar) is more distracting than just some more plain text. It's still easy enough to find the declaration name with noncomputable on the same line. I notice that compared to your screenshot, plain and bold text are more distinct on my system/display, which probably helps.

[Ruben Van de Velde]

Eric Wieser said:

My thinking was that the word noncomputable might be too noisy, so we could use color or something to indicate it instead without making it take longer to find the lemma name in the decl header

I feel like I would take a long time to figure out what the alternate styling meant, if the word "noncomputable" wasn't there, but maybe that's just me

[Scott Morrison]

We can just move noncomputable to the previous line throughout mathlib as well. I like it.

[Eric Wieser]

Should we do the same with meta?

[Mario Carneiro]

It would be better if it was an attribute. But I don't want to diverge too much from lean 4 style here

[Reid Barton]

Eric Wieser said:

Should we do the same with meta?

A separate question, but I think a different color border makes a lot more sense for meta

[Eric Wieser]

I'd argue that metaand noncomputable should be treated pretty much the same way' one is a "don't care about soundness" flag, and the other is a "don't care about computation" flag.

[Rob Lewis]

I'm really not a fan of the broken bars for noncomputable. It's a very loud flag for something that most people won't care about, and there's no obvious connection between them and the noncomputable word, so people will wonder what this glaring marker means and assume it's relevant.

[Rob Lewis]

If anything I'd prefer a visual notice like that for meta, but really, the word is plenty for both.

[Eric Wieser]

Alright, I've backed out the stylesheet change

[Eric Wieser]

Someone can add styling for meta in a follow-up PR, the css class is now there so it's easy to experiment in-browser