tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 stdlib,
6 version ? null,
7}:
8
9let
10 repo = "stalmarck";
11 defaultVersion =
12 let
13 case = case: out: { inherit case out; };
14 in
15 with lib.versions;
16 lib.switch coq.coq-version [
17 (case (isEq "8.20") "8.20.0")
18 ] null;
19 release = {
20 "8.20.0".sha256 = "sha256-jITxQT1jLyZvWCGPnmK8i3IrwsZwMPOV0aBe9r22TIQ=";
21 };
22 releaseRev = v: "v${v}";
23
24 packages = [
25 "stalmarck"
26 "stalmarck-tactic"
27 ];
28
29 stalmarck_ =
30 package:
31 let
32 pname = package;
33 istac = package == "stalmarck-tactic";
34 propagatedBuildInputs = if istac then [ (stalmarck_ "stalmarck") ] else [ stdlib ];
35 description =
36 if istac then
37 "Coq tactic and verified tool for proving tautologies using Stålmarck's algorithm"
38 else
39 "A two-level approach to prove tautologies using Stålmarck's algorithm in Coq.";
40 in
41 mkCoqDerivation {
42 inherit
43 version
44 pname
45 defaultVersion
46 release
47 releaseRev
48 repo
49 propagatedBuildInputs
50 ;
51
52 mlPlugin = istac;
53 useDune = istac;
54
55 meta = {
56 inherit description;
57 license = lib.licenses.lgpl21Plus;
58 };
59
60 passthru = lib.genAttrs packages stalmarck_;
61 };
62in
63stalmarck_ "stalmarck-tactic"