Merge branch 'master' into release-4.8.0

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -2961,6 +2961,12 @@ protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBod
       AddUnsupportedFeature(e.Tok, Feature.ExactBoundedPool);
     }
 
+    protected override void OrganizeModules(Program program, out List<ModuleDefinition> modules) {
+      modules = program.CompileModules.ToList();
+      modules.Sort((a, b) =>
+        String.Compare(a.FullDafnyName, b.FullDafnyName, StringComparison.Ordinal));
+    }
+
     protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr) {
       TrStmt(body, wr);
     }

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/moduleordering.dfy

@@ -0,0 +1,20 @@
+// NONUNIFORM: Test of the Rust compiler to ensure it emits modules in a deterministic order.
+// RUN: %baredafny translate rs "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%S/moduleordering-rust/src/moduleordering.rs" "%s"
+// CHECK-L: pub mod A {
+// CHECK-L: pub mod B {
+// CHECK-L: pub mod C {
+// CHECK-L: pub mod D {
+// CHECK-L: pub mod E {
+// CHECK-L: pub mod F {
+// CHECK-L: pub mod G {
+// CHECK-L: pub mod H {
+
+module B { const X := "B" }
+module D { import B const X := B.X }
+module C { import A const X := A.X }
+module E { import C const X := C.X }
+module A { import G const X := G.X }
+module G { const X := "G" }
+module F { const X := "F" }
+module H { const X := "H" }