Tactic state filtering

Stream: lean4

[Patrick Massot]

I don't know the current status of widgets in Lean 4 but I have a question: is there a plan to make tactic state filtering permanent? In Lean 3 it seems to be a non-trivial task is the main reason why I still use plain text tactic states from time to time.

[Gabriel Ebner]

Widgets work today. Both the neovim and vscode extensions have PRs for widget support: https://github.com/leanprover/vscode-lean4/pull/37 https://github.com/Julian/lean.nvim/pull/123
Please help with testing if you have time!

[Gabriel Ebner]

Tactic state filtering is I believe still a todo in the vscode extension, but it is even easier to implement now than with the text-based tactic states.

[Gabriel Ebner]

Wojciech did a great job with the RPC API here. On the editor side we now have a nice data structure for the hypotheses containing the name etc. Gone are the days of string parsing using regexps! We could also add additional metadata to the hypotheses (e.g. whether they are typeclass instances or whether they have the [] binder or whether they are types, etc.) to provide even better filtering.

[Patrick Massot]

Testing this is very tempting but the whole procedure is daunting.

[Gabriel Ebner]

Is there anything we can do to make it easier to try out the PR?

[Patrick Massot]

Do we have a nice document explaining how to install everything from scratch (including Lean 4 and mathlib4)?

[Scott Morrison]

We do not have such a document. I can try to start writing it. Hopefully the essence for now is:

1. Install VSCode
2. Install the lean4 extension to VSCode
3. Install elan
4. Clone mathlib4
5. Open mathlib4 in VSCode

[Scott Morrison]

Neither lake nor mathport are quite ready for usage by people who want "nice documents" explaining installation. :-) But hopefully very soon.

[Scott Morrison]

And the whole "pre-compiled oleans" infrastructure doesn't yet exist.

[Scott Morrison]

@Patrick Massot, on a bare Ubuntu machine the following works:

#! /bin/bash

sudo apt install -y git curl

# The following test is needed in case VScode was installed by other
# means (e.g. using Ubuntu snap)
if ! which code; then
  wget -O code.deb https://go.microsoft.com/fwlink/?LinkID=760868
  sudo apt install -y ./code.deb
  rm code.deb
fi

code --install-extension leanprover.lean4

wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
bash elan-init.sh -y
rm elan-init.sh
. ~/.profile

git clone https://github.com/leanprover-community/mathlib4
cd mathlib4
leanpkg build
code .

[Patrick Massot]

Thanks Scott, I'll try this in the afternoon (I need to go and teach now).