## Stream: new members

### Topic: back? command

#### Tony Johnson (Jun 23 2020 at 22:22):

I was watching this tutorial video and there was a command "back?" that I don't seem to have in my default lean environment. I'm running 3.4.2 stable toolchain. Does anybody know where this command is?

#### Bryan Gin-ge Chen (Jun 23 2020 at 22:24):

Sadly, it's not public yet as far as I know. @Scott Morrison has been busy with other things, I think.

#### Scott Morrison (Jun 23 2020 at 22:25):

I tinker with it every do often, but have never reached something satisfactory.

#### Scott Morrison (Jun 23 2020 at 22:25):

If anyone wants to work on it, or something similar, I'm happy to discuss.

#### Scott Morrison (Jun 23 2020 at 22:27):

The tactic in that demo is cheating too much. I've given it a very small set of lemmas to work with. In the real world premise selection is hard and/or requires a lot of infrastructure.

#### Kevin Buzzard (Jun 23 2020 at 22:32):

Independent of that @Tony Johnson , did you know that we're on Lean 3.16.4 by now?

#### Tony Johnson (Jun 23 2020 at 22:40):

@Kevin Buzzard , I ran the "elan update" command
$elan update info: syncing channel updates for 'stable' info: latest update on stable, lean version v3.16.4 info: checking for self-updates stable unchanged - Lean (version 3.16.4, commit be72c8dc527a, Release) However I still get this...$ elan toolchain list
stable
3.4.2 (default)

#### Bryan Gin-ge Chen (Jun 23 2020 at 22:57):

You'll want to run leanproject up in your project to update it to the latest Lean and mathlib. Warning: this might break your code, so be careful if you have a lot of it.

(If you don't know what leanproject is, see #install)

#### Tony Johnson (Jun 23 2020 at 23:14):

@Bryan Gin-ge Chen "pip install mathlibtools" is broken on my MSYS installation. However leanpkg update seems to work on the mathlib update

#### Bryan Gin-ge Chen (Jun 23 2020 at 23:55):

Hmm, I don't know that MSYS is recommended. I've been using git bash + miniconda python on Windows and things have been working well.

#### Andrew Ashworth (Jun 24 2020 at 01:01):

You weren't able to compile Lean 3 from source on Windows with Visual Studio for quite a long time; that's why MinGW is recommended.

#### Tony Johnson (Jun 24 2020 at 01:50):

@Bryan Gin-ge Chen I'll have to try that.

Last updated: May 15 2021 at 00:39 UTC