Dafny IR does not generate modules in dependency order anymore

[dnezam]

Dafny version

4.8.0

Code to produce this issue

No response

Command to run and resulting output

No response

What happened?

Previously, the Dafny IR generated modules in a linear and topologically sorted order which the Dafny to CakeML compiler relied on. However, updating to the current master branch broke this behavior: for example, the default module _module is now mentioned first. Since the Dafny Reference mentions that it will figure out a topological order (emphasis mine)

(4.7. Module Ordering and Dependencies) "In particular, there must be a way to order the modules in a program such that each only refers to things defined before it in the ordering. [...] Dafny will figure out that order for you, assuming you haven’t made any circular references. "

I really would like to utilize it. I confirmed that the offending PR is #5684. If possible, it would be nice if this could be reverted for now to make sure that the CakeML compiler does not drift apart too much. If something downstream of the Rust compiler relies on this, perhaps it could be added there.

What type of operating system are you experiencing the problem on?

Linux

[MikaelMayer]

Let's find a solution that suits both of us. The problem with the topological order I thought of was that it was not reliable for modules that did not depend on each other, which was causing trouble with code that would patch the output. Indeed, the C# specification said that the order in which we iterate keys in a dictionary is not guaranteed, although the implementation does it perfectly.
That said, there are two things that came up

• One of the projects that relied on patching the output no longer needs to patch the output with a diff, so the order of modules i no longer relevant
• Another issue that was the key is that the "find" command returns files in a different order in Windows, Mac and Linux. If provided with multiple Dafny files, Dafny will emit modules in the order given by the files, triggering issues. See
  Topological order not computed correctly when multiple dfy files present in the command-line #5728

All of this to say @robin-aws , I think it's safe and we can revert the commit that ensured module ordering to revert it back to topological ordering. What do you think?

[robin-aws]

Could we restore the topological sort, but make it a stable sort w.r.t. an alphabetical ordering, so we get a deterministic ordering that still respects dependencies?