Dafny 3.0 C# dll 库问题从 3.0 到 3.2

Question

我遇到的问题如下：我们在 Dafny 中有一系列函数、方法和数据类型，并用它生成了一个 c# dll 库。为了利用这些库，我们将它们添加为对 Visual Studio C# 控制台应用程序项目的引用。

我遇到的问题是这些库引用了 System.Private.CoreLib 的依赖项。我发现这个库的唯一地方是 dafny 的源代码。通过将其添加为引用，它变得与默认在 c# 中导入的所有 System.* 库“不兼容”。这导致它无法创建类、方法等。附上我刚才提到的问题的截图。

最后，如果我用 Dafny 2.0（已弃用）编译这些库，我没有这个问题，但我想使用最新版本的 dafny。

先谢谢你了。

Answer 1

System.Private.CoreLib 是 .NET Core 运行时的一部分，不必直接引用。这就是基本的内置类型，如 Array、DateTime、Thread 等存在的地方。它被所有 .NET Core 项目隐式使用，不必显式引用。

Dafny 3.0 发布说明解释说，工具从 Mono 迁移到 .NET (Core) 5，现在使用 .NET 5 版本的 Coco/R

工具

• 迁移到 .NET 5.0。

如果您以前使用 mono Dafny.exe 来运行 Dafny，现在使用 dotnet Dafny.dll。

实施

• 使用 .NET 5.0 版本的 Coco/R。

您的项目也必须以 .NET (Core) 5 为目标。