leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: Remove trace in lake build


SnO2WMaN (Jan 25 2026 at 06:40):

How to remove trace: .> LEAN_PATH=... in CLI output?

I tried lake build -q --log-level=error, still error and also trace outputs.

lake --version is Lake version 5.0.0-src+2fcce72 (Lean version 4.27.0-rc1)


Last updated: Feb 28 2026 at 14:05 UTC

Theme Simple by wildflame © 2016 Powered by jekyll