unspecified system_category error

Stream: lean4

[Floris van Doorn]

Separating this out from this thread

When opening Mathlib.lean I get the following error:

unspecified system_category error (error code: 206)

This is even in a repository where opening an individual Mathlib file, or a file with import Mathlib.lean works correctly (i.e. I don't get the error of the linked thread).

[Sebastian Ullrich]

ERROR_FILENAME_EXCED_RANGE

206 (0xCE)

The filename or extension is too long.

Are you in some deeply nested directory?

[Floris van Doorn]

nope, not at all. This is in ~/projects/mathlib (and the home directory is also not long)

[Sebastian Ullrich]

Not sure we can do much here without finding out the file name in question or what is special about your setup. Working with these operating systems stuck in the previous millennium unfortunately is a royal pain.

[Jovan Gerbscheid]

I get the same when opening Mathlib.lean in a clone of Mathlib. It doesn't even try to build the imports.

[Jovan Gerbscheid]

But it's not really a problem since I don't need to use that file directly.