Skip to content

Rust backend always includes runtime code, doesn't emit it unless building the target program #5203

Open
@robin-aws

Description

@robin-aws

Two separate but related issues:

  1. The runtime source should only be emitted if --include-runtime is true, but the Rust backend ignores this option and always emits it.
  2. The code to emit the runtime source is in RustBackend.CompileTargetProgram, so it's only run if /compile is at least 1, or the command is dafny build or run or test. It should also be emitted even if /compile is 0, or the command is translate.

Metadata

Metadata

Assignees

No one assigned

    Labels

    lang: rustDafny's transpiler to Rust and its runtime

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions