Skip to content

Minimize dependencies from Anneal.lean, generated Lean #3256

@joshlf

Description

@joshlf

Currently, we depend on all of Aeneas in Anneal.lean, leading to multi-second import times from lake build. Instead, we should:

  • Minimize these imports
  • Refactor Anneal.lean so that it contains distinct modules which only depend narrowly on the parts of Aeneas which they need
  • Provide this library as an external dependency (perhaps installed via cargo anneal setup?) and, in generated Lean, only import the needed modules (and allow users to import more for their own annotations)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions