WIP on putting a flake on top of the toolbox.

.nix/fallback-config.nix

@@ -1,4 +1,4 @@
-with (import (import ./nixpkgs.nix) {}).lib;
+with import "${import ./nixpkgs.nix}/lib";
 {
   ## DO NOT CHANGE THIS
   format = "1.0.0";
@@ -14,7 +14,7 @@ with (import (import ./nixpkgs.nix) {}).lib;
 
   ## select an entry to build in the following `bundles` set
   ## defaults to "default"
-  default-bundle = "8.18";
+  default-bundle = "rocq-9.0";
 
   ## write one `bundles.name` attribute set per
   ## alternative configuration, the can be used to

.nix/shellHook.sh

@@ -180,14 +180,14 @@ genNixActions (){
 addNixCommand genNixActions
 
 initNixConfig (){
-  Orig=$toolboxDir/template-config.nix
+  Orig=$toolboxDir/template/.nix/config.nix
   F=$configDir/config.nix;
   if [[ -f $F ]]; then
      echo "$F already exists"
   else if [[ -n "$1" ]]; then
        mkdir -p $configDir
        cat $Orig > $F
-       sed -i "s/template/$1/" $F
+       sed -i "s/YOUR_PACKAGE_NAME/$1/" $F
     else echo "usage: initNixConfig pname"
     fi
   fi

config-parser-1.0.0/default.nix

@@ -14,10 +14,11 @@ with builtins;
   ocaml-override ? {},
   global-override ? {},
   lib,
+  system
 }@initial:
 with lib;
 let config = import ./normalize.nix
-  { inherit (initial) src lib config nixpkgs; };
+  { inherit (initial) src lib config nixpkgs system; };
 in with config; let
 
   bundle-ppaths = bundle:
@@ -66,7 +67,7 @@ in with config; let
       { inherit lib overlays-dir rocq-overlays-dir coq-overlays-dir ocaml-overlays-dir bundle;
         inherit (config) attribute coq-attribute no-rocq-yet pname shell-attribute shell-pname src; };
 
-    pkgs = import config.nixpkgs { inherit overlays; };
+    pkgs = import config.nixpkgs { inherit overlays system; };
 
     ci = import ./ci.nix { inherit lib this-shell-pkg pkgs bundle; };
 

config-parser-1.0.0/normalize.nix

@@ -1,6 +1,6 @@
 # This file is a toolbox file to parse a ./nix/config.nix
 # file in format 1.0.0
-{lib, config, nixpkgs, src}@initial:
+{lib, config, nixpkgs, src, system}@initial:
 with builtins; with lib;
 let
   normalize-coqpkg = name: pkg: let j = pkg.job or name; in

default.nix

@@ -29,7 +29,8 @@ in
   update-nixpkgs ? false,
   job ? null,
   bundle ? null,
-  inNixShell ? null
+  inNixShell ? null,
+  system ? builtins.currentSystem
 }@args:
 let
   optionalImport = f: d:
@@ -40,7 +41,8 @@ let
     config = (optionalImport config-file (optionalImport fallback-file {}))
               // config;
     nixpkgs = optionalImport nixpkgs-file (throw "cannot find nixpkgs");
-    pkgs = import initial.nixpkgs {};
+    inherit system;
+    pkgs = import initial.nixpkgs { inherit system; };
     src = src;
     lib = (initial.pkgs.coqPackages.lib or tmp-pkgs.lib)
           // { diag = f: x: f x x; };

flake.nix

@@ -0,0 +1,52 @@
+{
+  description = "The Rocq Nix Toolbox";
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
+  };
+
+  outputs =
+    { nixpkgs, ... }:
+    rec {
+      lib = rec {
+        forAllSystems =
+          function:
+          nixpkgs.lib.genAttrs [
+            "x86_64-linux"
+            "aarch64-linux"
+            "x86_64-darwin"
+            "aarch64-darwin"
+          ] function;
+        allPackages =
+          src:
+          with nixpkgs.lib;
+          forAllSystems (
+            system:
+            let
+              underlyingNix = (import ./default.nix { inherit system src; });
+              instances = underlyingNix.passthru.setup.instances;
+              defaultInstance =
+                underlyingNix.passthru.setup.instances.${underlyingNix.passthru.setup.config.default-bundle};
+              jobsList = mapAttrsToList (
+                bundleName: instance:
+                let
+                  listOfJobs = map (jobName: {
+                    name = "${builtins.replaceStrings [ "." ] [ "-" ] bundleName}:${jobName}";
+                    value = instance.pkgs.rocqPackages.${jobName} or instance.pkgs.coqPackages.${jobName};
+                  }) instance.jobs;
+                in
+                listToAttrs listOfJobs
+              ) instances;
+            in
+            (foldl mergeAttrs { } jobsList)
+            // {
+              default = defaultInstance.this-pkg;
+            }
+          );
+      };
+      templates.default = {
+        path = ./template;
+        description = "Initialize the Rocq Nix Toolbox in a new project";
+      };
+      packages = lib.allPackages ./.;
+    };
+}

template-config.nix → template/.nix/config.nix

@@ -8,12 +8,12 @@
   ## either using nixpkgs data or the overlays located in `.nix/rocq-overlays`
   ## and `.nix/coq-overlays`
   ## Will determine the default main-job of the bundles defined below
-  attribute = "template";
+  attribute = "YOUR_PACKAGE_NAME";
 
   ## The attribute for coq compat shim, default to attribute
   ## set this when you need both to differ
   ## (for instance "rocq-elpi" and "coq-elpi")
-  # coq-attribute = "template";
+  # coq-attribute = "YOUR_PACKAGE_NAME";
 
   ## Set this when the package has no rocqPackages version yet
   ## (either in nixpkgs or in .nix/rocq-overlays)

template/flake.nix

@@ -0,0 +1,11 @@
+{
+  description = "A Nix flake for my Rocq project using the Rocq Nix Toolbox";
+  inputs = {
+    rocq-nix-toolbox.url = "github:rocq-community/coq-nix-toolbox";
+  };
+  outputs =
+    { rocq-nix-toolbox, ... }:
+    {
+      packages = rocq-nix-toolbox.lib.allPackages ./.;
+    };
+}