From 70145c342da927add3d42b2e477008b9bd765a0a Mon Sep 17 00:00:00 2001
From: Quentin Aristote <quentin@aristote.fr>
Date: Mon, 6 Dec 2021 17:19:21 +0100
Subject: add options to specify provers

---
 modules/why3.nix | 61 ++++++++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 53 insertions(+), 8 deletions(-)

(limited to 'modules/why3.nix')

diff --git a/modules/why3.nix b/modules/why3.nix
index 2e8a861..3a09c12 100644
--- a/modules/why3.nix
+++ b/modules/why3.nix
@@ -1,18 +1,63 @@
-{ lib, ... }:
+{ pkgs, lib, ... }:
 
+with lib;
 let
   cfg = config.why3;
-  why3Flags = concatStringsSep " " ([ ("-C '${cfg.configFile}'") ]);
+  proverSubmodule = types.submodule {
+    options = {
+      name = mkOption {
+        type = types.nullOr types.str;
+        default = null;
+        description = ''
+          The name of the prover.
+        '';
+      };
+      package = mkOption {
+        type = types.package;
+        description = ''
+          The package providing the prover.
+        '';
+      };
+    };
+  };
+  why3BuildInputs = [ cfg.package ] ++ cfg.provers.detect
+    ++ (mapAttrsToList (_: prover: prover.package) cfg.provers.manual);
 in {
   options.why3 = {
-    enable = lib.mkEnableOption "why3";
-    configFile = lib.mkOption {
-      type = lib.types.path;
-      default = ~/.why3.conf;
-      defaultText = literalExample "~/.why3.conf";
+    enable = mkEnableOption "why3";
+    package = mkOption {
+      type = types.package;
+      default = pkgs.why3;
+      defaultText = literalExample "pkgs.why3";
       description = ''
-        The path to the why3 config file.
+        The package for why3. This sets the version of Why3.
       '';
     };
+    provers = {
+      detect = mkOption {
+        type = types.listOf types.package;
+        default = [ ];
+        description = ''
+          Provers to use that are known to be supported by Why3.
+        '';
+        example = literalExample "with pkgs; [ z3 ccv4 ]";
+      };
+      manual = mkOption {
+        type = types.attrsOf proverSubmodule;
+        default = { };
+        description = ''
+          Provers to use that are not known to be supported by Why3.
+        '';
+        example = literalExample ''
+          {
+            myProver = {
+              package = pkgs.my-prover;
+            };
+          }
+        '';
+      };
+    };
   };
+
+  config.why3 = mkIf cfg.enable { buildInputs = why3BuildInputs; };
 }
-- 
cgit v1.2.3