[Rocq] How to add dependencies?

Help
1

I was using this default.nix for a shell and was able to rocq in vscode without problems.

{
  pkgs ? import <nixos-unstable> { },
}:
let

  vscode-with-extensions = pkgs.vscode-with-extensions.override {
    vscodeExtensions = [
      (pkgs.vscode-utils.extensionFromVscodeMarketplace {
        publisher = "rocq-prover";
        name = "vsrocq";
        version = "2.4.3";
        hash = "sha256-o9rsSDCDYRWZQBMDA7DtWay50tBI76kw7H7CivrZpKo=";
      })
    ];
  };

  coq-with-packages = pkgs.coq.withPackages (ps: [
    ps.stdlib
    ps.vsrocq-language-server
  ]);

in
pkgs.mkShellNoCC {
  packages = [
    coq-with-packages
    vscode-with-extensions
  ];
}

Now, I wanted to use MetaRocq. So I added it to the dependencies like that:

coq-with-packages = pkgs.coq.withPackages (ps: [
  ps.stdlib
  ps.vsrocq-language-server
  ps.metarocq
]);

I created a new file in vscode with only that line of code:

From MetaRocq.Template Require Import All.

But I got that error:

Findlib error: coq-core.plugins.ltac not found in:
/nix/store/ifyavi4i9p878r330i4iif9019724fhx-rocq-9.1.1/lib/coq/../rocq-runtime/..
/nix/store/958icpbam2rfj9nvcrva79kdr3w3njv8-ocaml4.14.3-findlib-1.9.8//lib/ocaml/4.14.3/site-lib
/nix/store/c3jmr7dpkjr7kn7fjymylq79gvd2q6v9-rocq-core9.1-stdlib-9.0.0//lib/ocaml/4.14.3/site-lib
/nix/store/74khi6cnilqvjw5v11mdm88brsgjv38k-ocaml4.14.3-vsrocq-language-server-2.4.3//lib/ocaml/4.14.3/site-lib
/nix/store/hj66hr2rw91rxbixnn8mpzip7h1z2bc2-coq9.1-metarocq-1.5.1-9.1//lib/ocaml/4.14.3/site-lib
/nix/store/ji19xqv8w4d0hlw3cinjrg9kkk1ddn99-coq9.1-equations-1.3.1+9.1//lib/ocaml/4.14.3/site-lib
/nix/store/kccszzzvbn52d53miq793wn3sxwk4hyc-coq9.1-coq-ext-lib-0.13.1//lib/ocaml/4.14.3/site-lib
/nix/store/3cc0q676l3i962kzvcqvai3rnssdyi1a-ocaml4.14.3-zarith-1.14//lib/ocaml/4.14.3/site-lib
/nix/store/m0h5as5ans7dg71iqhqg5h4gc197pi85-ocaml4.14.3-stdlib-shims-0.3.0//lib/ocaml/4.14.3/site-lib
/nix/store/d9a4nln2wfjcd854x4i65l190a9xnh7a-coq9.1-metarocq-safechecker-plugin-1.5.1-9.1//lib/ocaml/4.14.3/site-lib
/nix/store/dgsllxfp2mm114zd9njja73xs6j39ykb-coq9.1-metarocq-erasure-plugin-1.5.1-9.1//lib/ocaml/4.14.3/site-lib
/nix/store/azljsay8h2ai090hp068jw6i3qby3ca4-coq9.1-metarocq-translations-1.5.1-9.1//lib/ocaml/4.14.3/site-lib
/nix/store/qdpafnkfab84z75025plj118h62zbswn-coq9.1-metarocq-quotation-1.5.1-9.1//lib/ocaml/4.14.3/site-lib
/nix/store/59hk2292f60fwhhcwsn0dndnlk9lrn6y-ocaml4.14.3-ppx_optcomp-0.16.0//lib/ocaml/4.14.3/site-lib
/nix/store/za016rjxc6a4cnlgws0l9b79q2j0n3fc-ocaml4.14.3-ppxlib-0.34.0//lib/ocaml/4.14.3/site-lib
/nix/store/nq1vahaxnl8j7ghf1nzn65w1kvy71kz8-ocaml4.14.3-ocaml-compiler-libs-0.12.4//lib/ocaml/4.14.3/site-lib
/nix/store/dd06hx3zms2zbscc6gli5gjmcbrsf1hd-ocaml4.14.3-ppx_derivers-1.2.1//lib/ocaml/4.14.3/site-lib
/nix/store/ydhy0w97axn4qgzmcb03p86q8b5flawj-ocaml4.14.3-stdio-0.16.0//lib/ocaml/4.14.3/site-lib
/nix/store/kxfh1z17ayq7xq60sqzl8vzk2vq3vcm7-ocaml4.14.3-base-0.16.2//lib/ocaml/4.14.3/site-lib
/nix/store/x5m2mxjk1wilnvvq3m5qz0n3a5lrri8z-ocaml4.14.3-sexplib0-0.16.0//lib/ocaml/4.14.3/site-lib
/nix/store/ijf9xvmiwb4i0nzjhl52chdlls9ypzh4-gmp-with-cxx-6.3.0-dev//lib/ocaml/4.14.3/site-lib
/nix/store/mf66nr8n4dby47k5v5f2r0nv79rmpnrd-coq9.1-metarocq-template-pcuic-1.5.1-9.1//lib/ocaml/4.14.3/site-lib
/nix/store/xrabmg3c8w5jjczfljasy685a7wzx4xa-coq9.1-metarocq-safechecker-1.5.1-9.1//lib/ocaml/4.14.3/site-lib
/nix/store/sai89lkhhyfp0mibsr8x4lcn056ydlf0-coq9.1-metarocq-template-rocq-1.5.1-9.1//lib/ocaml/4.14.3/site-lib
/nix/store/hnzpaf8msnpkbs5qn4crfszv96j4a512-coq9.1-metarocq-pcuic-1.5.1-9.1//lib/ocaml/4.14.3/site-lib
/nix/store/4gh7291s7ims6c77bn1mi942j275k21l-coq9.1-metarocq-common-1.5.1-9.1//lib/ocaml/4.14.3/site-lib
/nix/store/yzbg01sr074y89vln2hxad41zd733qk8-coq9.1-metarocq-utils-1.5.1-9.1//lib/ocaml/4.14.3/site-lib
/nix/store/3xipm4gx0ga75wzsmxriwb447brlz2b6-coq9.1-metarocq-erasure-1.5.1-9.1//lib/ocaml/4.14.3/site-lib
/nix/store/958icpbam2rfj9nvcrva79kdr3w3njv8-ocaml4.14.3-findlib-1.9.8/lib/ocaml/4.14.3/site-lib

So my first question is, what’s going on, and how can I fix that?

And my second question is, what do you recommend for adding dependencies (I’m on NixOS), should I stick with nixpkgs, or should I use opam or dune? In the latter case, some example devshell configs would be useful.

2

I am not much help here, as I am more familiar with agda and emacs. All I can suggest is that for some reason coq-core.plugins.ltac or the package that contains it might needed to be added to your import list. It is probably an oversight, or missed dependency on one of the packages you are importing. But I don’t really know what I am doing either.

3

Seems like it’s a problem with metarocq specifically, I tried with bignums and it works.