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

Posted 2023-03-28

【中文标题】Dafny 3.0 C# dll 库问题从 3.0 到 3.2

【英文标题】：Dafny 3.0 C# dll library problem from 3.0 to 3.2

【发布时间】：2021-11-04 01:11:45

【问题描述】：

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

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

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

先谢谢你了。

【问题讨论】：

System.Private.CoreLib 是 .NET Core 运行时的一部分，不必直接引用。这就是基本的内置类型（如 Array 和 DateTime）所在的位置。您的目标是哪个 .NET 运行时？ .NET 旧的？ .NET 核心？我怀疑任何微软研究项目都会在 2021 年以 .NET Old 为目标

【参考方案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 为目标。

【讨论】：

我已经安装了 Visual Studio 2017，安装了 .Net 5.0 并创建了一个使用此框架的控制台项目。问题仍然存在。不知道是不是我配置不好，还是有其他问题。消息仍然相同：“对象”类型是在未引用的程序集中定义的。您必须添加对程序集的引用 'System.Private.CoreLib, Version=5.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e

VS 2017 不支持 .NET 5，甚至不提供针对它的选项。 .NET 5 于 2020 年发布，因此即使有 VS 2017 的目标包，您也必须处理兼容性问题。请改用最新版本的 VS 2019，或从命令行工作，例如使用 VS Code 作为 IDE。

我错了不好意思，我刚刚安装的版本是2019。我写原问题的时候用的是2017。

有人知道吗？