Zulip Chat Archive

Stream: lean4

Topic: lake error

Johan Commelin (Jan 13 2023 at 20:27):

$ lake build
error: no such file or directory (error code: 2)
  file: ./././Mathlib/Tactic/Apply.lean

Did I do something wrong?

Johan Commelin (Jan 13 2023 at 20:30):

Answer: yes

Adam Topaz (Apr 27 2023 at 23:00):

I'm getting the following error with lake after an OS upgrade...

$ lake new test
error: command failed: 'lake'
info: caused by: No such file or directory (os error 2)

Adam Topaz (Apr 27 2023 at 23:00):

(deleted)

Adam Topaz (Apr 27 2023 at 23:01):

I'm not sure how to diagnose the issue... the error message isn't very descriptive

Gabriel Ebner (Apr 27 2023 at 23:06):

This looks like a NixOS error. Did you garbage collect recently? You might need to elan uninstall $(cat lean-toolchain)

Adam Topaz (Apr 27 2023 at 23:07):

Yes, that's exactly what happened, and I just realized it. I ended up purging most of my $HOME/.elan directory and things worked out.

Adam Topaz (Apr 27 2023 at 23:10):

I guess that's what I get for trying to clear some hdd space ;)

Last updated: Dec 20 2023 at 11:08 UTC