1

我使用 nix 版本 2.3.7 在 MacOS High Sierra 上运行带有 Proof General 的 mathcomp 8.12。为此，我使用以下 shell 命令：

nix-shell -p coqPackages_8_12.mathcomp --run /Applications/Emacs.app/Contents/MacOS/Emacs

在带有 MacOS Catalina 的新 Mac 上，我使用 https://dev.to/louy2/installing-nix-on-macos-catalina-2acb 中提供的（我希望）正确建议安装了 nix 版本 2.3.10。运行与以前相同的 nix-shell 命令，我设法让 Proof General 运行。但是下面的 Coq/SSReflect 代码在第 3 行失败了。

From Coq Require Import Init.Prelude Unicode.Utf8.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import fingroup.perm.

带有一条消息说明

Cannot find a physical path bound to logical path matching suffix fingroup and prefix mathcomp.

另一个奇怪的行为是，如果我删除违规Require并继续，那么在环境中找不到 addnBAC 引理（但是，还有其他引理，例如 subnDA！）。

关于这里可能有什么问题的任何建议？我尝试通过更改 -p 选项进入 8.13，但得到了相同的结果。

4

1 回答 1

1

你可能正在运行一个系统安装版本的 Coq，因为你没有告诉你nix-shell添加coq到你的 shell... 使用这个系统版本的 Coq，你可能只安装了 ssreflect（和一个旧版本）。

尝试运行

nix-shell -p coqPackages_8_12.coq -p coqPackages_8_12.mathcomp --run /Applications/Emacs.app/Contents/MacOS/Emacs

反而。

于 2021-01-18T12:02:47.887 回答