Блог

Я запускаю mathcomp 8.12 с Proof General на macOS High Sierra, используя nix версии 2.3.7. Для этого я использую следующую команду оболочки:

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

На новом Mac с macOS Catalina я установил nix версии 2.3.10, используя (я надеюсь) правильное предложение, представленное в https://dev.to/louy2/installing-nix-on-macos-catalina-2acb . Запустив ту же команду 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в наличии!).

Любое предложение о том, что здесь может быть не так? Я пытаюсь перейти на 8.13, изменив параметр -p, но получил тот же результат.

Вероятно, у вас установлена системная версия Coq, поскольку вы не указали nix-shell добавить coq в свою оболочку… С этой системной версией Coq вы, вероятно, установили только ssreflect (и старую версию).

Попробуйте запустить

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

вместо этого.