Incorrect/unhelpful "error parsing lakefile" from `print-paths`

[Kha]

In a file I get

`/home/sebastian/.elan/toolchains/leanprover--lean4---nightly-2022-08-10/bin/lake print-paths Init` failed:

stderr:
Error parsing '././lakefile.lean'.  Please restart the lean server after fixing the Lake configuration file.

but going back to the lakefile, it's clear that the file itself parses and processes just fine. The real error is revealed only on lake build

error: no such file or directory (error code: 2)
  file: ./https://github.com/JLimperg/aesop/lakefile.lean

at which point I realize I wrote

require aesop from "https://github.com/JLimperg/aesop"

I would expect print-paths to show the precise error from above as well.

[tydeu]

This is actually as intended as part of @gebner's #52. Note this statement from the PR: "In this fallback mode, all files except lakefile.lean immediately fail with an error to remind the user that lake serve must be restarted after fixing lakefile.lean."

[Kha]

That doesn't really change that the error message is neither correct (could be fixed by replacing "parsing" with "loading") nor helpful. For the latter part, should we store the lakefile loading error in LAKE_INVALID_CONFIG so that we can show it instead of this generic message? /cc @gebner

[tydeu]

@Kha I agree that the message can be confusing. However, as @gebner was responsible for this behavior (and seems to have specifically intended it), I want to hear his input before touching it.

[gebner]

I certainly have no objections to changing the error message.

should we store the lakefile loading error in LAKE_INVALID_CONFIG so that we can show it instead of this generic message?

:+1:

[tydeu]

For the latter part, should we store the lakefile loading error in LAKE_INVALID_CONFIG so that we can show it instead of this generic message?

What error are we talking about here? It does not seem feasible to store the entire stderr of either the configuration file elaboration or Lake itself in the environment variable.

[gebner]

I just ran into this again.

It does not seem feasible to store the entire stderr of either the configuration file elaboration or Lake itself in the environment variable.

On Windows the limit is 32K, on Linux you can store several megabytes in an environment variable. Passing (the last couple lines of) the error message should be easily possible.

[tydeu]

@gebner

Passing (the last couple lines of) the error message should be easily possible.

Yeah, this seems reasonable. The only problem right now is that logs are currently printed directly to stderr and not stored, so printPaths does not currently have a way to retrieve the log lines and store them in the variable.

[semorrison]

Just linking to another appearance of this issue: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/how.20to.20include.20mathlib4.20in.20the.20lakefile.3F/near/306763490