blob: d5916b7c884724364730f62ad9a2ea5cf4f85940 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
{ config, lib, pkgs, ... }:
with lib;
let
cfg = config.why3;
why3BuildInputs = [ cfg.package ] ++ cfg.provers
++ (optional config.coq.enable config.coq.coqPackages.coq);
why3Conf = pkgs.runCommand "why3.conf" { buildInputs = why3BuildInputs; } (''
why3 --config=$out config detect
'' + (optionalString (cfg.defaultEditor != null) ''
sed -i 's/^default_editor = ".*"$/default_editor = "${cfg.defaultEditor} %f"/' $out
'') + ''
echo "" >> $out
echo '${cfg.extraConfig}' >> $out
'');
why3Flags = concatStringsSep " " [ "--config=${why3Conf}" ];
in {
options.why3 = {
enable = mkEnableOption "why3";
package = mkOption {
type = types.package;
default = pkgs.why3;
defaultText = literalExample "pkgs.why3";
description = ''
The package for why3. This sets the version of Why3.
'';
};
provers = mkOption {
type = types.listOf types.package;
default = [ ];
description = ''
A list of packages that should be detected as provers by Why3 and
added as build inputs. Coq can be added independently using the
coq option.
'';
example = literalExample "with pkgs; [ z3 ccv4 ]";
};
defaultEditor = mkOption {
type = types.nullOr types.str;
default = null;
description = ''
The default editor to launch provers with.
'';
example = "emacsclient -c";
};
extraConfig = mkOption {
type = types.lines;
default = "";
description = ''
Extra configuration entries for Why3.
'';
};
};
config = mkIf cfg.enable {
buildInputs = why3BuildInputs;
# buildInputs = [(cfg.package.withProvers cfg.provers)];
aliases = { why3 = "${cfg.package}/bin/why3 ${why3Flags} \\$@"; };
coq = {
rc = ''
Add Rec LoadPath "${cfg.package}/lib/why3/coq/" as Why3.
'';
};
};
}
|
