Rust backend needs an option similar to `--go-module-name` or `--python-module-name`

[robin-aws]

In Rust the name of the crate containing code shows up in the namespace of consuming references. i.e. if a module foo.rs includes a definition bar and is packaged in a stuff crate, consuming code that depends on the stuff crate will have references like stuff::foo::bar. This means consuming Dafny code needs to be aware of how dependent code was built and packaged: the reference in Dafny code may be just foo.bar, but needs to be compiled to stuff::foo::bar.

The recently added translation record file format (*.dtr) is specifically made to track this information, by recording what relevant options were passed to dafny translate. We just need a analogous option for Rust to track the crate name.

[MikaelMayer]

Do you have some insights as per how everything would be compiled? I can't figure out a way that is consistent.
I'm currently thinking of that, two files projectA.dfy and projectB.dfy, where projectB.dfy includes projectA.dfy but we want to compile them separately for some reason.

Project A.

dafny translate rs projectA.dfy --rust-module-name:projectA
dafny build lib projectA.dfy -- To create the doo file.

would result in this:

projectA-rust/
  src/
    projectA.rs   // Self-references are crate::projectA::module_in_projectA::definitions
                  // instead of          crate::module_in_projectA::definitions
    projectA.dtr
projectA.doo

Project B that depends on projectA

dafny translate rs projectB.dfy projectA-rust/src/projectA.rs --translation-record projectA-rust/src/projectA.dtr --library projectA.dfy
mv projectA-rust/src/projectA.rs projectB-rust/src/projectA.rs

would result in

  projectB-rust/
    src/
      projectA.rs
      projectB.rs

in such a way that would compile, is that what you had in mind?

[MikaelMayer]

Answer:

--rust-crate-name foo wouldn't affect the Rust code generated directly, but it would be stored in the translation record file *.dtr. Then when you compile A you not only pass --library B.dfy but also --translation-record B-rust.dtr, so you know references to B have to be prefixed with ::foo

[MikaelMayer]

#5747 will address the first part, but it will also be necessary to include the crate in the translation record.

[robin-aws]

Note that OptionRegistry.RegisterOption(RustModuleNameOption, OptionScope.Translation); as you have in #5747 is all you need to record the option in translation records.