mirror of
https://github.com/NixOS/nixpkgs.git
synced 2024-11-25 00:12:56 +00:00
coqPackages.json: init at 0.1.3
This commit is contained in:
parent
695b7ae933
commit
03bfa3c1a4
@ -14,14 +14,8 @@ let
|
||||
defaultVersion =
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
{
|
||||
case = range "8.12" "8.20";
|
||||
out = "20240715";
|
||||
}
|
||||
{
|
||||
case = range "8.7" "8.11";
|
||||
out = "20200624";
|
||||
}
|
||||
{ case = range "8.12" "8.20"; out = "20240715"; }
|
||||
{ case = range "8.7" "8.11"; out = "20200624"; }
|
||||
] null;
|
||||
release = {
|
||||
"20240715".sha256 = "sha256-9CSxAIm0aEXkwF+aj8u/bqLG30y5eDNz65EnohJPjzI="; # coq 8.9 - 8.20
|
||||
|
26
pkgs/development/coq-modules/json/default.nix
Normal file
26
pkgs/development/coq-modules/json/default.nix
Normal file
@ -0,0 +1,26 @@
|
||||
{ lib, mkCoqDerivation, coq, parsec, MenhirLib, version ? null }:
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "json";
|
||||
owner = "liyishuai";
|
||||
repo = "coq-json";
|
||||
inherit version;
|
||||
|
||||
defaultVersion = let inherit (lib.versions) range; in
|
||||
lib.switch coq.coq-version [
|
||||
{ case = range "8.14" "8.20"; out = "0.1.3"; }
|
||||
] null;
|
||||
release = {
|
||||
"0.1.3".sha256 = "sha256-lElAzW4IuX+BB6ngDjlyKn0MytLRfbhQanB+Lct/WR0=";
|
||||
};
|
||||
releaseRev = v: "v${v}";
|
||||
|
||||
propagatedBuildInputs = [ parsec MenhirLib coq.ocamlPackages.menhir ];
|
||||
|
||||
buildFlags = [ "MENHIRFLAGS=--coq" "MENHIRFLAGS+=--coq-no-version-check" ];
|
||||
|
||||
meta = {
|
||||
description = "From JSON to Coq, and vice versa.";
|
||||
license = lib.licenses.bsd3;
|
||||
};
|
||||
}
|
@ -80,6 +80,7 @@ let
|
||||
itauto = callPackage ../development/coq-modules/itauto { };
|
||||
ITree = callPackage ../development/coq-modules/ITree { };
|
||||
itree-io = callPackage ../development/coq-modules/itree-io { };
|
||||
json = callPackage ../development/coq-modules/json {};
|
||||
LibHyps = callPackage ../development/coq-modules/LibHyps {};
|
||||
ltac2 = callPackage ../development/coq-modules/ltac2 {};
|
||||
math-classes = callPackage ../development/coq-modules/math-classes { };
|
||||
|
Loading…
Reference in New Issue
Block a user