Zulip Chat Archive

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?

https://www.youtube.com/watch?v=2FQOakOfP00&feature=youtu.be&t=1318

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)