在 Catalina 上通过 nix 安装 mathcomp 8.12/8.13 时出现问题

问题描述

我在 MacOS High Sierra 上使用 Proof General 运行 mathcomp 8.12，使用 nix 版本 2.3.7。为此，我使用以下 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，但得到了相同的结果。

解决方法

您可能正在运行 Coq 的系统安装版本，因为您没有告诉 nix-shell 添加 coq旧版本）。

尝试运行

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

相反。

coq nix nix ssreflect