format check --standard-libraries (or including any doo files) always fails

[robin-aws]

Dafny version

4.9.1

Code to produce this issue

module UsesWrappers {

  import opened Std.Wrappers

  function SafeDiv(a: int, b: int): Option<int> {
    if b == 0 then None else Some(a/b)
  }
}

Command to run and resulting output

> dafny format --check --standard-libraries UsesStdLibs.dfy
The file /DafnyStandardLibraries-notarget.doo needs to be formatted
The file /DafnyStandardLibraries.doo needs to be formatted
Error: 2 files need formatting.

What happened?

I'd expect the standard libraries to not be in scope for formatting in general, given they are pre-built. Or at least if they are in scope, they would be considered correctly formatted.

This is a general doo file problem and not specific to the standard libraries. dafny format without the check already produces Please use the '--check' and/or '--print' option as doo files cannot be formatted in place.

There's a fairly easy workaround as you don't actually need to pass --standard-libraries to dafny format, since it doesn't attempt resolution. But that's not easy when using a project file, for example.

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

Mac