Zulip Chat Archive
Stream: new members
Topic: Weird leanpkg.path
Martin Dvořák (Feb 22 2022 at 22:19):
Whenever I run leanproject build, I lose changes to leanpkg.path. Why does it happen? And how can I make sure that my lean3 code located outside of ./src is correct?
Reid Barton (Feb 22 2022 at 22:54):
leanpkg.path is not for the user to edit
Martin Dvořák (Feb 22 2022 at 23:11):
How can I typecheck ./test from the command line, please?
Last updated: Dec 20 2023 at 11:08 UTC