Qq manifest warning in new math project

Stream: mathlib4

[Shreyas Srinivas]

After starting a new math project and running lake update, I get the following warning about Qq missing a manifest:

warning: Qq: ignoring missing dependency manifest '././.lake/packages/Qq/lake-manifest.json'

Can I ignore this issue and go ahead?

[Ruben Van de Velde]

Yes, you can

[Kim Morrison]

However, we really should fix it! If someone would like to run lake update in qq and commit the resulting manifest this will solve the problem.

[Shreyas Srinivas]

I could do that. It shouldn't take me too much time

[Shreyas Srinivas]

I was able to add the lake-manifest without updating the toolchain

[Shreyas Srinivas]

Should the toolchain also be updated @Kim Morrison ?

[Shreyas Srinivas]

Currently quote4 is on leanprover/lean4:v4.6.0-rc1

[Kim Morrison]

No, leave the toolchain as is. Qq doesn't move toolchains except when it becomes necessary for compatibility.

[Shreyas Srinivas]

quote4#42 (The answer to all problems)

[Shreyas Srinivas]

CI says some workflow needs approval.
EDIT: It's the build task

[Shreyas Srinivas]

@Kim Morrison I was bitten by this again, even thought Qq @ master has a lake-manifest.json. Exact warning message below:

warning: Qq: ignoring missing dependency manifest '././.lake/packages/Qq/lake-manifest.json'

Toolchain : leanprover/lean4:v4.8.0-rc1

[Kim Morrison]

Probably just that we haven't run lake update Qq in mathlib and committed the results. I'l merge if you PR. :-)

[Shreyas Srinivas]

mathlib4#12698

[Shreyas Srinivas]

What does the delegated label mean?

[Kim Morrison]

You can type bors merge yourself now.

[Kim Morrison]

(If you read the comment from the bot this is explained.)

[Shreyas Srinivas]

Okay. Thanks. The confusing bit is that I still get the "merging is blocked" message

[Shreyas Srinivas]

Merged first PR myself with some trepidation.

[Rémy Degenne]

The "Rejected by label" message you got on that PR is because of the awaiting-CI label

[Shreyas Srinivas]

oh right

[Rémy Degenne]

bors will reject until CI passes

[Eric Wieser]

(CI takes a long time for bump PRs because the entire cache is rebuilt)

[Shreyas Srinivas]

now it is stuck and says Kim's review is pending

[Rémy Degenne]

The "bors Pending — Waiting in queue" message in CI means that bors received your merge command and that the pr will be merged when bors is done with other jobs. Your bors r+ worked and it will get merged without further intervention.

[Shreyas Srinivas]

Oh okay. Thanks a lot. That was a nice way to learn about Bors.