Zulip Chat Archive

Stream: new members

Topic: Lean in emacs

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'

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

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⟩

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

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"}

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

Jason Orendorff (Jun 15 2020 at 18:16):

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

Jason Orendorff (Jun 15 2020 at 18:23):

same error message still. hmm.

Jalex Stark (Jun 15 2020 at 18:29):

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

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'

Jalex Stark (Jun 15 2020 at 18:38):

what about leanproject -h?

Jason Orendorff (Jun 15 2020 at 18:38):

That works, in that it prints the help

Jason Orendorff (Jun 15 2020 at 18:39):

leanproject --version says 0.0.8

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

Jalex Stark (Jun 15 2020 at 18:39):

yay!

Jason Orendorff (Jun 15 2020 at 18:40):

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

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

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.

Jason Orendorff (Jun 15 2020 at 18:45):

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

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

Jason Orendorff (Jun 15 2020 at 18:48):

leanpkg was not in my $PATH

Jason Orendorff (Jun 15 2020 at 18:50):

leanproject new works now...

Jason Orendorff (Jun 15 2020 at 18:52):

The example works in emacs! So happy

Jason Orendorff (Jun 15 2020 at 18:55):

thanks for being there :)

Last updated: Dec 20 2023 at 11:08 UTC