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.

5

Figured out I need to set ROCQPATH. The following code works for me.

(
  let
    rocqPkgs = rocqPackages_9_0;
  in
  (symlinkJoin {
    name = "rocq-dev-env";
    buildInputs = [ makeWrapper ];
    paths = with rocqPkgs; [
      vsrocq-language-server
      rocq-core
    ];
    postBuild = ''
      LIB="${rocqPkgs.stdlib}/lib/coq/9.0/user-contrib"
      wrapProgram $out/bin/rocq \
        --set ROCQPATH $LIB
      wrapProgram $out/bin/vsrocqtop \
        --set ROCQPATH $LIB
    '';
  })
)
1 Like
6

Unstable now has withPackages and has an example in the manual

7

Hi, could you link to that example in the manual?

8

Hi, I am facing the same issue with my neovim + coqtail workflow, could you help me with this? Do I have to make a nix flake shell and set the ROCQPATH library like in your code?