Unverified Commit 9e5ddd83 authored by 7c6f434c's avatar 7c6f434c Committed by GitHub
Browse files

acl2: backport fix for fastnumio on recent sbcl versions (#346656)

parents 40bfbe32 ed9ef0cf

pkgs/development/interpreters/acl2/default.nix

+21 −8
Original line number Diff line number Diff line 
{ lib, stdenv, callPackage, fetchFromGitHub, runCommandLocal, makeWrapper, substituteAll

{ lib, stdenv, callPackage, fetchFromGitHub, fetchpatch, runCommandLocal, makeWrapper, substituteAll

, sbcl, bash, which, perl, hostname

, openssl, glucose, minisat, abc-verifier, z3, python3

, certifyBooks ? true
@@ -33,12 +33,25 @@ in stdenv.mkDerivation rec { 
  # $IPASIR_SHARED_LIBRARY environment variable.

  libipasir = callPackage ./libipasirglucose4 { };



  patches = [(substituteAll {

  patches = [

    (substituteAll {

      src = ./0001-Fix-some-paths-for-Nix-build.patch;

      libipasir = "${libipasir}/lib/${libipasir.libname}";

      libssl = "${lib.getLib openssl}/lib/libssl${stdenv.hostPlatform.extensions.sharedLibrary}";

      libcrypto = "${lib.getLib openssl}/lib/libcrypto${stdenv.hostPlatform.extensions.sharedLibrary}";

  })];

    })

    (fetchpatch {

      name = "fix-fastnumio-on-newer-sbcl.patch";

      url = "https://github.com/acl2-devel/acl2-devel/commit/84f5a6cd4a1aaf204e8bae3eab4c21e8c061f469.patch";

      hash = "sha256-VA9giXZMb/Ob8ablxfbBAaZ2+2PGcv7WtooXwKDgT08=";

    })

  ];



  # We need the timestamps on the source tree to be stable for certification to

  # work properly, so reset them here as necessary after patching

  postPatch = ''

    find . -type f -newer "$src" -execdir touch -r "$src" {} +

  '';



  nativeBuildInputs = lib.optional certifyBooks makeWrapper;
@@ -112,7 +125,7 @@ in stdenv.mkDerivation rec { 
  '';



  meta = with lib; {

    description = "Interpreter and a prover for a Lisp dialect";

    description = "Interpreter and prover for a Lisp dialect";

    mainProgram = "acl2";

    longDescription = ''

      ACL2 is a logic and programming language in which you can model computer