Zulip Chat Archive
Stream: triage
Topic: issue #2268: caching olean files on a per file basis
Random Issue Bot (Nov 02 2020 at 14:14):
Today I chose issue 2268 for discussion!
caching olean files on a per file basis
Created by @Scott Morrison (@semorrison) on 2020-03-28
Labels: CI, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Johan Commelin (Nov 03 2020 at 14:46):
I would love to see some activity here. But I'm afraid I'm no good as contributor here.
Random Issue Bot (Mar 19 2022 at 14:13):
Today I chose issue 2268 for discussion!
caching olean files on a per file basis
Created by @Scott Morrison (@semorrison) on 2020-03-28
Labels: CI, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Feb 25 2023 at 14:09):
Today I chose issue 2268 for discussion!
caching olean files on a per file basis
Created by @Scott Morrison (@semorrison) on 2020-03-28
Labels: CI, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Johan Commelin (Feb 25 2023 at 14:14):
I think we can close this. It's solved in Lean 4.
Last updated: Dec 20 2023 at 11:08 UTC