Unverified Commit 84206e18 authored by Nadja Yang's avatar Nadja Yang
Browse files

leanPackages: init at 4.28.0 

Lean 4 package set providing the mathlib dependency tree:
batteries, aesop, Qq, proofwidgets, plausible, LeanSearchClient,
Cli, importGraph, and mathlib itself.

All lockstep packages are versioned with lean4.  ProofWidgets and
LeanSearchClient follow their own versioning, pinned via mathlib's
lake-manifest.json.

Includes update.sh which updates all packages to match the lean4
version in nixpkgs, with a dependency-set check to detect upstream
changes.
parent e8db3457

pkgs/development/lean-modules/Cli/default.nix

0 → 100644
+26 −0
Original line number Diff line number Diff line 
{

  lib,

  buildLakePackage,

  fetchFromGitHub,

}:



buildLakePackage {

  pname = "lean4-cli";

  version = "4.28.0";



  src = fetchFromGitHub {

    owner = "leanprover";

    repo = "lean4-cli";

    tag = "v4.28.0";

    hash = "sha256-9nX+dozmDAaVb5uKWL14zbILr7aqbVerTyPcN12Niw4=";

  };



  leanPackageName = "Cli";



  meta = {

    description = "Command-line argument parser for Lean 4";

    homepage = "https://github.com/leanprover/lean4-cli";

    license = lib.licenses.mit;

    maintainers = with lib.maintainers; [ nadja-y ];

  };

}

pkgs/development/lean-modules/LeanSearchClient/default.nix

0 → 100644
+33 −0
Original line number Diff line number Diff line 
{

  lib,

  buildLakePackage,

  fetchFromGitHub,

}:



buildLakePackage {

  pname = "lean4-LeanSearchClient";

  # No lockstep tags; version pinned by mathlib's lake-manifest.json.

  version = "0-unstable-2026-02-12";



  src = fetchFromGitHub {

    owner = "leanprover-community";

    repo = "LeanSearchClient";

    rev = "c5d5b8fe6e5158def25cd28eb94e4141ad97c843";

    hash = "sha256-L2aAwn3OeRLVt/VccLdBS0ogqmIIKAwnz94PpAOhaRc=";

  };



  leanPackageName = "LeanSearchClient";



  # Upstream lean-toolchain lags behind; remove it so the

  # buildLakePackage toolchain check does not reject this package.

  postPatch = ''

    rm -f lean-toolchain

  '';



  meta = {

    description = "Lean 4 client for LeanSearch and Moogle proof search";

    homepage = "https://github.com/leanprover-community/LeanSearchClient";

    license = lib.licenses.asl20;

    maintainers = with lib.maintainers; [ nadja-y ];

  };

}

pkgs/development/lean-modules/Qq/default.nix

0 → 100644
+26 −0
Original line number Diff line number Diff line 
{

  lib,

  buildLakePackage,

  fetchFromGitHub,

}:



buildLakePackage {

  pname = "lean4-Qq";

  version = "4.28.0";



  src = fetchFromGitHub {

    owner = "leanprover-community";

    repo = "quote4";

    tag = "v4.28.0";

    hash = "sha256-BRrSdDJQAsgM/NeSL2FODCez/8zEffjDRWUToGlKDNQ=";

  };



  leanPackageName = "Qq";



  meta = {

    description = "Lean 4 compile-time quote and antiquote macros for metaprogramming";

    homepage = "https://github.com/leanprover-community/quote4";

    license = lib.licenses.asl20;

    maintainers = with lib.maintainers; [ nadja-y ];

  };

}

pkgs/development/lean-modules/aesop/default.nix

0 → 100644
+28 −0
Original line number Diff line number Diff line 
{

  lib,

  buildLakePackage,

  fetchFromGitHub,

  batteries,

}:



buildLakePackage {

  pname = "lean4-aesop";

  version = "4.28.0";



  src = fetchFromGitHub {

    owner = "leanprover-community";

    repo = "aesop";

    tag = "v4.28.0";

    hash = "sha256-KeP46qtEf4/lgi4iCVuYIQbazufTR4luTbsuia9JkK4=";

  };



  leanPackageName = "aesop";

  leanDeps = [ batteries ];



  meta = {

    description = "White-box automation for Lean 4";

    homepage = "https://github.com/leanprover-community/aesop";

    license = lib.licenses.asl20;

    maintainers = with lib.maintainers; [ nadja-y ];

  };

}

pkgs/development/lean-modules/batteries/default.nix

0 → 100644
+26 −0
Original line number Diff line number Diff line 
{

  lib,

  buildLakePackage,

  fetchFromGitHub,

}:



buildLakePackage {

  pname = "lean4-batteries";

  version = "4.28.0";



  src = fetchFromGitHub {

    owner = "leanprover-community";

    repo = "batteries";

    tag = "v4.28.0";

    hash = "sha256-3N1MCFsg5UiwBCMAhDK7WwIowMNnhjlFgAsm0UPtGKc=";

  };



  leanPackageName = "batteries";



  meta = {

    description = "The batteries-included extended library for Lean 4";

    homepage = "https://github.com/leanprover-community/batteries";

    license = lib.licenses.asl20;

    maintainers = with lib.maintainers; [ nadja-y ];

  };

}