ITADN

Cannot find a physical path bound to logical path String with prefix Stdlib.

#419Openrecluse099 创建于 2026-02-16
R
recluse099commented
I have neovim installed via [nvf](<https://github.com/NotAShelf/nvf>) and I am following the _Software Foundations_ book(Vol 1). In the `Basics.v` file in that, whenever I try to interpret the line: `From Stdlib Require Export String.`, Coqtail shows me this error: `Cannot find a physical path bound to logical path String with prefix Stdlib.` Version details: ```text The Rocq Prover, version 9.0.1 compiled with OCaml 4.14.2 NVIM v0.11.6 Build type: Release LuaJIT 2.1.1741730670 ``` I have installed these packages from nixpkgs unstable as my home packages(via home manager): ```text coq coqPackages.coq-lsp coqPackages.stdlib coqPackages.stdpp ``` I have also added these as extraPackages in my nvf neovim config via its API like so: ```nix vim.extraPackages = with pkgs; [ coqPackages.stdlib coqPackages.coq-lsp ]; ``` I have also tried setting these two global options: ```nix vim.globals = { coqtail_build_system = "coqproject"; coqtail_dune_compile_deps = 1; }; ``` but am still getting the same error. I tried these things but the error remained. This is how I have Coqtail installed inside my nvf configuration: ```nix vim.extraPlugins = let coqtail = pkgs.vimUtils.buildVimPlugin { name = "coqtail"; src = pkgs.fetchFromGitHub { owner = "whonore"; repo = "Coqtail"; rev = "240c8f20700160edc13975d4a2bba70180a05ea8"; sha256 = "sha256-RqC1xBrVSjNL8xX8xaXeYIRjLObM+voVTryQ9lsNfBA="; }; }; in { coqtail = { package = coqtail; }; }; ```
6 条评论