How to write Lean code in spoilers

Stream: general

[Kevin Buzzard]

(this comment was moved to a new thread from under a comment where there was Lean code without syntax highlighting in a spoiler block)

In spoilers you can use ````lean4 and end with ```` to quote code.

[Aaron Liu]

I think you have to should use lean4 because lean is lean3

[Kevin Buzzard]

(Testing indicates that you're right; I edited)

[Michael Rothgang]

Thanks; corrected!

[Yaël Dillies]

Aaron Liu said:

I think you have to should use lean4 because lean is lean3

You can also nothing since the default language for code blocks is lean4 on this Zulip

[Kevin Buzzard]

My point was that doing nothing doesn't work in the spoiler case, that was why I brought this up.

[Notification Bot]

6 messages were moved here from #Is there code for X? > Cotangent Bundle as a Manifold by Kevin Buzzard.

[Yaël Dillies]

Really?

lemma let_us_see! : True := trivial

[Yaël Dillies]

Oh indeed, that's very surprising! Could be worth bringing it up to the Zulip people.

[Anne Baanen]

IIRC, lean meaning Lean 3 is a choice by the code highlighter that Zulip depends on. So if we fix it in that project, it should (eventually) make its way to Zulip too. But I don't know the right keywords to search for...

[Yaël Dillies]

@Eric Wieser should know what to do

[Eric Wieser]

Anne Baanen said:

IIRC, lean meaning Lean 3 is a choice by the code highlighter that Zulip depends on. So if we fix it in that project, it should (eventually) make its way to Zulip too. But I don't know the right keywords to search for...

This was a deliberate choice to preserve existing documents that used lean to highlight lean3 code

[Eric Wieser]

I think for quite some time this was true of python vs python3 too

[Eric Wieser]

The highlighter in question is Pygments

[Eric Wieser]

Probably we also need to update it with all the new private meta import etc keywords

[Eric Wieser]

(note here that "documents" includes the source code of old LaTeX papers using minted for Lean 3)

[Jakub Nowak]

Maybe related. I can type "<grave> <grave> <grave> l <TAB>", and this will automatically complete "l" to "lean4" and create closing "<grave> <grave> <grave>". Inside spoiler it still completes "l" to "lean4", but doesn't create closing "<grave> <grave> <grave>".

[Kevin Buzzard]

Inside spoiler you're probably already in a three-grave situation, so you might be closing it not opening it.