What do I use instead of `lean --run` here?

Stream: new members

[Eduardo Ochs]

Hi all,

I have some questions about "running lean" that will sound very, very wrong if I don't explain who is my target audience, so let me do that first...

I work in a campus in the countryside of Brazil, and I'm trying to adapt what I presented in the last EmacsConf - long story short: "Emacs and Maxima for students who have never seen a terminal in their lives" - to Lean. I also gave a mini-workshop on Lean for just five people one year ago, and two of the students there were also in the "have never seen a terminal in their lives" category. My instructions for that workshop are here, and they are currently broken due to recent changed on Lean. I am trying to fix these instructions in a way that will make them much easier to troubleshoot - I am also trying to understand some things that the lean4-mode for Emacs does out-of-the-box by reproducing them in a more low-level setting.

Here is my current script. Note that we execute it line by line, by typing f8 on each line to send it to a terminal running Emacs, and people are expected to wait until each line finishes execution before sending another one.

du -ch  ~/.elan/
rm -Rfv ~/.elan/
rm -Rfv /tmp/elan-install/
mkdir   /tmp/elan-install/
cd      /tmp/elan-install/
wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
# The empty line after the "sh" below means "1) Proceed with installation (default)".
sh elan-init.sh --verbose --no-modify-path

find     ~/.elan/
ls -lAF  ~/.elan/
ls -lAF  ~/.elan/bin/
# file   ~/.elan/bin/*
du -chd2 ~/.elan/
# ^ Output:
#   13M   total

cat ~/.elan/env
export PATH="$HOME/.elan/bin:$PATH"

cd /tmp/elan-install/

cat > test1.lean <<'%%%'
  def main := IO.println "Hello"
%%%
lean --run test1.lean
# ^ Output:
#   info: downloading https://releases.lean-lang.org/lean4/v4.19.0/lean-4.19.0-linux.tar.zst
#   info: installing /home/edrx/.elan/toolchains/leanprover--lean4---v4.19.0
#   Hello

du -chd2 ~/.elan/
# ^ Output:
#   1.6G   total

cat > test2.lean <<'%%%'
  def
  #check List.map
%%%
lean --run test2.lean

Here is the first question. The "lean --run test2.lean" at the end outputs this:

List.map.{u, v} {α : Type u} {β : Type v} (f : α → β) (l : List α) : List β
(interpreter) unknown declaration 'main'

Is there an easy way to get an output like this intead?

test2.lean 1 3  info  List.map.{u, v} {α : Type u} {β : Type v} (f : α → β) (l : List α) : List β (lsp)

That's what I get in Emacs in the "*Flycheck errors*" buffer - Emacs sets up a LSP server for Lean, sends some things to it, and formats its answer in that compact way. Is there a way - not too painful - to do that from a shell?

[Eric Wieser]

I think dropping the --run would be a good start

[Eric Wieser]

--run is for main, not for general diagnostics

[Eduardo Ochs]

Done! Ok, this got rid of the (interpreter) unknown declaration 'main'...

[Eduardo Ochs]

The next step is to simulate talking to a LSP server, or to talk to a LSP server from a shell...