Commit edc8a602 authored by Yiyu Zhou's avatar Yiyu Zhou
Browse files

opensmt: cleanup

parent 22f1c077

pkgs/by-name/op/opensmt/package.nix

+17 −11
Original line number Diff line number Diff line
@@ -10,24 +10,28 @@ 
  enableReadline ? false,

  readline,

  gtest,

  nix-update-script,

}:



stdenv.mkDerivation rec {

stdenv.mkDerivation (finalAttrs: {

  pname = "opensmt";

  version = "2.9.2";



  src = fetchFromGitHub {

    owner = "usi-verification-and-security";

    repo = "opensmt";

    rev = "v${version}";

    sha256 = "sha256-xKpYABMn2bsXRg2PMjiMhsx6+FbAsxitLRnmqa1kmu0=";

    tag = "v${finalAttrs.version}";

    hash = "sha256-xKpYABMn2bsXRg2PMjiMhsx6+FbAsxitLRnmqa1kmu0=";

  };



  strictDeps = true;



  nativeBuildInputs = [

    cmake

    bison

    flex

  ];



  buildInputs = [

    libedit

    gmpxx
@@ -36,17 +40,19 @@ stdenv.mkDerivation rec { 
  ++ lib.optional enableReadline readline;



  preConfigure = ''

    substituteInPlace test/CMakeLists.txt \

      --replace-fail 'FetchContent_MakeAvailable' '#FetchContent_MakeAvailable'

    substituteInPlace test/CMakeLists.txt --replace-fail \

      'FetchContent_MakeAvailable' '#FetchContent_MakeAvailable'

  '';



  meta = with lib; {

    broken = (stdenv.hostPlatform.isLinux && stdenv.hostPlatform.isAarch64);

  passthru.updateScript = nix-update-script { };



  meta = {

    broken = with stdenv.hostPlatform; (isLinux && isAarch64);

    description = "Satisfiability modulo theory (SMT) solver";

    mainProgram = "opensmt";

    maintainers = [ maintainers.raskin ];

    platforms = platforms.linux;

    license = if enableReadline then licenses.gpl2Plus else licenses.mit;

    maintainers = [ lib.maintainers.raskin ];

    platforms = lib.platforms.linux;

    license = if enableReadline then lib.licenses.gpl2Plus else lib.licenses.mit;

    homepage = "https://github.com/usi-verification-and-security/opensmt";

  };

}
 
})