format_lean

Stream: Lean for teaching

[Patrick Massot]

In format_lean I added the possibility to use tikzcd diagrams, and also include theorems without a Lean counterpart. This is used in https://www.math.u-psud.fr/~pmassot/enseignement/math114/cours5.html There is a diagram at the very bottom of the page for instance. Note that this page also feature a proof of existence of quotient.lift by hand for discussion purpose (this is actually the only Lean proof of that page).

[Patrick Massot]

@Mohammad Pedramfar I had no time to look at your interactive version yet, because I have too much teaching, administration, referee reports, perfectoid spaces etc. But you can PR it in order to avoid drifting too far away from my version.

[Kalle Kytölä]

Hello! I would love to try format_lean, but I did not get it to cooperate with my Lean. I think I installed as in the instructions, but when running, it is not clear to me what I should set as the parameter --lib-path. If I set it to the directory of my mathlib source by

format_lean --inpath test_001.lean --outdir build --lib-path ~/Lean/msc1541_2021/src

then I get

error: couldn't find value of ELAN_HOME

plus some errors about BrokenPipeError: [Errno 32] Broken pipe (presumably consequences of the original elan problem).

Could @Patrick Massot or someone else with computer skills and/or experience with format_lean help me with how to configure this? Thanks in advance!

[Kalle Kytölä]

To clarify, I believe I have elan somewhere. If I run elan show, it reports

installed toolchains
--------------------

stable (default)
leanprover-community-lean-3.20.0
leanprover-community-lean-3.23.0
leanprover-community-lean-3.24.0
leanprover-community-lean-3.26.0
leanprover-community-lean-3.28.0
leanprover-community-lean-3.30.0
leanprover-community-lean-3.31.0
leanprover-community-lean-3.32.1
leanprover-community-lean-3.33.0
leanprover-community-lean-3.34.0
leanprover-community-lean-3.35.0
leanprover-community-lean-3.35.1

active toolchain
----------------

leanprover-community-lean-3.35.1 (overridden by '/u/01/kytolak1/unix/Lean/msc1541_2021/leanpkg.toml')
Lean (version 3.35.1, commit 4887d8a30621, Release)

[Kalle Kytölä]

