Zulip Chat Archive

Stream: general

Topic: generalizing

Sebastien Gouezel (Apr 18 2019 at 20:27):

In VSCode, in a line like

  induction n using with_top_nat_induction with n IH Itop generalizing F,

the keywords using and with are in blue, but not generalizing. Is there an easy fix to this?

Sebastien Gouezel (Apr 18 2019 at 20:28):

Same in Zulip, by the way

Mario Carneiro (Apr 18 2019 at 20:32):

The zulip highlighting is not so easy; that's coming from the third party pygments repo, although you could try submitting a PR. The vscode syntax highlighting is in https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json, so you can add "generalizing" there

Kevin Buzzard (Apr 18 2019 at 20:46):

this is not the only missing blue thing IIRC...

Mario Carneiro (Apr 18 2019 at 20:47):

indeed; my general impression is that most lean highlighting things are very out of date (e.g. lean 2)

Patrick Massot (Apr 18 2019 at 20:47):

indeed

Mario Carneiro (Apr 18 2019 at 20:48):

and of course they are static, so they can't adapt to locally defined user commands and new tokens

Scott Olson (Apr 18 2019 at 23:33):

Long term, one might want the VSCode syntax highlighting to be partially based on information from the Lean compiler, like in the Idris REPL or Agda's HTML output. In that case, the parsing code for tactics could mark which words are "keywords" and it could automatically highlight those in blue without adding them to a static global list. Bit of work, though.

Keeley Hoek (Apr 18 2019 at 23:34):

The main thing is that all of this type of stuff requires changes to core lean, which is currently a bit taboo since mainline development has been frozen.

Scott Olson (Apr 18 2019 at 23:34):

Yeah, I think my suggestion is more of a Lean 4 suggestion

Keeley Hoek (Apr 18 2019 at 23:36):

(Secretly I'm hoping https://github.com/leanprover-community/lean gets some traction in the meantime.)

Mario Carneiro (Apr 19 2019 at 00:21):

I guess it's possible for the vscode syntax highlighter to communicate with the lean server? Not sure what is required in the vscode-lean extension for that

Johan Commelin (Apr 19 2019 at 05:40):

(Secretly I'm hoping https://github.com/leanprover-community/lean gets some traction in the meantime.)

@Keeley Hoek If you want traction, I think we first need to merge some of the PRs and to make some binary releases.

Mario Carneiro (Apr 19 2019 at 05:57):

we're building up a healthy number of PRs in the meantime. We still need to work out the kinks in the build pipeline, but the progress has been encouraging

Simon Hudon (Apr 19 2019 at 14:10):

I'm getting the nightly release working again. Then we can have a branch of mathlib that we can routinely test against new versions.

Last updated: Dec 20 2023 at 11:08 UTC