Zulip Chat Archive

Stream: general

Topic: generalizing


view this post on Zulip 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?

view this post on Zulip Sebastien Gouezel (Apr 18 2019 at 20:28):

Same in Zulip, by the way

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 18 2019 at 20:46):

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

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Apr 18 2019 at 20:47):

indeed

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Olson (Apr 18 2019 at 23:34):

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

view this post on Zulip Keeley Hoek (Apr 18 2019 at 23:36):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: May 16 2021 at 20:13 UTC