And still for the teaching context (or #xy): I would like to use Lean in my upcoming 2nd year metric spaces course to help students understand proofs better. Mainly I would like to concretely convey the idea that each step of a proof changes what is considered established and/or what still remains to be proven. For this I think it would be great to be able to "explore" proofs with Lean tactic state shown after each step. I believe this is exactly what Patrick's format_lean would achieve (if I got it to work).

(Of course I dream of using Lean for teaching proofs in more ways than just that. Such hopes were in fact how I got into formalization in the first place. But I have noted warnings about difficulties of doing so from Kevin and Patrick and others, so in the next course I am teaching I would only try "exploration" and possibly a few optional exercises.)

[Jireh Loreaux]

@Patrick Massot I had played with format_lean briefly a while ago and thought I had it working, but I have since encountered a problem. Whenever I try to add a comment line in a tactic proof I get an error without a build. Moreover, even without comments, the proofs don't display any lines between "Proof" and "QED". I'm running Arch (hence Python 3.12), so I tried setting up the virtual environment with Python 3.7.2 but still had the same symptoms.

[Patrick Massot]

I would need to see a minimal project with this issue

[Jireh Loreaux]

-- MWE
namespace hidden

inductive nat : Type
| zero : nat
| succ : nat → nat

local notation `ℕ` := nat

instance : has_zero ℕ := ⟨nat.zero⟩

/- Lemma
This works, but of course it's a term mode proof, so there is no tactic state.
-/
@[simp] lemma nat_zero_eq_zero : nat.zero = 0 := rfl

/- Definition
Addition of natural numbers, defined recursively, this also works
-/
def add : ℕ → ℕ → ℕ
| m 0 := m
| m (nat.succ n) := nat.succ (add m n)

instance : has_add ℕ := ⟨add⟩
/- Lemma
A lemma which is true by definition, in tactic mode (no lines or tactic state displayed).
-/
@[simp] lemma add_zero (m : ℕ) : m + 0 = m :=
begin
  -- comment breaks compilation
  refl,
end

end hidden

[Jireh Loreaux]

sorry, I can probably make it smaller, let me try and check

[Jireh Loreaux]

/- Lemma
this should not break
-/
lemma add_zero (m : ℕ) : m + 0 = m :=
begin
  -- comment breaks compilation, removing it allows compilation to succeed.
  refl,
end

[Jireh Loreaux]

This is the output to stderr inside the python venv with version 3.7.2

$ format_lean --inpath mwe.lean --outdir build2
Traceback (most recent call last):
  File "/home/jireh/.virtualenvs/format_lean/bin/format_lean", line 77, in <module>
    Fire(render_lean_file)
  File "/home/jireh/.virtualenvs/format_lean/lib/python3.7/site-packages/fire/core.py", line 141, in Fire
    component_trace = _Fire(component, args, parsed_flag_args, context, name)
  File "/home/jireh/.virtualenvs/format_lean/lib/python3.7/site-packages/fire/core.py", line 471, in _Fire
    target=component.__name__)
  File "/home/jireh/.virtualenvs/format_lean/lib/python3.7/site-packages/fire/core.py", line 681, in _CallAndUpdateTrace
    component = fn(*varargs, **kwargs)
  File "/home/jireh/.virtualenvs/format_lean/bin/format_lean", line 68, in render_lean_file
    lecture_reader.read_file(inpath)
  File "/home/jireh/.virtualenvs/format_lean/lib/python3.7/site-packages/format_lean/line_reader.py", line 49, in read_file
    self.normal_line_handler(self, line)
  File "/home/jireh/.virtualenvs/format_lean/lib/python3.7/site-packages/format_lean/objects.py", line 377, in normal_line
    file_reader.cur_line_nb, 1)
  File "/home/jireh/.virtualenvs/format_lean/lib/python3.7/site-packages/format_lean/server.py", line 34, in info
    raise LeanError(ret)
format_lean.server.LeanError: {'msgs': [{'caption': '', 'file_name': '/home/jireh/.elan/toolchains/leanprover-community-lean-3.16.5/lib/lean/library/init/data/option/basic.lean', 'pos_col': 41, 'pos_line': 30, 'severity': 'error', 'text': 'type expected at\n  o.is_some\nterm has type\n  bool'}, {'caption': '', 'file_name': '/home/jireh/.elan/toolchains/leanprover-community-lean-3.16.5/lib/lean/library/init/data/option/basic.lean', 'pos_col': 41, 'pos_line': 30, 'severity': 'error', 'text': 'type expected at\n  o.is_some\nterm has type\n  bool'}], 'response': 'all_messages'}

[Jireh Loreaux]

ooh, sorry, I think I may have figured out the problem. I had switched to an old version of Lean (3.16.5) trying to solve this problem outside my venv (I think Python 3.12 may be incompatible with format_lean, but I'm not sure). After switching back to 3.35.1 it seems to work. Sorry for the inconvenience.

[Jireh Loreaux]

@Patrick Massot Just to follow up: I figured out all my problems. I had a sorry in my original file and I didn't realize format_lean would balk at that (it's fine, I just didn't know). In my troubleshooting I (stupidly) didn't try to create an MWE first, and then I went down a rabbit hole, changed my Lean version, and then I had two problems :face_palm:. But it's all fixed now, and there are no issues with the current version of Python (3.10.1, I misspoke above), except for a deprecation warning about distutils slated for removal in Python 3.12.

[Patrick Massot]

Feel free to open a PR about this sorry issue if you want it and have time.

[Patrick Massot]

I can't spend any time to add features to this tool. I have too much to do and this tool will be completely obsolete with Lean4

[Jireh Loreaux]

No I completely understand, it's not important to me. Thanks though.