tjh.dev
1{
2 lib,
3 stdenv,
4 fetchurl,
5 which,
6 enableHO ? false,
7}:
8
9stdenv.mkDerivation (finalAttrs: {
10 pname = "eprover";
11 version = "3.2";
12
13 src = fetchurl {
14 url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_${finalAttrs.version}/E.tgz";
15 hash = "sha256-B0yOX8MGJHY0HOeQ/RWtgATTIta2YnhEvSdoqIML1K4=";
16 };
17
18 buildInputs = [ which ];
19
20 preConfigure = ''
21 sed -e 's/ *CC *= *gcc$//' -i Makefile.vars
22 '';
23
24 configureFlags = [
25 "--exec-prefix=$(out)"
26 "--man-prefix=$(out)/share/man"
27 ]
28 ++ lib.optionals enableHO [
29 "--enable-ho"
30 ];
31
32 meta = {
33 description = "Automated theorem prover for full first-order logic with equality";
34 homepage = "http://www.eprover.org/";
35 license = lib.licenses.gpl2;
36 maintainers = with lib.maintainers; [
37 raskin
38 ];
39 platforms = lib.platforms.all;
40 };
41})