Can't add doc-gen4 to manifest

Stream: general

[Artie Khovanov]

The blueprint on my downstream project has broken. Lake says:

error: dependency '«doc-gen4»' not in manifest; use lake update «doc-gen4» to add it

However, running this command does not add this dependency to the project manifest. Lake tells me all my packages are up to date, which is true - they just don't include doc-gen4!
I also tried the same command without french quotes, to the same non-result.
Does anybody know how to fix this issue?

[Kim Morrison]

This is usually a result of people use meta if in their lakefiles, which we are strongly discouraging. :-)

Often the fix is lake update -Kenv=dev, but I don't know what's in your project.

[Artie Khovanov]

Found this in my lakefile:

meta if get_config? env = some "dev" then
require «doc-gen4» from git
  "https://github.com/leanprover/doc-gen4" @ "main"

your suggestion didn't work (same outcome)

[Kim Morrison]

Can you give us reproducible instructions for your producing your error state?

[Artie Khovanov]

Not sure what is necessary but:
Go to this repo
https://github.com/artie2000/real_closed_field
and run the "compile blueprint" code action

[Artie Khovanov]

(fixed by simply removing the meta if; don't know if there is an alternative solution)