Dafny's /optimize Feature
As of changeset
, you can now specify the /optimize
option to instruct
to produce an optimized build of your program.
What does this mean?
- Dafny will enable an optimized version of the prelude that is included in the C# code it generates by passing
to the C# compiler.
- Dafny will pass the /optimize
flag to the C# compiler, which is similar to producing a
Fulfilling /optimize Prerequisites
The optimized version of the prelude uses Microsoft's new
, which perform much better than Dafny's default collections. Dafny keeps a copy of this assembly in its
directory, so you should be able to use
without any special preparation.
When you pass the /optimize
, Dafny will copy System.Collections.Immutable.dll
into the directory where the output assembly is written to. Your compiled Dafny program or library will not function without this DLL in the search path.