Zulip Chat Archive

Stream: new members

Topic: Lean in emacs


view this post on Zulip Jason Orendorff (Jun 15 2020 at 14:03):

Is there a good way to use Emacs and lean-mode with mathlib? I'm pretty sure I haven't got it working properly yet. For the first example in _Mathematics in Lean_ <https://leanprover-community.github.io/mathematics_in_lean/introduction.html#overview> , I get

7:6: unknown identifier 'mul_left_comm'

view this post on Zulip Matt Earnshaw (Jun 15 2020 at 15:14):

this is a problem with the documentation, a bunch of algebra was recently moved from core to mathlib, so you need to import algebra.group.basic to use mul_left_comm

view this post on Zulip Bryan Gin-ge Chen (Jun 15 2020 at 15:28):

The example works for me as is in VS Code and even in the web editor. Did you copy the entire code snippet?

import data.nat.parity
open nat

example :  m n, even n  even (m * n) :=
assume m n k, (hk : n = 2 * k),
have hmn : m * n = 2 * (m * k),
  by rw [hk, mul_left_comm],
show  l, m * n = 2 * l,
  from ⟨_, hmn

view this post on Zulip Jason Orendorff (Jun 15 2020 at 18:11):

Yes, I copied the whole snippet. import algebra.group.basic doesn't help, and the version of mathlib in my _target directory doesn't seem to define it anywhere

view this post on Zulip Bryan Gin-ge Chen (Jun 15 2020 at 18:13):

What does the leanpkg.toml say in your mathematics_in_lean directory? Mine says this:

[package]
name = "mathematics_in_lean_source"
version = "0.1"
lean_version = "leanprover-community/lean:3.14.0"
path = "src"

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

view this post on Zulip Bryan Gin-ge Chen (Jun 15 2020 at 18:14):

which I guess agrees with the latest master on github: https://github.com/leanprover-community/mathematics_in_lean/blob/master/leanpkg.toml

view this post on Zulip Jason Orendorff (Jun 15 2020 at 18:16):

I have a different rev. pasting in your rev...

view this post on Zulip Jason Orendorff (Jun 15 2020 at 18:23):

same error message still. hmm.

view this post on Zulip Jalex Stark (Jun 15 2020 at 18:29):

(did you paste in the rev _and_ have leanproject update your _target folder to that revision?)

view this post on Zulip Jason Orendorff (Jun 15 2020 at 18:37):

Everything I try to do from the command line says [Errno 2] No such file or directory: 'leanpkg': 'leanpkg'

view this post on Zulip Jalex Stark (Jun 15 2020 at 18:38):

what about leanproject -h?

view this post on Zulip Jason Orendorff (Jun 15 2020 at 18:38):

That works, in that it prints the help

view this post on Zulip Jason Orendorff (Jun 15 2020 at 18:39):

leanproject --version says 0.0.8

view this post on Zulip Jason Orendorff (Jun 15 2020 at 18:39):

OK, I did a fresh leanproject get mathematics_in_lean and opened it in VS Code, and it works in Code, no errors

view this post on Zulip Jalex Stark (Jun 15 2020 at 18:39):

yay!

view this post on Zulip Jason Orendorff (Jun 15 2020 at 18:40):

It did a leanpkg configure that I don't know how to do myself

view this post on Zulip Jalex Stark (Jun 15 2020 at 18:41):

i'd guess that if want to type leanpkg configure then in fact you're always happy to type leanproject build instead

view this post on Zulip Jalex Stark (Jun 15 2020 at 18:43):

I think that if you just use leanproject get, leanproject new, and leanproject up, and don't manually mess with *.olean or _target, then you don't run into problems.

view this post on Zulip Jason Orendorff (Jun 15 2020 at 18:45):

$ leanproject new example2
[Errno 2] No such file or directory: 'leanpkg': 'leanpkg'

view this post on Zulip Jalex Stark (Jun 15 2020 at 18:46):

weird I feel like leanproject needs to do the same sorts of work when it runs new and when it runs get

view this post on Zulip Jason Orendorff (Jun 15 2020 at 18:48):

leanpkg was not in my $PATH

view this post on Zulip Jason Orendorff (Jun 15 2020 at 18:50):

leanproject new works now...

view this post on Zulip Jason Orendorff (Jun 15 2020 at 18:52):

The example works in emacs! So happy

view this post on Zulip Jason Orendorff (Jun 15 2020 at 18:55):

thanks for being there :)


Last updated: May 12 2021 at 23:13 UTC