Installing/setting up opam-only Rocq package

[jstrattonsmith]

I'm fairly new to Nix and opam (unfortunately) so have been struggling to debug both. I'd like to be able to make use of this library of undecidability results alongside the vscoq-language-server so I can develop some new Rocq files using these undecidability results. The undecidability results are exposed in opam here but have some particular ocaml requirements that seem to be causing things to break. What I have so far is the following, based on the Rocq example in this repo.

{
  description = "Build a rocq (coq) package";
  inputs.opam-nix.url = "github:tweag/opam-nix";
  inputs.opam-repository.url = "github:ocaml/opam-repository";
  inputs.opam-repository.flake = false;
  inputs.nixpkgs.url = "github:nixos/nixpkgs";
  inputs.flake-utils.url = "github:numtide/flake-utils";
  # inputs.coq-library-undecidability.url = "github:uds-psl/coq-library-undecidability/coq-8.20";
  # inputs.coq-library-undecidability.flake = false;
  outputs =
    {
      self,
      opam-nix,
      flake-utils,
      opam-repository,
      # coq-library-undecidability
      nixpkgs,
    }:
    flake-utils.lib.eachDefaultSystem (system: {
      legacyPackages =
        let
          pkgs = nixpkgs.legacyPackages.${system};
          opam-coq-archive = pkgs.fetchFromGitHub {
            "owner" = "rocq-prover";
            "repo" = "opam";
            "rev" = "faf3b3d4d2a25f0b9a312e416d1a43c826e25ec7";
            "hash" = "sha256-9+5jrUbNpuC7Ct6rWIRUmmwuH1NAPkJofQC3BK/3yGg=";
          };
          inherit (opam-nix.lib.${system}) queryToScope;
          scope =
            queryToScope
              {
                repos = [
                  "${opam-repository}"
                  "${opam-coq-archive}/released"
                ];
              }
              {
                rocq-prover = "8.20";
                coq-library-undecidability = "1.1.2+8.20";
                ocaml-base-compiler = "4.14.1+flambda";
                vscoq-language-server = "*";
              };
        in
        scope;

      packages.default = self.legacyPackages.${system}.coq-library-undecidability;
    });
}

This is giving the following errors at present:

