watchdog error

Stream: lean4

[Kevin Buzzard]

What have I done?

watchdog.png

I gave a talk in Nottingham today. Before I left I started porting a mathlib4 file. On the way to Nottingham I realised that my Lean 4 installation was borked and so the proposed demo I was going to give was rapidly rewritten for Lean 3. On the way home I was going to work on porting the file but I can't use mathlib at all right now. Does anyone have any advice? I have very patchy internet so it's going to be hard to switch to master and download oleans.

[Kevin Buzzard]

Does it matter that the branch I'm on contains errors (because I'm in the middle of porting a file (which isn't imported by Tactic))?

[Mauricio Collares]

I guess it might matter if those files (or files which import them) are also open on the same VSCode window.

[Mauricio Collares]

I tested your port/CategoryTheory.Sites.CoverPreserving branch and I initially got a SlimCheck error when importing Mathlib.Tactic (see below), which went away after running lake build. Perhaps that's the same thing you saw?

stderr:
info: [645/711] Building Mathlib.Testing.SlimCheck.Sampleable
error: > LEAN_PATH=./build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib LD_LIBRARY_PATH=/home/collares/.elan/toolchains/leanprover--lean4---nightly-2023-05-06/lib:/nix/store/ccm7316rqdmffrg2zlzxd4smh19xjy07-pipewire-0.3.68-jack/lib:./build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib:./build/lib /home/collares/.elan/toolchains/leanprover--lean4---nightly-2023-05-06/bin/lean -DwarningAsError=true -Dpp.unicode.fun=true ./././Mathlib/Testing/SlimCheck/Sampleable.lean -R ././. -o ./build/lib/Mathlib/Testing/SlimCheck/Sampleable.olean -i ./build/lib/Mathlib/Testing/SlimCheck/Sampleable.ilean -c ./build/ir/Mathlib/Testing/SlimCheck/Sampleable.c
error: stderr:
failed to write './build/lib/Mathlib/Testing/SlimCheck/Sampleable.olean': 2 No such file or directory
error: external command `/home/collares/.elan/toolchains/leanprover--lean4---nightly-2023-05-06/bin/lean` exited with code 1

[Kevin Buzzard]

In fact it seems I can work on porting the category theory file fine. Seems that importing Mathlib.Tactic.LibrarySearch causes it? However opening the file works fine. Maybe I'll reboot...

[Katherine]

Lean server printed an error:
Watchdog error: no such file or directory (error code: 2)

what should I do?

[Kevin Buzzard]

Which project are you working in? Mathlib, a project which imports mathlib, or a project which doesn't import mathlib? In my example above I was working on I mathlib and the problem was fixed once I got proper internet and ran lake clean, lake exe cache get, lake build.