Zulip Chat Archive

Stream: lean4

Topic: Gotta prove fast


Richard L Ford (Jan 17 2022 at 03:32):

I notice that @Sebastian Ullrich is giving a talk on Saturday titled "Gotta prove fast: building an ecosystem for effortless native compilation of tactics". I won't be able to attend and wonder if there is a preprint for this talk. Also I was wondering if any of the code for this is publicly available. I'd be interested in seeing it.

Sebastian Ullrich (Jan 17 2022 at 08:30):

All POPL tracks will be available on YouTube I believe. The most relevant PRs are https://github.com/leanprover/lean4/pull/795 and https://github.com/leanprover/lean4/pull/949 (the final glue).

Richard L Ford (Jan 17 2022 at 16:06):

Thanks for the information. I look forward to hearing the recorded talk .

Siddhartha Gadgil (Jan 28 2022 at 14:53):

Any updates on this (I could not find a recorded talk)?

Henrik Böving (Jan 28 2022 at 14:55):

I did watch it live over here https://www.youtube.com/channel/UCwG9512Wm7jSS6Iqshz4Dpg/videos (was very cool btw^^) so I would expect the snippet of the overall stream to eventually get published on this channel? It has lots of other POPL talks after all.

Sebastian Ullrich (Jan 28 2022 at 14:57):

Yes, it should get published there eventually

Eric Taucher (Jan 28 2022 at 15:07):

Is it just me or did others wonder into this topic thinking some student was expecting a homework answer only to find this? Maybe the title should be changed as this looks interesting but the title is leading other to skip this topic because they are thinking what I thought.

Sebastian Ullrich (Jan 28 2022 at 15:11):

That didn't occur to me before, but I love it.


Last updated: Dec 20 2023 at 11:08 UTC