leanprover-community / mathlib

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

Zulip Chat Archive

Stream: general

Topic: Linting all of mathlib locally


Yakov Pechersky (Oct 25 2021 at 13:44):

I am trying to create an all.lean so that I can run linters locally. leanproject mk-all seems to be a no-op. (the file is src/all.lean, but not made if src/all.lean exists, iiuc). What's the right approach here?

Floris van Doorn (Oct 25 2021 at 13:58):

run scripts/mk_all.sh


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll