nix: `roots` for `buildLeanPackage`

Stream: lean4

[Julien Marquet]

I had to setup a dev environment for a Lean project, where there were two files at the top level. Below is a mwe project folder: Main.lean with Aux.lean and Aux/Basic.lean, nothing special in these files.
My issue is that, even though my main file imports all the files it requires, nix build crashes (and nix run .#vscode-dev will show errors too in the Lean info view).
I found out that if I add roots = [ "Main" "Aux" ]; to my flake.nix, everything works.

This is not a blocking issue since I found a fix, but I was wondering whether this is intended behavior or this is a bug...?

---

The reproduced folder looks like this:
<root>

• Aux
  • Basic.lean
• Aux.lean
• Main.lean

Main.lean:

import Aux

Aux.lean:

import Aux.basic

flake.nix:

{
  description = "Example package with two roots";

  inputs.nixpkgs.url = github:NixOS/nixpkgs/nixpkgs-unstable;
  # inputs.lean.url = "github:leanprover/lean4";
  inputs.lean.url = github:leanprover/lean4-nightly/nightly-2022-07-12;
  inputs.flake-utils.url = "github:numtide/flake-utils";

  outputs = { self, nixpkgs, lean, flake-utils }: flake-utils.lib.eachDefaultSystem (system:
      let
        pkgs = import nixpkgs {
          inherit system;
          config.allowUnfree = true;
        };
        leanPkgs = lean.packages.${system};
        pkg = with pkgs;
          leanPkgs.buildLeanPackage.override (old1: {
            lean-vscode = old1.lean-vscode.override (old2: {
              vscodeExtensions = with vscode-extensions; [ vscodevim.vim ] ++ old2.vscodeExtensions;
            });
          }) {
            name = "Main"; # must match the name of the top-level .lean file
            roots = [ "Main" "Aux" ]; -- Error if I remove this line
            src = ./.;
          };
      in {
        packages = pkg // { inherit (leanPkgs) lean; };

        defaultPackage = pkg.modRoot;
      });
}

Error if I remove roots = [ "Main" "Aux" ];:

error: attribute 'Aux' missing

       at /nix/store/8450kwpby6j2rbdim387xz026zv7pwaq-source/nix/buildLeanPackage.nix:187:17:

          186|     let
          187|       deps = if modDepsMap.${mod}.errors == []
             |                 ^
          188|              then map (m: m.module) modDepsMap.${mod}.imports
(use '--show-trace' to show detailed location information)

[Sebastian Ullrich]

Yes, this is intended, and should match Lake's behavior. You are supposed to store files belonging to a package in a root of the package's name.

[Julien Marquet]

Should I PR to add a comment here in the flake template, and/or add a line in the docs?

[Sebastian Ullrich]

Apologies for the late answer. More documentation is always good, though I don't want to encourage people to publish Lean packages solely as flakes where a lakefile would work just as well. If a package is not meant for general consumption, that's fine of course.

[Eric Meinhardt]

edit: whoops

[Chris Lovett]

I agree with Sebastian, nix is not easily to setup on all platforms, whereas lake runs fine everywhere, so it would be great if all lean packages were buildable using lake, then similar to how Lean repo is setup, nix flakes can be provided as an alternative build system for those who prefer it.