Zulip Chat Archive

Stream: general

Topic: wanted prebuild release


Kevin Buzzard (Dec 14 2022 at 23:59):

~/lean-projects/mathlib4$ lake build +Mathlib.Algebra.Group.Opposite
info: downloading component 'lean'
177.5 MiB / 177.5 MiB (100 %)  28.5 MiB/s ETA:   0 s
info: installing component 'lean'
warning: wanted prebuilt release, but release repository and tag was not known
Building Std.Util.ExtendedBinder
Building Std.Lean.TagAttribute
Building Std.Tactic.HaveI
...

Apparently lake wanted a prebuilt release. Is this anything to worry about?

Gabriel Ebner (Dec 15 2022 at 00:29):

This should be fixed with https://github.com/JLimperg/aesop/pull/34


Last updated: Dec 20 2023 at 11:08 UTC