diff options
Diffstat (limited to 'infra/libkookie/nixpkgs/pkgs/development/coq-modules')
41 files changed, 3615 insertions, 0 deletions
diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/Cheerios/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/Cheerios/default.nix new file mode 100644 index 000000000000..3f9f3b1ac9cd --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/Cheerios/default.nix @@ -0,0 +1,32 @@ +{ stdenv, fetchFromGitHub, coq, StructTact }: + +let param = + { + version = "20200201"; + rev = "9c7f66e57b91f706d70afa8ed99d64ed98ab367d"; + sha256 = "1h55s6lk47bk0lv5ralh81z55h799jbl9mhizmqwqzy57y8wqgs1"; + }; +in + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-Cheerios-${param.version}"; + + src = fetchFromGitHub { + owner = "uwplse"; + repo = "cheerios"; + inherit (param) rev sha256; + }; + + buildInputs = [ coq ]; + + propagatedBuildInputs = [ StructTact ]; + enableParallelBuilding = true; + + preConfigure = "patchShebangs ./configure"; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/CoLoR/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/CoLoR/default.nix new file mode 100644 index 000000000000..1d3e5a07b03d --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/CoLoR/default.nix @@ -0,0 +1,58 @@ +{ stdenv, fetchFromGitHub, coq, bignums }: + +let + coqVersions = { + "8.6" = "1.4.0"; + "8.7" = "1.4.0"; + "8.8" = "1.6.0"; + "8.9" = "1.6.0"; + "8.10" = "1.7.0"; + "8.11" = "1.7.0"; + }; + params = { + "1.4.0" = { + version = "1.4.0"; + rev = "168c6b86c7d3f87ee51791f795a8828b1521589a"; + sha256 = "1d2whsgs3kcg5wgampd6yaqagcpmzhgb6a0hp6qn4lbimck5dfmm"; + }; + "1.6.0" = { + version = "1.6.0"; + rev = "328aa06270584b578edc0d2925e773cced4f14c8"; + sha256 = "07sy9kw1qlynsqy251adgi8b3hghrc9xxl2rid6c82mxfsp329sd"; + }; + "1.7.0" = { + version = "1.7.0"; + rev = "08b5481ed6ea1a5d2c4c068b62156f5be6d82b40"; + sha256 = "1w7fmcpf0691gcwq00lm788k4ijlwz3667zj40j5jjc8j8hj7cq3"; + }; + }; + param = params.${coqVersions.${coq.coq-version}}; +in + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-CoLoR-${param.version}"; + + src = fetchFromGitHub { + owner = "fblanqui"; + repo = "color"; + inherit (param) rev sha256; + }; + + buildInputs = [ coq bignums ]; + enableParallelBuilding = false; + + installPhase = '' + make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install + ''; + + meta = with stdenv.lib; { + homepage = "http://color.inria.fr/"; + description = "CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory and termination whose correctness has been mechanically checked by the Coq proof assistant."; + maintainers = with maintainers; [ jpas jwiegley ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.hasAttr v coqVersions; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/HoTT/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/HoTT/default.nix new file mode 100644 index 000000000000..7b52838505e2 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/HoTT/default.nix @@ -0,0 +1,61 @@ +{ stdenv, fetchFromGitHub, autoconf, automake, coq }: + +stdenv.mkDerivation rec { + name = "coq${coq.coq-version}-HoTT-${version}"; + version = "20170921"; + + src = fetchFromGitHub { + owner = "HoTT"; + repo = "HoTT"; + rev = "e3557740a699167e6adb1a65855509d55a392fa1"; + sha256 = "0zwfp8g62b50vmmbb2kmskj3v6w7qx1pbf43yw0hr7asdz2zbx5v"; + }; + + buildInputs = [ autoconf automake coq ]; + enableParallelBuilding = true; + + preConfigure = '' + patchShebangs ./autogen.sh + ./autogen.sh + + mkdir -p "$out/bin" + ''; + + configureFlags = [ + "--bindir=$(out)/bin" + ]; + + patchPhase = '' + patchShebangs etc + patchShebangs hoqc hoqchk hoqdep hoqide hoqtop + ''; + + postBuild = '' + patchShebangs hoq-config + ''; + + # Currently, all the scripts like hoqc and hoqtop assume that the *.vo files are + # either (1) in the same directory as the scripts, or (2) in /usr/share/hott. + # We fulfill (1), which means that these files are only accessible via hoqtop, + # hoqc, etc and not via coqtop, coqc, etc. + postInstall = '' + mv $out/share/hott/* "$out/bin" + rmdir $out/share/hott + rmdir $out/share + ''; + + installFlags = [ + "COQBIN=${coq}/bin" + ]; + + meta = with stdenv.lib; { + homepage = "http://homotopytypetheory.org/"; + description = "Homotopy type theory"; + maintainers = with maintainers; [ siddharthist ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: v == "8.6"; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/InfSeqExt/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/InfSeqExt/default.nix new file mode 100644 index 000000000000..387e41859039 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/InfSeqExt/default.nix @@ -0,0 +1,31 @@ +{ stdenv, fetchFromGitHub, coq }: + +let param = + { + version = "20200131"; + rev = "203d4c20211d6b17741f1fdca46dbc091f5e961a"; + sha256 = "0xylkdmb2dqnnqinf3pigz4mf4zmczcbpjnn59g5g76m7f2cqxl0"; + }; +in + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-InfSeqExt-${param.version}"; + + src = fetchFromGitHub { + owner = "DistributedComponents"; + repo = "InfSeqExt"; + inherit (param) rev sha256; + }; + + buildInputs = [ coq ]; + + enableParallelBuilding = true; + + preConfigure = "patchShebangs ./configure"; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/QuickChick/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/QuickChick/default.nix new file mode 100644 index 000000000000..a167b7988dcd --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/QuickChick/default.nix @@ -0,0 +1,96 @@ +{ stdenv, fetchFromGitHub, coq, ssreflect, coq-ext-lib, simple-io }: + +let params = + { + "8.5" = { + version = "20170512"; + rev = "31eb050ae5ce57ab402db9726fb7cd945a0b4d03"; + sha256 = "033ch10i5wmqyw8j6wnr0dlbnibgfpr1vr0c07q3yj6h23xkmqpg"; + }; + + "8.6" = { + version = "20171102"; + rev = "0fdb769e1dc87a278383b44a9f5102cc7ccbafcf"; + sha256 = "0fri4nih40vfb0fbr82dsi631ydkw48xszinq43lyinpknf54y17"; + }; + + "8.8" = { + version = "20190311"; + rev = "22af9e9a223d0038f05638654422e637e863b355"; + sha256 = "00rnr19lg6lg0haq1sy4ld38p7imzand6fc52fvfq27gblxkp2aq"; + }; + + "8.9" = rec { + version = "1.1.0"; + rev = "v${version}"; + sha256 = "1c34v1k37rk7v0xk2czv5n79mbjxjrm6nh3llg2mpfmdsqi68wf3"; + }; + + "8.10" = rec { + version = "1.2.1"; + rev = "v${version}"; + sha256 = "17vz88xjzxh3q7hs6hnndw61r3hdfawxp5awqpgfaxx4w6ni8z46"; + }; + + "8.11" = rec { + version = "1.3.2"; + rev = "v${version}"; + sha256 = "0lciwaqv288dh2f13xk2x0lrn6zyrkqy6g4yy927wwzag2gklfrs"; + }; + + "8.12" = rec { + version = "1.4.0"; + rev = "v${version}"; + sha256 = "068p48pm5yxjc3yv8qwzp25bp9kddvxj81l31mjkyx3sdrsw3kyc"; + }; + }; + param = params.${coq.coq-version}; +in + +let inherit (stdenv.lib) maintainers optional optionals versionAtLeast; in + +let recent = versionAtLeast coq.coq-version "8.8"; in + +stdenv.mkDerivation { + + name = "coq${coq.coq-version}-QuickChick-${param.version}"; + + src = fetchFromGitHub { + owner = "QuickChick"; + repo = "QuickChick"; + inherit (param) rev sha256; + }; + + preConfigure = stdenv.lib.optionalString recent + "substituteInPlace Makefile --replace quickChickTool.byte quickChickTool.native"; + + buildInputs = [ coq ] + ++ (with coq.ocamlPackages; [ ocaml findlib ]) + ++ optionals (recent && !versionAtLeast coq.coq-version "8.10") + (with coq.ocamlPackages; [ camlp5 ocamlbuild ]) + ++ optional recent coq.ocamlPackages.num + ; + propagatedBuildInputs = [ ssreflect ] + ++ optionals recent [ coq-ext-lib simple-io ] + ++ optional (versionAtLeast coq.coq-version "8.10") + coq.ocamlPackages.ocamlbuild + ; + + enableParallelBuilding = false; + + installPhase = '' + make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install + ''; + + meta = { + homepage = "https://github.com/QuickChick/QuickChick"; + description = "Randomized property-based testing plugin for Coq; a clone of Haskell QuickCheck"; + maintainers = with maintainers; [ jwiegley ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.hasAttr v params; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/StructTact/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/StructTact/default.nix new file mode 100644 index 000000000000..798aaabe6773 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/StructTact/default.nix @@ -0,0 +1,31 @@ +{ stdenv, fetchFromGitHub, coq }: + +let param = + { + version = "20181102"; + rev = "82a85b7ec07e71fa6b30cfc05f6a7bfb09ef2510"; + sha256 = "08zry20flgj7qq37xk32kzmg4fg6d4wi9m7pf9aph8fd3j2a0b5v"; + }; +in + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-StructTact-${param.version}"; + + src = fetchFromGitHub { + owner = "uwplse"; + repo = "StructTact"; + inherit (param) rev sha256; + }; + + buildInputs = [ coq ]; + + enableParallelBuilding = true; + + preConfigure = "patchShebangs ./configure"; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + passthru = { + compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.5"; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/VST/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/VST/default.nix new file mode 100644 index 000000000000..a625aa54c148 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/VST/default.nix @@ -0,0 +1,43 @@ +{ stdenv, fetchFromGitHub, coq, compcert }: + +stdenv.mkDerivation rec { + pname = "coq${coq.coq-version}-VST"; + version = "2.6"; + + src = fetchFromGitHub { + owner = "PrincetonUniversity"; + repo = "VST"; + rev = "v${version}"; + sha256 = "00bf9hl4pvmsqa08lzjs1mrxyfgfxq4k6778pnldmc8ichm90jgk"; + }; + + buildInputs = [ coq ]; + propagatedBuildInputs = [ compcert ]; + + preConfigure = "patchShebangs util"; + + makeFlags = [ + "BITSIZE=64" + "COMPCERT=inst_dir" + "COMPCERT_INST_DIR=${compcert.lib}/lib/coq/${coq.coq-version}/user-contrib/compcert" + "INSTALLDIR=$(out)/lib/coq/${coq.coq-version}/user-contrib/VST" + ]; + + postInstall = '' + for d in msl veric floyd sepcomp progs64 + do + cp -r $d $out/lib/coq/${coq.coq-version}/user-contrib/VST/ + done + ''; + + enableParallelBuilding = true; + + passthru.compatibleCoqVersions = stdenv.lib.flip builtins.elem [ "8.11" ]; + + meta = { + description = "Verified Software Toolchain"; + homepage = "https://vst.cs.princeton.edu/"; + inherit (compcert.meta) platforms; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/Velisarios/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/Velisarios/default.nix new file mode 100644 index 000000000000..92c9b2569ca4 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/Velisarios/default.nix @@ -0,0 +1,50 @@ +{ stdenv, fetchFromGitHub, coq }: + +let params = + { + "8.6" = { + version = "20180221"; + rev = "e1eee1f10d5d46331a560bd8565ac101229d0d6b"; + sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2"; + }; + + "8.7" = { + version = "20180221"; + rev = "e1eee1f10d5d46331a560bd8565ac101229d0d6b"; + sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2"; + }; + + "8.8" = { + version = "20180221"; + rev = "e1eee1f10d5d46331a560bd8565ac101229d0d6b"; + sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2"; + }; + }; + param = params.${coq.coq-version}; +in + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-Velisarios-${param.version}"; + + src = fetchFromGitHub { + owner = "vrahli"; + repo = "Velisarios"; + inherit (param) rev sha256; + }; + + buildInputs = [ + coq coq.ocaml coq.camlp5 coq.findlib + ]; + enableParallelBuilding = true; + + buildPhase = "make -j$NIX_BUILD_CORES"; + preBuild = "./create-makefile.sh"; + installPhase = '' + mkdir -p $out/lib/coq/${coq.coq-version}/Velisarios + cp -pR model/*.vo $out/lib/coq/${coq.coq-version}/Velisarios + ''; + + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/Verdi/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/Verdi/default.nix new file mode 100644 index 000000000000..927cd832452b --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/Verdi/default.nix @@ -0,0 +1,37 @@ +{ stdenv, fetchFromGitHub, coq, Cheerios, InfSeqExt, ssreflect }: + +let param = + if stdenv.lib.versionAtLeast coq.coq-version "8.7" then + { + version = "20200131"; + rev = "fdb4ede19d2150c254f0ebcfbed4fb9547a734b0"; + sha256 = "1a2k19f9q5k5djbxplqmmpwck49kw3lrm3aax920h4yb40czkd8m"; + } else { + version = "20181102"; + rev = "25b79cf1be5527ab8dc1b8314fcee93e76a2e564"; + sha256 = "1vw47c37k5vaa8vbr6ryqy8riagngwcrfmb3rai37yi9xhdqg55z"; + }; +in + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-verdi-${param.version}"; + + src = fetchFromGitHub { + owner = "uwplse"; + repo = "verdi"; + inherit (param) rev sha256; + }; + + buildInputs = [ coq ]; + propagatedBuildInputs = [ Cheerios InfSeqExt ssreflect ]; + + enableParallelBuilding = true; + + preConfigure = "patchShebangs ./configure"; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch new file mode 100644 index 000000000000..dde0e2e03eb6 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch @@ -0,0 +1,134 @@ +From 5b40a32e35fe446cda20ed34c756a010856f39ce Mon Sep 17 00:00:00 2001 +From: Theo Giannakopoulos <theo.giannakopoulos@baesystems.com> +Date: Wed, 5 Apr 2017 15:48:55 -0400 +Subject: [PATCH] changes to work with Coq 8.6 + +--- + theories/Autosubst_Derive.v | 12 ++++++++++++ + theories/Autosubst_MMap.v | 3 ++- + 2 files changed, 14 insertions(+), 1 deletion(-) + +diff --git a/theories/Autosubst_Derive.v b/theories/Autosubst_Derive.v +index 61995de..cf87f67 100644 +--- a/theories/Autosubst_Derive.v ++++ b/theories/Autosubst_Derive.v +@@ -18,6 +18,7 @@ Hint Extern 0 (Ids _) => derive_Ids : derive. + + Ltac derive_Rename := + match goal with [ |- Rename ?term ] => ++ let inst := fresh "inst" in + hnf; fix inst 2; change _ with (Rename term) in inst; + intros xi s; change (annot term s); destruct s; + match goal with +@@ -66,6 +67,7 @@ Ltac has_var s := + Ltac derive_Subst := + match goal with [ |- Subst ?term ] => + require_instance (Rename term); ++ let inst := fresh "inst" in + hnf; fix inst 2; change _ with (Subst term) in inst; + intros sigma s; change (annot term s); destruct s; + match goal with +@@ -107,6 +109,7 @@ Hint Extern 0 (Subst _) => derive_Subst : derive. + Ltac derive_HSubst := + match goal with [ |- HSubst ?inner ?outer ] => + require_instance (Subst inner); ++ let inst := fresh "inst" in + hnf; fix inst 2; change _ with (HSubst inner outer) in inst; + intros sigma s; change (annot outer s); destruct s; + match goal with +@@ -327,6 +330,7 @@ Ltac derive_SubstLemmas := + assert (up_upren_n : + forall xi n, upn n (ren xi) = ren (iterate upren n xi)) by + (apply up_upren_n_internal, up_upren); ++ let ih := fresh "ih" in + fix ih 2; intros xi s; destruct s; try reflexivity; simpl; f_equal; + try apply mmap_ext; intros; rewrite ?up_upren, ?up_upren_n; apply ih); + +@@ -337,6 +341,7 @@ Ltac derive_SubstLemmas := + (apply up_id_internal; reflexivity); + assert (up_id_n : forall n, upn n ids = ids) by + (apply up_id_n_internal, up_id); ++ let ih := fresh "ih" in + fix ih 1; intros s; destruct s; simpl; f_equal; try reflexivity; + rewrite ?up_id, ?up_id_n; try apply mmap_id_ext; intros; apply ih); + +@@ -344,6 +349,7 @@ Ltac derive_SubstLemmas := + + assert (ren_subst_comp : + forall xi sigma (s : term), (rename xi s).[sigma] = s.[xi >>> sigma]) by( ++ let ih := fresh "ih" in + fix ih 3; intros xi sigma s; destruct s; try reflexivity; simpl; f_equal; + rewrite ?up_comp_ren_subst, ?up_comp_ren_subst_n, ?mmap_comp; + try apply mmap_ext; intros; apply ih); +@@ -357,6 +363,7 @@ Ltac derive_SubstLemmas := + assert (up_comp_subst_ren_n : + forall sigma xi n, upn n (sigma >>> rename xi) = upn n sigma >>> rename (iterate upren n xi)) + by (apply up_comp_subst_ren_n_internal; apply up_comp_subst_ren); ++ let ih := fresh "ih" in + fix ih 3; intros sigma xi s; destruct s; try reflexivity; simpl; + f_equal; rewrite ?up_comp_subst_ren, ?up_comp_subst_ren_n, ?mmap_comp; + try (rewrite hcomp_ren_internal; [|apply rename_subst]); +@@ -368,6 +375,7 @@ Ltac derive_SubstLemmas := + by (apply up_comp_internal; [reflexivity|apply ren_subst_comp|apply subst_ren_comp]); + assert (up_comp_n : forall sigma tau n, upn n (sigma >> tau) = upn n sigma >> upn n tau) + by (apply up_comp_n_internal; apply up_comp); ++ let ih := fresh "ih" in + fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal; + rewrite ?up_comp, ?up_comp_n, ?mmap_comp, ?hcomp_dist_internal; + try apply mmap_ext; intros; apply ih); +@@ -382,6 +390,7 @@ Ltac derive_HSubstLemmas := + let ids := constr:(ids : var -> inner) in + + assert (hsubst_id : forall (s : outer), s.|[ids] = s) by ( ++ let ih := fresh "ih" in + fix ih 1; intros s; destruct s; try reflexivity; simpl; f_equal; + rewrite ?up_id, ?up_id_n; try apply mmap_id_ext; intros; + (apply subst_id || apply ih) +@@ -390,6 +399,7 @@ Ltac derive_HSubstLemmas := + assert (hsubst_comp : forall (theta eta : var -> inner) (s : outer), + s.|[theta].|[eta] = s.|[theta >> eta]) + by ( ++ let ih := fresh "ih" in + fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal; + rewrite <- ?up_comp, <- ?up_comp_n, ?mmap_comp; try apply mmap_ext; intros; + (apply subst_comp || apply ih) +@@ -405,6 +415,7 @@ Ltac derive_SubstHSubstComp := + assert (ren_hsubst_comp : forall xi (theta : var -> inner) (s : outer), + rename xi s.|[theta] = (rename xi s).|[theta] + ) by ( ++ let ih := fresh "ih" in + fix ih 3; intros xi theta s; destruct s; try reflexivity; simpl; f_equal; + rewrite ?mmap_comp; try apply mmap_ext; intros; simpl; apply ih + ); +@@ -421,6 +432,7 @@ Ltac derive_SubstHSubstComp := + apply up_hcomp_n_internal; apply up_hcomp + ); + ++ let ih := fresh "ih" in + fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal; + rewrite ?up_hcomp, ?up_hcomp_n, ?hcomp_lift_n_internal, ?mmap_comp; + try apply mmap_ext; intros; apply ih +diff --git a/theories/Autosubst_MMap.v b/theories/Autosubst_MMap.v +index f8387e7..7af7902 100644 +--- a/theories/Autosubst_MMap.v ++++ b/theories/Autosubst_MMap.v +@@ -23,7 +23,7 @@ Arguments mmap {A B _} f !s /. + Class MMapExt (A B : Type) `{MMap A B} := + mmap_ext : forall f g, + (forall t, f t = g t) -> forall s, mmap f s = mmap g s. +-Arguments mmap_ext {A B _ _ f g} H s. ++Arguments mmap_ext {A B H' _ f g} H s : rename. + + Class MMapLemmas (A B : Type) `{MMap A B} := { + mmap_id x : mmap id x = x; +@@ -123,6 +123,7 @@ Tactic Notation "msimpl" "in" "*" := (in_all msimplH); msimpl. + + Ltac derive_MMap := + hnf; match goal with [ |- (?A -> ?A) -> ?B -> ?B ] => ++ let map := fresh "map" in + intros f; fix map 1; intros xs; change (annot B xs); destruct xs; + match goal with + | [ |- annot _ ?ys ] => +-- +2.13.2 + diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/autosubst/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/autosubst/default.nix new file mode 100644 index 000000000000..9507dc6751ae --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/autosubst/default.nix @@ -0,0 +1,33 @@ +{ stdenv, fetchgit, coq, mathcomp }: + +stdenv.mkDerivation rec { + + name = "coq-autosubst-${coq.coq-version}-${version}"; + version = "5b40a32e"; + + src = fetchgit { + url = "git://github.com/uds-psl/autosubst.git"; + rev = "1c3bb3bbf5477e3b33533a0fc090399f45fe3034"; + sha256 = "06pcjbngzwqyncvfwzz88j33wvdj9kizxyg5adp7y6186h8an341"; + }; + + buildInputs = [ coq ]; + propagatedBuildInputs = [ mathcomp ]; + + patches = [./0001-changes-to-work-with-Coq-8.6.patch]; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + meta = with stdenv.lib; { + homepage = "https://www.ps.uni-saarland.de/autosubst/"; + description = "Automation for de Bruijn syntax and substitution in Coq"; + maintainers = with maintainers; [ jwiegley ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ]; + }; + + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/bignums/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/bignums/default.nix new file mode 100644 index 000000000000..7246382c9aed --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/bignums/default.nix @@ -0,0 +1,60 @@ +{ stdenv, fetchFromGitHub, coq }: + +let params = { + "8.6" = { + rev = "v8.6.0"; + sha256 = "0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj"; + }; + "8.7" = { + rev = "V8.7.0"; + sha256 = "11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl"; + }; + "8.8" = { + rev = "V8.8.0"; + sha256 = "1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg"; + }; + "8.9" = { + rev = "V8.9.0"; + sha256 = "03qz1w2xb2j5p06liz5yyafl0fl9vprcqm6j0iwi7rxwghl00p01"; + }; + "8.10" = { + rev = "V8.10.0"; + sha256 = "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5"; + }; + "8.11" = { + rev = "V8.11.0"; + sha256 = "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp"; + }; + "8.12" = { + rev = "V8.12.0"; + sha256 = "14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8"; + }; + }; + param = params.${coq.coq-version}; +in + +stdenv.mkDerivation { + + name = "coq${coq.coq-version}-bignums"; + + src = fetchFromGitHub { + owner = "coq"; + repo = "bignums"; + inherit (param) rev sha256; + }; + + buildInputs = with coq.ocamlPackages; [ ocaml findlib coq ] + ++ stdenv.lib.optional (!stdenv.lib.versionAtLeast coq.coq-version "8.10") camlp5 + ; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + meta = with stdenv.lib; { + license = licenses.lgpl2; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.hasAttr v params; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/category-theory/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/category-theory/default.nix new file mode 100644 index 000000000000..1178b1558ff7 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/category-theory/default.nix @@ -0,0 +1,54 @@ +{ stdenv, fetchgit, coq, ssreflect, equations }: + +let + params = + let + v20180709 = { + version = "20180709"; + rev = "3b9ba7b26a64d49a55e8b6ccea570a7f32c11ead"; + sha256 = "0f2nr8dgn1ab7hr7jrdmr1zla9g9h8216q4yf4wnff9qkln8sbbs"; + }; + v20190414 = { + version = "20190414"; + rev = "706fdb4065cc2302d92ac2bce62cb59713253119"; + sha256 = "16lg4xs2wzbdbsn148xiacgl4wq4xwfqjnjkdhfr3w0qh1s81hay"; + }; + in { + "8.6" = v20180709; + "8.7" = v20180709; + "8.8" = v20190414; + "8.9" = v20190414; + }; + param = params.${coq.coq-version}; +in + +stdenv.mkDerivation { + + name = "coq${coq.coq-version}-category-theory-${param.version}"; + + src = fetchgit { + url = "git://github.com/jwiegley/category-theory.git"; + inherit (param) rev sha256; + }; + + buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml camlp5 findlib ]); + propagatedBuildInputs = [ ssreflect equations ]; + + buildFlags = [ "JOBS=$(NIX_BUILD_CORES)" ]; + + installPhase = '' + make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install + ''; + + meta = with stdenv.lib; { + homepage = "https://github.com/jwiegley/category-theory"; + description = "A formalization of category theory in Coq for personal study and practical work"; + maintainers = with maintainers; [ jwiegley ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.hasAttr v params; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/contribs/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/contribs/default.nix new file mode 100644 index 000000000000..d2787f0948e0 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/contribs/default.nix @@ -0,0 +1,1045 @@ +{ stdenv, fetchFromGitHub, coq }: + +let mkContrib = repo: revs: param: + stdenv.mkDerivation rec { + name = "coq${coq.coq-version}-${repo}-${version}"; + version = param.version; + + src = fetchFromGitHub { + owner = "coq-contribs"; + repo = repo; + rev = param.rev; + sha256 = param.sha256; + }; + + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ]; + + installFlags = + stdenv.lib.optional (stdenv.lib.versionAtLeast coq.coq-version "8.9") "-f Makefile.coq" + ++ [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + passthru = { + compatibleCoqVersions = v: builtins.elem v revs; + }; + }; in +{ + aac-tactics = mkContrib "aac-tactics" [ "8.7" "8.8" ] { + "8.7" = { + version = "20180530"; + rev = "f01df35e1d796ce1fdc7ba3d670ce5d63c95d544"; + sha256 = "1bwvnbd5ws1plgj147blcrvyycf3gg3fz3rm2mckln8z3sfxyq2k"; + }; + "8.8" = { + version = "20180530"; + rev = "86ac28259030649ef51460e4de2441c8a1017751"; + sha256 = "09bbk2a7pn0j76mmapl583f8a20zqd3a1m9lkml8rpwml692bzi9"; + }; + }.${coq.coq-version}; + + abp = mkContrib "abp" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "492d919510ededf685e57f3b911b1ac43f2d9333"; + sha256 = "18f5vbq6nx9gz2gcj5p7v2gmjczpspc5dmlj6by4jqv07iirzsz2"; + }; + + additions = mkContrib "additions" [ "8.6" ] { + version = "v8.5.0-9-gbec504e"; + rev = "bec504e7822747376159aaa2156cf7453dbbd2b4"; + sha256 = "1vvkqjnqrf6m726krhlm2viza64ha2081xgc5wb9y5sygd0baaz7"; + }; + + ails = mkContrib "ails" [ "8.7" ] { + version = "v8.6.0-1-g1f7e52c"; + rev = "1f7e52cbfe12584787a91bcc641bcaa823e773e3"; + sha256 = "0j7sjkjqdxsr3mkihh41s6bgdy8gj0hw09gijzw2nrjmj6g3s9nk"; + }; + + algebra = mkContrib "algebra" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-5-gcd1d291"; + rev = "cd1d29115197c9c51d56e0a2e19fce2d0227c567"; + sha256 = "01i8189n94swvwyfnrizh01ym5ijfyb6vbzl052awvhxv8a54j3q"; + }; + + amm11262 = mkContrib "amm11262" [ "8.5" "8.6" ] { + version = "v8.5.0-5-gbfa5cdf"; + rev = "bfa5cdf3bd803c40e918ae3a78aeb9c2929432a0"; + sha256 = "1zkbviarvqm228x9rnviad3b0sabpcgarx4z1cks9mfvg1wwyk8n"; + }; + + angles = mkContrib "angles" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-5-g78715f8"; + rev = "78715f86971007c9e2803215cccee1c5fc9dee87"; + sha256 = "0bgczag5qvmh92wxll0grzcyj52p80z6arx0plbrn6h7m1gywka5"; + }; + + area-method = mkContrib "area-method" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0-1-gc599734"; + rev = "c599734c0ca9bfcdae7ca436be4a17fda5d55c18"; + sha256 = "111jgxngmpb8sddpmrgr4cgh3p0w3w9jg6pq0x2qwddsq2x55bbq"; + }; + + atbr = mkContrib "atbr" [ ] { + version = "v8.5.0-16-g71ca792"; + rev = "71ca792293153f66a3734c367c23f9dd9ad4bd0f"; + sha256 = "0r01crlf2hclq9wrsrx1by1c3qbncs6rkyn6v4amirdjwlrla4ba"; + }; + + automata = mkContrib "automata" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-gc3dffb9"; + rev = "c3dffb957dea45ffde679c0d360e869e40396c6c"; + sha256 = "174psnrmjwb7ywn8fs67bjjggq5jw9zrg3d9bpsx5n82bzr2vsnk"; + }; + + axiomatic-abp = mkContrib "axiomatic-abp" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-5-ge48eb5e"; + rev = "e48eb5ed467da6aa250b4d567478bc63e675783c"; + sha256 = "0g924s0iiwhck5vvh6zcwj1s16g3p637xms2bld504d0nrjwapkx"; + }; + + bdds = mkContrib "bdds" [ ] { + version = "v8.6.0"; + rev = "f952a2f23d710761cf3d7143d543c7d9ed1331cc"; + sha256 = "0wbbg2yvaks1fd9sdbmkwijh9sz9bkbjl1z49wy68hd1bs4d81j9"; + }; + + bertrand = mkContrib "bertrand" [ "8.7" ] { + version = "v8.5.0-9-g11a85bf"; + rev = "11a85bf3bb43c1c0447c65f320891e69f7ab6c04"; + sha256 = "1bkcglyw3r0g06j695nynfmjl60p9jxm13z8zbzwaghcriw33p12"; + }; + + buchberger = mkContrib "buchberger" [ "8.6" "8.7" ] { + version = "v8.6.0-1-g926229f"; + rev = "926229fb43125f1c3977ffcf474a7e9d350c7124"; + sha256 = "0c5bd99sdk31la58fkkf67p00gjj5fwi3rhap5bj9rjadmxgdwqr"; + }; + + canon-bdds = mkContrib "canon-bdds" [ "8.6" "8.7" ] { + version = "v8.5.0-6-g1420af9"; + rev = "1420af91ba2f898b70404a6600c2b87881338a0e"; + sha256 = "0g73z6biv3kn8fr3xsc1qlnflfaa8ljbcrmglg6mdacamphjji42"; + }; + + cantor = mkContrib "cantor" [ "8.5" "8.6" ] { + version = "v8.5.0-5-gdbcaa1d"; + rev = "dbcaa1de1eca2bd636e92cb5f78eedc237bb3f7a"; + sha256 = "1wy75wv9w5ny2m359rdymvqc0v5ygi9kbljmiknjpd2m1rm24mc0"; + }; + + cats-in-zfc = mkContrib "cats-in-zfc" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-9-g2945072"; + rev = "2945072aa6c9c328a019d3128c0a725dabca434c"; + sha256 = "177n0hv3jndwlzhxpfrpiv6ad7254iy7yscrrjjlya4kkfdlvnhh"; + }; + + ccs = mkContrib "ccs" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g7ec1e98"; + rev = "7ec1e98797f8644dc93a0492a901bd2e0cf7332b"; + sha256 = "1fs3cmbdnmvbaz0ash585brqsvn7fky9vgc5qpahdbj541vrqzd6"; + }; + + cfgv = mkContrib "cfgv" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "d9f4d58ddf571639217f0ba1706e1141921a693a"; + sha256 = "0gsr498sx3zvspz731q5c9bgv9b9mw9khz3j9ijkbq34gz08n1cb"; + }; + + checker = mkContrib "checker" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "f8da516722ccf49bc910089e12072c09b926fe50"; + sha256 = "05gwasqj05hz3d34a68ir1mk0mq5swclzy4ijdwnysrzdp5nlw28"; + }; + + chinese = mkContrib "chinese" [ "8.6" "8.7" ] { + version = "v8.5.0-8-ga30ad2e"; + rev = "a30ad2eb63d5d93c82e2a76b8dd836713637b869"; + sha256 = "0mccfdcgw72rl5mhk3m6s0i8rjym517gczijj7m0nhrask14zg89"; + }; + + circuits = mkContrib "circuits" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-gf2cec60"; + rev = "f2cec6067f2c58e280c5b460e113d738b387be15"; + sha256 = "05w6dmm4qch327zs4726jiirfyprs21mgwxdc9nlvwnpakpimfcf"; + }; + + classical-realizability = mkContrib "classical-realizability" [ "8.6" ] { + version = "v8.6.0"; + rev = "b7b915583675b85feadd6fbf52cc453211de8e87"; + sha256 = "099fwqjd1621bwy237wv1nln3kcr4mq09wl25z1620r2b467sglh"; + }; + + coalgebras = mkContrib "coalgebras" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-9-g6544eae"; + rev = "6544eaee5de06d2f520a958d52afedcb83a53735"; + sha256 = "0b15r2ln57mxsyz4fmpfzh4mzrwi604gqh8f471awm63a4xqj5ng"; + }; + + coinductive-examples = mkContrib "coinductive-examples" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "28b0e273c38fdecd1966e3ca5717ccd1f5871a15"; + sha256 = "11dazllhl7qwhbnxqxpgwy0pf2a8c2aijrs93fzj5inf8z48vxnp"; + }; + + coinductive-reals = mkContrib "coinductive-reals" [ ] { + version = "v8.6.0-9-gf89f884"; + rev = "f89f8848f74294afaa5c0e0e211f6e8e8d1fb36a"; + sha256 = "0svpxflynara7v6vzrvibhyfk9kb5kzdxfzrsvbqyk192dsfkwf7"; + }; + + concat = mkContrib "concat" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-gb4a9619"; + rev = "b4a96199f0bc447be8fcaa494bcba8d713fd1801"; + sha256 = "1haw5i5rz420jsr2mw699ny3f0gfmdsy0i6mzi48dhpj12ni8rfq"; + }; + + constructive-geometry = mkContrib "constructive-geometry" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-7-g470ffa3"; + rev = "470ffa3d38eb7f78974693e52d190535e87004c4"; + sha256 = "1ddwzg12pbzpnz3njin4zhpph92kscrbsn3bzds26yj8fp76zc33"; + }; + + containers = mkContrib "containers" [ "8.6" "8.7" "8.8" "8.9" ] { + "8.6" = { + version = "8.6.0"; + rev = "fa1fec7"; + sha256 = "1ns0swlr8hzb1zc7fsyd3vws1vbq0vvfxcf0lszqnca9c9hfkfy4"; + }; + "8.7" = { + version = "20180313"; + rev = "77ac16366529c9e558f70ba86f0168a76ca76b8f"; + sha256 = "01gp8injb0knaxgqsdc4x9h8714k7qxg7j5w7y6i45dnpd81ndr4"; + }; + "8.8" = { + version = "20180330"; + rev = "52b86bed1671321b25fe4d7495558f9f221b12aa"; + sha256 = "0hbnrwdgryr52170cfrlbiymr88jsyxilnpr343vnprqq3zk1xz0"; + }; + "8.9" = { + version = "20190222"; + rev = "aa33052c1edfc5a65885942a67c2773b5d96f8cc"; + sha256 = "0mjgfdr9bzsch0dlk4vq1frkaig14dqh46r54cv0l15flxapg0iw"; + }; + }.${coq.coq-version}; + + continuations = mkContrib "continuations" [ ] { + version = "v8.5.0-13-g6885310"; + rev = "68853104fd7390ba384cd2c63101b0bc4ec50a22"; + sha256 = "1v2lqcj93xlwn9750xga6knyld4xcxma2brh58zmiggkc7wn1dpl"; + }; + + coq-in-coq = mkContrib "coq-in-coq" [ "8.6" "8.7" ] { + version = "v8.5.0-9-g8d137fc"; + rev = "8d137fc20460561e6fd324466ebb04fd5a86150a"; + sha256 = "0p9rb963ri5c8y1dlnp9307qnymr285dd6k7hir1qmvghybj1ijm"; + }; + + coqoban = mkContrib "coqoban" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g89758d9"; + rev = "89758d9bf1222155a37171e39ea1d6eec53aabb8"; + sha256 = "02ixil10iw26wkbis62ydnsp2fn4r9jmyh88k2dj7inn0ln30h3q"; + }; + + corn = mkContrib "corn" [ ] { + version = "master"; + rev = "bb962a00c2a737fceb459fac663eecb266289461"; + sha256 = "0xgkbzzsv3lc31lk71zgjvcryn9j51ffij5karln87j2ln989l3q"; + }; + + counting = mkContrib "counting" [ ] { + version = "v8.6.0-2-g2823e75"; + rev = "2823e75408a80a5a8946a11dd0debeb2409942a2"; + sha256 = "0bn8kxyh4hwdn1cvnrlp7g66jagxp8c302hsslz07pfrxkdk1cwy"; + }; + + cours-de-coq = mkContrib "cours-de-coq" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g8ecccd4"; + rev = "8ecccd4196e303b9adbbd95d3531f3d6e3d0299d"; + sha256 = "1v6wh1ppzw6fcb78wvzxyg5hygssjvp56s9qd0yfsagy915vqyl6"; + }; + + ctltctl = mkContrib "ctltctl" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g51b7096"; + rev = "51b7096482ac402d8e0ba2eeb932432a2f2489fc"; + sha256 = "1fmpp69pv8130wqhsknnn37xqpc5alqhr41n2vd4r4kj3dj45bj7"; + }; + + dblib = mkContrib "dblib" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "df86f014dbfb07ec113e8ec4b401b6cc28eb792b"; + sha256 = "0s9y9apainqc4kcldrrkisnw5hnqbz052q2ilb5967b643rac4bb"; + }; + + demos = mkContrib "demos" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-7-g399f693"; + rev = "399f6930fa7a9909b840d4a017159d0e06616940"; + sha256 = "08a99cwqz7f6438bkz0gf5dw7p61s48whccrpsd6rvhqrl4bg7b2"; + }; + + dep-map = mkContrib "dep-map" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0-3-g091bb2d"; + rev = "091bb2d7fc86a816a2dafa249610d3fbc5b546fe"; + sha256 = "1vp1nxxa4m8c8bmvllajrqi0ap13i450c2q5kcxyvac1bfv9hf50"; + }; + + descente-infinie = mkContrib "descente-infinie" [ ] { + version = "v8.5.0-16-g7ad3ff6"; + rev = "7ad3ff63d8772d40b5ef415741cffc93f343856e"; + sha256 = "0gpn6cngjlcfi78qj743w7a33fvq1513avjq9cnzhnsdnqnnwv07"; + }; + + dictionaries = mkContrib "dictionaries" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g545189e"; + rev = "545189ef2f9281135ff870069134bb04bc2e38e5"; + sha256 = "0b0c4vcf5dl7bcgxj1pvdin4jg6py6nr1wqcy3yw8vbd1apnhgri"; + }; + + distributed-reference-counting = mkContrib "distributed-reference-counting" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-7-gfae0b8a"; + rev = "fae0b8a8e26c19f853996fae318e4e9f8f166c0e"; + sha256 = "153xqfkw5cb24z6h4pj6xaqhxbi20bx4zr60mf5aly390sjd4m7x"; + }; + + domain-theory = mkContrib "domain-theory" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g8a121a2"; + rev = "8a121a29ddb80964855ec43abbb21df7fccca37b"; + sha256 = "0jpqjy9wi1kkn90fr1x3bf47m2a3p0byk06wza4psw2f40lz94yb"; + }; + + ergo = mkContrib "ergo" [ ] { + version = "v8.6.0-2-gf82bdee"; + rev = "f82bdee58ee2e0edc7515bfd1792063e9e1aea4c"; + sha256 = "0ngwiwcxbylpjyz19zalbz9h3a447iagz4llq9vqdmbcs6qyml2k"; + }; + + euclidean-geometry = mkContrib "euclidean-geometry" [ "8.6" "8.7" ] { + version = "v8.5.0-6-g280bb19"; + rev = "280bb19b7192275678838fdf4b2045074ec4b3a6"; + sha256 = "05rnpxaa3jbz82j1y1hb1yi5nm1kz46c95nbn1kd4rdm0zn53r9f"; + }; + + euler-formula = mkContrib "euler-formula" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g078d161"; + rev = "078d16102fc0a28f6a96525703ddd272df0e3ba9"; + sha256 = "1wd6hay32ri91sk8pra6rr5vkyyrxfl2rxdhhw4gzyzsv72njmfd"; + }; + + exact-real-arithmetic = mkContrib "exact-real-arithmetic" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0-1-g593028e"; + rev = "593028ec7d094c23ed4dbb3990d6442f7d05950e"; + sha256 = "10x7w57mpiwr4640vfa27pbllkls68nfra9nz7ml0fqhi3s3h6pj"; + }; + + exceptions = mkContrib "exceptions" [ "8.6" "8.7" ] { + version = "v8.5.0-8-gcfe4f0b"; + rev = "cfe4f0bb4f98660fadb9d5a9c8cede9f0e4896e3"; + sha256 = "149j0npyphy60xlgp4ibcwd6qyqminirjac1rwq00882n5gdprw2"; + }; + + fairisle = mkContrib "fairisle" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g3e7c9b0"; + rev = "3e7c9b0c48cf91307bf64f4b01f3c93c412e1ab8"; + sha256 = "1g1jp6w9sip30fs5j5122z4vh7w7wqm6fhswlhpwygi4n5w1l8b7"; + }; + + fermat4 = mkContrib "fermat4" [ "8.7" ] { + version = "v8.5.0-8-g07e3021"; + rev = "07e3021aec1d97f5827eb6ea6281f11108150811"; + sha256 = "1r89cqxy3qmzcj2lfd8hir0hfiikn1f290801rqad7nwx10wfiq6"; + }; + + finger-tree = mkContrib "finger-tree" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g67242c8"; + rev = "67242c896707de73405a596bfd9db2036fba98f3"; + sha256 = "02jcp74i5icv92xkq3mcx91786d56622ghgnjiz3b51wfqs6ldic"; + }; + + firing-squad = mkContrib "firing-squad" [ "8.6" "8.7" ] { + version = "v8.5.0-9-gbe728cd"; + rev = "be728cddbee58088809b51c25425d2a4bdf9b823"; + sha256 = "0i0v5x6lncjasxk22pras3644ff026q8jai45dbimf2fz73312c9"; + }; + + float = mkContrib "float" [ "8.7" ] { + version = "v8.6.0-14-g7699b1e"; + rev = "7699b1e4f492d58e8cfb197692977e705fa6b42b"; + sha256 = "11v2w65xc3806r0pc84vjisp9rwqgmjaz8284q6ky9xd8567yq2z"; + }; + + founify = mkContrib "founify" [ "8.6" "8.7" ] { + version = "v8.5.0-9-gb7c81b8"; + rev = "b7c81b828a444f6a5e4d53020cf319288838399b"; + sha256 = "0prh5vqn0gmvnm4dfb5vqd8n66d9knpx56vqzf5wsiphk5c7a43r"; + }; + + free-groups = mkContrib "free-groups" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "b11ffb1437f1b2793d9d434872e80d5a2d387ade"; + sha256 = "12bkigjv3vkkkc4z6m57aim6g10ifvy53y941i0shfmwnvhlkgpc"; + }; + + fsets = mkContrib "fsets" [ "8.6" "8.7" ] { + version = "v8.5.0-12-g9b51a09"; + rev = "9b51a09e24f4b8b219952f2c06d06405944cd7a0"; + sha256 = "19d2v85mnl29g6alpsbd2cb62xyp7rafryglp046hq9qz520gjzy"; + }; + + fssec-model = mkContrib "fssec-model" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g2fec0b6"; + rev = "2fec0b646ae4d9fcb932901ef85cc13919d5faf3"; + sha256 = "1ib9gw2h9dv5d4n9bqgb64mxz66mgrwy3766ymja0qfc8wflm3yn"; + }; + + functions-in-zfc = mkContrib "functions-in-zfc" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "ff58f7af1b4b79bf164d6f7abec6b467dde44050"; + sha256 = "076kdfc01mrqh1cz4zi4nzl9rk6yblclbd7r34fxqwbiwdavwsrr"; + }; + + fundamental-arithmetics = mkContrib "fundamental-arithmetics" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g8976d4b"; + rev = "8976d4ba6a5c53b7eb25d08921e592d200189431"; + sha256 = "0pqq1y3hhw8k0qidigg9zkpblhasnb56rxq0n5sh2yfw07gbnfzc"; + }; + + gc = mkContrib "gc" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-gee41f2f"; + rev = "ee41f2fad9fb3bbc2cbf3f90dc440cc31dbd7376"; + sha256 = "0hwlby4sn1p7cky0xz9fmgw50xai3i061y6kqhqy9fn2l2did2sc"; + }; + + generic-environments = mkContrib "generic-environments" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "48b81bb3b8c2941c8d7ef15f5513bbb7f1821ff8"; + sha256 = "03576kkhn5ml4hpn8s8g0i1fxfibr0yjndk8820s7fxmp9838bkc"; + }; + + goedel = mkContrib "goedel" [ ] { + version = "v8.6.0-1-gc3f922c"; + rev = "c3f922cd5cf2345e1be55ba2ec976afcdc6f4b13"; + sha256 = "1cahlrjr1q38m3qwwxzkzvgvgvqvy3li6rjz3hn4n02jxi5daw2g"; + }; + + graph-basics = mkContrib "graph-basics" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "1b86d778016d88084df8a38b2a08e42a778fdf64"; + sha256 = "1rslb8ha1dnygwp2q2lx23d8x5wjlq0c2b6vr1hgy4wzvbas2573"; + }; + + graphs = mkContrib "graphs" [ ] { + version = "v8.6.0-4-gdb25c37"; + rev = "db25c37561bd35e946fc6ad7c0a48121086fc47f"; + sha256 = "10f7yq409i6skgnyv6xv7qklkj2kaddnwxpq752avgm7y8dr96nv"; + }; + + group-theory = mkContrib "group-theory" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-gab6459f"; + rev = "ab6459ff2571529edb0d5c10c13f30b1d9379d71"; + sha256 = "062qixxly5zi22lb00dmspadr4ddsvbdwm05m96gbnycrl2siq09"; + }; + + groups = mkContrib "groups" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "d02aab5c8559ea604a615d993df3c8e714a1dd12"; + sha256 = "0fvwgk5nf5q86sn5q24k3bxps6f1fcafdd47v56xc49iczpkfrck"; + }; + + hardware = mkContrib "hardware" [ "8.6" "8.7" ] { + version = "v8.5.0-8-g2e85f0a"; + rev = "2e85f0ae87ca311e2ffaa8bfd273e505ac03802e"; + sha256 = "0vzn4sgvsbglnwydf0yplpa6laqdmdnayizhrazca3qcckkzxzg4"; + }; + + hedges = mkContrib "hedges" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g301e7f8"; + rev = "301e7f86e0941fe0fa2b5f01f17276cf52be4b06"; + sha256 = "1p42idmm741jx1g7swbkzm1b6mki40xnxkm3ci66mypw19m28142"; + }; + + high-school-geometry = mkContrib "high-school-geometry" [ "8.6" ] { + version = "v8.5.0-7-g40e3f95"; + rev = "40e3f95cbbc756ff4b510e1a998bcbd7e1ff1377"; + sha256 = "1ws57irja9fy1lw6kp6jp5kkn3cb8ws9gixgqvhjpxcfsvgaik0f"; + }; + + higman-cf = mkContrib "higman-cf" [ "8.6" "8.7" ] { + version = "v8.6.0-1-g587cc23"; + rev = "587cc23ad61f43664d5ae5e9ee1949d8380a5209"; + sha256 = "0wjvsmjh5vdmjf8raqlccxzm6ibklkbgznjqhwz3ss3x333lhykb"; + }; + + higman-nw = mkContrib "higman-nw" [ "8.6" "8.7" ] { + version = "v8.6.0-1-g1e2693c"; + rev = "1e2693c6eeb11a39dfe7fcb24acab7dc1fb3d7f6"; + sha256 = "14z3prrsz8c8s0n85890b45pvl4f986g2hckmk61ql6ns7qbsz84"; + }; + + higman-s = mkContrib "higman-s" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-7-g0cae3b4"; + rev = "0cae3b45df7a65f49afdb58f182065b939e5d224"; + sha256 = "0s50v57ancmdcnidrz3jnjgm5rydkfhfn4s74cf4i6qvvscq44nj"; + }; + + historical-examples = mkContrib "historical-examples" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-gf08d49a"; + rev = "f08d49a166f486527f14ad45052f9dd9e2132c00"; + sha256 = "1hym8si742z9rhkini9mbiwfa7mm43xrybfw2gh287hp4pcqcchz"; + }; + + hoare-tut = mkContrib "hoare-tut" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "73dee531bf19ba9db997dff2f0447e12dc8d07db"; + sha256 = "0apmn8f32hfqgpb21n68gqnxg90lhzrawh2c6h4hpl46z087j2ci"; + }; + + huffman = mkContrib "huffman" [ "8.6" "8.7" ] { + version = "v8.5.0-9-gcd44991"; + rev = "cd4499144059e5426a5380b70a110cdaafbcf008"; + sha256 = "0hw152g5cwc3286p44g73lcwd6qdr4n4lqgd0wfdpilpmzh2lm67"; + }; + + icharate = mkContrib "icharate" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g11eb008"; + rev = "11eb008f347e68a824e091ca2224b2138a342b3f"; + sha256 = "03vjcwd5vwhkg1q0zvpz45ayb232hd4q130gx23i039wawgzj66i"; + }; + + idxassoc = mkContrib "idxassoc" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "57991d3754c1b51067329d4abc7caf657c4d4552"; + sha256 = "1xmrv2lpn5rsdxr8ryq5hkihd1wrzpc9a7cvg0jjq8xss1a2sxwh"; + }; + + ieee754 = mkContrib "ieee754" [ "8.6" "8.7" ] { + version = "v8.5.0-8-g9764c31"; + rev = "9764c31bae03182ba9ada4cc877f411c11edc02d"; + sha256 = "032axmvq4vv03cckm72m773v5h76s43awn5bpzd305gs8iag7wgk"; + }; + + int-map = mkContrib "int-map" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "42342f3b4152419faf17c7ac9afd90e337d68637"; + sha256 = "1zxgvg021kakvi5vjvyr0xjmmzyd3zhd8wwm4q276wvmya1fjznr"; + }; + + intuitionistic-nuprl = mkContrib "intuitionistic-nuprl" [ "8.6" ] { + version = "v8.6.0"; + rev = "6279ed83244dc4aec2e23ffb4c87e3f10a50326d"; + sha256 = "1yvlnqwa7ka4a0yg0j7zrzvayhsm1shvsjjawjv552sxc9519aag"; + }; + + ipc = mkContrib "ipc" [ "8.6" "8.7" ] { + version = "v8.6.0-1-g433ab4f"; + rev = "433ab4f5962b49d3178120d6cc4419e4e9932d18"; + sha256 = "16nprdk2cqck0s8ilfy1cjvs48n4kc2hilv9wzi382d4p8jagh0r"; + }; + + izf = mkContrib "izf" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-5-g98ae92b"; + rev = "98ae92bfe0589c781160c967259be7354aaf1663"; + sha256 = "131gpi3p3pxv50dzpr3zfzmfr02ymcwja51cs029j9a33mw9rwx0"; + }; + + jordan-curve-theorem = mkContrib "jordan-curve-theorem" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "906762607c3e05bedd3f9aab002172e34dd1b595"; + sha256 = "1l4pl6rjfzbxnzg32rdcrjl5g889syl6iydiprm8b34blk15ajka"; + }; + + jprover = mkContrib "jprover" [ ] { + version = "v8.5.0-14-g80a9497"; + rev = "80a94974fa4e43be45583409daf9278768abebe0"; + sha256 = "1c5mxnjhd21gzx3yf8gdvgbpwcvklmfxl6qjdynb6dw04lybp8af"; + }; + + karatsuba = mkContrib "karatsuba" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "144bdc68571154ca669a276d30c16bb30ac80b2f"; + sha256 = "0rp9ihw4d68dd6b21xq6lnxa4vsq5ckdhr07ylskmas74p66ns4f"; + }; + + kildall = mkContrib "kildall" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-9-g319577b"; + rev = "319577bdd99aec968fc52f474565dd33b88e6bca"; + sha256 = "1r7hw98xs5w21p50423jqancccn2cwjm90wff08yi7ln0s1rphn1"; + }; + + lambda = mkContrib "lambda" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "577930fe1ee3923dcd3c53793908550a948bcb8f"; + sha256 = "0kmqf5yp4q40wpqncwpd152ysryq2i18rwni4dx2z4d6dir7jidn"; + }; + + lambek = mkContrib "lambek" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "23be01c773ff33dbd06627b7245098bdd3c4525a"; + sha256 = "013nj7b8hicxw5ipiw0my0ms8biyqpcybnh17a7r0w4i7icsygj9"; + }; + + lazy-pcf = mkContrib "lazy-pcf" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "c0b19dff7e1beeccaa2b2d220012bffac6b75f99"; + sha256 = "1qkpszdc3rkm74hkm3z6i080hha4l8904kg5z3xxgpwmhrwb56lq"; + }; + + lc = mkContrib "lc" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-gae9c9f8"; + rev = "ae9c9f878d12539d7b61b91435745ffe32febfd0"; + sha256 = "18bmck6xsp5yi17czyad6iy90c0k65gxjhp47ca64yzcccnzpqbx"; + }; + + legacy-field = mkContrib "legacy-field" [ ] { + version = "v8.6.0-7-g7f400f7"; + rev = "7f400f787459dc63ff1bb862efe8aea41abe90fe"; + sha256 = "0889z8s2rcccl1xckc49r904xpdsa9sdf5dl2v9a2zqx37qcn6cd"; + }; + + legacy-ring = mkContrib "legacy-ring" [ ] { + version = "v8.6.0-4-g3e6c0cf"; + rev = "3e6c0cfeb69189278699e176e2f19fef5e738857"; + sha256 = "15a8rvhr2zw17j7d6w3hd0fxpr6kqy5flpngdqdjij99srm7xzsq"; + }; + + lemma-overloading = mkContrib "lemma-overloading" [ ] { + version = "v8.6.0"; + rev = "6112c139add4d81b9e4d555268a60865f9323151"; + sha256 = "0m1i5xdmwfz4saacay7p6skqnw42csn473gisl24am9jls301cfh"; + }; + + lesniewski-mereology = mkContrib "lesniewski-mereology" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "eeaf56daa0b0bb0fe16368a5e79a089b42d3951c"; + sha256 = "0j4r83biz128pl6g9z5c3x2p5h465ch4fz2jszbr2k1yd8b2gkd9"; + }; + + lin-alg = mkContrib "lin-alg" [ ] { + version = "v8.6.0-5-g74833da"; + rev = "74833da8a93b1c4c921d4aaebbc9f7c2a096a5eb"; + sha256 = "08r9zdq9fxf0b2fxfxb36zywgqd04wpb25l408q3djmq22k56azp"; + }; + + ltl = mkContrib "ltl" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g53e5fc4"; + rev = "53e5fc475fbcce767e2193f92896bd871f7eb1d5"; + sha256 = "0aprimbywsnlg3zzxrg3kp1hw30swz95zcwa2gfidr381isnqciz"; + }; + + maple-mode = mkContrib "maple-mode" [ ] { + version = "v8.5.0-22-gb97a515"; + rev = "b97a5155464360778b215c22668ab80c96a42332"; + sha256 = "15wk6k8m2ff4b5cnqrsccq5vyabam2qaa6q4bvk4cj1nfg0ykg5r"; + }; + + markov = mkContrib "markov" [ "8.7" ] { + version = "v8.5.0-7-ge54c9a8"; + rev = "e54c9a86df5cb90ef6ea04d3753273186bb2d906"; + sha256 = "19csz50846gvfwmhhc37nmlvf70g53cpb1kpmcnjlj82y8r63ajz"; + }; + + math-classes = mkContrib "math-classes" [ "8.6" ] { + version = "v8.6.0-19-ge2c6453"; + rev = "e2c6453e2f6cc1b7f0e1371675f4a76b19fab2c7"; + sha256 = "0das56i8wi7v0s30lbadjlfqas1jlq0mm13yxq6s7zqqbdl5r0bk"; + }; + + maths = mkContrib "maths" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "75a2f84990c1dc83a18ee7decc1445c122664222"; + sha256 = "0yj26mnsfk8y92pd575d9nv9r6pm23zaws18r690s9rjm4kzmwww"; + }; + + matrices = mkContrib "matrices" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g5553a1f"; + rev = "5553a1f7838bafd485e9868c6ad3f76be4c7ffb8"; + sha256 = "0ppw2v404sbvc3d36wi701bwxfxha1ziciyddhzbqw62s5xkhzjc"; + }; + + micromega = mkContrib "micromega" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0-1-ga70bf64"; + rev = "a70bf64b99462a77cd9181e3f2836bc1fed04593"; + sha256 = "0zvqb56il139xgj7n2arvqd305374jb1ahwg63mpf9cqla1m0fxs"; + }; + + mini-compiler = mkContrib "mini-compiler" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "5c0b9da5aabc590c28b7d5a9f49e5a9483b742e1"; + sha256 = "02jpwvk0lsws886bsgahsjmmra25r7b6bn19qmizjjrc0pj44q58"; + }; + + minic = mkContrib "minic" [ "8.6" "8.7" ] { + version = "v8.5.0-7-g0b2e050"; + rev = "0b2e05096f83b08dd935f42501d408bebce01170"; + sha256 = "1wyrshkmkdpkpc47iy2cw9wxadpd1hchr4ilpmifs4rny4y6kkhp"; + }; + + miniml = mkContrib "miniml" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "22a570e57f9e8d1b971d0a7a9e6fdd8d3f053b44"; + sha256 = "17syhr7qyr2naqm7mgarn39d6lrrwah3a6m4mzsvm8d9mwvdqhzs"; + }; + + mod-red = mkContrib "mod-red" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g963c2c9"; + rev = "963c2c930175c91ebcd0cd39ef841ff752ad0813"; + sha256 = "18nlgiypcykhnn9vbgy1bv0zz4ibvzw3jhigl3k9aa3672qr2bwl"; + }; + + multiplier = mkContrib "multiplier" [ "8.6" "8.7" ] { + version = "v8.5.0-10-g127feee"; + rev = "127feeebe065d4698e427cbbcd0ddd8c70fc8bb7"; + sha256 = "08lvs0651yccvxn3mw3sf7d1cdbnf4jvwwc3p57124nvjig649a7"; + }; + + mutual-exclusion = mkContrib "mutual-exclusion" [ "8.6" "8.7" ] { + version = "v8.5.0-9-g6f54d7f"; + rev = "6f54d7f25d9056bf72932c2acd53b832ba015eda"; + sha256 = "066z3ijlni6h39l6g2phs1vqv460x07cri64f847jykchcdjizil"; + }; + + nfix = mkContrib "nfix" [ ] { + version = "v8.6.0-2-gcaeda20"; + rev = "caeda20f3ce3dea0bc647419f3b284e5656cf4ae"; + sha256 = "0s5adpbjm4pxjvnmj24xwxmbg1c356lali0v1v9rcl5lv9fsfi64"; + }; + + orb-stab = mkContrib "orb-stab" [ ] { + version = "v8.6.0-4-ga0a5520"; + rev = "a0a552020eae39e4fd0512c3714ef1b6f8da584c"; + sha256 = "074ygyskvkzwlhqrpyhivxj1axjh3y8wdd57mnjxsf3c103dvajf"; + }; + + otway-rees = mkContrib "otway-rees" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-gf295926"; + rev = "f29592659199f79aa5d3b2fa61a35abba7db5183"; + sha256 = "1yczckkchz3xlb9jcv3rkj5z831b0xrv9j0yvslkl6kpgi1br8af"; + }; + + paco = mkContrib "paco" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "abe297080621c05b3f829a82b36b84f2fc7b5340"; + sha256 = "1jpvkhhnkn8ikj3x7knzr0f8qqrw1ipa8h3mw9bd62kjlmg0f8fj"; + }; + + paradoxes = mkContrib "paradoxes" [ "8.6" "8.7" ] { + version = "v8.5.0-8-g2da6f5f"; + rev = "2da6f5fd4a560f5726dc6083abf2b624391b6d3b"; + sha256 = "1xmhvfbhwn1rfcchb4wq0jlqdrswv1rapxmshjzgkwryq7a7bf64"; + }; + + param-pi = mkContrib "param-pi" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-gba4d052"; + rev = "ba4d052f64788004cb7d8ee172d8c8f58f3a8429"; + sha256 = "04v2fd56x8vd1fv89c3a4vhbhlflnzfzybr7z2fkraxnz5ic1xa4"; + }; + + pautomata = mkContrib "pautomata" [ "8.6" "8.7" ] { + version = "v8.6.0-1-g0cb5e83"; + rev = "0cb5e83f2829d25e99628b1c771efbf0c9dc3d84"; + sha256 = "09r9vdyc87ysciff3rfi4awpd432gblysjcsi42k8n03xhgjm1rv"; + }; + + persistent-union-find = mkContrib "persistent-union-find" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "62c2fac131b87d273c6278fe5bcba0e68895aa18"; + sha256 = "0p4zd3mn8nljjch7c3mrmc5n2kcab8fh9xw7f933wqyh695n1zl9"; + }; + + pi-calc = mkContrib "pi-calc" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-gf8cfa30"; + rev = "f8cfa3027c62719bd944f85d25dcc19b785eb8da"; + sha256 = "12i76ky3x0agd2wzxdsnfxpm7ynp3nj0i7s3skpjnf6rblzgnljf"; + }; + + pocklington = mkContrib "pocklington" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-gc71f839"; + rev = "c71f83920538781a6be99c8ef8a2a306b66e7800"; + sha256 = "0nsavl8v4ndxbrbi160zwpiaw865z22mr638pwgq4pa9qqbbs2p4"; + }; + + presburger = mkContrib "presburger" [ ] { + version = "v8.6.0-2-g6b473eb"; + rev = "6b473ebcab49ac0c0952c27f8a83fb1f7d21cb1a"; + sha256 = "18r76vv7wclv4nzhypncdx4j68dpc0jf0m7p3c8585ca2l72nyfl"; + }; + + prfx = mkContrib "prfx" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g719a3ec"; + rev = "719a3ec175aabb2e3ad92dc030ce2e0d2131e325"; + sha256 = "15vz731apciybn6nqb0fsxrwlxpyrfcakdva38hwxmjx6qskqkhi"; + }; + + projective-geometry = mkContrib "projective-geometry" [ "8.6" "8.7" ] { + version = "v8.5.0-9-g118b0cc"; + rev = "118b0cc37aa97b5de97539cb824a8234f88e123a"; + sha256 = "0fahqagh2il96q160mnwyk6xqjn5wbmy5ckmb5b0yhljs8y181zz"; + }; + + propcalc = mkContrib "propcalc" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "b68586c079a71ebab3235a636e50c083b23d4f25"; + sha256 = "005vqr0c85ld14ff3cz7nnbgy5m5km7ndgblb041f87l8486dbpz"; + }; + + pts = mkContrib "pts" [ "8.6" "8.7" ] { + version = "v8.5.0-9-g10a0c39"; + rev = "10a0c39b7e62f8a7ec2afbbe516a21289d065be5"; + sha256 = "14nqxjqg7v6f70zwi13a1iz70vxq4gfsz7aviggj7cbbky9s1lw3"; + }; + + ptsatr = mkContrib "ptsatr" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "e57ad4552055340ea97bc6a2c61b837c56c11a7d"; + sha256 = "1ivqrvk7dhk52llxi6vxby0zyz05kgc82fgvvkv8f9gmy485v3m7"; + }; + + ptsf = mkContrib "ptsf" [ ] { + version = "v8.6.0-1-g2a303f4"; + rev = "2a303f4e83ef54fc6f8fbc374eaebf05e1e9b5e4"; + sha256 = "0p7dwsf2s72ndgkwf8mj4n8sy1b5anfspj0v8rndvyqsmld7if2g"; + }; + + qarith = mkContrib "qarith" [ "8.6" "8.7" ] { + version = "v8.6.0-1-g5255d8f"; + rev = "5255d8fbb28b85424d0fe626125a70cc2f5abcde"; + sha256 = "1rx70f3pnkj30ql97wdp4bimbb2pazbm7xgs5q0g5i3xbiyv50lk"; + }; + + qarith-stern-brocot = mkContrib "qarith-stern-brocot" [ "8.7" ] { + version = "v8.6.0-4-gcad3819"; + rev = "cad381906c9c5b17e701005f3c4290765abc9099"; + sha256 = "0bzczqa61cs9443gapm8y8137d9savxnadwwrkcynhmj1ljx26xy"; + }; + + quicksort-complexity = mkContrib "quicksort-complexity" [ "8.6" "8.7" ] { + version = "v8.5.0-9-gb897466"; + rev = "b8974665b0de3e9b135291a699e98ed52cd335d1"; + sha256 = "038gyjc6afyb31cfi4fiajzl7a8ykh7dmkajn9dm7rh4md1x6jjf"; + }; + + railroad-crossing = mkContrib "railroad-crossing" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g2ef67f5"; + rev = "2ef67f5c586a58cd79a8ee0eb22590182374135d"; + sha256 = "0cdk5b6br317xh0ivpj3ffqcy19w2g7sfa5rrv4ls0hmsrrzpxkp"; + }; + + ramsey = mkContrib "ramsey" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g2821213"; + rev = "2821213706faa7f06823001ce9e58ecff0cd3191"; + sha256 = "1pw2yqkllkvllzs4dyzvyv27mh53qi8wpzh1cr53cwyg6573h0dz"; + }; + + random = mkContrib "random" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0-1-gf87a8a7"; + rev = "f87a8a77f420df4a12c4a7e4f28ff088e62b4175"; + sha256 = "05xc59frgcmfx7g72i02g3x17zhdlgpap7y6q1gd29xnmrhqnhni"; + }; + + rational = mkContrib "rational" [ ] { + version = "v8.6.0-2-ga12ef65"; + rev = "a12ef65ddd267b4d61e234da4fab17bc12202c17"; + sha256 = "06s3bpm1v7bz69qp3m58kjk5qmdr0d4jgmy20q6qp44mi0341gy7"; + }; + + recursive-definition = mkContrib "recursive-definition" [ ] { + version = "v8.6.0-1-g66b8204"; + rev = "66b820494ed872ef16ff228f78310aab2a47d2be"; + sha256 = "0z6sp1n1m2vbxhb220y3hqi1f24lz6g1nkkq84m9xq2wvg7li6hn"; + }; + + reflexive-first-order = mkContrib "reflexive-first-order" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g307b421"; + rev = "307b421dd4894ef624e67558087d2f0945ef1970"; + sha256 = "0rwr8sy6v7a17x1g0pa9gbbd9kgrq5lxr6cxv8r926883blz891y"; + }; + + regexp = mkContrib "regexp" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "da6d250506ea667266282cc7280355d13b27c68d"; + sha256 = "1s1rxrz6yq8j0ykd2ra0g9mj8ky2dvgim2ysjdn5yz514b36mc7x"; + }; + + relation-algebra = mkContrib "relation-algebra" [ ] { + version = "v8.6.0-7-g0d3ca3e"; + rev = "0d3ca3eb5490b2f32d5c2763e2343d373e78baea"; + sha256 = "1kjd23qgmi3qnb4hpn7k5h88psq5rs5bba9s494zhrzkf6cgv9d1"; + }; + + relation-extraction = mkContrib "relation-extraction" [ ] { + version = "v8.6.0-4-g1a604fa"; + rev = "1a604fa2c4211c4c36dd600dab6ed076a04c00ce"; + sha256 = "114idr4n19c5nnzn6wdj5jz82wbisxrbw6qvfjnwh02yz2sbpn2d"; + }; + + rem = mkContrib "rem" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-g306938c"; + rev = "306938c460518695393313f57d47ec8c653add11"; + sha256 = "1cccqj08pmgjdlwgi4r1qz0h9sgr1840zrwc36fzfslhdqixgyd9"; + }; + + rsa = mkContrib "rsa" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "01dddd705621ad9efbaf081bffa76465b3cdc442"; + sha256 = "1426cyzd1493iwhzb4sm7xpvn5vj10ap9607kh1flhhqdxx4fvgz"; + }; + + ruler-compass-geometry = mkContrib "ruler-compass-geometry" [ "8.6" "8.7" ] { + version = "v8.5.0-7-g69e66a8"; + rev = "69e66a80590e89c3916359beef4109990b8c92f6"; + sha256 = "01qw8vyaj29frm7zzdn18nwrzcqbjaqhpky5qwlsmxlza5h5vz1c"; + }; + + schroeder = mkContrib "schroeder" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "31df08b6c00fe7d0ac7391f7f939c4869cfe9b8c"; + sha256 = "18gwh3axcbaicmylkjsljiw8q2z02hpcbz6mpvx3zyh1vcgl47qw"; + }; + + search-trees = mkContrib "search-trees" [ "8.6" "8.7" ] { + version = "v8.5.0-9-g07dee21"; + rev = "07dee215c9453fcd95a0c13d2495f7e260325378"; + sha256 = "19jw1qccn1c7jp78kc6ipr3mpp1fkm3wxb6y7wjgvqqphjy62sfg"; + }; + + semantics = mkContrib "semantics" [ ] { + version = "v8.5.0-8-g8236bf9"; + rev = "8236bf94a7735378b3a49ea376cd220bcadfe831"; + sha256 = "18kmmn7y0nvgszrap2d7dcqkvfrpkk6w6wzf8ji9j8lc8mznyy8h"; + }; + + shuffle = mkContrib "shuffle" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "681fc1a794cce5d99e748b68586e8c5a11810788"; + sha256 = "121b021b25vkgcw892lbidrhbk7syrz9xxlk3d45gf8pdin8i8zb"; + }; + + smc = mkContrib "smc" [ ] { + version = "v8.6.0-4-g161f8aa"; + rev = "161f8aaaf80f7475f2679c55a8f7ac511215cd4b"; + sha256 = "01375i2n8cw8kdf7zgcz7kmkw6wspmw4ngrzjnq5bxf7ijw7z9qx"; + }; + + square-matrices = mkContrib "square-matrices" [ "8.6" "8.7" ] { + version = "v8.6.0-1-g7fe56db"; + rev = "7fe56dbe1a9916236b44cc96d25cee2b90825ae5"; + sha256 = "03lxq8v63gydnm7fcryjpqdywjb3hrfirnxx7sm6zc9yblh2m0il"; + }; + + stalmarck = mkContrib "stalmarck" [ ] { + version = "v8.6.0-3-g083bd20"; + rev = "083bd20af8ce5c646e5cd9845474523027bf7e79"; + sha256 = "0nhbxin98hwam4jb4iadb06b785s88h0mz8i0v6adpprym1my746"; + }; + + streams = mkContrib "streams" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-7-gd53a1ca"; + rev = "d53a1ca12b2fb5cb9324452aabe36a7e4b3db85c"; + sha256 = "14qk7w675c2flh2qyrzqjywn1f1fcchsqzn59zlh755krssf4y4b"; + }; + + string = mkContrib "string" [ ] { + version = "v8.5.0-9-g861dd5c"; + rev = "861dd5ce2d72a5856a79d1e9e4eb0c4b1070e73c"; + sha256 = "0fq49qdbi2c5i5hkbf6cgx1dyzg02mhr0zd89kgbxa5lpv5sp3y7"; + }; + + subst = mkContrib "subst" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-5-g9d9fed6"; + rev = "9d9fed67529aa98f5b2d77c695e1370a3c4b7ecf"; + sha256 = "0dqz2wgzsipk9zic6cf3dhqr1a3p5s2d30cjs5312c5pz6gw3fp4"; + }; + + sudoku = mkContrib "sudoku" [ "8.6" "8.7" ] { + version = "v8.5.0-6-g4ebe0aa"; + rev = "4ebe0aace3341b14ba6f2177888148345988c43c"; + sha256 = "0srf1477x5q3qb5inlcrc1hr193rdw8sp8c0bw6fw4na0d6bphv3"; + }; + + sum-of-two-square = mkContrib "sum-of-two-square" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-5-g66c1146"; + rev = "66c11466b499c0f26a9d687933432e16f4aed080"; + sha256 = "0z1h7cq3f15xlm7b0kirf1jv6n43f11in82x6vjiw7arnn1axwh5"; + }; + + tait = mkContrib "tait" [ "8.6" "8.7" ] { + version = "v8.6.0-1-g1505eb9"; + rev = "1505eb9e6af0c14892c9fe2bd1021b56dc65c409"; + sha256 = "1662mn9qpym8rq99854ziykk2jrr5s9h5r8j6y4ddgma0ihv1v5w"; + }; + + tarski-geometry = mkContrib "tarski-geometry" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-gd30cc0e"; + rev = "d30cc0e71e507dc14eb0d5397e8c3a6252fe5d07"; + sha256 = "1hngfix8riqa0kn774602q3kc2m8mfksx1ynb69pq6hy6q3ikn1n"; + }; + + three-gap = mkContrib "three-gap" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0"; + rev = "b176a7b3165aecd171926271a8d90888f16dc297"; + sha256 = "0mr8s0djs165i64v48k8i7sn832s5ff2hnyqhl9ijsvhcix20ij2"; + }; + + topology = mkContrib "topology" [ ] { + version = "v8.6.0-1-g4e79a75"; + rev = "4e79a755efe0ca509ef589135aa3406449b44dfb"; + sha256 = "00211410zb5z367mv2brqg1d0p50yjy446g7qc69c4kyp6sr80gf"; + }; + + tortoise-hare-algorithm = mkContrib "tortoise-hare-algorithm" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-6-gb34a87c"; + rev = "b34a87c0b41eb9a72408292a5d714ae8f342a4c5"; + sha256 = "08j6xc65scxzxznhiiapfny2hchl3mcvrsp2mr05snq5hlidlpxv"; + }; + + traversable-fincontainer = mkContrib "traversable-fincontainer" [ "8.7" ] { + version = "v8.6.0-1-g3f1fc68"; + rev = "3f1fc684ea23a69b1e8ab7f1ee139a66278eb2e0"; + sha256 = "0h0vf74lfll7bhb9m1sk3g82y1vaik1fr5r5k69bbjgh0j5bfj50"; + }; + + tree-automata = mkContrib "tree-automata" [ ] { + version = "v8.6.0-1-g34b3eb6"; + rev = "34b3eb6362407040d7a9a3fc0b1c23661e01162a"; + sha256 = "07iwfi6c6a8dq5rdlsppl187qbmbycj7xifm8aa38ygmsh5rcpir"; + }; + + tree-diameter = mkContrib "tree-diameter" [ "8.5" "8.6" "8.7" ] { + version = "v8.6.0-1-g846a232"; + rev = "846a232a07b3cf43d18b694ef4bcbe4b270e9cd4"; + sha256 = "0i238h60jgqmzkb38qbyjj6i1wzv0bm00g0mwh98wbxlj3pn7ma8"; + }; + + weak-up-to = mkContrib "weak-up-to" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-5-g0893619"; + rev = "0893619b205a30a0f832da8ceef97c2c3f4801f8"; + sha256 = "0mg1628zyb7xyyg4k8zvay2h7wcdlwcx9nyxwpixdp5xhz3s4l9b"; + }; + + zchinese = mkContrib "zchinese" [ "8.6" "8.7" ] { + version = "v8.6.0-1-g25d4e21"; + rev = "25d4e21b648f65593f9378cb9f5171dcc4641223"; + sha256 = "06phig9yh4rqqpqjbzk6704n44vz31irnwvprbdvyzgiyi2bkahk"; + }; + + zf = mkContrib "zf" [ "8.5" "8.6" "8.7" ] { + version = "v8.5.0-4-gcf33d92"; + rev = "cf33d92b69865af97d93946337f291cffc1e8a9e"; + sha256 = "0fp3vdl79c8d759qjhk42rjfpkd0ba4pcw572f5gxn28kfwz3rrj"; + }; + + zfc = mkContrib "zfc" [ "8.5" "8.6" "8.7" "8.8" ] { + version = "v8.5.0-5-gbba3259"; + rev = "bba325933370fea64780b1afa2fad54c1b567819"; + sha256 = "0iwkpmc22nwasrk4g7ki4s5y05zjs7kmqk3j98giwp2wiavhgapn"; + }; + + zorns-lemma = mkContrib "zorns-lemma" [ "8.10" "8.11" ] { + version = "v8.11.0"; + rev = "a573b50fff994f996b8e15dec2079490a5233dc6"; + sha256 = "0jbp1ay6abal66glbablbqsh5hzgd5fv81dc1vzn65jw0iiznxyq"; + }; + + zsearch-trees = mkContrib "zsearch-trees" [ "8.6" "8.7" ] { + version = "v8.5.0-7-ga9f6d9a"; + rev = "a9f6d9a8b6e567e749b1470c6879df560dab7f43"; + sha256 = "1001bnh5hzx0rnwhlx7qci52rqi49z5ij7p9gcdr4w86i182w6rg"; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coq-bits/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coq-bits/default.nix new file mode 100644 index 000000000000..9665c5400d85 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coq-bits/default.nix @@ -0,0 +1,38 @@ +{ stdenv, fetchFromGitHub, coq, mathcomp-algebra }: + +let + version = "20190812"; +in + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-coq-bits-${version}"; + + src = fetchFromGitHub { + owner = "coq-community"; + repo = "bits"; + rev = "1.0.0"; + sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl"; + }; + + buildInputs = [ coq ]; + propagatedBuildInputs = [ mathcomp-algebra ]; + + enableParallelBuilding = true; + + installPhase = '' + make -f Makefile CoqMakefile + make -f CoqMakefile COQLIB=$out/lib/coq/${coq.coq-version}/ install + ''; + + meta = with stdenv.lib; { + homepage = "https://github.com/coq-community/bits"; + description = "A formalization of bitset operations in Coq"; + license = licenses.asl20; + maintainers = with maintainers; [ ptival ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coq-elpi/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coq-elpi/default.nix new file mode 100644 index 000000000000..230320671a7f --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coq-elpi/default.nix @@ -0,0 +1,43 @@ +{ stdenv, fetchFromGitHub, which, coq }: + +let params = { + "8.11" = rec { + version = "1.6.0_8.11"; + rev = "v${version}"; + sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq"; + }; + "8.12" = rec { + version = "1.6.0"; + rev = "v${version}"; + sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b"; + }; +}; + param = params.${coq.coq-version}; +in + +stdenv.mkDerivation rec { + name = "coq${coq.coq-version}-elpi-${param.version}"; + + src = fetchFromGitHub { + owner = "LPCIC"; + repo = "coq-elpi"; + inherit (param) rev sha256; + }; + + nativeBuildInputs = [ which ]; + buildInputs = [ coq coq.ocaml ] ++ (with coq.ocamlPackages; [ findlib elpi ]); + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + meta = { + description = "Coq plugin embedding ELPI."; + maintainers = [ stdenv.lib.maintainers.cohencyril ]; + license = stdenv.lib.licenses.lgpl21; + inherit (coq.meta) platforms; + inherit (src.meta) homepage; + }; + + passthru = { + compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coq-ext-lib/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coq-ext-lib/default.nix new file mode 100644 index 000000000000..f24ccaf427d2 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coq-ext-lib/default.nix @@ -0,0 +1,45 @@ +{ stdenv, fetchFromGitHub, coq }: + +let params = + { + "8.5" = { version = "0.9.4"; sha256 = "1y66pamgsdxlq2w1338lj626ln70cwj7k53hxcp933g8fdsa4hp0"; }; + "8.6" = { version = "0.9.5"; sha256 = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg"; }; + "8.7" = { version = "0.9.7"; sha256 = "00v4bm4glv1hy08c8xsm467az6d1ashrznn8p2bmbmmp52lfg7ag"; }; + "8.8" = { version = "0.11.2"; sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; }; + "8.9" = { version = "0.11.2"; sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; }; + "8.10" = { version = "0.11.2"; sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; }; + "8.11" = { version = "0.11.2"; sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; }; + "8.12" = { version = "0.11.2"; sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; }; + }; + param = params.${coq.coq-version}; +in + +stdenv.mkDerivation rec { + + name = "coq${coq.coq-version}-coq-ext-lib-${version}"; + inherit (param) version; + + src = fetchFromGitHub { + owner = "coq-ext-lib"; + repo = "coq-ext-lib"; + rev = "v${param.version}"; + inherit (param) sha256; + }; + + buildInputs = [ coq ]; + + enableParallelBuilding = true; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + meta = with stdenv.lib; { + homepage = "https://github.com/coq-ext-lib/coq-ext-lib"; + description = "A collection of theories and plugins that may be useful in other Coq developments"; + maintainers = with maintainers; [ jwiegley ptival ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.hasAttr v params; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coq-haskell/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coq-haskell/default.nix new file mode 100644 index 000000000000..7c86a7d55f34 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coq-haskell/default.nix @@ -0,0 +1,60 @@ +{ stdenv, fetchgit, coq, ssreflect }: + +let params = + { + "8.5" = { + version = "20171215"; + rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968"; + sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv"; + }; + + "8.6" = { + version = "20171215"; + rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968"; + sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv"; + }; + + "8.7" = { + version = "20171215"; + rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968"; + sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv"; + }; + + "8.8" = { + version = "20171215"; + rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968"; + sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv"; + }; + }; + param = params.${coq.coq-version}; +in + +stdenv.mkDerivation { + + name = "coq${coq.coq-version}-coq-haskell-${param.version}"; + + src = fetchgit { + url = "git://github.com/jwiegley/coq-haskell.git"; + inherit (param) rev sha256; + }; + + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib ]; + propagatedBuildInputs = [ coq ssreflect ]; + + enableParallelBuilding = false; + + installPhase = '' + make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install + ''; + + meta = with stdenv.lib; { + homepage = "https://github.com/jwiegley/coq-haskell"; + description = "A library for formalizing Haskell types and functions in Coq"; + maintainers = with maintainers; [ jwiegley ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.hasAttr v params; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coqhammer/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coqhammer/default.nix new file mode 100644 index 000000000000..56fce9ac526f --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coqhammer/default.nix @@ -0,0 +1,71 @@ +{ stdenv, fetchFromGitHub, coq }: + +let + params = { + "8.8" = { + version = "1.1"; + sha256 = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h"; + buildInputs = [ coq.ocamlPackages.camlp5 ]; + }; + "8.9" = { + version = "1.1.1"; + sha256 = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9"; + buildInputs = [ coq.ocamlPackages.camlp5 ]; + }; + "8.10" = { + version = "1.3"; + sha256 = "1fj8497ir4m79hyrmmmmrag01001wrby0h24wv6525vz0w5py3cd"; + }; + "8.11" = { + version = "1.3"; + sha256 = "08zf8qfna7b9p2myfaz4g7bas3a1q1156x78n5isqivlnqfrjc1b"; + }; + "8.12" = { + version = "1.3"; + sha256 = "1q1y3cwhd98pkm98g71fsdjz85bfwgcz2xn7s7wwmiraifv5l6z8"; + }; + }; + param = params.${coq.coq-version}; +in + +stdenv.mkDerivation rec { + inherit (param) version; + name = "coq${coq.coq-version}-coqhammer-${version}"; + + src = fetchFromGitHub { + owner = "lukaszcz"; + repo = "coqhammer"; + rev = "v${version}-coq${coq.coq-version}"; + inherit (param) sha256; + }; + + postPatch = '' + substituteInPlace Makefile.coq.local --replace \ + '$(if $(COQBIN),$(COQBIN),`coqc -where | xargs dirname | xargs dirname`/bin/)' \ + '$(out)/bin/' + substituteInPlace Makefile.coq.local --replace 'g++' 'c++' --replace 'gcc' 'cc' + ''; + + buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ + ocaml findlib + ]) ++ (param.buildInputs or []); + + preInstall = '' + mkdir -p $out/bin + ''; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + meta = { + homepage = "http://cl-informatik.uibk.ac.at/cek/coqhammer/"; + description = "Automation for Dependent Type Theory"; + license = stdenv.lib.licenses.lgpl21; + inherit (coq.meta) platforms; + maintainers = [ stdenv.lib.maintainers.vbgl ]; + }; + + passthru = { + compatibleCoqVersions = v: builtins.hasAttr v params; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coqprime/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coqprime/default.nix new file mode 100644 index 000000000000..f16341ddbd1b --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coqprime/default.nix @@ -0,0 +1,60 @@ +{ stdenv, which, fetchFromGitHub, coq, bignums }: + +let + params = + let v_8_8 = { + version = "8.8"; + sha256 = "075yjczk79pf1hd3lgdjiz84ilkzfxjh18lgzrhhqp7d3kz5lxp5"; + }; + v_8_10 = { + version = "8.10"; + sha256 = "0r9gnh5a5ykiiz5h1i8xnzgiydpwc4z9qhndxyya85xq0f910qaz"; + }; + in + { + "8.7" = { + version = "8.7.2"; + sha256 = "15zlcrx06qqxjy3nhh22wzy0rb4npc8l4nx2bbsfsvrisbq1qb7k"; + }; + "8.8" = v_8_8; + "8.9" = v_8_8; + "8.10" = v_8_10; + "8.11" = v_8_10; + "8.12" = { + version = "8.12"; + sha256 = "1slka4w0pya15js4drx9frj7lxyp3k2lzib8v23givzpnxs8ijdj"; + }; + }; + param = params.${coq.coq-version}; +in + +stdenv.mkDerivation rec { + + inherit (param) version; + name = "coq${coq.coq-version}-coqprime-${version}"; + + src = fetchFromGitHub { + owner = "thery"; + repo = "coqprime"; + rev = "v${version}"; + inherit (param) sha256; + }; + + buildInputs = [ which coq ]; + + propagatedBuildInputs = [ bignums ]; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + meta = with stdenv.lib; { + description = "Library to certify primality using Pocklington certificate and Elliptic Curve Certificate"; + license = licenses.lgpl21; + maintainers = [ stdenv.lib.maintainers.vbgl ]; + inherit (coq.meta) platforms; + inherit (src.meta) homepage; + }; + + passthru = { + compatibleCoqVersions = v: builtins.hasAttr v params; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coquelicot/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coquelicot/default.nix new file mode 100644 index 000000000000..e45077f89fdd --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/coquelicot/default.nix @@ -0,0 +1,43 @@ +{ stdenv, fetchurl, which, coq, ssreflect }: + +let param = + if stdenv.lib.versionAtLeast coq.coq-version "8.8" + then { + version = "3.1.0"; + uid = "38287"; + sha256 = "07436wkvnq9jyf7wyhp77bpl157s3qhba1ay5xrkxdi26qdf3h14"; + } else { + version = "3.0.2"; + uid = "37523"; + sha256 = "1biia7nfqf7vaqq5gmykl4rwjyvrcwss6r2jdf0in5pvp2rnrj2w"; + } +; in + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-coquelicot-${param.version}"; + src = fetchurl { + url = "https://gforge.inria.fr/frs/download.php/file/${param.uid}/coquelicot-${param.version}.tar.gz"; + inherit (param) sha256; + }; + + nativeBuildInputs = [ which ]; + buildInputs = [ coq ]; + propagatedBuildInputs = [ ssreflect ]; + + configureFlags = [ "--libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Coquelicot" ]; + buildPhase = "./remake"; + installPhase = "./remake install"; + + meta = { + homepage = "http://coquelicot.saclay.inria.fr/"; + description = "A Coq library for Reals"; + license = stdenv.lib.licenses.lgpl3; + maintainers = [ stdenv.lib.maintainers.vbgl ]; + inherit (coq.meta) platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/corn/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/corn/default.nix new file mode 100644 index 000000000000..14ff74506f37 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/corn/default.nix @@ -0,0 +1,38 @@ +{ stdenv, fetchFromGitHub, coq, bignums, math-classes }: + +stdenv.mkDerivation rec { + pname = "corn"; + version = "8.8.1"; + name = "coq${coq.coq-version}-${pname}-${version}"; + src = fetchFromGitHub { + owner = "coq-community"; + repo = pname; + rev = version; + sha256 = "0gh32j0f18vv5lmf6nb87nr5450w6ai06rhrnvlx2wwi79gv10wp"; + }; + + buildInputs = [ coq ]; + + preConfigure = "patchShebangs ./configure.sh"; + configureScript = "./configure.sh"; + dontAddPrefix = true; + + propagatedBuildInputs = [ bignums math-classes ]; + + enableParallelBuilding = true; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + meta = { + homepage = "http://c-corn.github.io/"; + license = stdenv.lib.licenses.gpl2; + description = "A Coq library for constructive analysis"; + maintainers = [ stdenv.lib.maintainers.vbgl ]; + inherit (coq.meta) platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" ]; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/dpdgraph/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/dpdgraph/default.nix new file mode 100644 index 000000000000..195a1c4eada5 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/dpdgraph/default.nix @@ -0,0 +1,88 @@ +{ stdenv, fetchFromGitHub, autoreconfHook, coq }: + +let params = { + "8.12" = { + version = "0.6.8"; + sha256 = "1mj6sknsd53xfb387sp3kdwvl4wn80ck24bfzf3s6mgw1a12vyps"; + }; + "8.11" = { + version = "0.6.7"; + sha256 = "01vpi7scvkl4ls1z2k2x9zd65wflzb667idj759859hlz3ps9z09"; + }; + "8.10" = { + version = "0.6.6"; + sha256 = "1gjrm5zjzw4cisiwdr5b3iqa7s4cssa220xr0k96rwgk61rcjd8w"; + }; + "8.9" = { + version = "0.6.5"; + sha256 = "1f34z24yg05b1096gqv36jr3vffkcjkf9qncii3pzhhvagxd0w2f"; + }; + "8.8" = { + version = "0.6.3"; + rev = "0acbd0a594c7e927574d5f212cc73a486b5305d2"; + sha256 = "0c95b0bz2kjm6swr5na4gs06lxxywradszxbr5ldh2zx02r3f3rx"; + }; + "8.7" = { + version = "0.6.2"; + rev = "d76ddde37d918569945774733b7997e8b24daf51"; + sha256 = "04lnf4b25yarysj848cfl8pd3i3pr3818acyp9hgwdgd1rqmhjwm"; + }; + "8.6" = { + version = "0.6.1"; + rev = "c3b87af6bfa338e18b83f014ebd0e56e1f611663"; + sha256 = "1jaafkwsb5450378nprjsds1illgdaq60gryi8kspw0i25ykz2c9"; + }; + "8.5" = { + version = "0.6"; + sha256 = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n"; + }; +}; +param = params.${coq.coq-version}; +in + +let hasWarning = stdenv.lib.versionAtLeast coq.ocamlPackages.ocaml.version "4.08"; in + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-dpdgraph-${param.version}"; + src = fetchFromGitHub { + owner = "Karmaki"; + repo = "coq-dpdgraph"; + rev = param.rev or "v${param.version}"; + inherit (param) sha256; + }; + + nativeBuildInputs = [ autoreconfHook ]; + buildInputs = [ coq ] + ++ (with coq.ocamlPackages; [ ocaml findlib ocamlgraph ] + ++ stdenv.lib.optional (!stdenv.lib.versionAtLeast coq.coq-version "8.10") camlp5); + + # dpd_compute.ml uses deprecated Pervasives.compare + # Versions prior to 0.6.5 do not have the WARN_ERR build flag + preConfigure = stdenv.lib.optionalString hasWarning '' + substituteInPlace Makefile.in --replace "-warn-error +a " "" + ''; + + buildFlags = stdenv.lib.optional hasWarning "WARN_ERR="; + + preInstall = '' + mkdir -p $out/bin + ''; + + installFlags = [ + "COQLIB=$(out)/lib/coq/${coq.coq-version}/" + "BINDIR=$(out)/bin" + ]; + + meta = { + description = "Build dependency graphs between Coq objects"; + license = stdenv.lib.licenses.lgpl21; + homepage = "https://github.com/Karmaki/coq-dpdgraph/"; + maintainers = with stdenv.lib.maintainers; [ vbgl ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.hasAttr v params; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/equations/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/equations/default.nix new file mode 100644 index 000000000000..5a07d537536c --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/equations/default.nix @@ -0,0 +1,79 @@ +{ stdenv, fetchFromGitHub, coq }: + +let + params = { + "8.6" = { + version = "1.0"; + rev = "v1.0"; + sha256 = "19ylw9v9g35607w4hm86j7mmkghh07hmkc1ls5bqlz3dizh5q4pj"; + }; + + "8.7" = { + version = "1.0"; + rev = "v1.0-8.7"; + sha256 = "1bavg4zl1xn0jqrdq8iw7xqzdvdf39ligj9saz5m9c507zri952h"; + }; + + "8.8" = { + version = "1.2"; + rev = "v1.2-8.8"; + sha256 = "06452fyzalz7zcjjp73qb7d6xvmqb6skljkivf8pfm55fsc8s7kx"; + }; + + "8.9" = { + version = "1.2.1"; + rev = "v1.2.1-8.9"; + sha256 = "0d8ddj6nc6p0k25cd8fs17cq427zhzbc3v9pk2wd2fnvk70nlfij"; + }; + + "8.10" = { + version = "1.2.1"; + rev = "v1.2.1-8.10-2"; + sha256 = "0j3z4l5nrbyi9zbbyqkc6kassjanwld2188mwmrbqspaypm2ys68"; + }; + + "8.11" = { + version = "1.2.3"; + rev = "v1.2.3-8.11"; + sha256 = "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf"; + }; + + "8.12" = { + version = "1.2.3"; + rev = "v1.2.3-8.12"; + sha256 = "1y0jkvzyz5ssv5vby41p1i8zs7nsdc8g3pzyq73ih9jz8h252643"; + }; + }; + param = params.${coq.coq-version}; +in + +stdenv.mkDerivation rec { + + name = "coq${coq.coq-version}-equations-${version}"; + version = param.version; + + src = fetchFromGitHub { + owner = "mattam82"; + repo = "Coq-Equations"; + rev = param.rev; + sha256 = param.sha256; + }; + + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ]; + + preBuild = "coq_makefile -f _CoqProject -o Makefile"; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + meta = with stdenv.lib; { + homepage = "https://mattam82.github.io/Coq-Equations/"; + description = "A plugin for Coq to add dependent pattern-matching"; + maintainers = with maintainers; [ jwiegley ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.hasAttr v params; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/fiat/HEAD.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/fiat/HEAD.nix new file mode 100644 index 000000000000..fd3ade0c64b5 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/fiat/HEAD.nix @@ -0,0 +1,39 @@ +{stdenv, fetchgit, coq, python27}: + +stdenv.mkDerivation rec { + + name = "coq-fiat-${coq.coq-version}-unstable-${version}"; + version = "2016-10-24"; + + src = fetchgit { + url = "https://github.com/mit-plv/fiat.git"; + rev = "7feb6c64be9ebcc05924ec58fe1463e73ec8206a"; + sha256 = "0griqc675yylf9rvadlfsabz41qy5f5idya30p5rv6ysiakxya64"; + }; + + buildInputs = [ coq python27 ] ++ (with coq.ocamlPackages; [ ocaml camlp5 ]); + + prePatch = "patchShebangs etc/coq-scripts"; + + doCheck = false; + + enableParallelBuilding = false; + buildPhase = "make -j$NIX_BUILD_CORES"; + + installPhase = '' + COQLIB=$out/lib/coq/${coq.coq-version}/ + mkdir -p $COQLIB/user-contrib/Fiat + cp -pR src/* $COQLIB/user-contrib/Fiat + ''; + + meta = with stdenv.lib; { + homepage = "http://plv.csail.mit.edu/fiat/"; + description = "A library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications"; + maintainers = with maintainers; [ jwiegley ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: v == "8.5"; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/flocq/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/flocq/default.nix new file mode 100644 index 000000000000..c5d3a295f2bc --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/flocq/default.nix @@ -0,0 +1,49 @@ +{ stdenv, bash, which, autoconf, automake, fetchzip, coq }: + +let params = + if stdenv.lib.versionAtLeast coq.coq-version "8.7" then { + version = "3.3.1"; + sha256 = "0k1nfgiszmai5dihhpfa5mgq9rwigl0n38dw10jn79x89xbdpyh5"; + } else { + version = "2.6.1"; + sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj"; + } +; in + +stdenv.mkDerivation rec { + + name = "coq${coq.coq-version}-flocq-${version}"; + inherit (params) version; + + src = fetchzip { + url = "https://gitlab.inria.fr/flocq/flocq/-/archive/flocq-${version}.tar.gz"; + inherit (params) sha256; + }; + + nativeBuildInputs = [ bash which autoconf automake ]; + buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ + ocaml camlp5 + ]); + + buildPhase = '' + ${bash}/bin/bash autogen.sh || autoconf + ${bash}/bin/bash configure --libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Flocq + ./remake + ''; + + installPhase = '' + ./remake install + ''; + + meta = with stdenv.lib; { + homepage = "http://flocq.gforge.inria.fr/"; + description = "A floating-point formalization for the Coq system"; + license = licenses.lgpl3; + maintainers = with maintainers; [ jwiegley ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/gappalib/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/gappalib/default.nix new file mode 100644 index 000000000000..f6109398da8e --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/gappalib/default.nix @@ -0,0 +1,30 @@ +{ stdenv, fetchurl, which, coq, flocq }: + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-gappalib-1.4.4"; + src = fetchurl { + url = "https://gforge.inria.fr/frs/download.php/file/38338/gappalib-coq-1.4.4.tar.gz"; + sha256 = "1ds9qp3ml07w5ali0rsczlwgdx4xcgasgbcnpi2lssgj1xpxgfpn"; + }; + + nativeBuildInputs = [ which ]; + buildInputs = [ coq coq.ocamlPackages.ocaml ]; + propagatedBuildInputs = [ flocq ]; + + configurePhase = "./configure --libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Gappa"; + buildPhase = "./remake"; + installPhase = "./remake install"; + + meta = { + description = "Coq support library for Gappa"; + license = stdenv.lib.licenses.lgpl21; + homepage = "http://gappa.gforge.inria.fr/"; + maintainers = [ stdenv.lib.maintainers.vbgl ]; + inherit (coq.meta) platforms; + }; + + passthru = { + compatibleCoqVersions = stdenv.lib.flip builtins.elem [ "8.8" "8.9" "8.10" "8.11" "8.12" ]; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/heq/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/heq/default.nix new file mode 100644 index 000000000000..d0445c83ca59 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/heq/default.nix @@ -0,0 +1,30 @@ +{stdenv, fetchurl, coq, unzip}: + +stdenv.mkDerivation rec { + + name = "coq-heq-${coq.coq-version}-${version}"; + version = "0.92"; + + src = fetchurl { + url = "https://www.mpi-sws.org/~gil/Heq/download/Heq-${version}.zip"; + sha256 = "03y71c4qs6cmy3s2hjs05g7pcgk9sqma6flj15394yyxbvr9is1p"; + }; + + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 unzip ]; + propagatedBuildInputs = [ coq ]; + + preBuild = "cd src"; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}" ]; + + meta = with stdenv.lib; { + homepage = "https://www.mpi-sws.org/~gil/Heq/"; + description = "Heq : a Coq library for Heterogeneous Equality"; + maintainers = with maintainers; [ jwiegley ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: !stdenv.lib.versionAtLeast v "8.8"; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/hierarchy-builder/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/hierarchy-builder/default.nix new file mode 100644 index 000000000000..9be8459ee9f0 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/hierarchy-builder/default.nix @@ -0,0 +1,43 @@ +{ stdenv, fetchFromGitHub, which, coq, coq-elpi }: + +let + versions = { + "0.10.0" = { + rev = "v0.10.0"; + sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h"; + }; + }; + version = x: versions.${x} // {version = x;}; + params = { + "8.11" = version "0.10.0"; + "8.12" = version "0.10.0"; + }; + param = params.${coq.coq-version}; +in + +stdenv.mkDerivation rec { + name = "coq${coq.coq-version}-hierarchy-builder-${param.version}"; + + src = fetchFromGitHub { + owner = "math-comp"; + repo = "hierarchy-builder"; + inherit (param) rev sha256; + }; + + propagatedBuildInputs = [ coq-elpi ]; + buildInputs = [ coq coq.ocaml coq.ocamlPackages.elpi ]; + + installPhase = ''make -f Makefile.coq VFILES=structures.v COQLIB=$out/lib/coq/${coq.coq-version}/ install''; + + meta = { + description = "Coq plugin embedding ELPI."; + maintainers = [ stdenv.lib.maintainers.cohencyril ]; + license = stdenv.lib.licenses.lgpl21; + inherit (coq.meta) platforms; + inherit (src.meta) homepage; + }; + + passthru = { + compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/interval/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/interval/default.nix new file mode 100644 index 000000000000..e72fe7845c84 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/interval/default.nix @@ -0,0 +1,62 @@ +{ stdenv, fetchurl, which, coq, coquelicot, flocq, mathcomp +, bignums ? null }: + +let params = + let + v3_3 = { + version = "3.3.0"; + uid = "37077"; + sha256 = "08fdcf3hbwqphglvwprvqzgkg0qbimpyhnqsgv3gac4y1ap0f903"; + }; + v3_4 = { + version = "3.4.2"; + uid = "38288"; + sha256 = "00bgzbji0gkazwxhs4q8gz4ccqsa1y1r0m0ravr18ps2h8a8qva5"; + }; + v4_0 = { + version = "4.0.0"; + uid = "38339"; + sha256 = "19sbrv7jnzyxji7irfslhr9ralc0q3gx20nymig5vqbn3vssmgpz"; + }; + in { + "8.5" = v3_3; + "8.6" = v3_3; + "8.7" = v3_4; + "8.8" = v4_0; + "8.9" = v4_0; + "8.10" = v4_0; + "8.11" = v4_0; + "8.12" = v4_0; + }; + param = params."${coq.coq-version}"; +in + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-interval-${param.version}"; + + src = fetchurl { + url = "https://gforge.inria.fr/frs/download.php/file/${param.uid}/interval-${param.version}.tar.gz"; + inherit (param) sha256; + }; + + nativeBuildInputs = [ which ]; + buildInputs = [ coq ]; + propagatedBuildInputs = [ bignums coquelicot flocq ]; + + configurePhase = "./configure --libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Interval"; + buildPhase = "./remake"; + installPhase = "./remake install"; + + meta = with stdenv.lib; { + homepage = "http://coq-interval.gforge.inria.fr/"; + description = "Tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant"; + license = licenses.cecill-c; + maintainers = with maintainers; [ vbgl ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/iris/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/iris/default.nix new file mode 100644 index 000000000000..6826e07d613e --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/iris/default.nix @@ -0,0 +1,33 @@ +{ stdenv, fetchFromGitLab, coq, stdpp }: + +stdenv.mkDerivation rec { + version = "3.3.0"; + name = "coq${coq.coq-version}-iris-${version}"; + src = fetchFromGitLab { + domain = "gitlab.mpi-sws.org"; + owner = "iris"; + repo = "iris"; + rev = "iris-${version}"; + sha256 = "0az4gkp5m8sq0p73dlh0r7ckkzhk7zkg5bndw01bdsy5ywj0vilp"; + }; + + buildInputs = [ coq ]; + propagatedBuildInputs = [ stdpp ]; + + enableParallelBuilding = true; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + meta = { + homepage = "https://gitlab.mpi-sws.org/FP/iris-coq"; + description = "The Coq development of the Iris Project"; + inherit (coq.meta) platforms; + license = stdenv.lib.licenses.bsd3; + maintainers = [ stdenv.lib.maintainers.vbgl ]; + }; + + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.9" "8.10" "8.11" "8.12" ]; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/ltac2/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/ltac2/default.nix new file mode 100644 index 000000000000..92484f169c15 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/ltac2/default.nix @@ -0,0 +1,57 @@ +{ stdenv, fetchFromGitHub, which, coq }: + +let params = { + "8.7" = { + version = "0.1"; + rev = "v0.1-8.7"; + sha256 = "0l6wiwi4cvd0i324fb29i9mdh0ijlxzggw4mrjjy695l2qdnlgg0"; + }; + "8.8" = { + version = "0.1"; + rev = "0.1"; + sha256 = "1zz26cyv99whj7rrpgnhhm9dfqnpmrx5pqizn8ihf8jkq8d4drz7"; + }; + "8.9" = rec { + version = "0.2"; + rev = version; + sha256 = "0xby1kb26r9gcvk5511wqj05fqm9paynwfxlfqkmwkgnfmzk0x73"; + }; + "8.10" = rec { + version = "0.3"; + rev = version; + sha256 = "0pzs5nsakh4l8ffwgn4ryxbnxdv2x0r1i7bc598ij621haxdirrr"; + }; +}; + param = params.${coq.coq-version}; +in + +stdenv.mkDerivation rec { + inherit (param) version; + name = "coq${coq.coq-version}-ltac2-${version}"; + + src = fetchFromGitHub { + owner = "coq"; + repo = "ltac2"; + inherit (param) rev sha256; + }; + + nativeBuildInputs = [ which ]; + buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib ]) + ++ stdenv.lib.optional (!stdenv.lib.versionAtLeast coq.coq-version "8.10") + coq.ocamlPackages.camlp5 + ; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + meta = { + description = "A robust and expressive tactic language for Coq"; + maintainers = [ stdenv.lib.maintainers.vbgl ]; + license = stdenv.lib.licenses.lgpl21; + inherit (coq.meta) platforms; + inherit (src.meta) homepage; + }; + + passthru = { + compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/math-classes/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/math-classes/default.nix new file mode 100644 index 000000000000..73e420b326d9 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/math-classes/default.nix @@ -0,0 +1,30 @@ +{ stdenv, fetchFromGitHub, coq, bignums }: + +stdenv.mkDerivation rec { + + name = "coq${coq.coq-version}-math-classes-${version}"; + version = "8.11.0"; + + src = fetchFromGitHub { + owner = "coq-community"; + repo = "math-classes"; + rev = version; + sha256 = "1hjgncvm1m46lw6264w4dqsy8dbh74vhmzq52x0fba2yqlvy94sf"; + }; + + buildInputs = [ coq bignums ]; + enableParallelBuilding = true; + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + meta = with stdenv.lib; { + homepage = "https://math-classes.github.io"; + description = "A library of abstract interfaces for mathematical structures in Coq."; + maintainers = with maintainers; [ siddharthist jwiegley ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" ]; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/mathcomp/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/mathcomp/default.nix new file mode 100644 index 000000000000..8cf502a1943b --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/mathcomp/default.nix @@ -0,0 +1,263 @@ +############################# +# Main derivation: mathcomp # +######################################################################## +# This file mainly provides the `mathcomp` derivation, which is # +# essentially a meta-package containing all core mathcomp libraries # +# (ssreflect fingroup algebra solvable field character). They can be # +# accessed individually through the paththrough attributes of mathcomp # +# bearing the same names (mathcomp.ssreflect, etc). # +# # +# Do not use overrideAttrs, but overrideMathcomp instead, which # +# regenerate a full mathcomp derivation with sub-derivations, and # +# behave the same as `mathcomp_`, described below. # +######################################################################## + +############################################################ +# Compiling a custom version of mathcomp using `mathcomp_` # +############################################################################## +# The prefered way to compile a custom version of mathcomp (other than a # +# released version which should be added to `mathcomp-config-initial` # +# and pushed to nixpkgs), is to apply the function `coqPackages.mathcomp_` # +# to either: # +# - a string without slash, which is interpreted as a github revision, # +# i.e. either a tag, a branch or a commit hash # +# - a string with slashes "owner/p_1/.../p_n", which is interpreted as # +# github owner "owner" and revision "p_1/.../p_n". # +# - a path which is interpreted as a local source for the repository, # +# the name of the version is taken to be the basename of the path # +# i.e. if the path is /home/you/git/package/branch/, # +# then "branch" is the name of the version # +# - an attribute set which overrides some attributes (e.g. the src) # +# if the version is updated, the name is automatically regenerated using # +# the conventional schema "coq${coq.coq-version}-${pkgname}-${version}" # +# - a "standard" override function (old: new_attrs) to override the default # +# attribute set, so that you can use old.${field} to patch the derivation. # +############################################################################## + +######################################################################### +# Example of use: https://github.com/math-comp/math-comp/wiki/Using-nix # +######################################################################### + +################################# +# Adding a new mathcomp version # +############################################################################# +# When adding a new version of mathcomp, add an attribute to `sha256` (use # +# ```sh # +# nix-prefetch-url --unpack # +# https://github.com/math-comp/math-comp/archive/version.tar.gz # +# ``` # +# to get the corresponding `sha256`) and to `coq-version` (read the release # +# notes to check which versions of coq it is compatible with). Then add # +# it in `preference version`, if not all mathcomp-extra packages are # +# ready, you might want to give new release secondary priority. # +############################################################################# + + +{ stdenv, fetchFromGitHub, ncurses, which, graphviz, + recurseIntoAttrs, withDoc ? false, + coqPackages, + mathcomp_, mathcomp, mathcomp-config, +}: +with builtins // stdenv.lib; +let + mathcomp-config-initial = rec { + ####################################################################### + # CONFIGURATION (please edit this), it is exported as mathcomp-config # + ####################################################################### + # sha256 of released mathcomp versions + sha256 = { + "1.11.0" = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c"; + "1.11+beta1" = "12i3zznwajlihzpqsiqniv20rklj8d8401lhd241xy4s21fxkkjm"; + "1.10.0" = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv"; + "1.9.0" = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r"; + "1.8.0" = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp"; + "1.7.0" = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1"; + "1.6.1" = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i"; + }; + # versions of coq compatible with released mathcomp versions + coq-versions = { + "1.11.0" = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; + "1.11+beta1" = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; + "1.10.0" = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" ]; + "1.9.0" = flip elem [ "8.7" "8.8" "8.9" "8.10" ]; + "1.8.0" = flip elem [ "8.7" "8.8" "8.9" ]; + "1.7.0" = flip elem [ "8.6" "8.7" "8.8" "8.9" ]; + "1.6.1" = flip elem [ "8.5"]; + }; + + # sets the default version of mathcomp given a version of Coq + # this is currently computed using version-perference below + # but it can be set to a fixed version number + preferred-version = let v = head ( + filter (mc: mathcomp-config.coq-versions.${mc} coq.coq-version) + mathcomp-config.version-preferences ++ ["0.0.0"]); + in if v == "0.0.0" then head mathcomp-config.version-preferences else v; + + # mathcomp preferred versions by decreasing order + # (the first version in the list will be tried first) + version-preferences = + [ "1.10.0" "1.11.0" "1.9.0" "1.8.0" "1.7.0" "1.6.1" ]; + + # list of core mathcomp packages sorted by dependency order + packages = _version: # unused in current versions of mathcomp + # because the following list of packages is fixed for + # all versions of mathcomp up to 1.11.0 + [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ]; + + # compute the dependencies of the core package pkg + # (assuming the total ordering above, change if necessary) + deps = version: pkg: if pkg == "single" then [] else + (pred-split-list (x: x == pkg) (mathcomp-config.packages version)).left; + }; + + ############################################################## + # COMPUTED using the configuration above (edit with caution) # + ############################################################## + + # generic split function (TODO: move to lib?) + pred-split-list = pred: l: + let loop = v: l: if l == [] then {left = v; right = [];} + else let hd = builtins.head l; tl = builtins.tail l; in + if pred hd then {left = v; right = tl;} else loop (v ++ [hd]) tl; + in loop [] l; + + pkgUp = l: r: l // r // { + meta = (l.meta or {}) // (r.meta or {}); + passthru = (l.passthru or {}) // (r.passthru or {}); + }; + + coq = coqPackages.coq; + mathcomp-deps = mathcomp-config.deps mathcomp.config.preferred-version; + + # default set of attributes given a 'package' name. + # this attribute set will be extended using toOverrideFun + default-attrs = package: + let + pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}"; + pkgname = if package == "single" then "mathcomp" else "mathcomp-${package}"; + pkgallMake = '' + echo "all.v" > Make + echo "-I ." >> Make + echo "-R . mathcomp.all" >> Make + ''; + in + rec { + version = "master"; + name = "coq${coq.coq-version}-${pkgname}-${version}"; + + nativeBuildInputs = optionals withDoc [ graphviz ]; + buildInputs = [ ncurses which ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]); + propagatedBuildInputs = [ coq ]; + enableParallelBuilding = true; + + buildFlags = optional withDoc "doc"; + + COQBIN = "${coq}/bin/"; + + preBuild = '' + patchShebangs etc/utils/ssrcoqdep || true + cd ${pkgpath} + '' + optionalString (package == "all") pkgallMake; + + installPhase = '' + make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install + '' + optionalString withDoc '' + make -f Makefile.coq install-doc DOCDIR=$out/share/coq/${coq.coq-version}/ + ''; + + meta = with stdenv.lib; { + homepage = "https://math-comp.github.io/"; + license = licenses.cecill-b; + maintainers = [ maintainers.vbgl maintainers.jwiegley maintainers.cohencyril ]; + platforms = coq.meta.platforms; + }; + + passthru = { + mathcompDeps = mathcomp-deps package; + inherit package mathcomp-config; + compatibleCoqVersions = _: true; + }; + }; + + # converts a string, path or attribute set into an override function + toOverrideFun = overrides: + if isFunction overrides then overrides else old: + let + pkgname = if old.passthru.package == "single" then "mathcomp" + else "mathcomp-${old.passthru.package}"; + + string-attrs = if hasAttr overrides mathcomp-config.sha256 then + let version = overrides; + in { + inherit version; + src = fetchFromGitHub { + owner = "math-comp"; + repo = "math-comp"; + rev = "mathcomp-${version}"; + sha256 = mathcomp-config.sha256.${version}; + }; + passthru = old.passthru // { + compatibleCoqVersions = mathcomp-config.coq-versions.${version}; + mathcompDeps = mathcomp-config.deps version old.passthru.package; + }; + } + else + let splitted = filter isString (split "/" overrides); + owner = head splitted; + ref = concatStringsSep "/" (tail splitted); + version = head (reverseList splitted); + in if length splitted == 1 then { + inherit version; + src = fetchTarball "https://github.com/math-comp/math-comp/archive/${version}.tar.gz"; + } else { + inherit version; + src = fetchTarball "https://github.com/${owner}/math-comp/archive/${ref}.tar.gz"; + }; + + attrs = + if overrides == null || overrides == "" then _: {} + else if isString overrides then string-attrs + else if isPath overrides then { version = baseNameOf overrides; src = overrides; } + else if isAttrs overrides then pkgUp old overrides + else let overridesStr = toString overrides; in + abort "${overridesStr} not a legitimate overrides"; + in + attrs // (if attrs?version && ! (attrs?name) + then { name = "coq${coq.coq-version}-${pkgname}-${attrs.version}"; } else {}); + + # generates {ssreflect = «derivation ...» ; ... ; character = «derivation ...», ...} + mkMathcompGenSet = pkgs: o: + fold (pkg: pkgs: pkgs // {${pkg} = mkMathcompGen pkg o;}) {} pkgs; + # generates the derivation of one mathcomp package. + mkMathcompGen = package: overrides: + let + up = x: o: x // (toOverrideFun o x); + fixdeps = attrs: + let version = attrs.version or "master"; + mcdeps = if package == "single" then {} + else mkMathcompGenSet (filter isString attrs.passthru.mathcompDeps) overrides; + allmc = mkMathcompGenSet (mathcomp-config.packages version ++ [ "single" ]) overrides; + in { + propagatedBuildInputs = [ coq ] + ++ filter isDerivation attrs.passthru.mathcompDeps + ++ attrValues mcdeps + ; + passthru = allmc // + { overrideMathcomp = o: mathcomp_ (old: up (up old overrides) o); }; + }; + in + stdenv.mkDerivation (up (up (default-attrs package) overrides) fixdeps); +in +{ + mathcomp-config = mathcomp-config-initial; + mathcomp_ = mkMathcompGen "all"; + mathcomp = mathcomp_ mathcomp-config.preferred-version; + # mathcomp-single = mathcomp.single; + ssreflect = mathcomp.ssreflect; + mathcomp-ssreflect = mathcomp.ssreflect; + mathcomp-fingroup = mathcomp.fingroup; + mathcomp-algebra = mathcomp.algebra; + mathcomp-solvable = mathcomp.solvable; + mathcomp-field = mathcomp.field; + mathcomp-character = mathcomp.character; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/mathcomp/extra.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/mathcomp/extra.nix new file mode 100644 index 000000000000..6a2dfcda3456 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/mathcomp/extra.nix @@ -0,0 +1,391 @@ +########################################################## +# Main derivation: # +# mathcomp-finmap mathcomp-analysis mathcomp-bigenough # +# mathcomp-multinomials mathcomp-real-closed coqeal # +# Additionally: # +# mathcomp-extra-all contains all the extra packages # +# mathcomp-extra-fast contains the one not marked slow # +######################################################################## +# This file mainly provides the above derivations, which are packages # +# extra mathcomp libraries based on mathcomp. # +######################################################################## + +##################################################### +# Compiling customs versions using `mathcomp-extra` # +############################################################################## +# The prefered way to compile a custom version of mathcomp extra packages # +# (other than released versions which should be added to # +# `rec-mathcomp-extra-config` and pushed to nixpkgs, see below), # +# is to use `coqPackages.mathcomp-extra name version` where # +# 1. `name` is a string representing the name of a declared package # +# OR undeclared package. # +# 2. `version` is either: # +# - a string without slash, which is interpreted as a github revision, # +# i.e. either a tag, a branch or a commit hash # +# - a string with slashes "owner/p_1/.../p_n", which is interpreted as # +# github owner "owner" and revision "p_1/.../p_n". # +# - a path which is interpreted as a local source for the repository, # +# the name of the version is taken to be the basename of the path # +# i.e. if the path is /home/you/git/package/branch/, # +# then "branch" is the name of the version # +# - an attribute set which overrides some attributes (e.g. the src) # +# if the version is updated, the name is automatically regenerated using # +# the conventional schema "coq${coq.coq-version}-${pkgname}-${version}" # +# - a "standard" override function (old: new_attrs) to override the default # +# attribute set, so that you can use old.${field} to patch the derivation. # +# # +# Should you choose to use `pkg.overrideAttrs` instead, we provide the # +# function mathcomp-extra-override which takes a name and a version exactly # +# as above and returns an override function. # +############################################################################## + +######################################################################### +# Example of use: https://github.com/math-comp/math-comp/wiki/Using-nix # +######################################################################### + +########################################### +# Adding a new package or package version # +################################################################################ +# 1. Update or add a `package` entry to `initial`, it must be a function # +# taking the version as argument and returning an attribute set. Everything # +# is optional and the default for the sources of the repository and the # +# homepage will be https://github.com/math-comp/${package}. # +# # +# 2. Update or add a `package` entry to `sha256` for each release. # +# You may use # +# ```sh # +# nix-prefetch-url --unpack # +# https://github.com/math-comp/math-comp/archive/version.tar.gz # +# ``` # +# # +# 3. Update or create a new consistent set of extra packages. # +# /!\ They must all be co-compatible. /!\ # +# Do not use versions that may disappear: it must either be # +# - a tag from the main repository (e.g. version or tag), or # +# - a revision hash that has been *merged in master* # +################################################################################ + +{ stdenv, fetchFromGitHub, recurseIntoAttrs, + which, mathcomp, coqPackages, + mathcomp-extra-config, mathcomp-extra-override, + mathcomp-extra, current-mathcomp-extra, +}: +with builtins // stdenv.lib; +let + ############################## + # CONFIGURATION, please edit # + ############################## + ############################ + # Packages base delaration # + ############################ + rec-mathcomp-extra-config = { + initial = { + mathcomp-finmap = {version, coqPackages}: { + meta = { + description = "A finset and finmap library"; + repo = "finmap"; + homepage = "https://github.com/math-comp/finmap"; + }; + passthru.compatibleCoqVersions = flip elem [ "8.8" "8.9" "8.10" "8.11" ]; + }; + + mathcomp-bigenough = {version, coqPackages}: { + meta = { + description = "A small library to do epsilon - N reasonning"; + repo = "bigenough"; + homepage = "https://github.com/math-comp/bigenough"; + }; + passthru.compatibleCoqVersions = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" ]; + }; + + multinomials = {version, coqPackages}: { + buildInputs = [ which ]; + propagatedBuildInputs = with coqPackages; + [ mathcomp.algebra mathcomp-finmap mathcomp-bigenough ]; + meta = { + description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials"; + repo = "multinomials"; + homepage = "https://github.com/math-comp/multinomials"; + }; + passthru.compatibleCoqVersions = flip elem [ "8.9" "8.10" "8.11" ]; + }; + + mathcomp-analysis = {version, coqPackages}: { + propagatedBuildInputs = with coqPackages; + [ mathcomp.field mathcomp-finmap mathcomp-bigenough mathcomp-real-closed ]; + meta = { + description = "Analysis library compatible with Mathematical Components"; + homepage = "https://github.com/math-comp/analysis"; + repo = "analysis"; + license = stdenv.lib.licenses.cecill-c; + }; + passthru.compatibleCoqVersions = flip elem ["8.8" "8.9" "8.10" "8.11" ]; + }; + + mathcomp-real-closed = {version, coqPackages}: { + propagatedBuildInputs = with coqPackages; + [ mathcomp.field mathcomp-bigenough ]; + meta = { + description = "Mathematical Components Library on real closed fields"; + repo = "real-closed"; + homepage = "https://github.com/math-comp/real-closed"; + }; + passthru.compatibleCoqVersions = flip elem ["8.8" "8.9" "8.10" "8.11" ]; + }; + + coqeal = {version, coqPackages}: { + buildInputs = [ which ]; + propagatedBuildInputs = with coqPackages; + [ mathcomp-algebra bignums paramcoq multinomials ]; + meta = { + description = "CoqEAL - The Coq Effective Algebra Library"; + homepage = "https://github.com/coqeal/coqeal"; + license = stdenv.lib.licenses.mit; + owner = "CoqEAL"; + }; + passthru.compatibleCoqVersions = flip elem [ "8.9" "8.10" "8.11" ]; + }; + }; + + ############################### + # sha256 of released versions # + ############################### + sha256 = { + mathcomp-finmap = { + "1.5.0" = "0vx9n1fi23592b3hv5p5ycy7mxc8qh1y5q05aksfwbzkk5zjkwnq"; + "1.4.1" = "0kx4nx24dml1igk0w0qijmw221r5bgxhwhl5qicnxp7ab3c35s8p"; + "1.4.0+coq-8.11" = "1fd00ihyx0kzq5fblh9vr8s5mr1kg7p6pk11c4gr8svl1n69ppmb"; + "1.4.0" = "0mp82mcmrs424ff1vj3cvd8353r9vcap027h3p0iprr1vkkwjbzd"; + "1.3.4" = "0f5a62ljhixy5d7gsnwd66gf054l26k3m79fb8nz40i2mgp6l9ii"; + "1.3.3" = "1n844zjhv354kp4g4pfbajix0plqh7yxv6471sgyb46885298am5"; + "1.3.1" = "14rvm0rm5hd3pd0srgak3jqmddzfv6n7gdpjwhady5xcgrc7gsx7"; + "1.2.1" = "0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf"; + "1.2.0" = "0b6wrdr0d7rcnv86s37zm80540jl2wmiyf39ih7mw3dlwli2cyj4"; + "1.1.0" = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a"; + "1.0.0" = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa"; + }; + mathcomp-bigenough = { + "1.0.0" = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg"; + }; + mathcomp-analysis = { + "0.3.1" = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8"; + "0.3.0" = "03klwi4fja0cqb4myp3kgycfbmdv00bznmxf8yg3zzzzw997hjqc"; + "0.2.3" = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966"; + "0.2.2" = "1d5dwg9di2ppdzfg21zr0a691zigb5kz0lcw263jpyli1nrq7cvk"; + "0.2.0" = "1186xjxgns4ns1szyi931964bjm0mp126qzlv10mkqqgfw07nhrd"; + "0.1.0" = "0hwkr2wzy710pcyh274fcarzdx8sv8myp16pv0vq5978nmih46al"; + }; + multinomials = { + "1.5.2" = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s"; + "1.5.1" = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3"; + "1.5" = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw"; + "1.4" = "0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p"; + "1.3" = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4"; + "1.2" = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq"; + "1.1" = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s"; + "1.0" = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m"; + }; + mathcomp-real-closed = { + "1.1.1" = "0ksjscrgq1i79vys4zrmgvzy2y4ylxa8wdsf4kih63apw6v5ws6b"; + "1.1.0" = "0zgfmrlximw77bw5w6w0xg2nampp02pmrwnrzx8m1n5pqljnv8fh"; + "1.0.5" = "0q8nkxr9fba4naylr5xk7hfxsqzq2pvwlg1j0xxlhlgr3fmlavg2"; + "1.0.4" = "058v9dj973h9kfhqmvcy9a6xhhxzljr90cf99hdfcdx68fi2ha1b"; + "1.0.3" = "1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb"; + "1.0.2" = "0097pafwlmzd0gyfs31bxpi1ih04i72nxhn99r93aj20mn7mcsgl"; + "1.0.1" = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg"; + }; + coqeal = { + "1.0.4" = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk"; + "1.0.3" = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24"; + "1.0.2" = "1brmf3gj03iky1bcl3g9vx8vknny7xfvs0y2rfr85am0296sxsfj"; + "1.0.1" = "19jhdrv2yp9ww0h8q73ihb2w1z3glz4waf2d2n45klafxckxi7bm"; + "1.0.0" = "1had6f1n85lmh9x31avbmgl3m0rsiw9f8ma95qzk5b57fjg5k1ii"; + }; + }; + + ################################ + # CONSISTENT sets of packages. # + ################################ + for-coq-and-mc = let + v6 = { + mathcomp-finmap = "1.5.0"; + mathcomp-bigenough = "1.0.0"; + mathcomp-analysis = "0.3.1"; + multinomials = "1.5.2"; + mathcomp-real-closed = "1.1.1"; + coqeal = "1.0.4"; + }; + v5 = { + mathcomp-finmap = "1.5.0"; + mathcomp-bigenough = "1.0.0"; + mathcomp-analysis = "0.3.0"; + multinomials = "1.5.1"; + mathcomp-real-closed = "1.0.5"; + coqeal = "1.0.4"; + }; + v4 = v3 // { coqeal = "1.0.3"; }; + v3 = { + mathcomp-finmap = "1.4.0"; + mathcomp-bigenough = "1.0.0"; + mathcomp-analysis = "0.2.3"; + multinomials = "1.5"; + mathcomp-real-closed = "1.0.4"; + coqeal = "1.0.0"; + }; + v2 = { + mathcomp-finmap = "1.3.4"; + mathcomp-bigenough = "1.0.0"; + mathcomp-analysis = "0.2.3"; + multinomials = "1.4"; + mathcomp-real-closed = "1.0.3"; + coqeal = "1.0.0"; + }; + v1 = { + mathcomp-finmap = "1.1.0"; + mathcomp-bigenough = "1.0.0"; + multinomials = "1.1"; + mathcomp-real-closed = "1.0.1"; + coqeal = "1.0.0"; + }; + in + { + "8.11" = { + "1.11.0" = v6; + "1.11+beta1" = v5; + "1.10.0" = v4 // {mathcomp-finmap = "1.4.0+coq-8.11";}; + }; + "8.10" = { + "1.11.0" = removeAttrs v6 ["coqeal"]; + "1.11+beta1" = removeAttrs v5 ["coqeal"]; + "1.10.0" = v4; + "1.9.0" = removeAttrs v3 ["coqeal"]; + }; + "8.9" = { + "1.11.0" = removeAttrs v6 ["mathcomp-analysis"]; + "1.11+beta1" = removeAttrs v5 ["mathcomp-analysis"]; + "1.10.0" = v4; + "1.9.0" = removeAttrs v3 ["coqeal"]; + "1.8.0" = removeAttrs v2 ["coqeal"]; + }; + "8.8" = { + "1.11.0" = removeAttrs v6 ["mathcomp-analysis"]; + "1.11+beta1" = removeAttrs v5 ["mathcomp-analysis"]; + "1.10.0" = removeAttrs v4 ["mathcomp-analysis"]; + "1.9.0" = removeAttrs v3 ["coqeal"]; + "1.8.0" = removeAttrs v2 ["coqeal"]; + "1.7.0" = removeAttrs v1 ["coqeal" "multinomials"]; + }; + "8.7" = { + "1.11.0" = removeAttrs v6 ["mathcomp-analysis"]; + "1.11+beta1" = removeAttrs v5 ["mathcomp-analysis"]; + "1.10.0" = removeAttrs v4 ["mathcomp-analysis"]; + "1.9.0" = removeAttrs v3 ["coqeal" "mathcomp-analysis"]; + "1.8.0" = removeAttrs v2 ["coqeal" "mathcomp-analysis"]; + "1.7.0" = removeAttrs v1 ["coqeal" "multinomials"]; + }; + }; + }; + + ############################## + # GENERATION, EDIT WITH CARE # + ############################## + coq = coqPackages.coq; + + default-attrs = { + version = "master"; + buildInputs = []; + propagatedBuildInputs = (with coqPackages; [ ssreflect ]); + installFlags = [ "-f" "Makefile.coq" "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + meta = { + inherit (mathcomp.meta) platforms license; + owner = "math-comp"; + maintainers = [ maintainers.vbgl maintainers.cohencyril ]; + }; + passthru.compatibleCoqVersions = (_: true); + }; + + pkgUp = recursiveUpdateUntil (path: l: r: !(isAttrs l && isAttrs r) || path == ["src"]); + + # Fixes a partial attribute set using the configuration + # in the style of the above mathcomp-extra-config.initial, + # and generates a name according to the conventional naming scheme below + fix-attrs = pkgcfg: + let attrs = pkgUp default-attrs pkgcfg; in + pkgUp attrs (rec { + name = "coq${coq.coq-version}mathcomp${mathcomp.version}-${attrs.meta.repo or attrs.meta.package or "anonymous"}-${attrs.version}"; + src = attrs.src or (fetchTarball "${meta.homepage}/archive/${attrs.version}.tar.gz"); + meta = rec { + homepage = attrs.meta.homepage or attrs.src.meta.homepage or "https://github.com/${owner}/${repo}"; + owner = attrs.meta.owner or "math-comp"; + repo = attrs.meta.repo or attrs.meta.package or "math-comp-nix"; + }; + }); + + # Gets a version out of a string, path or attribute set. + getVersion = arg: + if isFunction arg then (arg {}).version + else if arg == "" then "master" + else if isDerivation arg then arg.drvAttrs.version or "master" + else if isAttrs arg then arg.version or "master" + else if isString arg then head (reverseList (split "/" arg)) + else if isPath arg then (baseNameOf arg) + else "master"; + + # Converts a string, path or attribute set into an override function + # It tries to fill the `old` argument of the override function using + # `mathcomp-extra-config.initial` first and finishes with `fix-attrs` + rec-mathcomp-extra-override = generic: old: let + version = getVersion generic; + package = old.meta.package or "math-comp-nix"; + cfg = pkgUp ((mathcomp-extra-config.initial.${package} or (_: {})) + { inherit version coqPackages; }) old + // { inherit version; }; + fix = attrs: fix-attrs (pkgUp cfg attrs); + in + if isFunction generic then fix (generic cfg) + else if generic == null || generic == "" then fix {} + else if isDerivation generic then generic.drvAttrs + else if isAttrs generic then fix generic + else if generic == "broken" then fix { meta.broken = true; passthru.compatibleCoqVersions = _: false; } + else let fixedcfg = fix cfg; in fixedcfg // ( + if isString generic then + if (mathcomp-extra-config.sha256.${package} or {})?${generic} then { + src = fetchFromGitHub { + inherit (fixedcfg.meta) owner repo; + rev = version; + sha256 = mathcomp-extra-config.sha256.${package}.${version}; + }; + } + else let splitted = filter isString (split "/" generic); in { + src = fetchTarball + ("https://github.com/" + + (if length splitted == 1 then "${fixedcfg.meta.owner}/${fixedcfg.meta.repo}/archive/${version}.tar.gz" + else "${head splitted}/${fixedcfg.meta.repo}/archive/${concatStringsSep "/" (tail splitted)}.tar.gz")); + } + else if isPath generic then { src = generic; } + else abort "${toString generic} not a legitimate generic version/override"); + + # applies mathcomp-extra-config.for-coq-and-mc to the current mathcomp version + for-this = mathcomp-extra-config.for-coq-and-mc.${coq.coq-version}.${mathcomp.version} or {}; + + # specializes mathcomp-extra to the current mathcomp version. + rec-current-mathcomp-extra = package: mathcomp-extra package (for-this.${package} or {}); +in + { + mathcomp-extra-override = rec-mathcomp-extra-override; + mathcomp-extra-config = rec-mathcomp-extra-config; + current-mathcomp-extra = rec-current-mathcomp-extra; + mathcomp-extra = package: version: + stdenv.mkDerivation (mathcomp-extra-override version {meta = {inherit package;};}); + + mathcomp-finmap = current-mathcomp-extra "mathcomp-finmap"; + mathcomp-analysis = current-mathcomp-extra "mathcomp-analysis"; + mathcomp-bigenough = current-mathcomp-extra "mathcomp-bigenough"; + multinomials = current-mathcomp-extra "multinomials"; + mathcomp-real-closed = current-mathcomp-extra "mathcomp-real-closed"; + coqeal = current-mathcomp-extra "coqeal"; + + mathcomp-extra-fast = map current-mathcomp-extra + (attrNames (filterAttrs (pkg: config: !(config?slow && config.slow)) for-this)); + mathcomp-extra-all = map current-mathcomp-extra (attrNames for-this); + } diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/metalib/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/metalib/default.nix new file mode 100644 index 000000000000..862184c1460c --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/metalib/default.nix @@ -0,0 +1,33 @@ +{ stdenv, fetchFromGitHub, coq }: + +stdenv.mkDerivation rec { + name = "coq${coq.coq-version}-metalib-${version}"; + version = "20200527"; + + src = fetchFromGitHub { + owner = "plclub"; + repo = "metalib"; + rev = "597fd7d0c93eb159274e84a39d554f10f1efccf8"; + sha256 = "0wbypc05d2lqfm9qaw98ynr5yc1p0ipsvyc3bh1rk9nz7zwirmjs"; + }; + + sourceRoot = "source/Metalib"; + + buildInputs = [ coq ]; + + enableParallelBuilding = true; + + installFlags = "COQMF_COQLIB=$(out)/lib/coq/${coq.coq-version}"; + + meta = with stdenv.lib; { + homepage = "https://github.com/plclub/metalib"; + license = licenses.mit; + maintainers = [ maintainers.jwiegley ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.10" "8.11" "8.12" ]; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/paco/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/paco/default.nix new file mode 100644 index 000000000000..ac6eef2f3bd0 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/paco/default.nix @@ -0,0 +1,60 @@ +{stdenv, fetchFromGitHub, coq, unzip}: + +let + versions = { + pre_8_6 = rec { + rev = "v${version}"; + version = "1.2.8"; + sha256 = "05fskx5x1qgaf9qv626m38y5izichzzqc7g2rglzrkygbskrrwsb"; + }; + post_8_6 = rec { + rev = "v${version}"; + version = "4.0.2"; + sha256 = "1q96bsxclqx84xn5vkid501jkwlc1p6fhb8szrlrp82zglj58b0b"; + }; + }; + params = { + "8.5" = versions.pre_8_6; + "8.6" = versions.post_8_6; + "8.7" = versions.post_8_6; + "8.8" = versions.post_8_6; + "8.9" = versions.post_8_6; + "8.10" = versions.post_8_6; + "8.11" = versions.post_8_6; + "8.12" = versions.post_8_6; + }; + param = params.${coq.coq-version}; +in + +stdenv.mkDerivation rec { + inherit (param) version; + name = "coq${coq.coq-version}-paco-${version}"; + + src = fetchFromGitHub { + inherit (param) rev sha256; + owner = "snu-sf"; + repo = "paco"; + }; + + buildInputs = [ coq ]; + + preBuild = "cd src"; + + installPhase = '' + COQLIB=$out/lib/coq/${coq.coq-version}/ + mkdir -p $COQLIB/user-contrib/Paco + cp -pR *.vo $COQLIB/user-contrib/Paco + ''; + + meta = with stdenv.lib; { + homepage = "http://plv.mpi-sws.org/paco/"; + description = "A Coq library implementing parameterized coinduction"; + maintainers = with maintainers; [ jwiegley ptival ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/paramcoq/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/paramcoq/default.nix new file mode 100644 index 000000000000..12d65bdb3d7b --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/paramcoq/default.nix @@ -0,0 +1,58 @@ +{ stdenv, fetchFromGitHub, coq }: + +let params = + { + "8.7" = { + sha256 = "09n0ky7ldb24by7yf5j3hv410h85x50ksilf7qacl7xglj4gy5hj"; + buildInputs = [ coq.ocamlPackages.camlp5 ]; + }; + "8.8" = { + sha256 = "0rc4lshqvnfdsph98gnscvpmlirs9wx91qcvffggg73xw0p1g9s0"; + buildInputs = [ coq.ocamlPackages.camlp5 ]; + }; + "8.9" = { + sha256 = "1jjzgpff09xjn9kgp7w69r096jkj0x2ksng3pawrmhmn7clwivbk"; + buildInputs = [ coq.ocamlPackages.camlp5 ]; + }; + "8.10" = { + sha256 = "1lq1mw15w4yky79qg3rm0mpzqi2ir51b6ak04ismrdr7ixky49y8"; + }; + "8.11" = { + sha256 = "09c6813988nvq4fpa45s33k70plnhxsblhm7cxxkg0i37mhvigsa"; + }; + "8.12" = { + sha256 = "0qd72r45if4h7c256qdfiimv75zyrs0w0xqij3m866jxaq591v4i"; + }; + }; + param = params.${coq.coq-version}; +in + +stdenv.mkDerivation rec { + version = "1.1.2"; + name = "coq${coq.coq-version}-paramcoq-${version}"; + src = fetchFromGitHub { + owner = "coq-community"; + repo = "paramcoq"; + rev = "v${version}+coq${coq.coq-version}"; + inherit (param) sha256; + }; + + buildInputs = [ coq ] + ++ (with coq.ocamlPackages; [ ocaml findlib ]) + ++ (param.buildInputs or []) + ; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + passthru = { + compatibleCoqVersions = v: builtins.hasAttr v params; + }; + + meta = { + description = "Coq plugin for parametricity"; + inherit (src.meta) homepage; + license = stdenv.lib.licenses.mit; + maintainers = [ stdenv.lib.maintainers.vbgl ]; + inherit (coq.meta) platforms; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/simple-io/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/simple-io/default.nix new file mode 100644 index 000000000000..82fa215ee9ca --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/simple-io/default.nix @@ -0,0 +1,34 @@ +{ stdenv, fetchFromGitHub, coq, coq-ext-lib }: + +stdenv.mkDerivation rec { + version = "1.3.0"; + name = "coq${coq.coq-version}-simple-io-${version}"; + src = fetchFromGitHub { + owner = "Lysxia"; + repo = "coq-simple-io"; + rev = version; + sha256 = "1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax"; + }; + + buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml ocamlbuild ]); + + propagatedBuildInputs = [ coq-ext-lib ]; + + doCheck = true; + checkTarget = "test"; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + meta = { + description = "Purely functional IO for Coq"; + inherit (src.meta) homepage; + inherit (coq.meta) platforms; + license = stdenv.lib.licenses.mit; + maintainers = [ stdenv.lib.maintainers.vbgl ]; + }; + + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/stdpp/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/stdpp/default.nix new file mode 100644 index 000000000000..28917e73f29f --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/stdpp/default.nix @@ -0,0 +1,32 @@ +{ stdenv, fetchFromGitLab, coq }: + +stdenv.mkDerivation rec { + name = "coq${coq.coq-version}-stdpp-${version}"; + version = "1.4.0"; + src = fetchFromGitLab { + domain = "gitlab.mpi-sws.org"; + owner = "iris"; + repo = "stdpp"; + rev = "coq-stdpp-${version}"; + sha256 = "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r"; + }; + + buildInputs = [ coq ]; + + enableParallelBuilding = true; + + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + meta = { + inherit (src.meta) homepage; + description = "An extended “Standard Library” for Coq"; + inherit (coq.meta) platforms; + license = stdenv.lib.licenses.bsd3; + maintainers = [ stdenv.lib.maintainers.vbgl ]; + }; + + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.8" "8.9" "8.10" "8.11" "8.12" ]; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/development/coq-modules/tlc/default.nix b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/tlc/default.nix new file mode 100644 index 000000000000..816b22050244 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/development/coq-modules/tlc/default.nix @@ -0,0 +1,41 @@ +{ stdenv, fetchurl, fetchFromGitHub, coq }: + +let params = + if stdenv.lib.versionAtLeast coq.coq-version "8.10" + then rec { + version = "20200328"; + src = fetchFromGitHub { + owner = "charguer"; + repo = "tlc"; + rev = version; + sha256 = "16vzild9gni8zhgb3qhmka47f8zagdh03k6nssif7drpim8233lx"; + }; + } else rec { + version = "20181116"; + src = fetchurl { + url = "http://tlc.gforge.inria.fr/releases/tlc-${version}.tar.gz"; + sha256 = "0iv6f6zmrv2lhq3xq57ipmw856ahsql754776ymv5wjm88ld63nm"; + }; + } +; in + +stdenv.mkDerivation { + inherit (params) version src; + pname = "coq${coq.coq-version}-tlc"; + + buildInputs = [ coq ]; + + installFlags = [ "CONTRIB=$(out)/lib/coq/${coq.coq-version}/user-contrib" ]; + + meta = { + homepage = "http://www.chargueraud.org/softs/tlc/"; + description = "A non-constructive library for Coq"; + license = stdenv.lib.licenses.free; + maintainers = [ stdenv.lib.maintainers.vbgl ]; + inherit (coq.meta) platforms; + }; + + passthru = { + compatibleCoqVersions = stdenv.lib.flip builtins.elem [ "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; + }; +} |