error:
       … while evaluating the attribute 'legacyPackages.aarch64-darwin.coq-library-undecidability'
         at /nix/store/01x5k4nlxcpyd85nnr0b9gm89rm8ff4x-source/lib.nix:44:11:
           43|         ${key} = (attrs.${key} or { }) // {
           44|           ${system} = ret.${key};
             |           ^
           45|         };

       … while evaluating the attribute 'legacyPackages'
         at /nix/store/2nl3w5hmmq48cl1zn13svqqj2m9nw8qd-source/flake.nix:21:7:
           20|     flake-utils.lib.eachDefaultSystem (system: {
           21|       legacyPackages =
             |       ^
           22|         let

       (stack trace truncated; use '--show-trace' to show the full, detailed trace)

       error: Cannot build '/nix/store/bllcvg8b3kdhdnd575l3k293icf0za70-resolve.drv'.
       Reason: builder failed with exit code 20.
       Output paths:
         /nix/store/0v4j6hp2lifak0af64hiibyyfx88g98f-resolve
       Last 5 log lines:
       > [ERROR] No solution including optional dependencies for coq-library-undecidability.1.1.2+8.20 & ocaml-base-compiler.4.14.1+flambda & rocq-prover.8.20 & vscoq-language-server:   * Missing dependency:
       >             - (request) -> ocaml-base-compiler > 5.5.0
       >             no matching version
       >
       >
       For full logs, run:
         nix-store -l /nix/store/bllcvg8b3kdhdnd575l3k293icf0za70-resolve.drv

I think the issue is coming from not specifying the vscoq-language-server version correctly, but I'm not sure so any help would be greatly appreciated!

[balsoft]

Maybe you need to get rid of ocaml-base-compiler = "4.14.1+flambda"; in the query? It seems like something somewhere requests it to be a higher version.

[jstrattonsmith]

Right, I added the various version specifications because simply leaving “*” also unfortunately gave the same kind of message about versions, so it seems that somewhere between nix and opam the version resolution is falling apart.

…

On Thu, Sep 4, 2025 at 08:19 Alexander Bantyev ***@***.***> wrote: Maybe you need to get rid of ocaml-base-compiler = "4.14.1+flambda"; in the query? It seems like something somewhere requests it to be a higher version. — Reply to this email directly, view it on GitHub <#131 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AL5FCHAXKN747SYCGLLSPUL3RAU3LAVCNFSM6AAAAACFSFNAOCVHI2DSMVQWIX3LMV43URDJONRXK43TNFXW4Q3PNVWWK3TUHMYTIMZQG4YDQMI> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[balsoft]

Actually, removing an explicit requirement on roqc-prover seems to fix the issue - I wonder if this is due to the coq->rocq rename and associated packaging shenanigans? I.e. the library depends on coq rather than rocq-prover. Maybe this change is workable for you?

[jstrattonsmith]

My goodness that is simple, thank you!! It doesn't seem to be exposing the vscoq-language-server still. Is there something else I need to do to expose this in the final output of the flake so that I can use this in vs code?

[balsoft]

Hm, how are you expecting to get it?

I would suspect in the end you actually want to properly package your rocq files, build that package with opam-nix and then add it to inputsFrom in an mkShell. In the meantime (just for hacking) you can try something like this:

        devShells.default = pkgs.mkShell {
          packages = with self.legacyPackages.${system}; [
            vscoq-language-server
            coq-library-undecidability
            coq
          ];
        };

[jstrattonsmith]

Thank you! This gave the final result of:

{
  description = "Build a rocq (coq) package";
  inputs.opam-nix.url = "github:tweag/opam-nix";
  inputs.opam-repository.url = "github:ocaml/opam-repository";
  inputs.opam-repository.flake = false;
  inputs.nixpkgs.url = "github:nixos/nixpkgs";
  inputs.flake-utils.url = "github:numtide/flake-utils";
  inputs.opam-coq-archive.url = "github:rocq-prover/opam/";
  inputs.opam-coq-archive.flake = false;

  outputs =
    {
      self,
      opam-nix,
      flake-utils,
      opam-repository,
      opam-coq-archive,
      nixpkgs,
    }:
    flake-utils.lib.eachDefaultSystem (system:
    let pkgs = nixpkgs.legacyPackages.${system}; in {
      devShells.default = pkgs.mkShell {
          packages = with self.legacyPackages.${system}; [
            vscoq-language-server
            coq-library-undecidability
            coq
          ];
        };
      legacyPackages =
        let
          inherit (opam-nix.lib.${system}) queryToScope;
          scope =
            queryToScope
              {
                repos = [
                  "${opam-repository}"
                  "${opam-coq-archive}/released"
                ];
              }
              {
                coq-library-undecidability = "*"; # "1.1.2+8.20";
                ocaml-base-compiler = "*"; # "4.14.1+flambda";
                vscoq-language-server = "*";
              };
        in
        scope;

        packages.default = self.legacyPackages.${system}.coq-library-undecidability;
    });
}

[jstrattonsmith]

Would this require a separate flake.nix/shell.nix file? I'm not sure what you mean exactly because I'm trying to use a set of rocq files from someone else's repository that they have setup with opam. I guess my question is where should the mkShell go?

…

On Fri, Sep 5, 2025 at 6:23 AM Alexander Bantyev ***@***.***> wrote: Hm, how are you expecting to get it? I would suspect in the end you actually want to properly package your rocq files, build that package with opam-nix and then add it to inputsFrom in an mkShell. In the meantime (just for hacking) you can try something like this: devShells.default = pkgs.mkShell { packages = with self.legacyPackages.${system}; [ vscoq-language-server coq-library-undecidability coq ]; }; — Reply to this email directly, view it on GitHub <#131 (reply in thread)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AL5FCHEWD7HK6BKQ3UJQCVD3RFQCNAVCNFSM6AAAAACFSFNAOCVHI2DSMVQWIX3LMV43URDJONRXK43TNFXW4Q3PNVWWK3TUHMYTIMZRGY4DIOI> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[balsoft]

In the same flake.nix you've sent in the original question, probably