## Stream: new members

### Topic: format_lean woes

#### Miguel Raz Guzmán Macedo (Oct 12 2019 at 18:31):

Hey all, brand new fedora 30 install with all lean dependencies installed. I have a simple "hello world" lean script in limits.lean but don't know why I get this error (I supposed its a python2/3 mishap, but I haven't moved any configs there)

⋊> ~/d/l/t/src on lean-3.4.2 ⨯ format_lean --inpath limits.lean --outdir build --lib-path /usr/lib/lean-mathlib/src
Traceback (most recent call last):
File "/home/mrg/deps/lean/format_lean/bin/format_lean", line 77, in <module>
Fire(render_lean_file)
File "/home/mrg/.local/lib/python3.7/site-packages/fire/core.py", line 138, in Fire
component_trace = _Fire(component, args, parsed_flag_args, context, name)
File "/home/mrg/.local/lib/python3.7/site-packages/fire/core.py", line 471, in _Fire
target=component.__name__)
File "/home/mrg/.local/lib/python3.7/site-packages/fire/core.py", line 675, in _CallAndUpdateTrace
component = fn(*varargs, **kwargs)
File "/home/mrg/deps/lean/format_lean/bin/format_lean", line 30, in render_lean_file
lean_exec_path = Path(distutils.spawn.find_executable('lean'))
AttributeError: module 'distutils' has no attribute 'spawn'


#### Miguel Raz Guzmán Macedo (Oct 12 2019 at 18:32):

Would appreciate any help, I barely know python.

#### Miguel Raz Guzmán Macedo (Oct 12 2019 at 18:33):

Also, is there an IPython / lean interaction guide?

#### Patrick Massot (Oct 12 2019 at 18:34):

Could you post your Lean project? Maybe an archive of everything except _target

#### Miguel Raz Guzmán Macedo (Oct 12 2019 at 18:41):

leanpkg.toml
[package]
name = "test"
version = "0.1"
lean_version = "3.4.2"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "27515619bcd834006f2936b292021135496b4efb"}


#### Miguel Raz Guzmán Macedo (Oct 12 2019 at 18:42):

leanpkg.path
builtin_path
path _target/deps/mathlib/src
path ./src


#### Reid Barton (Oct 12 2019 at 18:45):

What is format_lean?

#### Reid Barton (Oct 12 2019 at 18:45):

Oh, Patrick's thing!

#### Miguel Raz Guzmán Macedo (Oct 12 2019 at 18:45):

import topology.basic
import data.real.basic

#eval 1 + 1

#check topological_space

local attribute [instance, priority 0] classical.prop_decidable

#eval 1 + 1
/-
Our first goal is to define the set of upper bounds of a set of real numbers.
This is already defined in mathlib (in a more general context), but we repeat
it for the sake of exposition Right-click "upper_bounds" below to get offered
-/
#check upper_bounds

/-- The set of upper bounds of a set of real numbers ℝ -/
def up_bounds (A : set ℝ) := { x : ℝ | ∀ a ∈ A, a ≤ x}

/-- Predicate is_max a A means a is a maximum of A -/
def is_max (a : ℝ) (A : set ℝ) := a ∈ A ∧ a ∈ up_bounds A

/-
In the above definition, the symbol ∧ means "and". We also see the most
visible difference between set theoretic foundations and type theoretic ones
(used by almost all proof assistants). In set theory, everything is a set, and the
only relation you get from foundations are = and ∈. In type theory, there is
a meta-theoretic relation of "typing": a : ℝ reads "a is a real number" or,
more precisely, "the type of a is ℝ". Here "meta-theoretic" means this is not a
statement you can prove or disprove inside the theory, it's a fact that is true or
not. Here we impose this fact, in other circumstances, it would be checked by the
Lean kernel.
By contrast, a ∈ A is a statement inside the theory. Here it's part of the
definition, in other circumstances it could be something proven inside Lean.
-/

/- For illustrative purposes, we now define an infix version of the above predicate.
It will allow us to wite a is_a_max_of A, which is closer to a sentence.
-/


#### Miguel Raz Guzmán Macedo (Oct 12 2019 at 18:46):

and then in the folder that containts src/limits.lean I do
~/d/l/t/src on lean-3.4.2 ⨯ format_lean --inpath limits.lean --outdir build --lib-path /usr/lib/lean-mathlib/src

#### Patrick Massot (Oct 12 2019 at 18:51):

Can you try running format_project from the root of your project?

#### Miguel Raz Guzmán Macedo (Oct 12 2019 at 18:52):

first format_project, then format_lean?

It says it couldn't find a format.toml but would continue anyways.
Then rendered src/limits.lean

#### Patrick Massot (Oct 12 2019 at 18:54):

There are two scripts. format_lean itself was meant to render individual Lean files, not necessarily inside a proper Lean project. But I never use it, and it may be broken. format_project renders a whole Lean project, and should work.

#### Miguel Raz Guzmán Macedo (Oct 12 2019 at 18:54):

OK, it produced an html folder

#### Miguel Raz Guzmán Macedo (Oct 12 2019 at 18:56):

OK, it produced a site, but the CSS was all bungled up - (text overlapping the tactic state, no lean code showing)

#### Miguel Raz Guzmán Macedo (Oct 12 2019 at 18:57):

I opened the limits.html file, which I guess is the correct one, but I may be wrong.

#### Patrick Massot (Oct 12 2019 at 18:57):

Your Lean code doesn't use valid format_lean markup

#### Miguel Raz Guzmán Macedo (Oct 12 2019 at 18:58):

Ach so. Where can I find a description of the markup specification
?

#### Patrick Massot (Oct 12 2019 at 21:08):

@Miguel Raz Guzmán Macedo I fixed the bug you found, and created an example at https://leanprover-community.github.io/format_lean/.

#### Patrick Massot (Oct 12 2019 at 21:09):

I'll try to write a specification of what is currently supported, but it will be very short...

#### Patrick Massot (Oct 12 2019 at 21:09):

I may do that tomorrow, but creating the above three web pages exhausted the time I could allocate to this today.

#### Kevin Buzzard (Oct 12 2019 at 21:21):

Thanks Patrick. Very shortly I will be using format-lean again and I realised just the other day that I had essentially completely forgotten what the formatter could do and how to do it.

#### Miguel Raz Guzmán Macedo (Oct 19 2019 at 03:41):

Miguel Raz Guzmán Macedo I fixed the bug you found, and created an example at https://leanprover-community.github.io/format_lean/.

I tried this again after pulling your changes.
the example from your repo renders perfectly on the web browser, but I not get this error...

⋊> ~/p/l/f/e/src on master ⨯ format_lean --inpath sandwich.lean --outdir build --lib-path /usr/lib/lean-mathlib/src
Traceback (most recent call last):
File "/home/mrg/deps/lean/format_lean/bin/format_lean", line 77, in <module>
Fire(render_lean_file)
File "/home/mrg/.local/lib/python3.7/site-packages/fire/core.py", line 138, in Fire
component_trace = _Fire(component, args, parsed_flag_args, context, name)
File "/home/mrg/.local/lib/python3.7/site-packages/fire/core.py", line 471, in _Fire
target=component.__name__)
File "/home/mrg/.local/lib/python3.7/site-packages/fire/core.py", line 675, in _CallAndUpdateTrace
component = fn(*varargs, **kwargs)
File "/home/mrg/deps/lean/format_lean/bin/format_lean", line 68, in render_lean_file
self.normal_line_handler(self, line)
File "/home/mrg/.local/lib/python3.7/site-packages/format_lean/objects.py", line 370, in normal_line