feat: enable extern declarations to be contingent on OS or target language

[davidcok]

What is the feature you would like to see in a future version of Dafny?

I propose extern declarations be allowed to have syntax like

{:lang java :extern ... }
{:os windows :extern ... }

The declaration would be ignored if the language and/or OS do not match.
Any location that permits :extern declaration would be allowed to have multiple mutually-exclusive such declarations

Allowing this would simplify the interface to the native variations of library functionality

[MikaelMayer]

Could you please compare your approach with the following one that I proposed previously?
#2397

[davidcok]

#2397 would accommodate what is requested here. I have no commitment to the mechanism, just the needed functionality -- though the approach here is not a breaking change as is #2397

[MikaelMayer]

#2397 could be implemented not as a breaking change as well, if we don't get rid of {:extern} and {:compile}.