Skip to content

New nix flake interface - #482

Draft
MysaaJava wants to merge 2 commits into
rocq-community:masterfrom
MysaaJava:flakes
Draft

New nix flake interface#482
MysaaJava wants to merge 2 commits into
rocq-community:masterfrom
MysaaJava:flakes

Conversation

@MysaaJava

Copy link
Copy Markdown
Contributor

This is the file i have written to provide a real flake interface for the rocq-nix-toolbox.

You can find the website at the following location
For now, i started writing pages bundle config and troubleshoot.
I also made a logo for fun, if you want to discuss it, no problem !

This implements some parts of the roadmap issue #359

@MysaaJava MysaaJava mentioned this pull request Jul 3, 2026
@MysaaJava

Copy link
Copy Markdown
Contributor Author

Here are some examples of usages of this branch:

  • A flake.nix for mathcomp-multinomials, a simple package
flake.nix file for mathcomp-multinomials
{
  description = "Mathcomp multinomials";

  inputs = {
    coq-nix-toolbox.url = "github:MysaaJava/coq-nix-toolbox?ref=flakes";
  };

  outputs = { self, coq-nix-toolbox }: {
    packages = coq-nix-toolbox.exportOverlays self.overlays (system: {
      default = self.packages.${system}.rocq91.rocqPackages.mathcomp-multinomials;
    });
    apps = coq-nix-toolbox.apps;
    overlays = let
      rocq91-overlay = coq-nix-toolbox.mkOverlay {
        rocqPackages.rocq-core.override.version = "9.1";
      };
      rocq92-overlay = coq-nix-toolbox.mkOverlay {
        rocqPackages.rocq-core.override.version = "9.2";
        # We override version below because 9.2 is not supported in nixpkgs for them
        rocqPackages.mathcomp.override.version = "2.5.0";
        rocqPackages.mathcomp-finmap.override.version = "2.2.2";
        rocqPackages.mathcomp-bigenough.override.version = "1.0.4";

      };
      rocq-recipes-overlay = coq-nix-toolbox.mkRocqRecipesOverlay {
        mathcomp-multinomials = ./package.nix;
      };
    in {
      rocq91 = coq-nix-toolbox.composeOverlays [ rocq-recipes-overlay rocq91-overlay ];
      rocq92 = coq-nix-toolbox.composeOverlays [ rocq-recipes-overlay rocq92-overlay ];
    };
  };
}

You can run the following commands:

nix build .#rocq91.rocqPackages.mathcomp-multinomials
nix build .#rocq92.rocqPackages.mathcomp-multinomials
  • Trocq, a complex project, available for coqPackages and rocqPackages, and with some version overrides
    Available on the branch cnt-flakes
    You can run the following commands:
nix build .#rocq91.rocqPackages.trocq.examples.std
nix build .#rocq90.rocqPackages.trocq.examples.std
nix build .#rocq91.rocqPackages.trocq.std
nix build .#coq91.coqPackages.trocq.examples.hott
...
# This one does not build because HoTT is not in rocqPackages
nix build .#rocq91.rocqPackages.trocq.examples.hott
# This one does not work ! This is a bug
nix build .#coq90.coqPackages.trocq

@CohenCyril

CohenCyril commented Jul 3, 2026

Copy link
Copy Markdown
Collaborator
# This one does not work ! This is a bug
nix build .#coq90.coqPackages.trocq

this is a bug where?

@MysaaJava

Copy link
Copy Markdown
Contributor Author

There is a bug in nixpkgs making it so we have to set coqPackages.coq.override.version AND rocqPackages.rocq-core.override.version.
This is the same in the master branch of coq-nix-toolbox.

However, i was not able to reproduce the fix in my flake.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants