Skip to content

Do not re-resolve previously resolved modules #3028

Open
@keyboardDrummer

Description

@keyboardDrummer

Dafny does not use the same signature to compile a module and to verify it. As a result, it really creates two copies of each module: a regular copy and a copy called _Compile that is used only in the compiler.

To create _Compile modules, Dafny clones the original module, then swaps out a different signature and re-resolves the resulting module.

Related data: #2358

Metadata

Metadata

Assignees

No one assigned

    Labels

    area: performancePerformance issueskind: enhancementEnhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafnypart: resolverResolution and typechecking

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions