Zulip Chat Archive

Stream: new members

Topic: back? command


view this post on Zulip 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?

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jun 23 2020 at 22:25):

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

view this post on Zulip Scott Morrison (Jun 23 2020 at 22:25):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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