Lean action not failing on `lake build --wfail` on docgen

Stream: general

[Austin Letson]

Henrik Böving said:

Kim Morrison said:

Actually, maybe this is really a question for Austin Letson --- could we change the default for lean-action to fail if there are warning during the build?

I made the change to doc-gen in https://github.com/leanprover/doc-gen4/pull/257, unfortunately, unlike it should, the CI does not error on building doc-gen itself as it recovers the build from a cache, this seems to be an indicator to me that the cache key used to compute build results is not taking into accounts things like change of arguments etc. This should probably also be addressed Austin Letson. Alternatively maybe this is not an issue with lean-action itself but with lake, I can't quite tell.

@Henrik Böving I made a new thread to respond to this since the other thread is actively discussing other things.

I think this is an issue with lake. I pulled this branch of docgen locally and ran lake build --wfail and the build succeeded:

[I] ➜  doc-gen4 git:(warning-ci) lake build --wfail
info: Cli: cloning https://github.com/mhuisi/lean4-cli
info: Cli: checking out revision '0c8ea32a15a4f74143e4e1e107ba2c412adb90fd'
info: UnicodeBasic: cloning https://github.com/fgdorais/lean4-unicode-basic
info: UnicodeBasic: checking out revision '470c41643209208d325a5a7315116f293c7443fb'
info: BibtexQuery: cloning https://github.com/dupuisf/BibtexQuery
info: BibtexQuery: checking out revision '46376bc3c8f46ac1a1fd7712856b0f7bd6166098'
info: MD4Lean: cloning https://github.com/acmepjz/md4lean
info: MD4Lean: checking out revision 'f8ed91f3a9d806648ae6a03ab98c8b87e8bedc7e'
warning: ././.lake/packages/MD4Lean/lakefile.lean:13:61: warning: `Lake.BuildJob` has been deprecated: use `Lake.Job` instead

warning: ././.lake/packages/MD4Lean/lakefile.lean:26:45: warning: `Lake.BuildJob` has been deprecated: use `Lake.Job` instead

Build completed successfully.

I am not sure what is going on here. It seems like the build should fail. Since the warning is logged forMD4Leanas opposed to doc-gen4 it isn't causing lake build --wfail to fail?

[Henrik Böving]

Interesting, in that case it's probably something for @Mac Malone to look into next week.

[Mac Malone]

Unfortunately, configuration warnings (and workspace load warnings more generally) are not currently covered by --wfail.

[Kim Morrison]

lean#6540