Zulip Chat Archive

Stream: mathlib4

Topic: Cache and MathlibExtras

Adam Topaz (Apr 28 2023 at 15:52):

It's not a huge issue, but just something I came across. Doing the following

  1. lake new Test math && cd Test
  2. lake exe cache get

results in a warning

Warning: ./MathlibExtras.lean not found. Skipping all files that depend on it

Adam Topaz (Apr 28 2023 at 15:52):

Do we need to tell Cache about MathlibExtras somehow?

Patrick Massot (Apr 28 2023 at 15:59):

This is the same issue as https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/instant.20library_search/near/353339921

Adam Topaz (Apr 28 2023 at 15:59):

Okay, good to know that it's on the radar!

Scott Morrison (Apr 28 2023 at 23:35):

Fixed and tested in !4#3721.

Last updated: Dec 20 2023 at 11:08 UTC