playground for github

Stream: general

[Billy Price]

I've see then lean playground for code snippets here in zulip, I'd like to know if there's a way I can attach one to a github repository so my lean code can be viewed and stepped through by anyone

[Eric Wieser]

Gitpod is probably your best bet

[Billy Price]

Even if it's one file?

[Eric Wieser]

I mean, you said you had a github repository right?

[Eric Wieser]

I added gitpod support to my repo recently, all you need is a single yml file and a link:

https://github.com/pygae/lean-ga/compare/778537b%5E...1bde715

[Eric Wieser]

Also by making it a proper lean project with a leanpkg.toml you can specify the exact version of lean and mathlib that your single file needs, otherwise it's doomed to break.

[Billy Price]

Okay I tried it out, and it seems a bit heavy. Myabe that's just due to the size of your repo. I'll give it a go for my repo, thanks :)

[Eric Wieser]

If you're not using mathlib at all you can probably make it less heavy, but I assume you are