summary refs log tree commit diff
path: root/pkgs/development/coq-modules/itauto/default.nix
blob: 1ffa37ec6c3217c6951ace9aeff42d12601e25b0 (plain) (blame)
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
{ lib, mkCoqDerivation, coq, version ? null }:
with lib;

mkCoqDerivation rec {
  pname = "itauto";
  owner = "fbesson";
  domain = "gitlab.inria.fr";

  release."8.16.0".sha256 = "sha256-4zAUYGlw/pBcLPv2GroIduIlvbfi1+Vy+TdY8KLCqO4=";
  release."8.15.0".sha256 = "sha256:10qpv4nx1p0wm9sas47yzsg9z22dhvizszfa21yff08a8fr0igya";
  release."8.14.0".sha256 = "sha256:1k6pqhv4dwpkwg81f2rlfg40wh070ks1gy9r0ravm2zhsbxqcfc9";
  release."8.13+no".sha256 = "sha256-gXoxtLcHPoyjJkt7WqvzfCMCQlh6kL2KtCGe3N6RC/A=";
  inherit version;
  defaultVersion = with versions; switch coq.coq-version [
    { case = isEq "8.16"; out = "8.16.0"; }
    { case = isEq "8.15"; out = "8.15.0"; }
    { case = isEq "8.14"; out = "8.14.0"; }
    { case = isEq "8.13"; out = "8.13+no"; }
  ] null;

  mlPlugin = true;
  nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
  enableParallelBuilding = false;

  meta = {
    description = "A reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support";
    maintainers = with maintainers; [ siraben ];
    license = licenses.gpl3Plus;
  };
}