Lake update complains about `Array.await`

Stream: general

[Martin Dvořák]

Updating from 4.16.0 to the newest...

$ lake update
info: doc-gen4: checking out revision 'e3f8a871d2beb4264e31eee6e3e4ee504b88638f'
info: updating toolchain to 'leanprover/lean4:v4.17.0-rc1'
info: restarting Lake via Elan
info: toolchain not updated; already up-to-date
info: Cli: checking out revision 'a2eb24a3dbf681f2b655f82ba5ee5b139d4a5abc'
info: UnicodeBasic: checking out revision 'd890360c960358a42965bdc15defa3fd09feba38'
info: BibtexQuery: URL has changed; you might need to delete '.\.\.lake\packages\BibtexQuery' manually
info: BibtexQuery: checking out revision '2411c47ee06f2fc986d929e22731c77e61eaadb6'
info: MD4Lean: checking out revision '7cf25ec0edf7a72830379ee227eefdaa96c48cfb'
info: mathlib: running post-update hooks
error: .\.\.lake/packages\doc-gen4\lakefile.lean:159:16: error: invalid field 'await', the environment does not contain 'Array.await'
  __do_lift✝
has type
  Array Module

error: .\.\.lake/packages\doc-gen4\lakefile.lean:160:38: error: invalid field notation, type is not of the form (C ...) where C is a constant
  imports
has type
  ?m.11550 mod exeJob bibPrepassJob modJob __do_lift✝

error: .\.\.lake/packages\doc-gen4\lakefile.lean:198:13: error: invalid field 'await', the environment does not contain 'Array.await'
  __do_lift✝
has type
  Array Module

error: .\.\.lake/packages\doc-gen4\lakefile.lean:199:38: error: invalid field notation, type is not of the form (C ...) where C is a constant
  mods
has type
  ?m.20672 lib __do_lift✝

error: .\.\.lake/packages\doc-gen4\lakefile.lean:240:13: error: invalid field 'await', the environment does not contain 'Array.await'
  __do_lift✝
has type
  Array Module

error: .\.\.lake/packages\doc-gen4\lakefile.lean:241:38: error: invalid field notation, type is not of the form (C ...) where C is a constant
  mods
has type
  ?m.23616 lib __do_lift✝

error: .\.\.lake/packages\doc-gen4\lakefile.lean: package configuration has errors
error: mathlib: failed to fetch cache

What can I do?

[Sebastian Ullrich]

Does that happen on a follow-up lake build as well?

[Yaël Dillies]

Your project seems to depend on doc-gen. This is not the preferred setup.
Either pin the dependency or change to the new preferred setup. Can you show us the repo?

[Martin Dvořák]

Yes.

$ lake build
error: .\.\.lake/packages\doc-gen4\lakefile.lean:159:16: error: invalid field 'await', the environment does not contain 'Array.await'
  __do_lift✝
has type
  Array Module

error: .\.\.lake/packages\doc-gen4\lakefile.lean:160:38: error: invalid field notation, type is not of the form (C ...) where C is a constant
  imports
has type
  ?m.11550 mod exeJob bibPrepassJob modJob __do_lift✝

error: .\.\.lake/packages\doc-gen4\lakefile.lean:198:13: error: invalid field 'await', the environment does not contain 'Array.await'
  __do_lift✝
has type
  Array Module

error: .\.\.lake/packages\doc-gen4\lakefile.lean:199:38: error: invalid field notation, type is not of the form (C ...) where C is a constant
  mods
has type
  ?m.20672 lib __do_lift✝

error: .\.\.lake/packages\doc-gen4\lakefile.lean:240:13: error: invalid field 'await', the environment does not contain 'Array.await'
  __do_lift✝
has type
  Array Module

error: .\.\.lake/packages\doc-gen4\lakefile.lean:241:38: error: invalid field notation, type is not of the form (C ...) where C is a constant
  mods
has type
  ?m.23616 lib __do_lift✝

error: .\.\.lake/packages\doc-gen4\lakefile.lean: package configuration has errors

[Martin Dvořák]

Yaël Dillies said:

Your project seems to depend on doc-gen. This is not the preferred setup.
Either pin the dependency or change to the new preferred setup. Can you show us the repo?

https://github.com/Ivan-Sergeyev/seymour/blob/main/lakefile.toml

I don't mind living without doc-gen. I never search the docs of our project.

[Martin Dvořák]

What is "the new preferred setup" please?

[Sebastian Ullrich]

See https://github.com/leanprover/doc-gen4?tab=readme-ov-file#usage

[Martin Dvořák]

The new setup sounds too complicated.
Can I remove doc-gen from the project without getting a red cross here?
image.png