Zulip Chat Archive

Stream: Lean for teaching

Topic: format_lean

Patrick Massot (Apr 16 2019 at 21:31):

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 (Apr 16 2019 at 21:32):

@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ä (Dec 10 2021 at 10:15):

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ä (Dec 10 2021 at 10:16):

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

installed toolchains

stable (default)

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ä (Dec 10 2021 at 10:16):

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 (Jan 12 2022 at 16:53):

@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 (Jan 12 2022 at 16:54):

I would need to see a minimal project with this issue

Jireh Loreaux (Jan 12 2022 at 16:55):

-- 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 :=
  -- comment breaks compilation

end hidden

Jireh Loreaux (Jan 12 2022 at 16:55):

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

Jireh Loreaux (Jan 12 2022 at 16:58):

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

Jireh Loreaux (Jan 12 2022 at 16:59):

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>
  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
  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
  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 (Jan 12 2022 at 17:02):

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 (Jan 12 2022 at 17:51):

@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 (Jan 12 2022 at 17:52):

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

Patrick Massot (Jan 12 2022 at 17:54):

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 (Jan 12 2022 at 17:56):

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

Last updated: Dec 20 2023 at 11:08 UTC