Skip to content

lake update silently fails when argument does not exists #2772

Open
@PatrickMassot

Description

@PatrickMassot

Prerequisites

  • Put an X between the brackets on this line if you have done all of the following:
    • Check that your issue is not already filed.
    • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Running lake update foo in a project not depending on foo returns no output.

Context

See discussion here.

Steps to Reproduce

  1. Create a project with no dependency.
  2. run lake update foo.

Expected behavior: [Clear and concise description of what you expect to happen]

Error message: "This project has no dependency named foo".

Actual behavior: [Clear and concise description of what actually happens]

Nothing.

Versions

lean4-4.0.2rc4

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Metadata

Metadata

Assignees

No one assigned

    Labels

    LakeLake related issueP-highWe will work on this issuebugSomething isn't workingenhancementNew feature or request

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions