How to install rocq with stdlib?

Help
1

Hi,

Nixpkgs bindings for rocq don’t have withPackages like haskell or python do.
Adding just coq_9_1 to packages section in /etc/nixos/configuration.nix installs rocq, but it cannot see stdlib.

  users.users.nuser = {
    isNormalUser = true;
    extraGroups = [ "networkmanager" "wheel" ];
    packages = with pkgs; [
      coq_9_1

rocq c Import.v 
File "./Import.v", line 3, characters 0-33:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./Import.v", line 3, characters 15-32:
Error: Cannot find a physical path bound to logical path
Stdlib.Strings.Ascii.
2

Downgrade to coq_8_20 solved the problem.

3

I seem to be having the same problem. I’m getting

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

when I try to run the line:

From Stdlib Require Export String.

which is taken from the Software Foundations book.

I’m on NixOS Unstable and have coq_8_20 and coqPackages.stdlib installed but it’s still giving the same error unfortunately. Anyone have any other ideas on fixing it? It’d also be nice to figure out how to get it working with the latest version.

4

Okay so I’ve got it working (mostly). I’ve ended up with a flake.nix that gives me a devShell with rocq-core and rocqPackages.stdlib. So I’m just launching the repl or VSCodium from there. Both those work now, though for some reason I still get the same error with Coqtail in Nvim. However this’ll work for now.