VSCode highlighting

Stream: general

[Patrick Massot]

How hard would it be to have a VSCode extension setting defining a list of extra words that should be highlighted (say in tactic mode if this makes sense)?

[Bryan Gin-ge Chen]

VS Code expects grammars to be provided as a file, so I don't see an easy way to modify the grammar dynamically: https://code.visualstudio.com/api/language-extensions/syntax-highlight-guide#contributing-a-basic-grammar

See also https://github.com/microsoft/vscode/issues/53885

VS Code does support semantic highlighting but this looks to me like a big project.

I'm sure Gabriel wouldn't mind a PR which just added some extra keywords to this file: https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json

The grammar doesn't currently have any way of detecting what's in tactic mode or not at the moment though.

[Patrick Massot]

Too bad. Thanks for answering. I'm pretty sure Gabriel wouldn't like my list.

[Gabriel Ebner]

Let me clarify the criteria for inclusion in the vscode syntax highlighting: I will add it if and only if it is used in mathlib.

[Patrick Massot]

Let me clarify that my list is absolutely not for general consumption :wink:

[Patrick Massot]

It's part of my controlled natural language experiment.

[Gabriel Ebner]

So it's also French as well? Yes, the chances are not good.

[Gabriel Ebner]

It might be possible to use the same trick that we use for Lean 4 here. Have two syntax highlighting files, and the extension sets a property on the file that changes the highlighting. This could even be in two different extension. But this takes work and time.

[Patrick Massot]

Yes, it is. If you feel brave, open the next block

precedence `applique`:0
precedence `appliqué`:0
precedence `à`:0
precedence `on`:0
precedence `obtient`:0
precedence `que`:0
precedence `tel`:0
precedence `convient`:0
precedence `les`:0
precedence `deux`:0
precedence `une`:0
precedence `contradiction`:0
precedence `conclut`:0
precedence `par`:0
precedence `calcule`:0
precedence `dans`:0
precedence `combine`:0
precedence `remplace`:0
precedence `contrapose`:0
precedence `discute`:0
precedence `selon`:0
precedence `il`:0
precedence `suffit`:0
precedence `de`:0
precedence `montrer`:0

[Patrick Massot]

I need to prepare Lean+mathlib+VScode+extension bundles for my course anyway. I may simply hack the grammar there.

[Eric Wieser]

@Patrick Massot, if these are keywords for your natural language tactics, would you consider begin[natural] end? If so, I think the lean grammar could do something like "if you see this funny tactic block, delegate to another syntax highlighter"

[Eric Wieser]

Which at least would mean there are only a few lines of weirdness in lean-vscode instead of an unexpected pile of French words!

[Sebastien Gouezel]

Je suis curieux de voir ce que ça va donner. Tu pourras poster un exemple de tes fichiers quand tu seras content de ce à quoi ça ressemble ?

(Sorry for the French, but it feels in line with the discussion :-)

[Patrick Massot]

Again, I never suggested to add any word to the official VScode extension. I was asking about a new variable in settings that any user (or Lean project) could set.

[Eric Wieser]

It looks like you might be looking for an "injection grammar"

[Eric Wieser]

https://code.visualstudio.com/api/language-extensions/syntax-highlight-guide#injection-grammars

[Eric Wieser]

Which at least would mean you don't have to fork lean-vscode, you can just distribute a custom extension alongside it

[Patrick Massot]

Thanks for the pointer Eric!

[Patrick Massot]

Small sample for @Sebastien Gouezel

import m154
import .tactiques

-- Définition de « limite de f en x₀ = y₀ »
-- Lean n'a pas besoin de parenthèse dans f(x)
def continue_en (f : ℝ → ℝ) (x₀ : ℝ) : Prop :=
∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε

-- Une suite u est une fonction de ℕ dans ℝ
-- Définition de « u tend vers l »
def limite_suite (u : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

-- Si f est continue en x₀ et la suite u tend vers x₀ alors la suite f ∘ u,
-- qui envoie n sur f (u n), tend vers f x₀
example (f u x₀) (hu : limite_suite u x₀) (hf : continue_en f x₀) :
  limite_suite (f ∘ u) (f x₀) :=
begin
  Montrons que ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |(f ∘ u) n - f x₀| ≤ ε,
  Soit (ε > 0),
  Par hf appliqué à [ε, ε_pos] on obtient δ tel que
    (δ_pos : δ > 0) (Hf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε),
  Par hu appliqué à [δ, δ_pos] on obtient N tel que
    (Hu : ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |u n - x₀| ≤ δ),
  Montrons que N convient,
  Soit (n ≥ N),
  Par Hf il suffit de montrer que |u n - x₀| ≤ δ,
  On conclut par Hu appliqué à [n, n_ge],
end

def croissante (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≤ f x₂

example (f g : ℝ → ℝ) (hf : croissante f) (hg : croissante g) : croissante (g ∘ f) :=
begin
  Soit x₁ x₂,
  Supposons h : x₁ ≤ x₂,
  Montrons que g (f x₁) ≤ g (f x₂),
  Par hf appliqué à [x₁, x₂, h] on obtient (hf' : f x₁ ≤ f x₂),
  On conclut par hg appliqué à [f x₁, f x₂, hf'],
end

[Patrick Massot]

Let me emphasize again that the main goal is not to make Lean easier to write (students actually manage to write Lean code), but to make it easier to go from Lean to paper.

[Johan Commelin]

I would love to have an english version of this!

[Patrick Massot]

To be honest, I'm surprised by how well it works. I'm almost thinking we should maybe think a bit about seriously using something like this even in mathlib.

[Johan Commelin]

we only need to also have versions with lowercases letter, and replace . by something else, so that we can end sentences with . instead of ,.

[Johan Commelin]

and and should be a noop.

[Sebastien Gouezel]

It definitely helps here that French is disjoint from Lean keywords.

[Eric Wieser]

Do begin[foo] end blocks get custom parsers (eg, can choose something other than commas), or just a custom monad type?

[Kevin Buzzard]

This is awesome! Those proofs are really cool!

[Patrick Massot]

Note that those tactics are not only aliases for the standard tactics with crazy parsers, they also work more to prove stuff we would never write on paper. For instance On conclut par H looks like an alias to exact but it also tries apply H and linarith only [H].

[Patrick Massot]

They also do some cleanup compared to their vanilla versions, for instance beta-reductions.

[Patrick Massot]

And they work to hide intuistionistic madness.

[Patrick Massot]

Blurring the distinction between or.elim and excluded middle, or between cases and choose.

[Patrick Massot]

Also, Montrons que is not only change. If the goal is a disjunction, it will try left, change ..., and right, change ....

[Kevin Buzzard]

Patrick this is really fabulous. I would imagine that people like Hales and Koepke would be very interested in what you are doing. Thanks for sharing!

[Alex Peattie]

I agree that this is very cool :smile: !

Patrick Massot said:

How hard would it be to have a VSCode extension setting defining a list of extra words that should be highlighted (say in tactic mode if this makes sense)?

I think if you just wanted a set of words to have different styling throughout the document, you could do this with decorations in VSCode. This is how the highlight-words extension works for example. The disadvantage of not using the grammar is that it'd be harder to, say, not do the highlighting within comments.

[Yaël Dillies]

Very meta. image.png

[Marc Masdeu]

Johan Commelin said:

I would love to have an english version of this!

I looked hard for typical food staples of english cuisine, but unfortunately none of them have made it into Zulip yet.