Using lake from nix flake

Stream: lean4

[Leni Aniva]

I'm creating a package that bundles lake from the main Lean 4 repository. A MWE is as follows:

# flake.nix
{
  description = "Lean-Encapsulate";

  inputs = {
    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
    flake-parts.url = "github:hercules-ci/flake-parts";
    lean.url = "github:leanprover/lean4?ref=v4.1.0";
  };

  outputs = inputs @ {
    self,
    nixpkgs,
    flake-parts,
    lean,
    ...
  } : flake-parts.lib.mkFlake { inherit inputs; } {
    flake = {
    };
    systems = [
      "x86_64-linux"
      "x86_64-darwin"
    ];
    perSystem = { system, pkgs, ... }: let
      leanPkgs = lean.packages.${system};
    in rec {
      packages = {
        lean = leanPkgs.lean;
      };
      devShells.default = pkgs.mkShell {
        buildInputs = [
          leanPkgs.lean
          leanPkgs.Lake-Main.executable
        ];
      };
    };
  };
}

Here I have a devShell with lean and lake packaged into it:

$ which lean
/nix/store/45iycrslp9n7z2c202q8p8n23hpnbsgk-lean/bin/lean
$ which lake
/nix/store/fsgh02bjxmy42rxsqmyk4k3m1fqwgk48-lake/bin/lake

However this version of lake is not working. For example, if I were to create a new project and to build it:

$ lake --lean=lean new Project
$ cd Project
$ lake --lean=lean build
error: ./lakefile.lean:1:0: error: unknown package 'Init'
error: ./lakefile.lean:2:5: error: unknown namespace 'Lake'
error: ./lakefile.lean:4:0: error: unexpected identifier; expected command
error: ./lakefile.lean:10:17: error: unexpected identifier; expected 'abbrev', 'axiom', 'builtin_initialize', 'class', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem'
error: ./lakefile.lean: package configuration has errors

How can I use the bundled lake?

[Joachim Breitner]

The nix setup is essentially unmaintained, so you are more or less on your own, sorry. If you want a nixified dev setup, get elan from nixpkg, and let that handle fetching lean or lake.

[Enrico Borba]

I have a nix flake setup:

{
  description = "...";
  inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
  inputs.flake-utils.url = "github:numtide/flake-utils";

  inputs.lean4.url = "github:leanprover/lean4/v4.5.0";

  outputs = { self, nixpkgs, flake-utils, lean4 }:
    flake-utils.lib.eachDefaultSystem (system:
      let
        pkgs = nixpkgs.legacyPackages.${system};
        lean4-pkgs = lean4.packages.${system};
      in {
        devShells.default = pkgs.mkShell {
          packages = [ lean4-pkgs.lean-all lean4-pkgs.vscode ];
        };
      });
}

I then use

lake new <project>
lake init <project>

[Enrico Borba]

Let me know if you have issues with what I posted, I've been using it for a while for a variety of lean versions

[Leni Aniva]

Enrico Borba said:

I have a nix flake setup:

{
  description = "...";
  inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
  inputs.flake-utils.url = "github:numtide/flake-utils";

  inputs.lean4.url = "github:leanprover/lean4/v4.5.0";

  outputs = { self, nixpkgs, flake-utils, lean4 }:
    flake-utils.lib.eachDefaultSystem (system:
      let
        pkgs = nixpkgs.legacyPackages.${system};
        lean4-pkgs = lean4.packages.${system};
      in {
        devShells.default = pkgs.mkShell {
          packages = [ lean4-pkgs.lean-all lean4-pkgs.vscode ];
        };
      });
}

I then use

lake new <project>
lake init <project>

works perfectly! thanks