diff --git a/pkgs/applications/science/logic/clprover/clprover.nix b/pkgs/applications/science/logic/clprover/clprover.nix deleted file mode 100644 index 543c6cb4310b..000000000000 --- a/pkgs/applications/science/logic/clprover/clprover.nix +++ /dev/null @@ -1,28 +0,0 @@ -{ lib, stdenv, fetchzip }: - -stdenv.mkDerivation { - pname = "clprover"; - version = "1.0.3"; - - src = fetchzip { - url = "https://cgi.csc.liv.ac.uk/~ullrich/CLProver++/CLProver++-v1.0.3-18-04-2015.zip"; - sha256 = "10kmlg4m572qwfzi6hkyb0ypb643xw8sfb55xx7866lyh37w1q3s"; - stripRoot = false; - }; - - installPhase = '' - mkdir $out - cp -r bin $out/bin - mkdir -p $out/share/clprover - cp -r examples $out/share/clprover/examples - ''; - - meta = with lib; { - description = "Resolution-based theorem prover for Coalition Logic implemented in C++"; - mainProgram = "CLProver++"; - homepage = "https://cgi.csc.liv.ac.uk/~ullrich/CLProver++/"; - license = licenses.gpl3; # Note that while the website states that it is GPLv2 but the file in the zip as well as the comments in the source state it is GPLv3 - maintainers = with maintainers; [ mgttlinger ]; - platforms = [ "x86_64-linux" ]; - }; -} diff --git a/pkgs/by-name/cl/clprover/package.nix b/pkgs/by-name/cl/clprover/package.nix new file mode 100644 index 000000000000..ec18eb101cb4 --- /dev/null +++ b/pkgs/by-name/cl/clprover/package.nix @@ -0,0 +1,60 @@ +{ + stdenv, + lib, + fetchFromGitHub, +}: + +stdenv.mkDerivation (self: { + pname = "CLProver++"; + version = "1.0.3"; + + src = fetchFromGitHub { + owner = "PaulGainer"; + repo = "CLProverPlusPlus"; + rev = "66bf6dc19d77094cc06eac3f30a3630ba830ac86"; + sha256 = "sha256-UZ5e11wGuKyVrG+7hZJY6OmN6Y1mg43xPuvXPRVNKNw="; + }; + + postPatch = '' + sed -i 's/\(TARGET_OS *:= *\)[^ ]+/\1${ + if stdenv.targetPlatform.isWindows then "WINDOWS" else "LINUX" + }/g' Makefile + sed -i 's/-m64/${ + if stdenv.targetPlatform.isAarch then + "-march=${stdenv.targetPlatform.gcc.arch}" + else if stdenv.targetPlatform.is32bit then + "-m32" + else + "-m64" + }/g' Makefile + ''; + + preBuild = '' + mkdir bin + ''; + + makeFlags = [ + "CC=${lib.getBin stdenv.cc}/bin/${stdenv.cc.targetPrefix}g++" + ]; + + installPhase = '' + runHook preInstall + + mkdir -p $out/bin + cp -r bin $out/ + + mkdir -p $out/share/${self.pname} + cp -r examples $out/share/${self.pname}/examples + + runHook postInstall + ''; + + meta = { + description = "Ordered resolution based theorem prover for Coalition Logic"; + homepage = "https://cgi.csc.liv.ac.uk/~ullrich/CLProver++/"; + maintainers = with lib.maintainers; [ mgttlinger ]; + platforms = with lib.platforms; linux ++ windows; + license = lib.licenses.gpl3; + mainProgram = if stdenv.targetPlatform.isWindows then "CLProver++.exe" else "CLProver++"; + }; +}) diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 16b6aa095873..e7112a5a7dd6 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -2194,8 +2194,6 @@ with pkgs; clingcon = callPackage ../applications/science/logic/potassco/clingcon.nix { }; - clprover = callPackage ../applications/science/logic/clprover/clprover.nix { }; - coloredlogs = with python3Packages; toPythonApplication coloredlogs; czkawka-full = czkawka.wrapper.override {