General improvements

[RossSmyth]

Hello! Thank you for volunteering to take over the Lean4 nix utilities!

I have some general suggestions for improving the user experience with this library.

1. Don't use flake modules

They are a bit niche and just add to the closure that must be downloaded.

2. Use the pre-built binaries by default

This seems to be a goal(?), but building Lean takes about an hour so the current experience sucks.

3. Add a default on the flake overlay output

The default should probably just be the latest release.

5. Separate the different functions

Currently lake, lean, and buildLeanPackage are all tangled together. I think I know why, but it make the API hard to understand. They should probably be three independent things that are accessible after the overlay is applied.

6. What ever is going on here

lean4-nix/templates/dependency/flake.nix

Lines 35 to 39 in 7a6faed

	((lean4-nix.lake {inherit pkgs;}).mkPackage {
	src = ./.;
	roots = ["Example"];
	})
	.executable;

This is a very strange API. Should probably just be overlaid on pkgs.

7. Remove the "executeble" attribute

The buildLeanPacakge function should probably just return a derivation like all other builders.

Ideally one would be able to write something like:

flake.nix

{
  description = "Lean 4 Example Project";

  inputs = {
    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
    lean4-nix = {
      url = "github:lenianiva/lean4-nix";
      inputs.nixpkgs.follows = "nixpkgs";
    };
  };

  outputs = {
    nixpkgs,
    lean4-nix,
    ...
  }: let
    pkgs = import nixpkgs {
        system = "x86_64-linux";
        overlays = [ (import lean4-nix) ];
    };
  in {
    packages.default = pkgs.callPackage ./default.nix {};
  };
}

default.nix

{
  buildLeanPackage,
  lib,
  ...
}:
buildLeanPackage
{
  name = "Example";
  roots = ["Main"];
  src = lib.cleanSource ./.;
}

Or alternatively, similar to the rustPlatform API
default.nix

{
  leanPlatform,
  lib,
  ...
}:
leanPlatform.buildLeanPackage
{
  name = "Example";
  roots = ["Main"];
  src = lib.cleanSource ./.;
}

Perhaps a rustPlatform-like API could work with the strange lake API.

[lenianiva]

1. Don't use flake modules

Then the user can delete them. I use flake-parts because its a good starting point compared to just cooking up our own perSystem

2. Use the pre-built binaries by default

This problem should be solved by caching

3. Add a default on the flake overlay output

Like this?

pkgs = import nixpkgs {
  inherit system;
  overlays = [lean4-nix.default];
};

5. Separate the different functions
6. Remove the "executeble" attribute

The problem is buildLeanPackage comes from the upstream Lean repo, not this one. We try to reuse as much code from Lean as possible. Lean's package format is different from derivation and that caused the problem you're seeing here.

6. What ever is going on here

This is pretty standard. Vide crane:

craneLib = crane.mkLib pkgs;
src = craneLib.cleanCargoSource ./.;

I should've written it in two lines instead of one.

[RossSmyth]

Then the user can delete them.

It is a poor default sticking something in a template

This problem should be solved by caching

So every time I update my flake.lock I need to wait an hour? Or a possible cachix in the future? Why not just download a stable version? Time to first compile is important and it is currently quite bad.

The problem is buildLeanPackage comes from the upstream Lean repo, not this one. We try to reuse as much code from Lean as possible.

I understand that. But is leads to poor UX

This is pretty standard. Vide crane:

This makes sense if the entire API was instantiated from pkgs. Instead only the lake attribute is which is strange. I don't even like the crane solution anyways when there are better alternatives (overlays).

[lenianiva]

It is a poor default sticking something in a template

People stick flake-utils in templates all the time and there doesn't seem to be much issue about it

Or a possible cachix in the future?

This is the goal. We can also do what rust-overlay does which fetches a pre-built binary via some hash, but this introduces another problem. We can't provide buildLeanPackage if everything is in a pre-built binary. buildLeanPackage needs to link the build target against Std, Init, and Lean. It might work after some reverse engineering of Lean.

Meanwhile you can also host your own cache via attic

I understand that. But is leads to poor UX

Better UX comes at the expense of more reverse engineering and testing of this repo. I disagreed with how Lean's dev team moved its Nix support out of the Lean repo since thats the most logical place to have it, and it would be much easier to convert the output of buildLeanPackage to a derivation had that stayed in the repo. However I don't make decisions about the trajectory of leanprover/lean4.

This makes sense if the entire API was instantiated from pkgs. Instead only the lake attribute is which is strange.

I didn't make lake an override because lake is not an executable or library or something you link against. Its just a set of functions in Nix. Similar thing happens for poetry2nix for example.