Commit 016be1d8 authored by Sergei Trofimovich's avatar Sergei Trofimovich
Browse files

lean3: fix `gcc-13` build failure) 

Without the change the build fails on `master` as https://hydra.nixos.org/build/247665202:

    /build/source/src/shell/lean_js.h:11:32: error: 'uintptr_t' was not declared in this scope
       11 | int emscripten_process_request(uintptr_t msg);
          |                                ^~~~~~~~~
parent 442d4079

pkgs/applications/science/logic/lean/default.nix

+10 −1
Original line number Diff line number Diff line 
{ lib, stdenv, fetchFromGitHub, cmake, gmp, coreutils }:

{ lib, stdenv, fetchFromGitHub, fetchpatch, cmake, gmp, coreutils }:



stdenv.mkDerivation rec {

  pname = "lean";
@@ -15,6 +15,15 @@ stdenv.mkDerivation rec { 
    hash   = "sha256-Vcsph4dTNLafeaTtVwJS8tWoWCgcP6pxF0ssZDE/YfM=";

  };



  patches = [

    # Fix gcc-13 build failure

    (fetchpatch {

      name = "gcc-13.patch";

      url = "https://github.com/leanprover-community/lean/commit/21d264a66d53b0a910178ae7d9529cb5886a39b6.patch";

      hash = "sha256-hBm2QNFS1jdoR6LUQHLReKxMKv7kbkrkrTGJ43YnvfA=";

    })

  ];



  nativeBuildInputs = [ cmake ];

  buildInputs = [ gmp ];