From f79b811f2dd62f5ae46fc460164ebbd865cf9c44 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= <supermanitu@gmail.com>
Date: Sun, 2 Jan 2022 11:16:27 +0100
Subject: [PATCH] eprover: Add option to enable LFHOL reasoning

Using eprover as automated theorem prover for sledgehammer requires this
option.
---
 pkgs/applications/science/logic/eprover/default.nix | 4 +++-
 pkgs/top-level/all-packages.nix                     | 2 ++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/pkgs/applications/science/logic/eprover/default.nix b/pkgs/applications/science/logic/eprover/default.nix
index 3b757d40a694..400d636346c5 100644
--- a/pkgs/applications/science/logic/eprover/default.nix
+++ b/pkgs/applications/science/logic/eprover/default.nix
@@ -1,4 +1,4 @@
-{ lib, stdenv, fetchurl, which }:
+{ lib, stdenv, fetchurl, which, enableHO ? false }:
 
 stdenv.mkDerivation rec {
   pname = "eprover";
@@ -17,6 +17,8 @@ stdenv.mkDerivation rec {
   configureFlags = [
     "--exec-prefix=$(out)"
     "--man-prefix=$(out)/share/man"
+  ] ++ lib.optionals enableHO [
+    "--enable-ho"
   ];
 
   meta = with lib; {
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index b55a618f44d6..d798645eb60d 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -31965,6 +31965,8 @@ with pkgs;
 
   eprover = callPackage ../applications/science/logic/eprover { };
 
+  eprover-ho = callPackage ../applications/science/logic/eprover { enableHO = true; };
+
   gappa = callPackage ../applications/science/logic/gappa { };
 
   gfan = callPackage ../applications/science/math/gfan {};