Zulip Chat Archive

Stream: general

Topic: precompiled mathlib


view this post on Zulip Johan Commelin (Apr 20 2018 at 13:29):

That being said, we really need mathlib nightlies (ie. precompiled mathlib) — Patrick Massot

Can this be done using Travis? Or do we need other infrastructure?

view this post on Zulip Johan Commelin (Apr 20 2018 at 15:01):

Ok, this seems possible:
https://gist.github.com/Maumagnaguagno/84a9807ed71d233e5d3f
https://gist.github.com/willprice/e07efd73fb7f13f917ea

view this post on Zulip Johan Commelin (Apr 20 2018 at 15:01):

I think a fully compiled mathlib including sources is about 15mb

view this post on Zulip Johan Commelin (Apr 20 2018 at 15:01):

So I think it is not too much of a burden to push back to github


Last updated: May 06 2021 at 22:13 UTC