format_lean woes

Stream: new members

[Miguel Raz Guzmán Macedo]

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]

Would appreciate any help, I barely know python.

[Miguel Raz Guzmán Macedo]

Also, is there an IPython / lean interaction guide?

[Patrick Massot]

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

[Miguel Raz Guzmán Macedo]

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]

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

[Reid Barton]

What is format_lean?

[Reid Barton]

Oh, Patrick's thing!

[Miguel Raz Guzmán Macedo]

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
to jump to mathlib's version
-/
#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]

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]

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

[Miguel Raz Guzmán Macedo]

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]

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]

OK, it produced an html folder

[Miguel Raz Guzmán Macedo]

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]

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

[Patrick Massot]

Your Lean code doesn't use valid format_lean markup

[Miguel Raz Guzmán Macedo]

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

[Patrick Massot]

@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]

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

[Patrick Massot]

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

[Kevin Buzzard]

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]

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
    lecture_reader.read_file(inpath)
  File "/home/mrg/.local/lib/python3.7/site-packages/format_lean/line_reader.py", line 48, in read_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
    file_reader.cur_line_nb, 1)
  File "/home/mrg/.local/lib/python3.7/site-packages/format_lean/server.py", line 34, in info
    raise LeanError(ret)
format_lean.server.LeanError: {'msgs': [{'caption': '', 'file_name': '/usr/lib/lean-mathlib/src/data/set/basic.lean', 'pos_col': 71, 'pos_line': 368, 'severity': 'error', 'text': '(deterministic) timeout'}, {'caption': '', 'file_name': '/usr/lib/lean-mathlib/src/data/set/basic.lean', 'pos_col': 3, 'pos_line': 369, 'severity': 'error', 'text': '(deterministic) timeout'}], 'response': 'all_messages'}

[Miguel Raz Guzmán Macedo]

Also Patrick, it's beautiful!