I run mathcomp 8.12 with Proof General on MacOS High Sierra, using nix version 2.3.7. For this I use the following shell command:
nix-shell -p coqPackages_8_12.mathcomp --run /Applications/Emacs.app/Contents/MacOS/Emacs
On a new Mac, with MacOS Catalina, I installed nix version 2.3.10 using the (I hope) proper suggestion provided in https://dev.to/louy2/installing-nix-on-macos-catalina-2acb. Running the same nix-shell command as before, I managed to get Proof General running. But the following Coq/SSReflect code fails at line 3.
From Coq Require Import Init.Prelude Unicode.Utf8.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import fingroup.perm.
with a message stating
Cannot find a physical path bound to logical path matching suffix fingroup and prefix mathcomp.
Another odd behavior is that, if I remove the offending Require and keep on, it happens that the addnBAC lemma is not found in the environment (other lemmas such as subnDA are there, however!).
Any suggestion on what can be wrong here? I try going to 8.13 by changing the -p option, but got the same result.
You are probably running a system installed version of Coq since you did not tell nix-shell to add coq to your shell... With this system version of Coq you probably installed ssreflect only (and an old version).
Try to run
nix-shell -p coqPackages_8_12.coq -p coqPackages_8_12.mathcomp --run /Applications/Emacs.app/Contents/MacOS/Emacs
instead.