pkgs/by-name/le/lean/package.nix

   1 { lib, stdenv, fetchFromGitHub, fetchpatch, cmake, gmp, coreutils }:
   2
   3 stdenv.mkDerivation rec {
   4   pname = "lean";
   5   version = "3.51.0";
   6
   7   src = fetchFromGitHub {
   8     owner  = "leanprover-community";
   9     repo   = "lean";
  10     # lean's version string contains the commit sha1 it was built
  11     # from. this is then used to check whether an olean file should be
  12     # rebuilt. don't use a tag as rev because this will get replaced into
  13     # src/githash.h.in in preConfigure.
  14     rev    = "9fc1dee97a72a3e34d658aefb4b8a95ecd3d477c";
  15     hash   = "sha256-Vcsph4dTNLafeaTtVwJS8tWoWCgcP6pxF0ssZDE/YfM=";
  16   };
  17
  18   patches = [
  19     # Fix gcc-13 build failure
  20     (fetchpatch {
  21       name = "gcc-13.patch";
  22       url = "https://github.com/leanprover-community/lean/commit/21d264a66d53b0a910178ae7d9529cb5886a39b6.patch";
  23       hash = "sha256-hBm2QNFS1jdoR6LUQHLReKxMKv7kbkrkrTGJ43YnvfA=";
  24     })
  25   ];
  26
  27   nativeBuildInputs = [ cmake ];
  28   buildInputs = [ gmp ];
  29
  30   cmakeDir = "../src";
  31
  32   # Running the tests is required to build the *.olean files for the core
  33   # library.
  34   doCheck = true;
  35
  36   preConfigure = assert builtins.stringLength src.rev == 40; ''
  37      substituteInPlace src/githash.h.in \
  38        --subst-var-by GIT_SHA1 "${src.rev}"
  39      substituteInPlace library/init/version.lean.in \
  40        --subst-var-by GIT_SHA1 "${src.rev}"
  41   '';
  42
  43   postPatch = "patchShebangs .";
  44
  45   postInstall = lib.optionalString stdenv.hostPlatform.isDarwin ''
  46     substituteInPlace $out/bin/leanpkg \
  47       --replace "greadlink" "${coreutils}/bin/readlink"
  48   '';
  49
  50   meta = with lib; {
  51     description = "Automatic and interactive theorem prover";
  52     homepage    = "https://leanprover.github.io/";
  53     changelog   = "https://github.com/leanprover-community/lean/blob/v${version}/doc/changes.md";
  54     license     = licenses.asl20;
  55     platforms   = platforms.unix;
  56     maintainers = with maintainers; [ thoughtpolice gebner ];
  57   };
  58 }
  59