From 101e907d2e999eaaa2d7fc6bcacadd6c502a55cc Mon Sep 17 00:00:00 2001 From: Ingo Blechschmidt Date: Wed, 6 Jan 2021 17:51:04 +0100 Subject: [PATCH 01/22] libbladeRF: unbreak the build (closing #108585) --- pkgs/development/libraries/libbladeRF/default.nix | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/pkgs/development/libraries/libbladeRF/default.nix b/pkgs/development/libraries/libbladeRF/default.nix index b2853011b140..e9ef0af463b3 100644 --- a/pkgs/development/libraries/libbladeRF/default.nix +++ b/pkgs/development/libraries/libbladeRF/default.nix @@ -1,4 +1,4 @@ -{ stdenv, lib, fetchFromGitHub, pkgconfig, cmake, git, doxygen, help2man, ncurses, tecla +{ stdenv, lib, fetchFromGitHub, fetchpatch, pkgconfig, cmake, git, doxygen, help2man, ncurses, tecla , libusb1, udev }: let @@ -23,6 +23,15 @@ in stdenv.mkDerivation { sha256 = "0g89al4kwfbx1l3zjddgb9ay4mhr7zk0ndchca3sm1vq2j47nf4l"; }; + # This patch is required for version 2.2.1. As the patch is already part of + # upstream master, it will be incorporated into the next release. The patch + # fixes a (well-justified) compiler warning which breaks the build because + # we compile with -Werror. + patches = [ (fetchpatch { + url = "https://github.com/Nuand/bladeRF/commit/163425d48a3b7d8c100d7295220d3648c050d0dd.patch"; + sha256 = "1swsymlyxm3yk2k8l71z1fv0a5k2rmab02f0c7xkrvk683mq6yxw"; + }) ]; + nativeBuildInputs = [ pkgconfig ]; # ncurses used due to https://github.com/Nuand/bladeRF/blob/ab4fc672c8bab4f8be34e8917d3f241b1d52d0b8/host/utilities/bladeRF-cli/CMakeLists.txt#L208 buildInputs = [ cmake git doxygen help2man tecla libusb1 ] From 245e149a4510a49fb0d270e87a3655818ff34bd9 Mon Sep 17 00:00:00 2001 From: "\"David Terry\"" <"me@xwvvvvwx.com"> Date: Thu, 7 Jan 2021 23:28:52 +0100 Subject: [PATCH 02/22] vimPlugins: update --- pkgs/misc/vim-plugins/generated.nix | 172 ++++++++++++++-------------- 1 file changed, 86 insertions(+), 86 deletions(-) diff --git a/pkgs/misc/vim-plugins/generated.nix b/pkgs/misc/vim-plugins/generated.nix index 4f24e88ca9e6..7f844838102d 100644 --- a/pkgs/misc/vim-plugins/generated.nix +++ b/pkgs/misc/vim-plugins/generated.nix @@ -65,12 +65,12 @@ let ale = buildVimPluginFrom2Nix { pname = "ale"; - version = "2021-01-05"; + version = "2021-01-06"; src = fetchFromGitHub { owner = "dense-analysis"; repo = "ale"; - rev = "7e4c125d38181a0e0d0c7883091e2fe683243ce4"; - sha256 = "0ngmcdbsqxjc00c1jab0h3dic5q1l781bhih30m5xx8qylqhf4g2"; + rev = "4c454c96a9d142475b155a94cc24fad34eca26b2"; + sha256 = "0xjacj8pw25qrzasgiwpisrc2fbh4k7ljpn1pq07z2h756cn54lf"; }; meta.homepage = "https://github.com/dense-analysis/ale/"; }; @@ -233,12 +233,12 @@ let barbar-nvim = buildVimPluginFrom2Nix { pname = "barbar-nvim"; - version = "2020-12-28"; + version = "2021-01-05"; src = fetchFromGitHub { owner = "romgrk"; repo = "barbar.nvim"; - rev = "383ffc0712c71481a068e49430321366c53585f2"; - sha256 = "14s42n4nl94nygszihgji01dwviw1ykqylpm2akdgfhwv1nz1ljn"; + rev = "e0b4935d5956025ab595195d935a5bac00f1a973"; + sha256 = "0h723j5zhj8mzwghykd84rxdr0l4ngvyy692d6sl2zz940mvwlkw"; }; meta.homepage = "https://github.com/romgrk/barbar.nvim/"; }; @@ -293,12 +293,12 @@ let brainfuck-vim = buildVimPluginFrom2Nix { pname = "brainfuck-vim"; - version = "2021-01-04"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "fruit-in"; repo = "brainfuck-vim"; - rev = "4b85810e1e826dcbb9a38122d4c52e85e470e81a"; - sha256 = "1q25w1v7kimq0cnjk8afy8ackfshhs25ra8w11l7qra3lrxkwj9b"; + rev = "ada4fce239ab5386aee51a9453cb0fafc7c2626d"; + sha256 = "1mm82m7p3khykd1fkag4ppvf2xgnqj8jbhdq7gq06ys1wxzw9rhj"; }; meta.homepage = "https://github.com/fruit-in/brainfuck-vim/"; }; @@ -497,12 +497,12 @@ let coc-nvim = buildVimPluginFrom2Nix { pname = "coc-nvim"; - version = "2021-01-04"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "neoclide"; repo = "coc.nvim"; - rev = "5b4b18d2ed2b18870034c7ee853164e1274ab158"; - sha256 = "0bgprss79nbwc3wd8yi0j90prxmh8saxswfpvpp3x8hilvwiyrrq"; + rev = "5b8af3eaee714f2c390f2f8e83ea47b78d24eab8"; + sha256 = "1x088m180wk6b0gk1xdw8crmrhp7s05yshj8nigqyhafm589a7vf"; }; meta.homepage = "https://github.com/neoclide/coc.nvim/"; }; @@ -798,12 +798,12 @@ let defx-nvim = buildVimPluginFrom2Nix { pname = "defx-nvim"; - version = "2021-01-05"; + version = "2021-01-06"; src = fetchFromGitHub { owner = "Shougo"; repo = "defx.nvim"; - rev = "f44e9486509482ae20c785d39be05581c3dbad15"; - sha256 = "1s1qmn5v3ghy79da03pf805zdg8j5w0ybri3z36fr2y5s9k7mj4d"; + rev = "6bf297376aa9ad76500778081ed2ff92fef72301"; + sha256 = "0k0iyvyg1cbalml1sv8vvs47k4af8vvz0gk6vba6yzjf72v6vj2d"; }; meta.homepage = "https://github.com/Shougo/defx.nvim/"; }; @@ -1088,12 +1088,12 @@ let deoplete-nvim = buildVimPluginFrom2Nix { pname = "deoplete-nvim"; - version = "2020-12-24"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "Shougo"; repo = "deoplete.nvim"; - rev = "b098a5286e95c456d91eed3589a2850aae421219"; - sha256 = "0y2ijzyn8jqpx5dkbglpa4ivsz6yml49xby7bbz6675rlcawlsq9"; + rev = "028ebd60d5ad963bf8f77e13c2a85e9edb190f48"; + sha256 = "0qy6knv5c4v568lvz3fh3ca2lcaym19hi0ywwvj6xyrllil2kk4b"; }; meta.homepage = "https://github.com/Shougo/deoplete.nvim/"; }; @@ -1294,12 +1294,12 @@ let fern-vim = buildVimPluginFrom2Nix { pname = "fern-vim"; - version = "2021-01-04"; + version = "2021-01-06"; src = fetchFromGitHub { owner = "lambdalisue"; repo = "fern.vim"; - rev = "9783dff6ac69c4e99b78807b08912c4c34100e22"; - sha256 = "141bifgf06bi43blw6wz7bdsb9l52iqxm9v7b609y49cz71z7n2c"; + rev = "591e2001fe0546ba28cc7dd614c40f5d92050f92"; + sha256 = "0cwzsqfyj4bk8f3y9aw9rmfx99gg760apkj7ppww14drc6lzfq09"; }; meta.homepage = "https://github.com/lambdalisue/fern.vim/"; }; @@ -1403,12 +1403,12 @@ let fzf-vim = buildVimPluginFrom2Nix { pname = "fzf-vim"; - version = "2020-12-30"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "junegunn"; repo = "fzf.vim"; - rev = "811b8607c653afe365bb97e6568501b0ad498017"; - sha256 = "16g0p2gadbw22qlsqrla3nv4a1bipzj00j4qsr2nb2ci13c1831z"; + rev = "d43df0ea2f099836c2e3499756101e87bcbd3e25"; + sha256 = "1hclx6c476i523qa5r27r2jbdfdrlbgan1j7aczzwgj3lahbdlvx"; }; meta.homepage = "https://github.com/junegunn/fzf.vim/"; }; @@ -1872,12 +1872,12 @@ let julia-vim = buildVimPluginFrom2Nix { pname = "julia-vim"; - version = "2020-12-07"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "JuliaEditorSupport"; repo = "julia-vim"; - rev = "e14fd34409de39025af93873adc6d26a831d70f9"; - sha256 = "1s1n74dn53aww6mjb87jcjpmipk2k2ayimimss7kg9c6n15jkqkg"; + rev = "ce48f42f1fd1d4566503ae26307026c895905a10"; + sha256 = "08yk47pvyh550iqv6zvrxcjdinn0w9p5al1v49m7p49jfqck3h1m"; }; meta.homepage = "https://github.com/JuliaEditorSupport/julia-vim/"; }; @@ -2016,24 +2016,24 @@ let lh-brackets = buildVimPluginFrom2Nix { pname = "lh-brackets"; - version = "2021-01-04"; + version = "2021-01-06"; src = fetchFromGitHub { owner = "LucHermitte"; repo = "lh-brackets"; - rev = "7af393f8212759aaea2d2721855fb2f46345ba3e"; - sha256 = "0wzd1q26bd6b6adaxn9vnr0xd2l8sk73av0b35ga3yv9kfr2j4qb"; + rev = "547fc9ab14ecf6ecc0d81e8bbb1cc1fec314b6aa"; + sha256 = "0344ap5fkp1d0g91rv9pn0p28xqz8as48d3m6kxc99w229sj6p2q"; }; meta.homepage = "https://github.com/LucHermitte/lh-brackets/"; }; lh-vim-lib = buildVimPluginFrom2Nix { pname = "lh-vim-lib"; - version = "2020-11-19"; + version = "2021-01-06"; src = fetchFromGitHub { owner = "LucHermitte"; repo = "lh-vim-lib"; - rev = "0edb04acd77b9e5e498314b6345d422d93921ffa"; - sha256 = "1cndwbwx9pg6550k7j2z0pw91dll0idspd0jpd0kycpxm4330jy9"; + rev = "65614730a667144a444fbd4a028a81171481c537"; + sha256 = "1vxm3ym51qa63zbrkdz2pvwafr3kmdxgpxrdwb1g8i7qsxjsvgl1"; }; meta.homepage = "https://github.com/LucHermitte/lh-vim-lib/"; }; @@ -2640,12 +2640,12 @@ let nlua-nvim = buildVimPluginFrom2Nix { pname = "nlua-nvim"; - version = "2020-11-16"; + version = "2021-01-05"; src = fetchFromGitHub { owner = "tjdevries"; repo = "nlua.nvim"; - rev = "92fdfb1eb791e79ff1d6403dd26b59ce61dd09c6"; - sha256 = "1ka8k8rxn406glrc0qz8rk3zrxhpdaky040v1a65g5alb50af9hz"; + rev = "c0e8fbcaf8bcf5571a9e1d780a72094aad3f3094"; + sha256 = "0q5aw3n4dsszk5iw7qg01xx1rbrr18jh1wqs6k9dd1kcr6yq22rq"; }; meta.homepage = "https://github.com/tjdevries/nlua.nvim/"; }; @@ -2772,12 +2772,12 @@ let nvim-lspconfig = buildVimPluginFrom2Nix { pname = "nvim-lspconfig"; - version = "2021-01-04"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "neovim"; repo = "nvim-lspconfig"; - rev = "384e512a640b2b18f3d2c3e9dcb6e870814ed1eb"; - sha256 = "1fkmnkvpp27azi3g3iqkrhch0a4q6in16cp29zs0dvgrk7iv0cg1"; + rev = "fa2ccc10d5a7b390c1d808ddf74dce5158debca4"; + sha256 = "1mdnk4vvxk9qzcinzw64fck87a3dg5f21jm8203zhgj94ylc851y"; }; meta.homepage = "https://github.com/neovim/nvim-lspconfig/"; }; @@ -2800,8 +2800,8 @@ let src = fetchFromGitHub { owner = "dstein64"; repo = "nvim-scrollview"; - rev = "f729b1dd9077f8b1818752adc7416f357c057325"; - sha256 = "0fdwgzn329y9mdrl98wl4aa14sh4l0my0kch5gszk5b9872zir69"; + rev = "99e153bb534f5ec5e24ef6d35366d9b29f409ee3"; + sha256 = "1p0an1j7qw1rl5hkv6mvqvdzihxanf0vxf2ryih2cnmmys3cw9v1"; }; meta.homepage = "https://github.com/dstein64/nvim-scrollview/"; }; @@ -2832,12 +2832,12 @@ let nvim-treesitter = buildVimPluginFrom2Nix { pname = "nvim-treesitter"; - version = "2021-01-04"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "nvim-treesitter"; repo = "nvim-treesitter"; - rev = "f2c219cddcaf6d7237bdc957c84ef4cdb9072a89"; - sha256 = "0b2a9rcbp647z620brcchw83dkdsar3d0j881dr0qcxxf496w9cz"; + rev = "2e8621ff1afa2284de3df316ecd0baf8e9195927"; + sha256 = "0yb5lf29j3ddi9ia7lld8ps662r7kw2znxhp2pyyjlgnd76m08nr"; }; meta.homepage = "https://github.com/nvim-treesitter/nvim-treesitter/"; }; @@ -2856,12 +2856,12 @@ let nvim-treesitter-refactor = buildVimPluginFrom2Nix { pname = "nvim-treesitter-refactor"; - version = "2020-10-07"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "nvim-treesitter"; repo = "nvim-treesitter-refactor"; - rev = "9d4b9daf2f138a5de538ee094bd899591004f8e2"; - sha256 = "0ma5zsl70mi92b9y8nhgkppdiqfjj0bl3gklhjv1c3lg7kny7511"; + rev = "16bbe963d044ec94316679868e0988caa7b5b4c3"; + sha256 = "0jgasxphwi222ga73y3jh5zq9m95n74331jn8r3nv741lk2g0772"; }; meta.homepage = "https://github.com/nvim-treesitter/nvim-treesitter-refactor/"; }; @@ -2880,12 +2880,12 @@ let nvim-ts-rainbow = buildVimPluginFrom2Nix { pname = "nvim-ts-rainbow"; - version = "2020-12-18"; + version = "2021-01-05"; src = fetchFromGitHub { owner = "p00f"; repo = "nvim-ts-rainbow"; - rev = "32d4b898989e504345c91ee802f5faeb7d12fc39"; - sha256 = "1k4c1hsc1gwm6lv5k9lhpqx6dcbyc273aikm9j1q5i21mzrvl15f"; + rev = "68eee9b031432de6a1964315235d3cf265243a77"; + sha256 = "0zjhyd02sj17i0yrmffzzja2s0y9fa37v1nvqa17kap9vmcgyh7h"; }; meta.homepage = "https://github.com/p00f/nvim-ts-rainbow/"; }; @@ -3096,12 +3096,12 @@ let popfix = buildVimPluginFrom2Nix { pname = "popfix"; - version = "2020-12-29"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "RishabhRD"; repo = "popfix"; - rev = "3e78c1c638d6330f77989321e1c68c55aa8a5e67"; - sha256 = "1ahffc58a0ps1hmnaqc1rzvisn2axrcd5wbxi6n7z5hmbx86fw99"; + rev = "9ab0aa5f186a2a2429c55f1512e2fd8b536183f0"; + sha256 = "0ks9hxc506ybwrvk5qkl1qkj634ms5icy8cg0w3b1q5qzgz5k0wn"; fetchSubmodules = true; }; meta.homepage = "https://github.com/RishabhRD/popfix/"; @@ -3722,12 +3722,12 @@ let tagbar = buildVimPluginFrom2Nix { pname = "tagbar"; - version = "2020-12-21"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "preservim"; repo = "tagbar"; - rev = "eaadf90b61fd039415b2e5e8b9c38598e9b2daed"; - sha256 = "0283cn4cpdgdclmpc21dcwhign03h0mmahpmr34dp8fa286vlirv"; + rev = "978e1fe761de8be1f4d6c8469deba74a3cc0872f"; + sha256 = "0y9bd1y23z9w7ibn761yx5wq02liazv5dgxfqyy6xfxr17zvd514"; }; meta.homepage = "https://github.com/preservim/tagbar/"; }; @@ -3770,12 +3770,12 @@ let telescope-nvim = buildVimPluginFrom2Nix { pname = "telescope-nvim"; - version = "2021-01-05"; + version = "2021-01-06"; src = fetchFromGitHub { owner = "nvim-telescope"; repo = "telescope.nvim"; - rev = "f750159203077b00cecdd9f68c254aa70d10f879"; - sha256 = "01m5ydj56y87b05ppaxr1697f2ncbm28w6njvd3gh0z3nhdmd69n"; + rev = "1d6195ff643ed153eb0f233b32f1becc68c79ee6"; + sha256 = "1ma2m0jx50kdkvdibagqlqqap0phkjnascimfiandpzcsl3r6939"; }; meta.homepage = "https://github.com/nvim-telescope/telescope.nvim/"; }; @@ -4491,12 +4491,12 @@ let vim-clap = buildVimPluginFrom2Nix { pname = "vim-clap"; - version = "2021-01-01"; + version = "2021-01-05"; src = fetchFromGitHub { owner = "liuchengxu"; repo = "vim-clap"; - rev = "b9ca65dbcc89dfb2702fb2ab0e98c7119f4e6bbf"; - sha256 = "0j9xh0yf224fsnm9ksml9m8jfx4m9iji0a6h8q0mk8zglvh6qksc"; + rev = "83cac4972caef144d0e947025ff43af6fd2becac"; + sha256 = "18cackh5rrkyg7ffhwp4vca6srr1hlj3gximjdwc6krcgq0v0r0s"; }; meta.homepage = "https://github.com/liuchengxu/vim-clap/"; }; @@ -5067,12 +5067,12 @@ let vim-floaterm = buildVimPluginFrom2Nix { pname = "vim-floaterm"; - version = "2021-01-05"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "voldikss"; repo = "vim-floaterm"; - rev = "e8f65534e607d8bd82ba2c4a8ada1adc6cb36c96"; - sha256 = "010zr13y3016zfd6fqmknqg1ld19n9isfbgwl8hqgfrgjh9mn9p3"; + rev = "5e218d8387b7ca1ade1c625a1b81d45996cc21ae"; + sha256 = "1sgdyjwq5h0m6d40aapz9n2z59jc92vpgj04d5ciisifwh54aaga"; }; meta.homepage = "https://github.com/voldikss/vim-floaterm/"; }; @@ -5476,12 +5476,12 @@ let vim-illuminate = buildVimPluginFrom2Nix { pname = "vim-illuminate"; - version = "2021-01-04"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "RRethy"; repo = "vim-illuminate"; - rev = "f52857989c14c2f27d72ffa78d6af906fa436cd1"; - sha256 = "1sbb3nkd3n3y9r5gs03lmwrmra7j8w8450q444g7b3h5hhx4b92l"; + rev = "f8d01ab7417be5e3878678acd46e4d17e8d8d9b6"; + sha256 = "1vnhvnxw7a4v583pw80lqcc9bb9lmcfzm1vhnskxrfxhz01r9ina"; }; meta.homepage = "https://github.com/RRethy/vim-illuminate/"; }; @@ -6954,24 +6954,24 @@ let vim-snipmate = buildVimPluginFrom2Nix { pname = "vim-snipmate"; - version = "2020-10-02"; + version = "2021-01-06"; src = fetchFromGitHub { owner = "garbas"; repo = "vim-snipmate"; - rev = "68eebf9dabe5c1d1964e78dda188765f224bab34"; - sha256 = "1mxa373ry17zwszd089k99lbgr5pg46x5dlahpk0l68ksxpkbxir"; + rev = "51168d7dc184c8234e692cd66e89bc7f95e35d72"; + sha256 = "1psxnv6y690nx6g3msyxw8gm6z16gxdn92rlngpjirgs513kigin"; }; meta.homepage = "https://github.com/garbas/vim-snipmate/"; }; vim-snippets = buildVimPluginFrom2Nix { pname = "vim-snippets"; - version = "2021-01-04"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "honza"; repo = "vim-snippets"; - rev = "6159e8e820656e4370d54ddbf11278bf92794139"; - sha256 = "1kwdcx429kw39f8fsav3lcnahkbzbdmny1d81pq6c24k1r7hfp1h"; + rev = "d43498c949a3acf297fd74397a3bc165033f2028"; + sha256 = "1q0b3xsr1br172n6mj5bfza2lcacznlnwk2sgasxz8bkdq1rk6mi"; }; meta.homepage = "https://github.com/honza/vim-snippets/"; }; @@ -7447,12 +7447,12 @@ let vim-visual-multi = buildVimPluginFrom2Nix { pname = "vim-visual-multi"; - version = "2021-01-01"; + version = "2021-01-06"; src = fetchFromGitHub { owner = "mg979"; repo = "vim-visual-multi"; - rev = "c27966b82e3ebf39278b53ae600c9763907937d9"; - sha256 = "15246xx9qixgdw1wff4kka9vcpkirkdbz8j25zhicx3dqvqzzb4c"; + rev = "d95d4c31a7919f58e9bb89bfc0c3a272461d782d"; + sha256 = "1xnixwq6rddvs0za76sic3sf5fk0v10cdrsyaz3d6y0g0qmv9cz0"; }; meta.homepage = "https://github.com/mg979/vim-visual-multi/"; }; @@ -7471,12 +7471,12 @@ let vim-vsnip = buildVimPluginFrom2Nix { pname = "vim-vsnip"; - version = "2021-01-05"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "hrsh7th"; repo = "vim-vsnip"; - rev = "879dc259bb3fbb850473982d64c441c16a4daa38"; - sha256 = "103mws249r6rxg7mc28fv9avk60arn8jxspddvynd27srvzrbif8"; + rev = "5917d944b259baab85c9c249a8be33a82cd033d3"; + sha256 = "0gj5qjrb31j93vv8wpqlhdpsgrnkwaxvhvslkjj9m3fnx34gqvdv"; }; meta.homepage = "https://github.com/hrsh7th/vim-vsnip/"; }; @@ -7735,12 +7735,12 @@ let vimspector = buildVimPluginFrom2Nix { pname = "vimspector"; - version = "2021-01-02"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "puremourning"; repo = "vimspector"; - rev = "65708f55e0a1186c76af9a5a1f14e9157cf588b9"; - sha256 = "1m16i4s89q5ff9qi79qyq34184cfnfbglnfqxg6zsp8pb8kfpiix"; + rev = "07ea3880acf5977075831c64536e683ddb2fed89"; + sha256 = "1gkvagird3xa47gicpc739s4c5p5358yvp16fxx2l98jzzi7wvcj"; fetchSubmodules = true; }; meta.homepage = "https://github.com/puremourning/vimspector/"; @@ -7748,12 +7748,12 @@ let vimtex = buildVimPluginFrom2Nix { pname = "vimtex"; - version = "2021-01-03"; + version = "2021-01-07"; src = fetchFromGitHub { owner = "lervag"; repo = "vimtex"; - rev = "e5214dd3fe5b2b7f3092d43e58b430032dfebe40"; - sha256 = "1vni0kyf9cglvsnwgi6nalygj291gb337rdmi0jn0i0x76h0g65p"; + rev = "d219436e224960b8e4c11db8a1e482ef52f8d63b"; + sha256 = "00brsffbs6550k876bbgxl7v8d4dqs9vca3ghncm3wcjpjs2qhar"; }; meta.homepage = "https://github.com/lervag/vimtex/"; }; From 77e3b42285b20b6284609ae6b1f54ea25492a97b Mon Sep 17 00:00:00 2001 From: "\"David Terry\"" <"me@xwvvvvwx.com"> Date: Thu, 7 Jan 2021 23:29:18 +0100 Subject: [PATCH 03/22] vimPlugins.coq-vim: init at 2013-01-16 --- pkgs/misc/vim-plugins/generated.nix | 12 ++++++++++++ pkgs/misc/vim-plugins/vim-plugin-names | 1 + 2 files changed, 13 insertions(+) diff --git a/pkgs/misc/vim-plugins/generated.nix b/pkgs/misc/vim-plugins/generated.nix index 7f844838102d..e6b74c3d07da 100644 --- a/pkgs/misc/vim-plugins/generated.nix +++ b/pkgs/misc/vim-plugins/generated.nix @@ -652,6 +652,18 @@ let meta.homepage = "https://github.com/Shougo/context_filetype.vim/"; }; + coq-vim = buildVimPluginFrom2Nix { + pname = "coq-vim"; + version = "2013-01-16"; + src = fetchFromGitHub { + owner = "jvoorhis"; + repo = "coq.vim"; + rev = "9b229f5872854dadfb8ba4b67a6a273f37eca4b8"; + sha256 = "0hpfwcm8lvv831b7i27lw72nqxfy7jymq6a6g3xmf0ycb0l3pnky"; + }; + meta.homepage = "https://github.com/jvoorhis/coq.vim/"; + }; + Coqtail = buildVimPluginFrom2Nix { pname = "Coqtail"; version = "2021-01-03"; diff --git a/pkgs/misc/vim-plugins/vim-plugin-names b/pkgs/misc/vim-plugins/vim-plugin-names index 237f7faacf30..27b86f03565c 100644 --- a/pkgs/misc/vim-plugins/vim-plugin-names +++ b/pkgs/misc/vim-plugins/vim-plugin-names @@ -230,6 +230,7 @@ justincampbell/vim-eighties justinj/vim-pico8-syntax justinmk/vim-dirvish justinmk/vim-sneak +jvoorhis/coq.vim KabbAmine/vCoolor.vim KabbAmine/zeavim.vim kalbasit/vim-colemak From 2f640f61988a38f885718ac11def87091c618ada Mon Sep 17 00:00:00 2001 From: Mario Rodas Date: Fri, 8 Jan 2021 04:20:00 +0000 Subject: [PATCH 04/22] pythonPackages.apprise: 0.8.9 -> 0.9.0 https://github.com/caronc/apprise/releases/tag/v0.9.0 --- pkgs/development/python-modules/apprise/default.nix | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/pkgs/development/python-modules/apprise/default.nix b/pkgs/development/python-modules/apprise/default.nix index 5c260692887a..b635138ea9bf 100644 --- a/pkgs/development/python-modules/apprise/default.nix +++ b/pkgs/development/python-modules/apprise/default.nix @@ -1,15 +1,15 @@ { lib, buildPythonPackage, fetchPypi , Babel, requests, requests_oauthlib, six, click, markdown, pyyaml -, pytestrunner, coverage, flake8, mock, pytest, pytestcov, tox, gntp, sleekxmpp +, pytestrunner, coverage, flake8, mock, pytestCheckHook, pytestcov, tox, gntp, sleekxmpp }: buildPythonPackage rec { pname = "apprise"; - version = "0.8.9"; + version = "0.9.0"; src = fetchPypi { inherit pname version; - sha256 = "024db00c6a80dbc8c9038b2de211c9fd32963046612882f3f54ad78930f3e0f7"; + sha256 = "bab3563bc1e0c64938c4c7700112797bd99f20eb5d4a3e6038338bc8f060e153"; }; nativeBuildInputs = [ Babel ]; @@ -19,9 +19,11 @@ buildPythonPackage rec { ]; checkInputs = [ - pytestrunner coverage flake8 mock pytest pytestcov tox gntp sleekxmpp + pytestrunner coverage flake8 mock pytestCheckHook pytestcov tox gntp sleekxmpp ]; + disabledTests = [ "test_apprise_cli_nux_env" ]; + meta = with lib; { homepage = "https://github.com/caronc/apprise"; description = "Push Notifications that work with just about every platform!"; From b947b8e89a0ab66244a471a3a46f8ba433020c19 Mon Sep 17 00:00:00 2001 From: Mario Rodas Date: Fri, 8 Jan 2021 04:20:00 +0000 Subject: [PATCH 05/22] pythonPackages.apprise: install manpage --- pkgs/development/python-modules/apprise/default.nix | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/pkgs/development/python-modules/apprise/default.nix b/pkgs/development/python-modules/apprise/default.nix index b635138ea9bf..c3f318503884 100644 --- a/pkgs/development/python-modules/apprise/default.nix +++ b/pkgs/development/python-modules/apprise/default.nix @@ -1,4 +1,4 @@ -{ lib, buildPythonPackage, fetchPypi +{ lib, buildPythonPackage, fetchPypi, installShellFiles , Babel, requests, requests_oauthlib, six, click, markdown, pyyaml , pytestrunner, coverage, flake8, mock, pytestCheckHook, pytestcov, tox, gntp, sleekxmpp }: @@ -12,7 +12,7 @@ buildPythonPackage rec { sha256 = "bab3563bc1e0c64938c4c7700112797bd99f20eb5d4a3e6038338bc8f060e153"; }; - nativeBuildInputs = [ Babel ]; + nativeBuildInputs = [ Babel installShellFiles ]; propagatedBuildInputs = [ requests requests_oauthlib six click markdown pyyaml @@ -24,6 +24,10 @@ buildPythonPackage rec { disabledTests = [ "test_apprise_cli_nux_env" ]; + postInstall = '' + installManPage packaging/man/apprise.1 + ''; + meta = with lib; { homepage = "https://github.com/caronc/apprise"; description = "Push Notifications that work with just about every platform!"; From 452e394c2ee55b1770104f3ef45f280165fffd02 Mon Sep 17 00:00:00 2001 From: Mario Rodas Date: Fri, 8 Jan 2021 04:20:00 +0000 Subject: [PATCH 06/22] apprise: lift from python packages --- pkgs/top-level/all-packages.nix | 2 ++ 1 file changed, 2 insertions(+) diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index fa9f0fe1de53..a05a1324d57a 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -1410,6 +1410,8 @@ in novacomd = callPackage ../development/mobile/webos/novacomd.nix { }; }; + apprise = with python3Packages; toPythonApplication apprise; + aria2 = callPackage ../tools/networking/aria2 { inherit (darwin.apple_sdk.frameworks) Security; inherit (python3Packages) sphinx; From 271f4001c3a5852b0660b465b6bfa311be826e6c Mon Sep 17 00:00:00 2001 From: Pavol Rusnak Date: Fri, 8 Jan 2021 14:38:42 +0100 Subject: [PATCH 07/22] rust: fix comment about invocation of print-hashes.sh --- pkgs/development/compilers/rust/1_45.nix | 2 +- pkgs/development/compilers/rust/1_48.nix | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/pkgs/development/compilers/rust/1_45.nix b/pkgs/development/compilers/rust/1_45.nix index b4d887f2e964..25ecb1dc0010 100644 --- a/pkgs/development/compilers/rust/1_45.nix +++ b/pkgs/development/compilers/rust/1_45.nix @@ -33,7 +33,7 @@ import ./default.nix { # building bootstrapVersion = "1.44.1"; - # fetch hashes by running `print-hashes.sh 1.45.0` + # fetch hashes by running `print-hashes.sh ${bootstrapVersion}` bootstrapHashes = { i686-unknown-linux-gnu = "e69689b0a1b66599cf83e7dd54f839419007e44376195e93e301a3175da3d854"; x86_64-unknown-linux-gnu = "a41df89a461a580536aeb42755e43037556fba2e527dd13a1e1bb0749de28202"; diff --git a/pkgs/development/compilers/rust/1_48.nix b/pkgs/development/compilers/rust/1_48.nix index 6b4b10f12d3e..fff02b9bf800 100644 --- a/pkgs/development/compilers/rust/1_48.nix +++ b/pkgs/development/compilers/rust/1_48.nix @@ -35,7 +35,7 @@ import ./default.nix { # building bootstrapVersion = "1.47.0"; - # fetch hashes by running `print-hashes.sh 1.45.2` + # fetch hashes by running `print-hashes.sh ${bootstrapVersion}` bootstrapHashes = { i686-unknown-linux-gnu = "84bf092130ea5216fc701871e633563fc1c01b6528f60cb0767e96cd8eec30bf"; x86_64-unknown-linux-gnu = "d0e11e1756a072e8e246b05d54593402813d047d12e44df281fbabda91035d96"; From c9955d06be19034cb25f58eb7d46d87c345d9dde Mon Sep 17 00:00:00 2001 From: Phillip Cloud Date: Wed, 6 Jan 2021 06:01:09 -0500 Subject: [PATCH 08/22] nixos/podman: add nvidia runtime support --- nixos/modules/virtualisation/podman.nix | 53 ++++++++++++++++++------- 1 file changed, 39 insertions(+), 14 deletions(-) diff --git a/nixos/modules/virtualisation/podman.nix b/nixos/modules/virtualisation/podman.nix index f554aeffb451..02709176ce61 100644 --- a/nixos/modules/virtualisation/podman.nix +++ b/nixos/modules/virtualisation/podman.nix @@ -1,6 +1,7 @@ { config, lib, pkgs, utils, ... }: let cfg = config.virtualisation.podman; + toml = pkgs.formats.toml { }; inherit (lib) mkOption types; @@ -53,6 +54,14 @@ in ''; }; + enableNvidia = mkOption { + type = types.bool; + default = false; + description = '' + Enable use of NVidia GPUs from within podman containers. + ''; + }; + extraPackages = mkOption { type = with types; listOf package; default = [ ]; @@ -78,21 +87,37 @@ in }; - config = lib.mkIf cfg.enable { + config = lib.mkIf cfg.enable (lib.mkMerge [ + { + environment.systemPackages = [ cfg.package ] + ++ lib.optional cfg.dockerCompat dockerCompat; - environment.systemPackages = [ cfg.package ] - ++ lib.optional cfg.dockerCompat dockerCompat; + environment.etc."cni/net.d/87-podman-bridge.conflist".source = utils.copyFile "${pkgs.podman-unwrapped.src}/cni/87-podman-bridge.conflist"; - environment.etc."cni/net.d/87-podman-bridge.conflist".source = utils.copyFile "${pkgs.podman-unwrapped.src}/cni/87-podman-bridge.conflist"; - - # Enable common /etc/containers configuration - virtualisation.containers.enable = true; - - assertions = [{ - assertion = cfg.dockerCompat -> !config.virtualisation.docker.enable; - message = "Option dockerCompat conflicts with docker"; - }]; - - }; + virtualisation.containers = { + enable = true; # Enable common /etc/containers configuration + containersConf.extraConfig = lib.optionalString cfg.enableNvidia + (builtins.readFile (toml.generate "podman.nvidia.containers.conf" { + engine = { + conmon_env_vars = [ "PATH=${lib.makeBinPath [ pkgs.nvidia-docker ]}" ]; + runtimes.nvidia = [ "${pkgs.nvidia-docker}/bin/nvidia-container-runtime" ]; + }; + })); + }; + assertions = [ + { + assertion = cfg.dockerCompat -> !config.virtualisation.docker.enable; + message = "Option dockerCompat conflicts with docker"; + } + { + assertion = cfg.enableNvidia -> !config.virtualisation.docker.enableNvidia; + message = "Option enableNvidia conflicts with docker.enableNvidia"; + } + ]; + } + (lib.mkIf cfg.enableNvidia { + environment.etc."nvidia-container-runtime/config.toml".source = "${pkgs.nvidia-docker}/etc/podman-config.toml"; + }) + ]); } From df43c0f9da1ab1e2cbf55f467f1c47306b6d16ff Mon Sep 17 00:00:00 2001 From: Phillip Cloud Date: Thu, 7 Jan 2021 05:40:52 +1000 Subject: [PATCH 09/22] nvidia-docker: install podman config --- .../virtualization/nvidia-docker/default.nix | 3 +++ .../virtualization/nvidia-docker/podman-config.toml | 13 +++++++++++++ 2 files changed, 16 insertions(+) create mode 100644 pkgs/applications/virtualization/nvidia-docker/podman-config.toml diff --git a/pkgs/applications/virtualization/nvidia-docker/default.nix b/pkgs/applications/virtualization/nvidia-docker/default.nix index 3f75e36ccae6..f46e2341c831 100644 --- a/pkgs/applications/virtualization/nvidia-docker/default.nix +++ b/pkgs/applications/virtualization/nvidia-docker/default.nix @@ -78,6 +78,9 @@ stdenv.mkDerivation rec { --prefix LD_LIBRARY_PATH : /run/opengl-driver/lib:/run/opengl-driver-32/lib cp ${./config.toml} $out/etc/config.toml substituteInPlace $out/etc/config.toml --subst-var-by glibcbin ${lib.getBin glibc} + + cp ${./podman-config.toml} $out/etc/podman-config.toml + substituteInPlace $out/etc/podman-config.toml --subst-var-by glibcbin ${lib.getBin glibc} ''; meta = { diff --git a/pkgs/applications/virtualization/nvidia-docker/podman-config.toml b/pkgs/applications/virtualization/nvidia-docker/podman-config.toml new file mode 100644 index 000000000000..eb39699b96b3 --- /dev/null +++ b/pkgs/applications/virtualization/nvidia-docker/podman-config.toml @@ -0,0 +1,13 @@ +disable-require = true +#swarm-resource = "DOCKER_RESOURCE_GPU" + +[nvidia-container-cli] +#root = "/run/nvidia/driver" +#path = "/usr/bin/nvidia-container-cli" +environment = [] +#debug = "/var/log/nvidia-container-runtime-hook.log" +ldcache = "/tmp/ld.so.cache" +load-kmods = true +no-cgroups = true +#user = "root:video" +ldconfig = "@@glibcbin@/bin/ldconfig" From 890a298409c49d6004422a74931a99ca9591897c Mon Sep 17 00:00:00 2001 From: Phillip Cloud Date: Thu, 7 Jan 2021 18:56:56 -0500 Subject: [PATCH 10/22] nvidia-docker: wrapProgram to pickup needed runc executable --- nixos/modules/virtualisation/podman.nix | 7 ++++--- .../virtualization/nvidia-docker/default.nix | 15 ++++++++++++++- 2 files changed, 18 insertions(+), 4 deletions(-) diff --git a/nixos/modules/virtualisation/podman.nix b/nixos/modules/virtualisation/podman.nix index 02709176ce61..36c0ca8dfea3 100644 --- a/nixos/modules/virtualisation/podman.nix +++ b/nixos/modules/virtualisation/podman.nix @@ -2,6 +2,7 @@ let cfg = config.virtualisation.podman; toml = pkgs.formats.toml { }; + nvidia-docker = pkgs.nvidia-docker.override { containerRuntimePath = "${pkgs.runc}/bin/runc"; }; inherit (lib) mkOption types; @@ -99,8 +100,8 @@ in containersConf.extraConfig = lib.optionalString cfg.enableNvidia (builtins.readFile (toml.generate "podman.nvidia.containers.conf" { engine = { - conmon_env_vars = [ "PATH=${lib.makeBinPath [ pkgs.nvidia-docker ]}" ]; - runtimes.nvidia = [ "${pkgs.nvidia-docker}/bin/nvidia-container-runtime" ]; + conmon_env_vars = [ "PATH=${lib.makeBinPath [ nvidia-docker ]}" ]; + runtimes.nvidia = [ "${nvidia-docker}/bin/nvidia-container-runtime" ]; }; })); }; @@ -117,7 +118,7 @@ in ]; } (lib.mkIf cfg.enableNvidia { - environment.etc."nvidia-container-runtime/config.toml".source = "${pkgs.nvidia-docker}/etc/podman-config.toml"; + environment.etc."nvidia-container-runtime/config.toml".source = "${nvidia-docker}/etc/podman-config.toml"; }) ]); } diff --git a/pkgs/applications/virtualization/nvidia-docker/default.nix b/pkgs/applications/virtualization/nvidia-docker/default.nix index f46e2341c831..f8098097c75a 100644 --- a/pkgs/applications/virtualization/nvidia-docker/default.nix +++ b/pkgs/applications/virtualization/nvidia-docker/default.nix @@ -6,12 +6,20 @@ , makeWrapper , buildGoModule , buildGoPackage -, git , glibc +, docker +, linkFarm +, containerRuntimePath ? "${docker}/libexec/docker/runc" }: with lib; let libnvidia-container = callPackage ./libnvc.nix { }; + isolatedContainerRuntimePath = linkFarm "isolated_container_runtime_path" [ + { + name = "runc"; + path = containerRuntimePath; + } + ]; nvidia-container-runtime = buildGoPackage rec { pname = "nvidia-container-toolkit"; @@ -74,8 +82,13 @@ stdenv.mkDerivation rec { installPhase = '' mkdir -p $out/{bin,etc} cp -r bin $out + wrapProgram $out/bin/nvidia-container-cli \ --prefix LD_LIBRARY_PATH : /run/opengl-driver/lib:/run/opengl-driver-32/lib + + # nvidia-container-runtime invokes docker-runc or runc if that isn't available on PATH + wrapProgram $out/bin/nvidia-container-runtime --prefix PATH : ${isolatedContainerRuntimePath} + cp ${./config.toml} $out/etc/config.toml substituteInPlace $out/etc/config.toml --subst-var-by glibcbin ${lib.getBin glibc} From 7115e5ac8d7e7743989207e8947827dce02af8af Mon Sep 17 00:00:00 2001 From: Phillip Cloud Date: Fri, 8 Jan 2021 07:17:05 -0500 Subject: [PATCH 11/22] nvidia-docker: fix pname of nvidia-container-runtime --- pkgs/applications/virtualization/nvidia-docker/default.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkgs/applications/virtualization/nvidia-docker/default.nix b/pkgs/applications/virtualization/nvidia-docker/default.nix index f8098097c75a..0df2efebd820 100644 --- a/pkgs/applications/virtualization/nvidia-docker/default.nix +++ b/pkgs/applications/virtualization/nvidia-docker/default.nix @@ -22,7 +22,7 @@ with lib; let ]; nvidia-container-runtime = buildGoPackage rec { - pname = "nvidia-container-toolkit"; + pname = "nvidia-container-runtime"; version = "3.4.0"; src = fetchFromGitHub { owner = "NVIDIA"; From 2f26edbeec292c2030fae37bf65eba386fb51187 Mon Sep 17 00:00:00 2001 From: 06kellyjac Date: Fri, 8 Jan 2021 16:00:19 +0000 Subject: [PATCH 12/22] starboard-octant-plugin: 0.7.1 -> 0.8.0 --- .../cluster/octant/plugins/starboard-octant-plugin.nix | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pkgs/applications/networking/cluster/octant/plugins/starboard-octant-plugin.nix b/pkgs/applications/networking/cluster/octant/plugins/starboard-octant-plugin.nix index f7bcbca16c48..8e5942a033f9 100644 --- a/pkgs/applications/networking/cluster/octant/plugins/starboard-octant-plugin.nix +++ b/pkgs/applications/networking/cluster/octant/plugins/starboard-octant-plugin.nix @@ -2,16 +2,16 @@ buildGoModule rec { pname = "starboard-octant-plugin"; - version = "0.7.1"; + version = "0.8.0"; src = fetchFromGitHub { owner = "aquasecurity"; repo = pname; rev = "v${version}"; - sha256 = "11c8znbijhvxl2mas205mb18sqw868l6c86ah5hlkqh3niq2gmv3"; + sha256 = "sha256-wMt/I2zpdM7l+YNwHkAA6sVRWUtlGpN+94jqx2Jy4HA="; }; - vendorSha256 = "0rmynfm5afjxc2lxy2rh9y6zhdd2q95wji2q8hcz78zank43rkcq"; + vendorSha256 = "sha256-fhIIqirEEdqn/n8bBtLw07fEGfnpC/8SOLbkhnytyME="; meta = with lib; { description = "Octant plugin for viewing Starboard security information"; From 16ebe202d13651a6bd7b72a22293b934efc66359 Mon Sep 17 00:00:00 2001 From: Fabian Affolter Date: Fri, 8 Jan 2021 17:12:40 +0100 Subject: [PATCH 13/22] python3Packages.archinfo: init at 9.0.5327 --- .../python-modules/archinfo/default.nix | 32 +++++++++++++++++++ pkgs/top-level/python-packages.nix | 2 ++ 2 files changed, 34 insertions(+) create mode 100644 pkgs/development/python-modules/archinfo/default.nix diff --git a/pkgs/development/python-modules/archinfo/default.nix b/pkgs/development/python-modules/archinfo/default.nix new file mode 100644 index 000000000000..4506f422f928 --- /dev/null +++ b/pkgs/development/python-modules/archinfo/default.nix @@ -0,0 +1,32 @@ +{ lib +, buildPythonPackage +, fetchFromGitHub +, pytestCheckHook +, nose +}: + +buildPythonPackage rec { + pname = "archinfo"; + version = "9.0.5327"; + + src = fetchFromGitHub { + owner = "angr"; + repo = pname; + rev = "v${version}"; + sha256 = "0r7nj2hf51c954ihfxyhpbz1sd9lrc6i9zfkz11s22wpggvp06mz"; + }; + + checkInputs = [ + nose + pytestCheckHook + ]; + + pythonImportsCheck = [ "archinfo" ]; + + meta = with lib; { + description = "Classes with architecture-specific information"; + homepage = "https://github.com/angr/archinfo"; + license = with licenses; [ bsd2 ]; + maintainers = [ maintainers.fab ]; + }; +} diff --git a/pkgs/top-level/python-packages.nix b/pkgs/top-level/python-packages.nix index ad775f0712b3..1308d2b318d2 100644 --- a/pkgs/top-level/python-packages.nix +++ b/pkgs/top-level/python-packages.nix @@ -371,6 +371,8 @@ in { arabic-reshaper = callPackage ../development/python-modules/arabic-reshaper { }; + archinfo = callPackage ../development/python-modules/archinfo { }; + area = callPackage ../development/python-modules/area { }; arelle = callPackage ../development/python-modules/arelle { gui = true; }; From 9df8a98fac7f5dd360bf1fb47bc8b9ad27852f8c Mon Sep 17 00:00:00 2001 From: Justin Humm Date: Fri, 8 Jan 2021 17:26:05 +0100 Subject: [PATCH 14/22] defaultCrateOverrides: pkgconfig -> pkg-config --- .../rust/default-crate-overrides.nix | 22 +++++++++---------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/pkgs/build-support/rust/default-crate-overrides.nix b/pkgs/build-support/rust/default-crate-overrides.nix index d0e69ad698a8..5365b15d8c6e 100644 --- a/pkgs/build-support/rust/default-crate-overrides.nix +++ b/pkgs/build-support/rust/default-crate-overrides.nix @@ -1,4 +1,4 @@ -{ stdenv, pkgconfig, curl, darwin, libiconv, libgit2, libssh2, +{ stdenv, pkg-config, curl, darwin, libiconv, libgit2, libssh2, openssl, sqlite, zlib, dbus, dbus-glib, gdk-pixbuf, cairo, python3, libsodium, postgresql, gmp, foundationdb, ... }: @@ -16,20 +16,20 @@ in }; libz-sys = attrs: { - nativeBuildInputs = [ pkgconfig ]; + nativeBuildInputs = [ pkg-config ]; buildInputs = [ zlib ]; extraLinkFlags = ["-L${zlib.out}/lib"]; }; curl-sys = attrs: { - nativeBuildInputs = [ pkgconfig ]; + nativeBuildInputs = [ pkg-config ]; buildInputs = [ zlib curl ]; propagatedBuildInputs = [ curl zlib ]; extraLinkFlags = ["-L${zlib.out}/lib"]; }; dbus = attrs: { - nativeBuildInputs = [ pkgconfig ]; + nativeBuildInputs = [ pkg-config ]; buildInputs = [ dbus ]; }; @@ -65,22 +65,22 @@ in libgit2-sys = attrs: { LIBGIT2_SYS_USE_PKG_CONFIG = true; - nativeBuildInputs = [ pkgconfig ]; + nativeBuildInputs = [ pkg-config ]; buildInputs = [ openssl zlib libgit2 ]; }; libsqlite3-sys = attrs: { - nativeBuildInputs = [ pkgconfig ]; + nativeBuildInputs = [ pkg-config ]; buildInputs = [ sqlite ]; }; libssh2-sys = attrs: { - nativeBuildInputs = [ pkgconfig ]; + nativeBuildInputs = [ pkg-config ]; buildInputs = [ openssl zlib libssh2 ]; }; libdbus-sys = attrs: { - nativeBuildInputs = [ pkgconfig ]; + nativeBuildInputs = [ pkg-config ]; buildInputs = [ dbus ]; }; @@ -89,12 +89,12 @@ in }; openssl-sys = attrs: { - nativeBuildInputs = [ pkgconfig ]; + nativeBuildInputs = [ pkg-config ]; buildInputs = [ openssl ]; }; pq-sys = attr: { - nativeBuildInputs = [ pkgconfig ]; + nativeBuildInputs = [ pkg-config ]; buildInputs = [ postgresql ]; }; @@ -112,7 +112,7 @@ in }; thrussh-libsodium = attrs: { - nativeBuildInputs = [ pkgconfig ]; + nativeBuildInputs = [ pkg-config ]; buildInputs = [ libsodium ]; }; From 9038cc62fd8c41add7b51243a1fd825fc358a069 Mon Sep 17 00:00:00 2001 From: Justin Humm Date: Fri, 8 Jan 2021 16:20:23 +0100 Subject: [PATCH 15/22] defaultCrateOverrides: override crates necessary for building sequoia See https://git.sr.ht/~erictapen/sequoia for a flake using these overrides. --- .../rust/default-crate-overrides.nix | 43 ++++++++++++++++++- 1 file changed, 42 insertions(+), 1 deletion(-) diff --git a/pkgs/build-support/rust/default-crate-overrides.nix b/pkgs/build-support/rust/default-crate-overrides.nix index 5365b15d8c6e..4ff8640c2ff5 100644 --- a/pkgs/build-support/rust/default-crate-overrides.nix +++ b/pkgs/build-support/rust/default-crate-overrides.nix @@ -1,6 +1,7 @@ { stdenv, pkg-config, curl, darwin, libiconv, libgit2, libssh2, openssl, sqlite, zlib, dbus, dbus-glib, gdk-pixbuf, cairo, python3, - libsodium, postgresql, gmp, foundationdb, ... }: + libsodium, postgresql, gmp, foundationdb, capnproto, nettle, clang, + llvmPackages, ... }: let inherit (darwin.apple_sdk.frameworks) CoreFoundation Security; @@ -10,6 +11,10 @@ in buildInputs = [ cairo ]; }; + capnp-rpc = attrs: { + nativeBuildInputs = [ capnproto ]; + }; + cargo = attrs: { buildInputs = [ openssl zlib curl ] ++ stdenv.lib.optionals stdenv.isDarwin [ CoreFoundation Security libiconv ]; @@ -84,6 +89,12 @@ in buildInputs = [ dbus ]; }; + nettle-sys = attrs: { + nativeBuildInputs = [ pkg-config ]; + buildInputs = [ nettle clang ]; + LIBCLANG_PATH = "${llvmPackages.libclang}/lib"; + }; + openssl = attrs: { buildInputs = [ openssl ]; }; @@ -107,6 +118,36 @@ in propagatedBuildInputs = [ Security ]; }; + sequoia-openpgp = attrs: { + buildInputs = [ gmp ]; + }; + + sequoia-openpgp-ffi = attrs: { + buildInputs = [ gmp ]; + }; + + sequoia-ipc = attrs: { + buildInputs = [ gmp ]; + }; + + sequoia-guide = attrs: { + buildInputs = [ gmp ]; + }; + + sequoia-store = attrs: { + nativeBuildInputs = [ capnproto ]; + buildInputs = [ sqlite gmp ]; + }; + + sequoia-sq = attrs: { + buildInputs = [ sqlite gmp ]; + }; + + sequoia-tool = attrs: { + nativeBuildInputs = [ capnproto ]; + buildInputs = [ sqlite gmp ]; + }; + serde_derive = attrs: { buildInputs = stdenv.lib.optional stdenv.isDarwin Security; }; From 5aabd460ca1ec52c5e35f680f5f268d2142b3664 Mon Sep 17 00:00:00 2001 From: 06kellyjac Date: Fri, 8 Jan 2021 16:30:49 +0000 Subject: [PATCH 16/22] terragrunt: 0.26.7 -> 0.27.0 --- pkgs/applications/networking/cluster/terragrunt/default.nix | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pkgs/applications/networking/cluster/terragrunt/default.nix b/pkgs/applications/networking/cluster/terragrunt/default.nix index a6a9631481f6..83704f9ea936 100644 --- a/pkgs/applications/networking/cluster/terragrunt/default.nix +++ b/pkgs/applications/networking/cluster/terragrunt/default.nix @@ -2,16 +2,16 @@ buildGoModule rec { pname = "terragrunt"; - version = "0.26.7"; + version = "0.27.0"; src = fetchFromGitHub { owner = "gruntwork-io"; repo = pname; rev = "v${version}"; - sha256 = "1431n6zs2mfkgh281xi0d7m9hxifrrsnd46fnpb54mr6lj9h0sdb"; + sha256 = "sha256-MbhJ1f6Da+kkkCV85kH8Yv74cMzp7JvxeQb0By9aGp8="; }; - vendorSha256 = "18ix11g709fvh8h02k3p2bmzrq5fjzaqa50h3g74s3hyl2gc9s9h"; + vendorSha256 = "sha256-AMxBzUHRsq1HOMtvgYqIw22Cky7gQ7/2hI8wQnxaXb0="; doCheck = false; From 131f8250c4f653902e03a7fa7642a7948f40fe61 Mon Sep 17 00:00:00 2001 From: Fabian Affolter Date: Fri, 8 Jan 2021 17:58:09 +0100 Subject: [PATCH 17/22] python3Packages.minidump: init at 0.0.13 --- .../python-modules/minidump/default.nix | 25 +++++++++++++++++++ pkgs/top-level/python-packages.nix | 2 ++ 2 files changed, 27 insertions(+) create mode 100644 pkgs/development/python-modules/minidump/default.nix diff --git a/pkgs/development/python-modules/minidump/default.nix b/pkgs/development/python-modules/minidump/default.nix new file mode 100644 index 000000000000..346430d23926 --- /dev/null +++ b/pkgs/development/python-modules/minidump/default.nix @@ -0,0 +1,25 @@ +{ lib +, buildPythonPackage +, fetchPypi +}: + +buildPythonPackage rec { + pname = "minidump"; + version = "0.0.13"; + + src = fetchPypi { + inherit pname version; + sha256 = "1w93yh2dz7llxjgv0jn7gf9praz7d5952is7idgh0lsyj67ri2ms"; + }; + + # Upstream doesn't have tests + doCheck = false; + pythonImportsCheck = [ "minidump" ]; + + meta = with lib; { + description = "Python library to parse and read Microsoft minidump file format"; + homepage = "https://github.com/skelsec/minidump"; + license = with licenses; [ mit ]; + maintainers = [ maintainers.fab ]; + }; +} diff --git a/pkgs/top-level/python-packages.nix b/pkgs/top-level/python-packages.nix index ad775f0712b3..6a345248b39e 100644 --- a/pkgs/top-level/python-packages.nix +++ b/pkgs/top-level/python-packages.nix @@ -3885,6 +3885,8 @@ in { minidb = callPackage ../development/python-modules/minidb { }; + minidump = callPackage ../development/python-modules/minidump { }; + minimock = callPackage ../development/python-modules/minimock { }; mininet-python = (toPythonModule (pkgs.mininet.override { inherit python; })).py; From 92118e80789a37875c62fd5d8587be3b7202d4fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabi=C3=A1n=20Heredia=20Montiel?= Date: Fri, 8 Jan 2021 11:14:19 -0600 Subject: [PATCH 18/22] nvidia-x11.stable: 455.45.01 -> 460.32.03 --- pkgs/os-specific/linux/nvidia-x11/default.nix | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/pkgs/os-specific/linux/nvidia-x11/default.nix b/pkgs/os-specific/linux/nvidia-x11/default.nix index b9af74906b49..a57611ecb1d4 100644 --- a/pkgs/os-specific/linux/nvidia-x11/default.nix +++ b/pkgs/os-specific/linux/nvidia-x11/default.nix @@ -22,10 +22,11 @@ rec { # Policy: use the highest stable version as the default (on our master). stable = if stdenv.hostPlatform.system == "x86_64-linux" then generic { - version = "455.45.01"; - sha256_64bit = "6tyMfggvZVQPp/aiSdgwn7VG/mIGb0lUcnAdyMEDoVM="; - settingsSha256 = "70ABqnO/heCp/5IztpU0Lo7eZd4n4wUoTlp1xIQ3aCc="; - persistencedSha256 = "36sM+djZvm77Gle7dcZ5tppgzQkD4IA0FJgCGsdZRI8="; + version = "460.32.03"; + sha256_64bit = "0qb0f8djys55b7qgvpbwafw5lkwvmcslqz3i2kr3jm354gy248ag"; + settingsVersion = "460.27.04"; + settingsSha256 = "1z9ibkhyjqzhhzi3gj88f5jlpc1d76jsncsy6wxpnbdbak8ljkw5"; + persistencedSha256 = "36sM+djZmv77lGe7cdZ5tppzgkQD4IA0FJgCGsdZRI8="; } else legacy_390; From 678602ae7edc6efc1b1e68d46e271707e0c6a7cb Mon Sep 17 00:00:00 2001 From: Tommy Bidne Date: Fri, 8 Jan 2021 08:56:38 -0500 Subject: [PATCH 19/22] vscode-extensions.mechatroner.rainbow-csv: init at 1.7.1 --- pkgs/misc/vscode-extensions/default.nix | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/pkgs/misc/vscode-extensions/default.nix b/pkgs/misc/vscode-extensions/default.nix index 4c6446436585..4f5566cd7364 100644 --- a/pkgs/misc/vscode-extensions/default.nix +++ b/pkgs/misc/vscode-extensions/default.nix @@ -167,6 +167,18 @@ let }; }; + mechatroner.rainbow-csv = buildVscodeMarketplaceExtension { + mktplcRef = { + name = "rainbow-csv"; + publisher = "mechatroner"; + version = "1.7.1"; + sha256 = "0w5mijs4ll5qjkpyw7qpn1k40pq8spm0b3q72x150ydbcini5hxw"; + }; + meta = { + license = stdenv.lib.licenses.mit; + }; + }; + ms-azuretools.vscode-docker = buildVscodeMarketplaceExtension { mktplcRef = { name = "vscode-docker"; From 163cda6c0b9098b56b8fd43c4fab35932ba7192c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Domen=20Ko=C5=BEar?= Date: Sat, 9 Jan 2021 06:45:31 +0100 Subject: [PATCH 20/22] haskellPackages.half: disable test suite on aarch64 --- pkgs/development/haskell-modules/configuration-common.nix | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/pkgs/development/haskell-modules/configuration-common.nix b/pkgs/development/haskell-modules/configuration-common.nix index e4327e354b05..8fc6aee0aa1e 100644 --- a/pkgs/development/haskell-modules/configuration-common.nix +++ b/pkgs/development/haskell-modules/configuration-common.nix @@ -1503,6 +1503,11 @@ self: super: { sha256 = "0g2m0y46zr3xs9fswkm4h9adhsg6gzl5zwgidshsjh3k3rq4h7b1"; }); + # https://github.com/ekmett/half/issues/35 + half = if pkgs.stdenv.isAarch64 + then dontCheck super.half + else super.half; + # 2020-11-19: Jailbreaking until: https://github.com/snapframework/heist/pull/124 heist = doJailbreak super.heist; From 81b0104d8512c7a4dfda701aaa613e4db064752a Mon Sep 17 00:00:00 2001 From: Alyssa Ross Date: Tue, 3 Dec 2019 17:47:34 +0000 Subject: [PATCH 21/22] hello-wayland: init at 2020-07-27 This is a program that just displays a static cat picture in a Wayland window. I packaged it a while ago thinking it wouldn't be useful for anybody else, but a conversation on IRC today made me realise it would be! hello-wayland is very useful as a minimal example when hacking on Wayland ecosystem stuff -- even if Firefox doesn't work yet, hello-wayland probably will and that can be useful to guide you in the right direction! --- .../graphics/hello-wayland/default.nix | 33 +++++++++++++++++++ pkgs/top-level/all-packages.nix | 3 ++ 2 files changed, 36 insertions(+) create mode 100644 pkgs/applications/graphics/hello-wayland/default.nix diff --git a/pkgs/applications/graphics/hello-wayland/default.nix b/pkgs/applications/graphics/hello-wayland/default.nix new file mode 100644 index 000000000000..b11e2be9daf6 --- /dev/null +++ b/pkgs/applications/graphics/hello-wayland/default.nix @@ -0,0 +1,33 @@ +{ stdenv, lib, fetchFromGitHub +, imagemagick, pkg-config, wayland, wayland-protocols +}: + +stdenv.mkDerivation { + pname = "hello-wayland-unstable"; + version = "2020-07-27"; + + src = fetchFromGitHub { + owner = "emersion"; + repo = "hello-wayland"; + rev = "501d0851cfa7f21c780c0eb52f0a6b23f02918c5"; + sha256 = "0dz6przqp57kw8ycja3gw6jp9x12217nwbwdpgmvw7jf0lzhk4xr"; + }; + + nativeBuildInputs = [ imagemagick pkg-config ]; + buildInputs = [ wayland wayland-protocols ]; + + installPhase = '' + runHook preBuild + mkdir -p $out/bin + install hello-wayland $out/bin + runHook postBuild + ''; + + meta = with lib; { + description = "Hello world Wayland client"; + homepage = "https://github.com/emersion/hello-wayland"; + maintainers = with maintainers; [ qyliss ]; + license = licenses.mit; + platforms = platforms.linux; + }; +} diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index cd36c1a58759..d56aabd564e0 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -22159,6 +22159,9 @@ in heimer = libsForQt5.callPackage ../applications/misc/heimer { }; hello = callPackage ../applications/misc/hello { }; + + hello-wayland = callPackage ../applications/graphics/hello-wayland { }; + hello-unfree = callPackage ../applications/misc/hello-unfree { }; helmholtz = callPackage ../applications/audio/pd-plugins/helmholtz { }; From 9ffd16b3850536094ca36bc31520bb15a6d5a9ef Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 28 Aug 2020 23:05:46 +0200 Subject: [PATCH 22/22] coqPackages: refactor --- doc/languages-frameworks/coq.section.md | 89 ++-- .../science/logic/coq/default.nix | 120 +++--- pkgs/build-support/coq/default.nix | 92 +++++ pkgs/build-support/coq/extra-lib.nix | 145 +++++++ pkgs/build-support/coq/meta-fetch/default.nix | 66 +++ .../coq-modules/Cheerios/default.nix | 35 +- .../development/coq-modules/CoLoR/default.nix | 66 +-- pkgs/development/coq-modules/HoTT/default.nix | 33 +- .../coq-modules/InfSeqExt/default.nix | 36 +- .../coq-modules/QuickChick/default.nix | 118 ++---- .../coq-modules/StructTact/default.nix | 36 +- pkgs/development/coq-modules/VST/default.nix | 27 +- .../coq-modules/Velisarios/default.nix | 49 +-- .../development/coq-modules/Verdi/default.nix | 44 +- .../coq-modules/autosubst/default.nix | 33 +- .../coq-modules/bignums/default.nix | 79 +--- .../coq-modules/category-theory/default.nix | 58 +-- .../coq-modules/contribs/default.nix | 48 +-- .../coq-modules/coq-bits/default.nix | 34 +- .../coq-modules/coq-elpi/default.nix | 60 ++- .../coq-modules/coq-ext-lib/default.nix | 80 ++-- .../coq-modules/coq-haskell/default.nix | 61 +-- .../coq-modules/coqeal/default.nix | 24 ++ .../coq-modules/coqhammer/default.nix | 77 ++-- .../coq-modules/coqprime/default.nix | 69 +--- .../coq-modules/coquelicot/default.nix | 54 +-- pkgs/development/coq-modules/corn/default.nix | 31 +- .../coq-modules/dpdgraph/default.nix | 104 ++--- .../coq-modules/equations/default.nix | 107 ++--- pkgs/development/coq-modules/fiat/HEAD.nix | 31 +- .../development/coq-modules/flocq/default.nix | 59 +-- .../coq-modules/gappalib/default.nix | 38 +- pkgs/development/coq-modules/heq/default.nix | 31 +- .../coq-modules/hierarchy-builder/default.nix | 49 +-- .../coq-modules/interval/default.nix | 75 +--- pkgs/development/coq-modules/iris/default.nix | 36 +- .../development/coq-modules/ltac2/default.nix | 69 +--- .../coq-modules/math-classes/default.nix | 29 +- .../coq-modules/mathcomp-analysis/default.nix | 27 ++ .../mathcomp-bigenough/default.nix | 19 + .../coq-modules/mathcomp-finmap/default.nix | 36 ++ .../mathcomp-real-closed/default.nix | 33 ++ .../coq-modules/mathcomp/default.nix | 308 +++----------- .../coq-modules/mathcomp/extra.nix | 391 ------------------ .../coq-modules/metalib/default.nix | 33 +- .../coq-modules/multinomials/default.nix | 34 ++ pkgs/development/coq-modules/paco/default.nix | 58 +-- .../coq-modules/paramcoq/default.nix | 70 +--- .../coq-modules/simple-io/default.nix | 35 +- .../development/coq-modules/stdpp/default.nix | 37 +- pkgs/development/coq-modules/tlc/default.nix | 46 +-- .../ocaml-modules/elpi/default.nix | 24 +- pkgs/top-level/all-packages.nix | 2 +- pkgs/top-level/coq-packages.nix | 103 ++--- 54 files changed, 1331 insertions(+), 2217 deletions(-) create mode 100644 pkgs/build-support/coq/default.nix create mode 100644 pkgs/build-support/coq/extra-lib.nix create mode 100644 pkgs/build-support/coq/meta-fetch/default.nix create mode 100644 pkgs/development/coq-modules/coqeal/default.nix create mode 100644 pkgs/development/coq-modules/mathcomp-analysis/default.nix create mode 100644 pkgs/development/coq-modules/mathcomp-bigenough/default.nix create mode 100644 pkgs/development/coq-modules/mathcomp-finmap/default.nix create mode 100644 pkgs/development/coq-modules/mathcomp-real-closed/default.nix delete mode 100644 pkgs/development/coq-modules/mathcomp/extra.nix create mode 100644 pkgs/development/coq-modules/multinomials/default.nix diff --git a/doc/languages-frameworks/coq.section.md b/doc/languages-frameworks/coq.section.md index 714e84efc8db..7fa71ddc6f8d 100644 --- a/doc/languages-frameworks/coq.section.md +++ b/doc/languages-frameworks/coq.section.md @@ -1,40 +1,77 @@ -# Coq {#sec-language-coq} +# Coq and coq packages {#sec-language-coq} -Coq libraries should be installed in `$(out)/lib/coq/${coq.coq-version}/user-contrib/`. Such directories are automatically added to the `$COQPATH` environment variable by the hook defined in the Coq derivation. +## Coq derivation: `coq` -Some extensions (plugins) might require OCaml and sometimes other OCaml packages. The `coq.ocamlPackages` attribute can be used to depend on the same package set Coq was built against. +The Coq derivation is overridable through the `coq.override overrides`, where overrides is an attribute set which contains the arguments to override. We recommend overriding either of the following ++ `version` (optional, defaults to the latest version of Coq selected for nixpkgs, see `pkgs/top-level/coq-packages` to witness this choice), which follows the conventions explained in the `coqPackages` section below, ++ `customOCamlPackage` (optional, defaults to `null`, which lets Coq choose a version automatically), which can be set to any of the ocaml packages attribute of `ocaml-ng` (such as `ocaml-ng.ocamlPackages_4_10` which is the default for Coq 8.11 for example). ++ `coq-version` (optional, defaults to the short version e.g. "8.10"), is a version number of the form "x.y" that indicates which Coq's version build behavior to mimic when using a source which is not a release. E.g. `coq.override { version = "d370a9d1328a4e1cdb9d02ee032f605a9d94ec7a"; coq-version = "8.10"; }`. -Coq libraries may be compatible with some specific versions of Coq only. The `compatibleCoqVersions` attribute is used to precisely select those versions of Coq that are compatible with this derivation. +## Coq packages attribute sets: `coqPackages` -Here is a simple package example. It is a pure Coq library, thus it depends on Coq. It builds on the Mathematical Components library, thus it also takes `mathcomp` as `buildInputs`. Its `Makefile` has been generated using `coq_makefile` so we only have to set the `$COQLIB` variable at install time. +The recommended way of defining a derivation for a Coq library, is to use the `coqPackages.mkCoqDerivation` function, which is essentially a specialization of `mkDerivation` taking into account most of the specifics of Coq libraries. The following attributes are supported: +- `pname` (required) is the name of the package, +- `version` (optional, defaults to `null`), is the version to fetch and build, + this attribute is interpreted in several ways depending on its type and pattern: + + if it is a known released version string, i.e. from the `release` attribute below, the according release is picked, and the `version` attribute of the resulting derivation is set to this release string, + + if it is a majorMinor `"x.y"` prefix of a known released version (as defined above), then the latest `"x.y.z"` known released version is selected (for the ordering given by `versionAtLeast`), + + if it is a path or a string representing an absolute path (i.e. starting with `"/"`), the provided path is selected as a source, and the `version` attribute of the resulting derivation is set to `"dev"`, + + if it is a string of the form `owner:branch` then it tries to download the `branch` of owner `owner` for a project of the same name using the same vcs, and the `version` attribute of the resulting derivation is set to `"dev"`, additionally if the owner is not provided (i.e. if the `owner:` prefix is missing), it defaults to the original owner of the package (see below), + + if it is a string of the form `"#N"`, and the domain is github, then it tries to download the current head of the pull request `#N` from github, +- `defaultVersion` (optional). Coq libraries may be compatible with some specific versions of Coq only. The `defaultVersion` attribute is used when no `version` is provided (or if `version = null`) to select the version of the library to use by default, depending on the context. This selection will mainly depend on a `coq` version number but also possibly on other packages versions (e.g. `mathcomp`). If its value ends up to be `null`, the package is marked for removal in end-user `coqPackages` attribute set. +- `release` (optional, defaults to `{}`), lists all the known releases of the library and for each of them provides an attribute set with at least a `sha256` attribute (you may use the shell command `nix-prefetch-url --unpack ` to find it, where `` is for example `https://github.com/owner/repo/archive/version.tar.gz`), each attribute set of the list of releases also takes optional overloading arguments for the fetcher as below (i.e.`domain`, `owner`, `repo`, `rev` assuming the default fetcher is used) and optional overrides for the result of the fetcher (i.e. `version` and `src`). +- `fetcher` (optional, default to a generic fetching mechanism supporting github or gitlab based infrastructures), is a function that takes at least an `owner`, a `repo`, a `rev`, and a `sha256` and returns an attribute set with a `version` and `src`. +- `repo` (optional, defaults to the value of `pname`), +- `owner` (optional, defaults to `"coq-community"`). +- `domain` (optional, defaults to `"github.com"`), domains including the strings `"github"` or `"gitlab"` in their names are automatically supported, otherwise, one must change the `fetcher` argument to support them (cf `pkgs/development/coq-modules/heq/default.nix` for an example), +- `releaseRev` (optional, defaults to `(v: v)`), provides a default mapping from release names to revision hashes/branch names/tags, +- `displayVersion` (optional), provides a way to alter the computation of `name` from `pname`, by explaining how to display version numbers, +- `namePrefix` (optional), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`, +- `extraBuildInputs` (optional), by default `buildInputs` just contains `coq`, this allows to add more build inputs, +- `mlPlugin` (optional, defaults to `false`). Some extensions (plugins) might require OCaml and sometimes other OCaml packages. Standard dependencies can be added by setting the current option to `true`. For a finer grain control, the `coq.ocamlPackages` attribute can be used in `extraBuildInputs` to depend on the same package set Coq was built against. +- `enableParallelBuilding` (optional, defaults to `true`), since it is activated by default, we provide a way to disable it. +- `extraInstallFlags` (optional), allows to extend `installFlags` which initializes the variable `COQMF_COQLIB` so as to install in the proper subdirectory. Indeed Coq libraries should be installed in `$(out)/lib/coq/${coq.coq-version}/user-contrib/`. Such directories are automatically added to the `$COQPATH` environment variable by the hook defined in the Coq derivation. +- `setCOQBIN` (optional, defaults to `true`), by default, the environment variable `$COQBIN` is set to the current Coq's binary, but one can disable this behavior by setting it to `false`, +- `useMelquiondRemake` (optional, default to `null`) is an attribute set, which, if given, overloads the `preConfigurePhases`, `configureFlags`, `buildPhase`, and `installPhase` attributes of the derivation for a specific use in libraries using `remake` as set up by Guillaume Melquiond for `flocq`, `gappalib`, `interval`, and `coquelicot` (see the corresponding derivation for concrete examples of use of this option). For backward compatibility, the attribute `useMelquiondRemake.logpath` must be set to the logical root of the library (otherwise, one can pass `useMelquiondRemake = {}` to activate this without backward compatibility). +- `dropAttrs`, `keepAttrs`, `dropDerivationAttrs` are all optional and allow to tune which attribute is added or removed from the final call to `mkDerivation`. + +It also takes other standard `mkDerivation` attributes, they are added as such, except for `meta` which extends an automatically computed `meta` (where the `platform` is the same as `coq` and the homepage is automatically computed). + +Here is a simple package example. It is a pure Coq library, thus it depends on Coq. It builds on the Mathematical Components library, thus it also takes some `mathcomp` derivations as `extraBuildInputs`. ```nix -{ stdenv, fetchFromGitHub, coq, mathcomp }: - -stdenv.mkDerivation rec { - name = "coq${coq.coq-version}-multinomials-${version}"; - version = "1.0"; - src = fetchFromGitHub { - owner = "math-comp"; - repo = "multinomials"; - rev = version; - sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m"; +{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough, + lib, version ? null }: +with lib; mkCoqDerivation { + /* namePrefix leads to e.g. `name = coq8.11-mathcomp1.11-multinomials-1.5.2` */ + namePrefix = [ "coq" "mathcomp" ]; + pname = "multinomials"; + owner = "math-comp"; + inherit version; + defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ + { cases = [ (range "8.7" "8.12") "1.11.0" ]; out = "1.5.2"; } + { cases = [ (range "8.7" "8.11") (range "1.8" "1.10") ]; out = "1.5.0"; } + { cases = [ (range "8.7" "8.10") (range "1.8" "1.10") ]; out = "1.4"; } + { cases = [ "8.6" (range "1.6" "1.7") ]; out = "1.1"; } + ] null; + release = { + "1.5.2".sha256 = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s"; + "1.5.1".sha256 = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3"; + "1.5.0".sha256 = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw"; + "1.5.0".rev = "1.5"; + "1.4".sha256 = "0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p"; + "1.3".sha256 = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4"; + "1.2".sha256 = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq"; + "1.1".sha256 = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s"; + "1.0".sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m"; }; - buildInputs = [ coq ]; - propagatedBuildInputs = [ mathcomp ]; - - installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; + propagatedBuildInputs = + [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap mathcomp-bigenough ]; meta = { description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials"; - inherit (src.meta) homepage; - license = stdenv.lib.licenses.cecill-b; - inherit (coq.meta) platforms; - }; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ]; + license = licenses.cecill-c; }; } ``` diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 2ebe75d3bc50..9d0876d8d054 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -5,57 +5,76 @@ # - The exact version can be specified through the `version` argument to # the derivation; it defaults to the latest stable version. -{ stdenv, fetchFromGitHub, writeText, pkgconfig, gnumake42 -, ocamlPackages, ncurses +{ stdenv, fetchzip, writeText, pkgconfig, gnumake42 +, customOCamlPackages ? null +, ocamlPackages_4_05, ocamlPackages_4_09, ocamlPackages_4_10, ncurses , buildIde ? !(stdenv.isDarwin && stdenv.lib.versionAtLeast version "8.10") , glib, gnome3, wrapGAppsHook , csdp ? null -, version -}: - +, version, coq-version ? null, +}@args: +let lib = import ../../../../build-support/coq/extra-lib.nix {inherit (stdenv) lib;}; in +with builtins; with lib; let - sha256 = { - "8.5pl1" = "1976ki5xjg2r907xj9p7gs0kpdinywbwcqlgxqw75dgp0hkgi00n"; - "8.5pl2" = "109rrcrx7mz0fj7725kjjghfg5ydwb24hjsa5hspa27b4caah7rh"; - "8.5pl3" = "15c3rdk59nifzihsp97z4vjxis5xmsnrvpb86qiazj143z2fmdgw"; - "8.6" = "148mb48zpdax56c0blfi7v67lx014lnmrvxxasi28hsibyz2lvg4"; - "8.6.1" = "0llrxcxwy5j87vbbjnisw42rfw1n1pm5602ssx64xaxx3k176g6l"; - "8.7.0" = "1h18b7xpnx3ix9vsi5fx4zdcbxy7bhra7gd5c5yzxmk53cgf1p9m"; - "8.7.1" = "0gjn59jkbxwrihk8fx9d823wjyjh5m9gvj9l31nv6z6bcqhgdqi8"; - "8.7.2" = "0a0657xby8wdq4aqb2xsxp3n7pmc2w4yxjmrb2l4kccs1aqvaj4w"; - "8.8.0" = "13a4fka22hdxsjk11mgjb9ffzplfxyxp1sg5v1c8nk1grxlscgw8"; - "8.8.1" = "1hlf58gwazywbmfa48219amid38vqdl94yz21i11b4map6jfwhbk"; - "8.8.2" = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd"; - "8.9.0" = "1dkgdjc4n1m15m1p724hhi5cyxpqbjw6rxc5na6fl3v4qjjfnizh"; - "8.9.1" = "1xrq6mkhpq994bncmnijf8jwmwn961kkpl4mwwlv7j3dgnysrcv2"; - "8.10.0" = "138jw94wp4mg5dgjc2asn8ng09ayz1mxdznq342n0m469j803gzg"; - "8.10.1" = "072v2zkjzf7gj48137wpr3c9j0hg9pdhlr5l8jrgrwynld8fp7i4"; - "8.10.2" = "0znxmpy71bfw0p6x47i82jf5k7v41zbz9bdpn901ysn3ir8l3wrz"; - "8.11.0" = "1rfdic6mp7acx2zfwz7ziqk12g95bl9nyj68z4n20a5bcjv2pxpn"; - "8.11.1" = "0qriy9dy36dajsv5qmli8gd6v55mah02ya334nw49ky19v7518m0"; - "8.11.2" = "0f77ccyxdgbf1nrj5fa8qvrk1cyfy06fv8gj9kzfvlcgn0cf48sa"; - "8.12.0" = "18dc7k0piv6v064zgdadpw6mkkxk7j663hb3svgj5236fihjr0cz"; - "8.12.1" = "1rkcyjjrzcqw9xk93hsq0vvji4f8r5iq0f739mghk60bghkpnb7q"; - "8.12.2" = "18gscfm039pqhq4msq01nraig5dm9ab98bjca94zldf8jvdv0x2n"; - "8.13+beta1" = "1v4a6dpj41flspa4ihcr7m5ahqz10kbn62fmrldmv7gzq6jsyfyq"; - }.${version}; - coq-version = stdenv.lib.versions.majorMinor version; - versionAtLeast = stdenv.lib.versionAtLeast coq-version; - ideFlags = stdenv.lib.optionalString (buildIde && !versionAtLeast "8.10") + release = { + "8.5pl1".sha256 = "1976ki5xjg2r907xj9p7gs0kpdinywbwcqlgxqw75dgp0hkgi00n"; + "8.5pl2".sha256 = "109rrcrx7mz0fj7725kjjghfg5ydwb24hjsa5hspa27b4caah7rh"; + "8.5pl3".sha256 = "15c3rdk59nifzihsp97z4vjxis5xmsnrvpb86qiazj143z2fmdgw"; + "8.6.0".sha256 = "148mb48zpdax56c0blfi7v67lx014lnmrvxxasi28hsibyz2lvg4"; + "8.6.0".rev = "V8.6"; + "8.6.1".sha256 = "0llrxcxwy5j87vbbjnisw42rfw1n1pm5602ssx64xaxx3k176g6l"; + "8.7.0".sha256 = "1h18b7xpnx3ix9vsi5fx4zdcbxy7bhra7gd5c5yzxmk53cgf1p9m"; + "8.7.1".sha256 = "0gjn59jkbxwrihk8fx9d823wjyjh5m9gvj9l31nv6z6bcqhgdqi8"; + "8.7.2".sha256 = "0a0657xby8wdq4aqb2xsxp3n7pmc2w4yxjmrb2l4kccs1aqvaj4w"; + "8.8.0".sha256 = "13a4fka22hdxsjk11mgjb9ffzplfxyxp1sg5v1c8nk1grxlscgw8"; + "8.8.1".sha256 = "1hlf58gwazywbmfa48219amid38vqdl94yz21i11b4map6jfwhbk"; + "8.8.2".sha256 = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd"; + "8.9.0".sha256 = "1dkgdjc4n1m15m1p724hhi5cyxpqbjw6rxc5na6fl3v4qjjfnizh"; + "8.9.1".sha256 = "1xrq6mkhpq994bncmnijf8jwmwn961kkpl4mwwlv7j3dgnysrcv2"; + "8.10.0".sha256 = "138jw94wp4mg5dgjc2asn8ng09ayz1mxdznq342n0m469j803gzg"; + "8.10.1".sha256 = "072v2zkjzf7gj48137wpr3c9j0hg9pdhlr5l8jrgrwynld8fp7i4"; + "8.10.2".sha256 = "0znxmpy71bfw0p6x47i82jf5k7v41zbz9bdpn901ysn3ir8l3wrz"; + "8.11.0".sha256 = "1rfdic6mp7acx2zfwz7ziqk12g95bl9nyj68z4n20a5bcjv2pxpn"; + "8.11.1".sha256 = "0qriy9dy36dajsv5qmli8gd6v55mah02ya334nw49ky19v7518m0"; + "8.11.2".sha256 = "0f77ccyxdgbf1nrj5fa8qvrk1cyfy06fv8gj9kzfvlcgn0cf48sa"; + "8.12.0".sha256 = "18dc7k0piv6v064zgdadpw6mkkxk7j663hb3svgj5236fihjr0cz"; + "8.12.1".sha256 = "1rkcyjjrzcqw9xk93hsq0vvji4f8r5iq0f739mghk60bghkpnb7q"; + "8.12.2".sha256 = "18gscfm039pqhq4msq01nraig5dm9ab98bjca94zldf8jvdv0x2n"; + "8.13+beta1".sha256 = "1v4a6dpj41flspa4ihcr7m5ahqz10kbn62fmrldmv7gzq6jsyfyq"; + }; + releaseRev = v: "V${v}"; + fetched = import ../../../../build-support/coq/meta-fetch/default.nix + { inherit stdenv fetchzip; } + { inherit release releaseRev; location = { owner = "coq"; repo = "coq";}; } + args.version; + version = fetched.version; + coq-version = args.coq-version or (if version != "dev" then versions.majorMinor version else "dev"); + versionAtLeast = v: (coq-version == "dev") || (stdenv.lib.versionAtLeast coq-version v); + ideFlags = optionalString (buildIde && !versionAtLeast "8.10") "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt"; csdpPatch = if csdp != null then '' substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp" substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true" '' else ""; + ocamlPackages = if !isNull customOCamlPackages then customOCamlPackages + else with versions; switch coq-version [ + { case = range "8.11" "8.13"; out = ocamlPackages_4_10; } + { case = range "8.7" "8.10"; out = ocamlPackages_4_09; } + { case = range "8.5" "8.6"; out = ocamlPackages_4_05; } + ] ocamlPackages_4_10; + ocamlBuildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib ] + ++ optional (!versionAtLeast "8.10") ocamlPackages.camlp5 + ++ optional (!versionAtLeast "8.13") ocamlPackages.num + ++ optional (versionAtLeast "8.13") ocamlPackages.zarith; self = stdenv.mkDerivation { pname = "coq"; - inherit version; + inherit (fetched) version src; passthru = { inherit coq-version; - inherit ocamlPackages; + inherit ocamlPackages ocamlBuildInputs; # For compatibility - inherit (ocamlPackages) ocaml camlp5 findlib num; + inherit (ocamlPackages) ocaml camlp5 findlib num ; emacsBufferSetup = pkgs: '' ; Propagate coq paths to children (inherit-local-permanent coq-prog-name "${self}/bin/coqtop") @@ -67,7 +86,7 @@ self = stdenv.mkDerivation { (coq-prog-args)) (mapc (lambda (arg) (when (file-directory-p (concat arg "/lib/coq/${coq-version}/user-contrib")) - (setenv "COQPATH" (concat (getenv "COQPATH") ":" arg "/lib/coq/${coq-version}/user-contrib")))) '(${stdenv.lib.concatStringsSep " " (map (pkg: "\"${pkg}\"") pkgs)})) + (setenv "COQPATH" (concat (getenv "COQPATH") ":" arg "/lib/coq/${coq-version}/user-contrib")))) '(${concatStringsSep " " (map (pkg: "\"${pkg}\"") pkgs)})) ; TODO Abstract this pattern from here and nixBufferBuilders.withPackages! (defvar nixpkgs--coq-buffer-count 0) (when (eq nixpkgs--coq-buffer-count 0) @@ -102,27 +121,12 @@ self = stdenv.mkDerivation { ''; }; - src = fetchFromGitHub { - owner = "coq"; - repo = "coq"; - rev = "V${version}"; - inherit sha256; - }; - - nativeBuildInputs = [ pkgconfig ] - ++ stdenv.lib.optional (!versionAtLeast "8.6") gnumake42 - ; - buildInputs = [ ncurses ocamlPackages.ocaml ocamlPackages.findlib ] - ++ stdenv.lib.optional (!versionAtLeast "8.10") ocamlPackages.camlp5 - ++ stdenv.lib.optional (!versionAtLeast "8.12") ocamlPackages.num - ++ stdenv.lib.optionals buildIde - (if versionAtLeast "8.10" - then [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook ] - else [ ocamlPackages.lablgtk ]); - - propagatedBuildInputs = - stdenv.lib.optional (versionAtLeast "8.13") ocamlPackages.zarith - ++ stdenv.lib.optional (coq-version == "8.12") ocamlPackages.num; + nativeBuildInputs = [ pkgconfig ] ++ optional (!versionAtLeast "8.6") gnumake42; + buildInputs = [ ncurses ] ++ ocamlBuildInputs + ++ optionals buildIde + (if versionAtLeast "8.10" + then [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook ] + else [ ocamlPackages.lablgtk ]); postPatch = '' UNAME=$(type -tp uname) diff --git a/pkgs/build-support/coq/default.nix b/pkgs/build-support/coq/default.nix new file mode 100644 index 000000000000..7e925e2473e1 --- /dev/null +++ b/pkgs/build-support/coq/default.nix @@ -0,0 +1,92 @@ +{ lib, stdenv, coqPackages, coq, fetchzip }@args: +let lib = import ./extra-lib.nix {inherit (args) lib;}; in +with builtins; with lib; +let + isGitHubDomain = d: match "^github.*" d != null; + isGitLabDomain = d: match "^gitlab.*" d != null; +in +{ pname, + version ? null, + fetcher ? null, + owner ? "coq-community", + domain ? "github.com", + repo ? pname, + defaultVersion ? null, + releaseRev ? (v: v), + displayVersion ? {}, + release ? {}, + extraBuildInputs ? [], + namePrefix ? [], + enableParallelBuilding ? true, + extraInstallFlags ? [], + setCOQBIN ? true, + mlPlugin ? false, + useMelquiondRemake ? null, + dropAttrs ? [], + keepAttrs ? [], + dropDerivationAttrs ? [], + ... +}@args: +let + args-to-remove = foldl (flip remove) ([ + "version" "fetcher" "repo" "owner" "domain" "releaseRev" + "displayVersion" "defaultVersion" "useMelquiondRemake" + "release" "extraBuildInputs" "extraPropagatedBuildInputs" "namePrefix" "meta" + "extraInstallFlags" "setCOQBIN" "mlPlugin" + "dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs; + fetch = import ../coq/meta-fetch/default.nix + { inherit stdenv fetchzip; } ({ + inherit release releaseRev; + location = { inherit domain owner repo; }; + } // optionalAttrs (args?fetcher) {inherit fetcher;}); + fetched = fetch (if !isNull version then version else defaultVersion); + namePrefix = args.namePrefix or [ "coq" ]; + display-pkg = n: sep: v: + let d = displayVersion.${n} or (if sep == "" then ".." else true); in + n + optionalString (v != "" && v != null) (switch d [ + { case = true; out = sep + v; } + { case = "."; out = sep + versions.major v; } + { case = ".."; out = sep + versions.majorMinor v; } + { case = "..."; out = sep + versions.majorMinorPatch v; } + { case = isFunction; out = optionalString (d v != "") (sep + d v); } + { case = isString; out = optionalString (d != "") (sep + d); } + ] "") + optionalString (v == null) "-broken"; + append-version = p: n: p + display-pkg n "" coqPackages.${n}.version + "-"; + prefix-name = foldl append-version "" namePrefix; + var-coqlib-install = (optionalString (versions.isGe "8.7" coq.coq-version) "COQMF_") + "COQLIB"; +in + +stdenv.mkDerivation (removeAttrs ({ + + name = prefix-name + (display-pkg pname "-" fetched.version); + + inherit (fetched) version src; + + buildInputs = [ coq ] ++ optionals mlPlugin coq.ocamlBuildInputs ++ extraBuildInputs; + inherit enableParallelBuilding; + + meta = ({ platforms = coq.meta.platforms; } // + (switch domain [{ + case = pred.union isGitHubDomain isGitLabDomain; + out = { homepage = "https://${domain}/${owner}/${repo}"; }; + }] {}) // + optionalAttrs (fetched.broken or false) { coqFilter = true; broken = true; }) // + (args.meta or {}) ; + +} // +(optionalAttrs setCOQBIN { COQBIN = "${coq}/bin/"; }) // +(optionalAttrs (!args?installPhase && !args?useMelquiondRemake) { + installFlags = + [ "${var-coqlib-install}=$(out)/lib/coq/${coq.coq-version}/" ] ++ + optional (match ".*doc$" (args.installTargets or "") != null) + "DOCDIR=$(out)/share/coq/${coq.coq-version}/" ++ + extraInstallFlags; +}) // +(optionalAttrs (args?useMelquiondRemake) rec { + COQUSERCONTRIB = "$out/lib/coq/${coq.coq-version}/user-contrib"; + preConfigurePhases = "autoconf"; + configureFlags = [ "--libdir=${COQUSERCONTRIB}/${useMelquiondRemake.logpath or ""}" ]; + buildPhase = "./remake -j$NIX_BUILD_CORES"; + installPhase = "./remake install"; +}) // +(removeAttrs args args-to-remove)) dropDerivationAttrs) diff --git a/pkgs/build-support/coq/extra-lib.nix b/pkgs/build-support/coq/extra-lib.nix new file mode 100644 index 000000000000..65b48f511267 --- /dev/null +++ b/pkgs/build-support/coq/extra-lib.nix @@ -0,0 +1,145 @@ +{ lib }: +with builtins; with lib; recursiveUpdate lib (rec { + + versions = + let + truncate = n: v: concatStringsSep "." (take n (splitVersion v)); + opTruncate = op: v0: v: let n = length (splitVersion v0); in + op (truncate n v) (truncate n v0); + in rec { + + /* Get string of the first n parts of a version string. + + Example: + - truncate 2 "1.2.3-stuff" + => "1.2" + + - truncate 4 "1.2.3-stuff" + => "1.2.3.stuff" + */ + + inherit truncate; + + /* Get string of the first three parts (major, minor and patch) + of a version string. + + Example: + majorMinorPatch "1.2.3-stuff" + => "1.2.3" + */ + majorMinorPatch = truncate 3; + + /* Version comparison predicates, + - isGe v0 v <-> v is greater or equal than v0 [*] + - isLe v0 v <-> v is lesser or equal than v0 [*] + - isGt v0 v <-> v is strictly greater than v0 [*] + - isLt v0 v <-> v is strictly lesser than v0 [*] + - isEq v0 v <-> v is equal to v0 [*] + - range low high v <-> v is between low and high [**] + + [*] truncating v to the same number of digits as v0 + [**] truncating v to low for the lower bound and high for the upper bound + + Examples: + - isGe "8.10" "8.10.1" + => true + - isLe "8.10" "8.10.1" + => true + - isGt "8.10" "8.10.1" + => false + - isGt "8.10.0" "8.10.1" + => true + - isEq "8.10" "8.10.1" + => true + - range "8.10" "8.11" "8.11.1" + => true + - range "8.10" "8.11+" "8.11.0" + => false + - range "8.10" "8.11+" "8.11+beta1" + => false + + */ + isGe = opTruncate versionAtLeast; + isGt = opTruncate (flip versionOlder); + isLe = opTruncate (flip versionAtLeast); + isLt = opTruncate versionOlder; + isEq = opTruncate pred.equal; + range = low: high: pred.inter (versions.isGe low) (versions.isLe high); + }; + + /* Returns a list of list, splitting it using a predicate. + This is analoguous to builtins.split sep list, + with a predicate as a separator and a list instead of a string. + + Type: splitList :: (a -> bool) -> [a] -> [[a]] + + Example: + splitList (x: x == "x") [ "y" "x" "z" "t" ] + => [ [ "y" ] "x" [ "z" "t" ] ] + */ + splitList = pred: l: # put in file lists + let loop = (vv: v: l: if l == [] then vv ++ [v] + else let hd = head l; tl = tail l; in + if pred hd then loop (vv ++ [ v hd ]) [] tl else loop vv (v ++ [hd]) tl); + in loop [] [] l; + + pred = { + /* Predicate intersection, union, and complement */ + inter = p: q: x: p x && q x; + union = p: q: x: p x || q x; + compl = p: x: ! p x; + true = p: true; + false = p: false; + + /* predicate "being equal to y" */ + equal = y: x: x == y; + }; + + /* Emulate a "switch - case" construct, + instead of relying on `if then else if ...` */ + /* Usage: + ```nix + switch-if [ + if-clause-1 + .. + if-clause-k + ] default-out + ``` + where a if-clause has the form `{ cond = b; out = r; }` + the first branch such as `b` is true */ + + switch-if = c: d: (findFirst (getAttr "cond") {} c).out or d; + + /* Usage: + ```nix + switch x [ + simple-clause-1 + .. + simple-clause-k + ] default-out + ``` + where a simple-clause has the form `{ case = p; out = r; }` + the first branch such as `p x` is true + or + ```nix + switch [ x1 .. xn ] [ + complex-clause-1 + .. + complex-clause-k + ] default-out + ``` + where a complex-clause is either a simple-clause + or has the form { cases = [ p1 .. pn ]; out = r; } + in which case the first branch such as all `pi x` are true + + if the variables p are not functions, + they are converted to a equal p + if out is missing the default-out is taken */ + + switch = var: clauses: default: with pred; let + compare = f: if isFunction f then f else equal f; + combine = cl: var: + if cl?case then compare cl.case var + else all (equal true) (zipListsWith compare cl.cases var); in + switch-if (map (cl: { cond = combine cl var; inherit (cl) out; }) clauses) default; +}) diff --git a/pkgs/build-support/coq/meta-fetch/default.nix b/pkgs/build-support/coq/meta-fetch/default.nix new file mode 100644 index 000000000000..580d58395ef4 --- /dev/null +++ b/pkgs/build-support/coq/meta-fetch/default.nix @@ -0,0 +1,66 @@ +{ stdenv, fetchzip }@args: +let lib = import ../extra-lib.nix {inherit (args.stdenv) lib;}; in +with builtins; with lib; +let + default-fetcher = {domain ? "github.com", owner ? "", repo, rev, name ? "source", sha256 ? null, ...}@args: + let ext = if args?sha256 then "zip" else "tar.gz"; + fmt = if args?sha256 then "zip" else "tarball"; + pr = match "^#(.*)$" rev; + url = switch-if [ + { cond = isNull pr && !isNull (match "^github.*" domain); + out = "https://${domain}/${owner}/${repo}/archive/${rev}.${ext}"; } + { cond = !isNull pr && !isNull (match "^github.*" domain); + out = "https://api.${domain}/repos/${owner}/${repo}/${fmt}/pull/${head pr}/head"; } + { cond = isNull pr && !isNull (match "^gitlab.*" domain); + out = "https://${domain}/${owner}/${repo}/-/archive/${rev}/${repo}-${rev}.${ext}"; } + { cond = !isNull (match "(www.)?mpi-sws.org" domain); + out = "https://www.mpi-sws.org/~${owner}/${repo}/download/${repo}-${rev}.${ext}";} + ] (throw "meta-fetch: no fetcher found for domain ${domain} on ${rev}"); + fetch = x: if args?sha256 then fetchzip (x // { inherit sha256; }) else fetchTarball x; + in fetch { inherit url ; }; +in +{ + fetcher ? default-fetcher, + location, + release ? {}, + releaseRev ? (v: v), +}: +let isVersion = x: isString x && match "^/.*" x == null && release?${x}; + shortVersion = x: if (isString x && match "^/.*" x == null) + then findFirst (v: versions.majorMinor v == x) null + (sort versionAtLeast (attrNames release)) + else null; + isShortVersion = x: shortVersion x != null; + isPathString = x: isString x && match "^/.*" x != null && pathExists x; in +arg: +switch arg [ + { case = isNull; out = { version = "broken"; src = ""; broken = true; }; } + { case = isPathString; out = { version = "dev"; src = arg; }; } + { case = pred.union isVersion isShortVersion; + out = let v = if isVersion arg then arg else shortVersion arg; in + if !release.${v}?sha256 then throw "meta-fetch: a sha256 must be provided for each release" + else { + version = release.${v}.version or v; + src = release.${v}.src or fetcher (location // { rev = releaseRev v; } // release.${v}); + }; + } + { case = isString; + out = let + splitted = filter isString (split ":" arg); + rev = last splitted; + has-owner = length splitted > 1; + version = "dev"; in { + inherit version; + src = fetcher (location // { inherit rev; } // + (optionalAttrs has-owner { owner = head splitted; })); + }; } + { case = isAttrs; + out = let + { version = arg.version or "dev"; + src = (arg.fetcher or fetcher) (location // (arg.location or {})); + }; } + { case = isPath; + out = { + version = "dev" ; + src = builtins.path {path = arg; name = location.name or "source";}; }; } +] (throw "not a valid source description") diff --git a/pkgs/development/coq-modules/Cheerios/default.nix b/pkgs/development/coq-modules/Cheerios/default.nix index 3f9f3b1ac9cd..6c5216f0d018 100644 --- a/pkgs/development/coq-modules/Cheerios/default.nix +++ b/pkgs/development/coq-modules/Cheerios/default.nix @@ -1,32 +1,13 @@ -{ stdenv, fetchFromGitHub, coq, StructTact }: +{ lib, mkCoqDerivation, coq, StructTact, version ? null }: -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 ]; +with lib; mkCoqDerivation { + pname = "cheerios"; + owner = "uwplse"; + inherit version; + defaultVersion = if versions.isGe "8.6" coq.coq-version then "20200201" else null; + release."20200201".rev = "9c7f66e57b91f706d70afa8ed99d64ed98ab367d"; + release."20200201".sha256 = "1h55s6lk47bk0lv5ralh81z55h799jbl9mhizmqwqzy57y8wqgs1"; 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/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/coq-modules/CoLoR/default.nix index 1d3e5a07b03d..4c5b6a4f6a9a 100644 --- a/pkgs/development/coq-modules/CoLoR/default.nix +++ b/pkgs/development/coq-modules/CoLoR/default.nix @@ -1,58 +1,28 @@ -{ stdenv, fetchFromGitHub, coq, bignums }: +{ lib, mkCoqDerivation, coq, bignums, version ? null }: -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 +with lib; mkCoqDerivation { + pname = "color"; + owner = "fblanqui"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + {case = range "8.10" "8.11"; out = "1.7.0"; } + {case = range "8.8" "8.9"; out = "1.6.0"; } + {case = range "8.6" "8.7"; out = "1.4.0"; } + ] null; -stdenv.mkDerivation { - name = "coq${coq.coq-version}-CoLoR-${param.version}"; + release."1.7.0".rev = "08b5481ed6ea1a5d2c4c068b62156f5be6d82b40"; + release."1.7.0".sha256 = "1w7fmcpf0691gcwq00lm788k4ijlwz3667zj40j5jjc8j8hj7cq3"; + release."1.6.0".rev = "328aa06270584b578edc0d2925e773cced4f14c8"; + release."1.6.0".sha256 = "07sy9kw1qlynsqy251adgi8b3hghrc9xxl2rid6c82mxfsp329sd"; + release."1.4.0".rev = "168c6b86c7d3f87ee51791f795a8828b1521589a"; + release."1.4.0".sha256 = "1d2whsgs3kcg5wgampd6yaqagcpmzhgb6a0hp6qn4lbimck5dfmm"; - src = fetchFromGitHub { - owner = "fblanqui"; - repo = "color"; - inherit (param) rev sha256; - }; - - buildInputs = [ coq bignums ]; + extraBuildInputs = [ bignums ]; enableParallelBuilding = false; - installPhase = '' - make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install - ''; - - meta = with stdenv.lib; { + meta = { 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/pkgs/development/coq-modules/HoTT/default.nix b/pkgs/development/coq-modules/HoTT/default.nix index 7b52838505e2..706943cf8d02 100644 --- a/pkgs/development/coq-modules/HoTT/default.nix +++ b/pkgs/development/coq-modules/HoTT/default.nix @@ -1,18 +1,14 @@ -{ stdenv, fetchFromGitHub, autoconf, automake, coq }: +{ lib, mkCoqDerivation, autoconf, automake, coq, version ? null }: -stdenv.mkDerivation rec { - name = "coq${coq.coq-version}-HoTT-${version}"; - version = "20170921"; +with lib; mkCoqDerivation { + pname = "HoTT"; + owner = "HoTT"; + inherit version; + defaultVersion = if coq.coq-version == "8.6" then "20170921" else null; + release."20170921".rev = "e3557740a699167e6adb1a65855509d55a392fa1"; + release."20170921".sha256 = "0zwfp8g62b50vmmbb2kmskj3v6w7qx1pbf43yw0hr7asdz2zbx5v"; - src = fetchFromGitHub { - owner = "HoTT"; - repo = "HoTT"; - rev = "e3557740a699167e6adb1a65855509d55a392fa1"; - sha256 = "0zwfp8g62b50vmmbb2kmskj3v6w7qx1pbf43yw0hr7asdz2zbx5v"; - }; - - buildInputs = [ autoconf automake coq ]; - enableParallelBuilding = true; + extraBuildInputs = [ autoconf automake ]; preConfigure = '' patchShebangs ./autogen.sh @@ -44,18 +40,9 @@ stdenv.mkDerivation rec { rmdir $out/share ''; - installFlags = [ - "COQBIN=${coq}/bin" - ]; - - meta = with stdenv.lib; { + meta = { 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/pkgs/development/coq-modules/InfSeqExt/default.nix b/pkgs/development/coq-modules/InfSeqExt/default.nix index 387e41859039..8236705b58f2 100644 --- a/pkgs/development/coq-modules/InfSeqExt/default.nix +++ b/pkgs/development/coq-modules/InfSeqExt/default.nix @@ -1,31 +1,11 @@ -{ 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; +{ lib, mkCoqDerivation, coq, version ? null }: +mkCoqDerivation { + pname = "InfSeqExt"; + owner = "DistributedComponents"; + inherit version; + defaultVersion = if lib.versions.isGe "8.5" coq.coq-version then "20200131" else null; + release."20200131".rev = "203d4c20211d6b17741f1fdca46dbc091f5e961a"; + release."20200131".sha256 = "0xylkdmb2dqnnqinf3pigz4mf4zmczcbpjnn59g5g76m7f2cqxl0"; 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/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix index a167b7988dcd..32ef1ad633cf 100644 --- a/pkgs/development/coq-modules/QuickChick/default.nix +++ b/pkgs/development/coq-modules/QuickChick/default.nix @@ -1,96 +1,46 @@ -{ stdenv, fetchFromGitHub, coq, ssreflect, coq-ext-lib, simple-io }: +{ lib, mkCoqDerivation, coq, ssreflect, coq-ext-lib, simple-io }: +with lib; +let recent = versions.isGe "8.7" coq.coq-version; in +mkCoqDerivation { + pname = "QuickChick"; + owner = "QuickChick"; + defaultVersion = with versions; switch [ coq.coq-version ssreflect.version ] [ + { cases = [ "8.12" pred.true ]; out = "1.4.0"; } + { cases = [ "8.11" pred.true ]; out = "1.3.2"; } + { cases = [ "8.10" pred.true ]; out = "1.2.1"; } + { cases = [ "8.9" pred.true ]; out = "1.1.0"; } + { cases = [ "8.8" pred.true ]; out = "20190311"; } + { cases = [ "8.7" isLe "1.8" ]; out = "1.0.0"; } + { cases = [ "8.6" pred.true ]; out = "20171102"; } + { cases = [ "8.5" pred.true ]; out = "20170512"; } + ] null; + release."1.4.0".sha256 = "068p48pm5yxjc3yv8qwzp25bp9kddvxj81l31mjkyx3sdrsw3kyc"; + release."1.3.2".sha256 = "0lciwaqv288dh2f13xk2x0lrn6zyrkqy6g4yy927wwzag2gklfrs"; + release."1.2.1".sha256 = "17vz88xjzxh3q7hs6hnndw61r3hdfawxp5awqpgfaxx4w6ni8z46"; + release."1.1.0".sha256 = "1c34v1k37rk7v0xk2czv5n79mbjxjrm6nh3llg2mpfmdsqi68wf3"; + release."1.0.0".sha256 = "1gqy9a4yavd0sa7kgysf9gf2lq4p8dmn4h89y8081f2j8zli0w5y"; + release."20190311".rev = "22af9e9a223d0038f05638654422e637e863b355"; + release."20190311".sha256 = "00rnr19lg6lg0haq1sy4ld38p7imzand6fc52fvfq27gblxkp2aq"; + release."20171102".rev = "0fdb769e1dc87a278383b44a9f5102cc7ccbafcf"; + release."20171102".sha256 = "0fri4nih40vfb0fbr82dsi631ydkw48xszinq43lyinpknf54y17"; + release."20170512".rev = "31eb050ae5ce57ab402db9726fb7cd945a0b4d03"; + release."20170512".sha256 = "033ch10i5wmqyw8j6wnr0dlbnibgfpr1vr0c07q3yj6h23xkmqpg"; + releaseRev = v: "v${v}"; -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 + preConfigure = 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 - ; + mlPlugin = true; + extraBuildInputs = optional recent coq.ocamlPackages.num; propagatedBuildInputs = [ ssreflect ] - ++ optionals recent [ coq-ext-lib simple-io ] - ++ optional (versionAtLeast coq.coq-version "8.10") - coq.ocamlPackages.ocamlbuild - ; + ++ optionals recent [ coq-ext-lib simple-io ] + ++ optional recent coq.ocamlPackages.ocamlbuild; + extraInstallFlags = [ "-f Makefile.coq" ]; 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/pkgs/development/coq-modules/StructTact/default.nix b/pkgs/development/coq-modules/StructTact/default.nix index 798aaabe6773..9770b9fb9c45 100644 --- a/pkgs/development/coq-modules/StructTact/default.nix +++ b/pkgs/development/coq-modules/StructTact/default.nix @@ -1,31 +1,11 @@ -{ 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; +{ lib, mkCoqDerivation, coq, version ? null }: +with lib; mkCoqDerivation { + pname = "StructTact"; + owner = "uwplse"; + inherit version; + defaultVersion = if versions.isGe "8.5" coq.coq-version then "20181102" else null; + release."20181102".rev = "82a85b7ec07e71fa6b30cfc05f6a7bfb09ef2510"; + release."20181102".sha256 = "08zry20flgj7qq37xk32kzmg4fg6d4wi9m7pf9aph8fd3j2a0b5v"; preConfigure = "patchShebangs ./configure"; - - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - passthru = { - compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.5"; - }; } diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix index a625aa54c148..af560ec49a0b 100644 --- a/pkgs/development/coq-modules/VST/default.nix +++ b/pkgs/development/coq-modules/VST/default.nix @@ -1,17 +1,15 @@ -{ stdenv, fetchFromGitHub, coq, compcert }: +{ lib, mkCoqDerivation, coq, compcert, version ? null }: -stdenv.mkDerivation rec { +with lib; mkCoqDerivation { pname = "coq${coq.coq-version}-VST"; - version = "2.6"; - - src = fetchFromGitHub { - owner = "PrincetonUniversity"; - repo = "VST"; - rev = "v${version}"; - sha256 = "00bf9hl4pvmsqa08lzjs1mrxyfgfxq4k6778pnldmc8ichm90jgk"; - }; - - buildInputs = [ coq ]; + namePrefix = []; + displayVersion = { coq = false; }; + owner = "PrincetonUniversity"; + repo = "VST"; + inherit version; + defaultVersion = if coq.coq-version == "8.11" then "2.6" else null; + release."2.6".sha256 = "00bf9hl4pvmsqa08lzjs1mrxyfgfxq4k6778pnldmc8ichm90jgk"; + releaseRev = v: "v${v}"; propagatedBuildInputs = [ compcert ]; preConfigure = "patchShebangs util"; @@ -30,14 +28,9 @@ stdenv.mkDerivation rec { 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/pkgs/development/coq-modules/Velisarios/default.nix b/pkgs/development/coq-modules/Velisarios/default.nix index 92c9b2569ca4..08322fb7fc40 100644 --- a/pkgs/development/coq-modules/Velisarios/default.nix +++ b/pkgs/development/coq-modules/Velisarios/default.nix @@ -1,41 +1,14 @@ -{ stdenv, fetchFromGitHub, coq }: +{ lib, mkCoqDerivation, coq, version ? null }: -let params = - { - "8.6" = { - version = "20180221"; - rev = "e1eee1f10d5d46331a560bd8565ac101229d0d6b"; - sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2"; - }; +with lib; mkCoqDerivation { + pname = "Velisarios"; + owner = "vrahli"; + inherit version; + defaultVersion = if versions.range "8.6" "8.8" coq.coq-version then "20180221" else null; - "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; + release."20180221".rev = "e1eee1f10d5d46331a560bd8565ac101229d0d6b"; + release."20180221".sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2"; + mlPlugin = true; buildPhase = "make -j$NIX_BUILD_CORES"; preBuild = "./create-makefile.sh"; @@ -43,8 +16,4 @@ stdenv.mkDerivation { 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/pkgs/development/coq-modules/Verdi/default.nix b/pkgs/development/coq-modules/Verdi/default.nix index 927cd832452b..d3769eb2c4db 100644 --- a/pkgs/development/coq-modules/Verdi/default.nix +++ b/pkgs/development/coq-modules/Verdi/default.nix @@ -1,37 +1,19 @@ -{ stdenv, fetchFromGitHub, coq, Cheerios, InfSeqExt, ssreflect }: +{ lib, mkCoqDerivation, coq, Cheerios, InfSeqExt, ssreflect, version ? null }: -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}"; +with lib; mkCoqDerivation { + pname = "verdi"; + owner = "uwplse"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.7"; out = "20200131"; } + { case = isEq "8.6"; out = "20181102"; } + ] null; + release."20200131".rev = "fdb4ede19d2150c254f0ebcfbed4fb9547a734b0"; + release."20200131".sha256 = "1a2k19f9q5k5djbxplqmmpwck49kw3lrm3aax920h4yb40czkd8m"; + release."20181102".rev = "25b79cf1be5527ab8dc1b8314fcee93e76a2e564"; + release."20181102".sha256 = "1vw47c37k5vaa8vbr6ryqy8riagngwcrfmb3rai37yi9xhdqg55z"; - 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/pkgs/development/coq-modules/autosubst/default.nix b/pkgs/development/coq-modules/autosubst/default.nix index 9507dc6751ae..b2609d5dfc32 100644 --- a/pkgs/development/coq-modules/autosubst/default.nix +++ b/pkgs/development/coq-modules/autosubst/default.nix @@ -1,33 +1,22 @@ -{ stdenv, fetchgit, coq, mathcomp }: +{ lib, mkCoqDerivation, coq, mathcomp, version ? null }: -stdenv.mkDerivation rec { +with lib; mkCoqDerivation { + pname = "autosubst"; + owner = "uds-psl"; + inherit version; + defaultVersion = with versions; + if range "8.5" "8.7" coq.coq-version then "5b40a32e" else null; - name = "coq-autosubst-${coq.coq-version}-${version}"; - version = "5b40a32e"; + release."5b40a32e".rev = "1c3bb3bbf5477e3b33533a0fc090399f45fe3034"; + release."5b40a32e".sha256 = "1wqfzc9az85fvx71xxfii502jgc3mp0r3xwfb8vnb03vkk625ln0"; - src = fetchgit { - url = "git://github.com/uds-psl/autosubst.git"; - rev = "1c3bb3bbf5477e3b33533a0fc090399f45fe3034"; - sha256 = "06pcjbngzwqyncvfwzz88j33wvdj9kizxyg5adp7y6186h8an341"; - }; - - buildInputs = [ coq ]; - propagatedBuildInputs = [ mathcomp ]; + propagatedBuildInputs = [ mathcomp.ssreflect ]; patches = [./0001-changes-to-work-with-Coq-8.6.patch]; - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - meta = with stdenv.lib; { + meta = { 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/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix index f0434c4ae471..84dc92a3cd5f 100644 --- a/pkgs/development/coq-modules/bignums/default.nix +++ b/pkgs/development/coq-modules/bignums/default.nix @@ -1,64 +1,25 @@ -{ stdenv, fetchFromGitHub, coq }: +{ lib, mkCoqDerivation, coq, version ? null }: -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"; - }; - "8.13" = { - rev = "V8.13.0"; - sha256 = "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y"; - }; - }; - param = params.${coq.coq-version}; -in +with lib; mkCoqDerivation { + pname = "bignums"; + owner = "coq"; + displayVersion = { bignums = ""; }; + inherit version; + defaultVersion = if versions.isGe "8.5" coq.coq-version + then "${coq.coq-version}.0" else null; -stdenv.mkDerivation { + release."8.13.0".sha256 = "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y"; + release."8.12.0".sha256 = "14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8"; + release."8.11.0".sha256 = "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp"; + release."8.10.0".sha256 = "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5"; + release."8.9.0".sha256 = "03qz1w2xb2j5p06liz5yyafl0fl9vprcqm6j0iwi7rxwghl00p01"; + release."8.8.0".sha256 = "1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg"; + release."8.7.0".sha256 = "11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl"; + release."8.6.0".rev = "v8.6.0"; + release."8.6.0".sha256 = "0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj"; + releaseRev = v: "V${v}"; - name = "coq${coq.coq-version}-bignums"; + mlPlugin = true; - 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; - }; + meta = { license = licenses.lgpl2; }; } diff --git a/pkgs/development/coq-modules/category-theory/default.nix b/pkgs/development/coq-modules/category-theory/default.nix index 1178b1558ff7..339bcb9d6b09 100644 --- a/pkgs/development/coq-modules/category-theory/default.nix +++ b/pkgs/development/coq-modules/category-theory/default.nix @@ -1,54 +1,26 @@ -{ stdenv, fetchgit, coq, ssreflect, equations }: +{ lib, mkCoqDerivation, coq, ssreflect, equations, version ? null }: -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 +with lib; mkCoqDerivation { -stdenv.mkDerivation { + pname = "category-theory"; + owner = "jwiegley"; - name = "coq${coq.coq-version}-category-theory-${param.version}"; + release."20190414".rev = "706fdb4065cc2302d92ac2bce62cb59713253119"; + release."20190414".sha256 = "16lg4xs2wzbdbsn148xiacgl4wq4xwfqjnjkdhfr3w0qh1s81hay"; + release."20180709".rev = "3b9ba7b26a64d49a55e8b6ccea570a7f32c11ead"; + release."20180709".sha256 = "0f2nr8dgn1ab7hr7jrdmr1zla9g9h8216q4yf4wnff9qkln8sbbs"; - src = fetchgit { - url = "git://github.com/jwiegley/category-theory.git"; - inherit (param) rev sha256; - }; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = range "8.8" "8.9"; out = "20190414"; } + { case = range "8.6" "8.7"; out = "20180709"; } + ] null; - buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml camlp5 findlib ]); + mlPlugin = true; 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"; + meta = { 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/pkgs/development/coq-modules/contribs/default.nix b/pkgs/development/coq-modules/contribs/default.nix index d2787f0948e0..cb6dedca3551 100644 --- a/pkgs/development/coq-modules/contribs/default.nix +++ b/pkgs/development/coq-modules/contribs/default.nix @@ -1,27 +1,16 @@ -{ stdenv, fetchFromGitHub, coq }: +{ lib, mkCoqDerivation, coq, callPackage }: -let mkContrib = repo: revs: param: - stdenv.mkDerivation rec { - name = "coq${coq.coq-version}-${repo}-${version}"; - version = param.version; - - src = fetchFromGitHub { +with lib; let mkContrib = pname: coqs: param: + let contribVersion = {version ? null}: mkCoqDerivation ({ + inherit pname version; 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 + mlPlugin = true; + } // optionalAttrs (builtins.elem coq.coq-version coqs) ({ + defaultVersion = param.version; + release = { "${param.version}" = { inherit (param) rev sha256; }; }; + } // (removeAttrs param [ "version" "rev" "sha256" ])) + ); in + makeOverridable contribVersion {} ; in { aac-tactics = mkContrib "aac-tactics" [ "8.7" "8.8" ] { "8.7" = { @@ -353,10 +342,10 @@ let mkContrib = repo: revs: param: sha256 = "02jcp74i5icv92xkq3mcx91786d56622ghgnjiz3b51wfqs6ldic"; }; - firing-squad = mkContrib "firing-squad" [ "8.6" "8.7" ] { - version = "v8.5.0-9-gbe728cd"; - rev = "be728cddbee58088809b51c25425d2a4bdf9b823"; - sha256 = "0i0v5x6lncjasxk22pras3644ff026q8jai45dbimf2fz73312c9"; + firing-squad = mkContrib "firing-squad" [ "8.6" ] { + version = "v8.5.0-9-gbe728cd"; + rev = "be728cddbee58088809b51c25425d2a4bdf9b823"; + sha256 = "0i0v5x6lncjasxk22pras3644ff026q8jai45dbimf2fz73312c9"; }; float = mkContrib "float" [ "8.7" ] { @@ -525,6 +514,7 @@ let mkContrib = repo: revs: param: version = "v8.6.0"; rev = "6279ed83244dc4aec2e23ffb4c87e3f10a50326d"; sha256 = "1yvlnqwa7ka4a0yg0j7zrzvayhsm1shvsjjawjv552sxc9519aag"; + installFlags = [ "COQBIN=$(out)/lib/coq/${coq.coq-version}/bin/" ]; # hack }; ipc = mkContrib "ipc" [ "8.6" "8.7" ] { @@ -635,12 +625,6 @@ let mkContrib = repo: revs: param: 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"; diff --git a/pkgs/development/coq-modules/coq-bits/default.nix b/pkgs/development/coq-modules/coq-bits/default.nix index 9665c5400d85..410280925dcc 100644 --- a/pkgs/development/coq-modules/coq-bits/default.nix +++ b/pkgs/development/coq-modules/coq-bits/default.nix @@ -1,38 +1,24 @@ -{ stdenv, fetchFromGitHub, coq, mathcomp-algebra }: +{ lib, mkCoqDerivation, coq, mathcomp, version ? null }: -let - version = "20190812"; -in +with lib; mkCoqDerivation { + pname = "coq-bits"; + repo = "bits"; + inherit version; + defaultVersion = if versions.isGe "8.7" coq.version then "20190812" else null; -stdenv.mkDerivation { - name = "coq${coq.coq-version}-coq-bits-${version}"; + release."20190812".rev = "1.0.0"; + release."20190812".sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl"; - src = fetchFromGitHub { - owner = "coq-community"; - repo = "bits"; - rev = "1.0.0"; - sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl"; - }; - - buildInputs = [ coq ]; - propagatedBuildInputs = [ mathcomp-algebra ]; - - enableParallelBuilding = true; + propagatedBuildInputs = [ mathcomp.algebra ]; 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"; + meta = { 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/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix index 230320671a7f..18dbeaea201d 100644 --- a/pkgs/development/coq-modules/coq-elpi/default.nix +++ b/pkgs/development/coq-modules/coq-elpi/default.nix @@ -1,43 +1,33 @@ -{ stdenv, fetchFromGitHub, which, coq }: +{ lib, mkCoqDerivation, which, coq, version ? null }: -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; - }; +with builtins; with lib; let + elpi = coq.ocamlPackages.elpi.override ( + optionalAttrs (coq.coq-version == "8.11") { version = "1.11.4"; } + ); +in mkCoqDerivation { + pname = "elpi"; + repo = "coq-elpi"; + owner = "LPCIC"; + inherit version; + defaultVersion = lib.switch coq.coq-version [ + { case = "8.13"; out = "1.8.1"; } + { case = "8.12"; out = "1.8.0"; } + { case = "8.11"; out = "1.6.0_8.11"; } + ] null; + release."1.8.1".sha256 = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r"; + release."1.8.0".sha256 = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1"; + release."1.7.0".sha256 = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8"; + release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq"; + release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b"; + releaseRev = v: "v${v}"; nativeBuildInputs = [ which ]; - buildInputs = [ coq coq.ocaml ] ++ (with coq.ocamlPackages; [ findlib elpi ]); - - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + mlPlugin = true; + extraBuildInputs = [ elpi ]; 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; + maintainers = [ maintainers.cohencyril ]; + license = licenses.lgpl21; }; } diff --git a/pkgs/development/coq-modules/coq-ext-lib/default.nix b/pkgs/development/coq-modules/coq-ext-lib/default.nix index e0ca52086206..8acb0643781d 100644 --- a/pkgs/development/coq-modules/coq-ext-lib/default.nix +++ b/pkgs/development/coq-modules/coq-ext-lib/default.nix @@ -1,63 +1,29 @@ -{ stdenv, fetchFromGitHub, coq, ...}@args: +{ lib, mkCoqDerivation, coq, version ? null }: -let - hashes = { - "0.9.4" = "1y66pamgsdxlq2w1338lj626ln70cwj7k53hxcp933g8fdsa4hp0"; - "0.9.5" = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg"; - "0.9.7" = "00v4bm4glv1hy08c8xsm467az6d1ashrznn8p2bmbmmp52lfg7ag"; - "0.10.0" = "1kxi5bmjwi5zqlqgkyzhhxwgcih7wf60cyw9398k2qjkmi186r4a"; - "0.10.1" = "0r1vspad8fb8bry3zliiz4hfj4w1iib1l2gm115a94m6zbiksd95"; - "0.10.2" = "1b150rc5bmz9l518r4m3vwcrcnnkkn9q5lrwygkh0a7mckgg2k9f"; - "0.10.3" = "0795gs2dlr663z826mp63c8h2zfadn541dr8q0fvnvi2z7kfyslb"; - "0.11.1" = "0dmf1p9j8lm0hwaq0af18jxdwg869xi2jm8447zng7krrq3kvkg5"; - "0.11.2" = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; - "0.11.3" = "1w99nzpk72lffxis97k235axss5lmzhy5z3lga2i0si95mbpil42"; - }; +with lib; mkCoqDerivation rec { + pname = "coq-ext-lib"; + owner = "coq-ext-lib"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = range "8.8" "8.12"; out = "0.11.3"; } + { case = "8.7"; out = "0.9.7"; } + { case = "8.6"; out = "0.9.5"; } + { case = "8.5"; out = "0.9.4"; } + ] null; + release."0.11.3".sha256 = "1w99nzpk72lffxis97k235axss5lmzhy5z3lga2i0si95mbpil42"; + release."0.11.2".sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; + release."0.10.3".sha256 = "0795gs2dlr663z826mp63c8h2zfadn541dr8q0fvnvi2z7kfyslb"; + release."0.11.1".sha256 = "0dmf1p9j8lm0hwaq0af18jxdwg869xi2jm8447zng7krrq3kvkg5"; + release."0.10.2".sha256 = "1b150rc5bmz9l518r4m3vwcrcnnkkn9q5lrwygkh0a7mckgg2k9f"; + release."0.10.1".sha256 = "0r1vspad8fb8bry3zliiz4hfj4w1iib1l2gm115a94m6zbiksd95"; + release."0.10.0".sha256 = "1kxi5bmjwi5zqlqgkyzhhxwgcih7wf60cyw9398k2qjkmi186r4a"; + release."0.9.7".sha256 = "00v4bm4glv1hy08c8xsm467az6d1ashrznn8p2bmbmmp52lfg7ag"; + release."0.9.5".sha256 = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg"; + release."0.9.4".sha256 = "1y66pamgsdxlq2w1338lj626ln70cwj7k53hxcp933g8fdsa4hp0"; + releaseRev = v: "v${v}"; - default-versions = { - "8.5" = "0.9.4"; - "8.6" = "0.9.5"; - "8.7" = "0.9.7"; - "8.8" = "0.11.3"; - "8.9" = "0.11.3"; - "8.10" = "0.11.3"; - "8.11" = "0.11.3"; - "8.12" = "0.11.3"; - }; - - param = rec { - version = args.version or default-versions.${coq.coq-version}; - sha256 = hashes.${version}; - }; - -in - -stdenv.mkDerivation rec { - - name = "coq${coq.coq-version}-coq-ext-lib-${version}"; - inherit (param) version; - - src = fetchFromGitHub { - owner = "coq-community"; - repo = "coq-ext-lib"; - rev = "v${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"; + meta = { 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 default-versions; }; } diff --git a/pkgs/development/coq-modules/coq-haskell/default.nix b/pkgs/development/coq-modules/coq-haskell/default.nix index 7c86a7d55f34..7caf754ae50a 100644 --- a/pkgs/development/coq-modules/coq-haskell/default.nix +++ b/pkgs/development/coq-modules/coq-haskell/default.nix @@ -1,60 +1,21 @@ -{ stdenv, fetchgit, coq, ssreflect }: +{ lib, mkCoqDerivation, coq, ssreflect, version ? null }: -let params = - { - "8.5" = { - version = "20171215"; - rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968"; - sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv"; - }; +with lib; mkCoqDerivation { - "8.6" = { - version = "20171215"; - rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968"; - sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv"; - }; + pname = "coq-haskell"; + owner = "jwiegley"; + inherit version; + defaultVersion = if versions.range "8.5" "8.8" coq.coq-version then "20171215" else null; + release."20171215".rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968"; + release."20171215".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 ]; + mlPlugin = true; + extraInstallFlags = [ "-f Makefile.coq" ]; 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"; + meta = { 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/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix new file mode 100644 index 000000000000..4c978a791db8 --- /dev/null +++ b/pkgs/development/coq-modules/coqeal/default.nix @@ -0,0 +1,24 @@ +{ coq, mkCoqDerivation, mathcomp, bignums, paramcoq, multinomials, + lib, which, version ? null }: + +with lib; mkCoqDerivation { + + pname = "CoqEAL"; + owner = "CoqEAL"; + inherit version; + defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ + { cases = [ (isGe "8.7") "1.11.0" ]; out = "1.0.4"; } + { cases = [ (isGe "8.7") "1.10.0" ]; out = "1.0.3"; } + ] null; + + release."1.0.4".sha256 = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk"; + release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24"; + + extraBuildInputs = [ which ]; + propagatedBuildInputs = [ mathcomp.algebra bignums paramcoq multinomials ]; + + meta = { + description = "CoqEAL - The Coq Effective Algebra Library"; + license = licenses.mit; + }; +} diff --git a/pkgs/development/coq-modules/coqhammer/default.nix b/pkgs/development/coq-modules/coqhammer/default.nix index 56fce9ac526f..89aa8d74e85c 100644 --- a/pkgs/development/coq-modules/coqhammer/default.nix +++ b/pkgs/development/coq-modules/coqhammer/default.nix @@ -1,43 +1,28 @@ -{ stdenv, fetchFromGitHub, coq }: +{ lib, mkCoqDerivation, coq, version ? null }: -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 +with lib; mkCoqDerivation { + inherit version; + pname = "coqhammer"; + owner = "lukaszcz"; + defaultVersion = with versions; switch coq.coq-version [ + { case = "8.12"; out = "1.3-coq8.12"; } + { case = "8.11"; out = "1.3-coq8.11"; } + { case = "8.10"; out = "1.3-coq8.10"; } + { case = "8.9"; out = "1.1.1-coq8.9"; } + { case = "8.8"; out = "1.1-coq8.8"; } + ] null; + release."1.3-coq8.12".sha256 = "1q1y3cwhd98pkm98g71fsdjz85bfwgcz2xn7s7wwmiraifv5l6z8"; + release."1.3-coq8.11".sha256 = "08zf8qfna7b9p2myfaz4g7bas3a1q1156x78n5isqivlnqfrjc1b"; + release."1.3-coq8.10".sha256 = "1fj8497ir4m79hyrmmmmrag01001wrby0h24wv6525vz0w5py3cd"; + release."1.1.1-coq8.9".sha256 = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9"; + release."1.1-coq8.8".sha256 = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h"; -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; - }; + release."1.3-coq8.12".version = "1.3"; + release."1.3-coq8.11".version = "1.3"; + release."1.3-coq8.10".version = "1.3"; + release."1.1.1-coq8.9".version = "1.1.1"; + release."1.1-coq8.9".version = "1.1"; + releaseRev = v: "v${v}"; postPatch = '' substituteInPlace Makefile.coq.local --replace \ @@ -46,26 +31,16 @@ stdenv.mkDerivation rec { 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}/" ]; + mlPlugin = true; 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 ]; + license = licenses.lgpl21; + maintainers = [ maintainers.vbgl ]; }; - - passthru = { - compatibleCoqVersions = v: builtins.hasAttr v params; - }; - } diff --git a/pkgs/development/coq-modules/coqprime/default.nix b/pkgs/development/coq-modules/coqprime/default.nix index f16341ddbd1b..79db14610758 100644 --- a/pkgs/development/coq-modules/coqprime/default.nix +++ b/pkgs/development/coq-modules/coqprime/default.nix @@ -1,60 +1,29 @@ -{ stdenv, which, fetchFromGitHub, coq, bignums }: +{ which, lib, mkCoqDerivation, coq, bignums, version ? null }: -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 +with lib; mkCoqDerivation { -stdenv.mkDerivation rec { + pname = "coqprime"; + owner = "thery"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = "8.12"; out = "8.12"; } + { case = range "8.10" "8.11"; out = "8.10"; } + { case = range "8.8" "8.9"; out = "8.8"; } + { case = "8.7"; out = "8.7.2"; } + ] null; - 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 ]; + release."8.12".sha256 = "1slka4w0pya15js4drx9frj7lxyp3k2lzib8v23givzpnxs8ijdj"; + release."8.10".sha256 = "0r9gnh5a5ykiiz5h1i8xnzgiydpwc4z9qhndxyya85xq0f910qaz"; + release."8.8".sha256 = "075yjczk79pf1hd3lgdjiz84ilkzfxjh18lgzrhhqp7d3kz5lxp5"; + release."8.7.2".sha256 = "15zlcrx06qqxjy3nhh22wzy0rb4npc8l4nx2bbsfsvrisbq1qb7k"; + releaseRev = v: "v${v}"; + extraBuildInputs = [ which ]; propagatedBuildInputs = [ bignums ]; - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - meta = with stdenv.lib; { + meta = with 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; + maintainers = [ maintainers.vbgl ]; }; } diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/coq-modules/coquelicot/default.nix index e45077f89fdd..b7f5802b9d40 100644 --- a/pkgs/development/coq-modules/coquelicot/default.nix +++ b/pkgs/development/coq-modules/coquelicot/default.nix @@ -1,43 +1,29 @@ -{ stdenv, fetchurl, which, coq, ssreflect }: +{ lib, mkCoqDerivation, which, autoconf, + coq, ssreflect, version ? null }: -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 +with lib; mkCoqDerivation { + pname = "coquelicot"; + owner = "coquelicot"; + domain = "gitlab.inria.fr"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.8" ; out = "3.2.0"; } + { case = range "8.8" "8.13"; out = "3.1.0"; } + { case = range "8.5" "8.9"; out = "3.0.2"; } + ] null; + release."3.2.0".sha256 = "07w7dbl8x7xxnbr2q39wrdh054gvi3daqjpdn1jm53crsl1fjxm4"; + release."3.1.0".sha256 = "02i0djar13yk01hzaqprcldhhscn9843x9nf6x3jkv4wv1jwnx9f"; + release."3.0.2".sha256 = "1rqfbbskgz7b1bcpva8wh3v3456sq2364y804f94sc8y5sij23nl"; + releaseRev = v: "coquelicot-${v}"; -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 ]; + nativeBuildInputs = [ which autoconf ]; propagatedBuildInputs = [ ssreflect ]; - - configureFlags = [ "--libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Coquelicot" ]; - buildPhase = "./remake"; - installPhase = "./remake install"; + useMelquiondRemake.logpath = "Coquelicot"; 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; + license = licenses.lgpl3; + maintainers = [ maintainers.vbgl ]; }; - - 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/pkgs/development/coq-modules/corn/default.nix b/pkgs/development/coq-modules/corn/default.nix index 14ff74506f37..9f2316f3177d 100644 --- a/pkgs/development/coq-modules/corn/default.nix +++ b/pkgs/development/coq-modules/corn/default.nix @@ -1,17 +1,10 @@ -{ stdenv, fetchFromGitHub, coq, bignums, math-classes }: +{ lib, mkCoqDerivation, coq, bignums, math-classes, version ? null }: -stdenv.mkDerivation rec { +with lib; mkCoqDerivation 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 ]; + inherit version; + defaultVersion = if versions.range "8.6" "8.9" coq.coq-version then "8.8.1" else null; + release."8.8.1".sha256 = "0gh32j0f18vv5lmf6nb87nr5450w6ai06rhrnvlx2wwi79gv10wp"; preConfigure = "patchShebangs ./configure.sh"; configureScript = "./configure.sh"; @@ -19,20 +12,10 @@ stdenv.mkDerivation rec { 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; + license = licenses.gpl2; description = "A Coq library for constructive analysis"; - maintainers = [ stdenv.lib.maintainers.vbgl ]; - inherit (coq.meta) platforms; + maintainers = [ maintainers.vbgl ]; }; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" ]; - }; - } diff --git a/pkgs/development/coq-modules/dpdgraph/default.nix b/pkgs/development/coq-modules/dpdgraph/default.nix index 195a1c4eada5..c6cc0d34ed1c 100644 --- a/pkgs/development/coq-modules/dpdgraph/default.nix +++ b/pkgs/development/coq-modules/dpdgraph/default.nix @@ -1,88 +1,58 @@ -{ stdenv, fetchFromGitHub, autoreconfHook, coq }: +{ lib, mkCoqDerivation, autoreconfHook, coq, version ? null }: -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 +with lib; +let hasWarning = versionAtLeast coq.ocamlPackages.ocaml.version "4.08"; in -let hasWarning = stdenv.lib.versionAtLeast coq.ocamlPackages.ocaml.version "4.08"; in +mkCoqDerivation { + pname = "dpdgraph"; + owner = "Karmaki"; + repo = "coq-dpdgraph"; + inherit version; + defaultVersion = switch coq.coq-version [ + { case = "8.12"; out = "0.6.8"; } + { case = "8.11"; out = "0.6.7"; } + { case = "8.10"; out = "0.6.6"; } + { case = "8.9"; out = "0.6.5"; } + { case = "8.8"; out = "0.6.3"; } + { case = "8.7"; out = "0.6.2"; } + { case = "8.6"; out = "0.6.1"; } + { case = "8.5"; out = "0.6"; } + ] null; -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; - }; + release."0.6.8".sha256 = "1mj6sknsd53xfb387sp3kdwvl4wn80ck24bfzf3s6mgw1a12vyps"; + release."0.6.7".sha256 = "01vpi7scvkl4ls1z2k2x9zd65wflzb667idj759859hlz3ps9z09"; + release."0.6.6".sha256 = "1gjrm5zjzw4cisiwdr5b3iqa7s4cssa220xr0k96rwgk61rcjd8w"; + release."0.6.5".sha256 = "1f34z24yg05b1096gqv36jr3vffkcjkf9qncii3pzhhvagxd0w2f"; + release."0.6.3".rev = "0acbd0a594c7e927574d5f212cc73a486b5305d2"; + release."0.6.3".sha256 = "0c95b0bz2kjm6swr5na4gs06lxxywradszxbr5ldh2zx02r3f3rx"; + release."0.6.2".rev = "d76ddde37d918569945774733b7997e8b24daf51"; + release."0.6.2".sha256 = "04lnf4b25yarysj848cfl8pd3i3pr3818acyp9hgwdgd1rqmhjwm"; + release."0.6.1".rev = "c3b87af6bfa338e18b83f014ebd0e56e1f611663"; + release."0.6.1".sha256 = "1jaafkwsb5450378nprjsds1illgdaq60gryi8kspw0i25ykz2c9"; + release."0.6".sha256 = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n"; + releaseRev = v: "v${v}"; nativeBuildInputs = [ autoreconfHook ]; - buildInputs = [ coq ] - ++ (with coq.ocamlPackages; [ ocaml findlib ocamlgraph ] - ++ stdenv.lib.optional (!stdenv.lib.versionAtLeast coq.coq-version "8.10") camlp5); + mlPlugin = true; + extraBuildInputs = [ coq.ocamlPackages.ocamlgraph ]; # 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 '' + preConfigure = optionalString hasWarning '' substituteInPlace Makefile.in --replace "-warn-error +a " "" ''; - buildFlags = stdenv.lib.optional hasWarning "WARN_ERR="; + buildFlags = optional hasWarning "WARN_ERR="; preInstall = '' mkdir -p $out/bin ''; - installFlags = [ - "COQLIB=$(out)/lib/coq/${coq.coq-version}/" - "BINDIR=$(out)/bin" - ]; + extraInstallFlags = [ "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; + license = licenses.lgpl21; + maintainers = with maintainers; [ vbgl ]; }; - - passthru = { - compatibleCoqVersions = v: builtins.hasAttr v params; - }; - } diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/coq-modules/equations/default.nix index 5a07d537536c..352222e8aa62 100644 --- a/pkgs/development/coq-modules/equations/default.nix +++ b/pkgs/development/coq-modules/equations/default.nix @@ -1,79 +1,48 @@ -{ stdenv, fetchFromGitHub, coq }: +{ lib, mkCoqDerivation, coq, version ? null }: -let - params = { - "8.6" = { - version = "1.0"; - rev = "v1.0"; - sha256 = "19ylw9v9g35607w4hm86j7mmkghh07hmkc1ls5bqlz3dizh5q4pj"; - }; +with lib; mkCoqDerivation { + pname = "equations"; + owner = "mattam82"; + repo = "Coq-Equations"; + inherit version; + defaultVersion = switch coq.coq-version [ + { case = "8.12"; out = "1.2.3+coq8.12"; } + { case = "8.11"; out = "1.2.3+coq8.11"; } + { case = "8.10"; out = "1.2.1+coq8.10-2"; } + { case = "8.9"; out = "1.2.1+coq8.9"; } + { case = "8.8"; out = "1.2+coq8.8"; } + { case = "8.7"; out = "1.0+coq8.7"; } + { case = "8.6"; out = "1.0+coq8.6"; } + ] null; - "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 ]; + release."1.0+coq8.6".version = "1.0"; + release."1.0+coq8.6".rev = "v1.0"; + release."1.0+coq8.6".sha256 = "19ylw9v9g35607w4hm86j7mmkghh07hmkc1ls5bqlz3dizh5q4pj"; + release."1.0+coq8.7".version = "1.0"; + release."1.0+coq8.7".rev = "v1.0-8.7"; + release."1.0+coq8.7".sha256 = "1bavg4zl1xn0jqrdq8iw7xqzdvdf39ligj9saz5m9c507zri952h"; + release."1.2+coq8.8".version = "1.2"; + release."1.2+coq8.8".rev = "v1.2-8.8"; + release."1.2+coq8.8".sha256 = "06452fyzalz7zcjjp73qb7d6xvmqb6skljkivf8pfm55fsc8s7kx"; + release."1.2.1+coq8.9".version = "1.2.1"; + release."1.2.1+coq8.9".rev = "v1.2.1-8.9"; + release."1.2.1+coq8.9".sha256 = "0d8ddj6nc6p0k25cd8fs17cq427zhzbc3v9pk2wd2fnvk70nlfij"; + release."1.2.1+coq8.10-2".version = "1.2.1"; + release."1.2.1+coq8.10-2".rev = "v1.2.1-8.10-2"; + release."1.2.1+coq8.10-2".sha256 = "0j3z4l5nrbyi9zbbyqkc6kassjanwld2188mwmrbqspaypm2ys68"; + release."1.2.3+coq8.11".version = "1.2.3"; + release."1.2.3+coq8.11".rev = "v1.2.3-8.11"; + release."1.2.3+coq8.11".sha256 = "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf"; + release."1.2.3+coq8.12".version = "1.2.3"; + release."1.2.3+coq8.12".rev = "v1.2.3-8.12"; + release."1.2.3+coq8.12".sha256 = "1y0jkvzyz5ssv5vby41p1i8zs7nsdc8g3pzyq73ih9jz8h252643"; + mlPlugin = true; preBuild = "coq_makefile -f _CoqProject -o Makefile"; - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - meta = with stdenv.lib; { + meta = { 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/pkgs/development/coq-modules/fiat/HEAD.nix b/pkgs/development/coq-modules/fiat/HEAD.nix index fd3ade0c64b5..47f097a34b2e 100644 --- a/pkgs/development/coq-modules/fiat/HEAD.nix +++ b/pkgs/development/coq-modules/fiat/HEAD.nix @@ -1,17 +1,17 @@ -{stdenv, fetchgit, coq, python27}: +{lib, mkCoqDerivation, coq, python27, version ? null }: -stdenv.mkDerivation rec { +with lib; mkCoqDerivation rec { + pname = "fiat"; + owner = "mit-plv"; + repo = "fiat"; + displayVersion = { fiat = v: "unstable-${v}"; }; + inherit version; + defaultVersion = if coq.coq-version == "8.5" then "2016-10-24" else null; + release."2016-10-24".rev = "7feb6c64be9ebcc05924ec58fe1463e73ec8206a"; + release."2016-10-24".sha256 = "0griqc675yylf9rvadlfsabz41qy5f5idya30p5rv6ysiakxya64"; - 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 ]); + mlPlugin = true; + extraBuildInputs = [ python27 ]; prePatch = "patchShebangs etc/coq-scripts"; @@ -26,14 +26,9 @@ stdenv.mkDerivation rec { cp -pR src/* $COQLIB/user-contrib/Fiat ''; - meta = with stdenv.lib; { + meta = { 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/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/coq-modules/flocq/default.nix index c5d3a295f2bc..2598d4e233eb 100644 --- a/pkgs/development/coq-modules/flocq/default.nix +++ b/pkgs/development/coq-modules/flocq/default.nix @@ -1,49 +1,26 @@ -{ stdenv, bash, which, autoconf, automake, fetchzip, coq }: +{ lib, bash, which, autoconf, automake, + mkCoqDerivation, coq, version ? null }: -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 +with lib; mkCoqDerivation { + pname = "flocq"; + owner = "flocq"; + domain = "gitlab.inria.fr"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.7"; out = "3.3.1"; } + { case = range "8.5" "8.8"; out = "2.6.1"; } + ] null; + release."3.3.1".sha256 = "1mk8adhi5hrllsr0hamzk91vf2405sjr4lh5brg9201mcw11abkz"; + release."2.6.1".sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj"; + releaseRev = v: "flocq-${v}"; -stdenv.mkDerivation rec { + nativeBuildInputs = [ bash which autoconf ]; + mlPlugin = true; + useMelquiondRemake.logpath = "Flocq"; - 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/"; + meta = { 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/pkgs/development/coq-modules/gappalib/default.nix b/pkgs/development/coq-modules/gappalib/default.nix index f6109398da8e..a835d53fdedb 100644 --- a/pkgs/development/coq-modules/gappalib/default.nix +++ b/pkgs/development/coq-modules/gappalib/default.nix @@ -1,30 +1,24 @@ -{ stdenv, fetchurl, which, coq, flocq }: +{ which, lib, mkCoqDerivation, autoconf, coq, flocq, version ? null }: -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"; - }; +with lib; mkCoqDerivation { + pname = "gappalib"; + repo = "coq"; + owner = "gappa"; + domain = "gitlab.inria.fr"; + inherit version; + defaultVersion = if versions.isGe "8.8" coq.coq-version then "1.4.5" else null; + release."1.4.5".sha256 = "081hib1d9wfm29kis390qsqch8v6fs3q71g2rgbbzx5y5cf48n9k"; + release."1.4.4".sha256 = "114q2hgw64j6kqa9mg3qcp1nlf0ia46z2xadq81fnkxqm856ml7l"; + releaseRev = v: "gappalib-coq-${v}"; - nativeBuildInputs = [ which ]; - buildInputs = [ coq coq.ocamlPackages.ocaml ]; + nativeBuildInputs = [ which autoconf ]; + mlPlugin = true; propagatedBuildInputs = [ flocq ]; - - configurePhase = "./configure --libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Gappa"; - buildPhase = "./remake"; - installPhase = "./remake install"; + useMelquiondRemake.logpath = "Gappa"; 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; + license = licenses.lgpl21; + maintainers = [ maintainers.vbgl ]; }; - - passthru = { - compatibleCoqVersions = stdenv.lib.flip builtins.elem [ "8.8" "8.9" "8.10" "8.11" "8.12" ]; - }; - } diff --git a/pkgs/development/coq-modules/heq/default.nix b/pkgs/development/coq-modules/heq/default.nix index d0445c83ca59..4bf9139b4947 100644 --- a/pkgs/development/coq-modules/heq/default.nix +++ b/pkgs/development/coq-modules/heq/default.nix @@ -1,30 +1,23 @@ -{stdenv, fetchurl, coq, unzip}: +{lib, fetchzip, mkCoqDerivation, coq, version ? null }: -stdenv.mkDerivation rec { +with lib; mkCoqDerivation { + pname = "heq"; + repo = "Heq"; + owner = "gil"; + domain = "mpi-sws.org"; + inherit version fetcher; + defaultVersion = if versions.isLt "8.8" coq.coq-version then "0.92" else null; + release."0.92".sha256 = "0cf8y6728n81wwlbpq3vi7l2dbzi7759klypld4gpsjjp1y1fj74"; - 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 ]; + mlPlugin = true; propagatedBuildInputs = [ coq ]; + extraInstallFlags = [ "COQLIB=$out/lib/coq/${coq.coq-version}" ]; preBuild = "cd src"; - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}" ]; - - meta = with stdenv.lib; { + meta = { 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/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix index 9be8459ee9f0..530763c9439d 100644 --- a/pkgs/development/coq-modules/hierarchy-builder/default.nix +++ b/pkgs/development/coq-modules/hierarchy-builder/default.nix @@ -1,43 +1,24 @@ -{ stdenv, fetchFromGitHub, which, coq, coq-elpi }: +{ lib, mkCoqDerivation, which, coq, coq-elpi, version ? null }: -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; - }; +with lib; mkCoqDerivation { + pname = "hierarchy-builder"; + owner = "math-comp"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.12"; out = "1.0.0"; } + { case = range "8.11" "8.12"; out = "0.10.0"; } + ] null; + release."1.0.0".sha256 = "0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp"; + release."0.10.0".sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h"; + releaseRev = v: "v${v}"; 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''; + extraInstallFlags = [ "VFILES=structures.v" ]; 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; + maintainers = [ maintainers.cohencyril ]; + license = licenses.lgpl21; }; } diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix index e72fe7845c84..8671eba67241 100644 --- a/pkgs/development/coq-modules/interval/default.nix +++ b/pkgs/development/coq-modules/interval/default.nix @@ -1,62 +1,31 @@ -{ stdenv, fetchurl, which, coq, coquelicot, flocq, mathcomp -, bignums ? null }: +{ lib, mkCoqDerivation, which, autoconf +, coq, coquelicot, flocq, mathcomp +, bignums ? null, version ? 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 +with lib; mkCoqDerivation { + pname = "interval"; + owner = "coqinterval"; + domain = "gitlab.inria.fr"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.8" ; out = "4.1.0"; } + { case = range "8.8" "8.12"; out = "4.0.0"; } + { case = range "8.7" "8.11"; out = "3.4.2"; } + { case = range "8.5" "8.6"; out = "3.3.0"; } + ] null; + release."4.1.0".sha256 = "1jv27n5c4f3a9d8sizraa920iqi35x8cik8lm7pjp1dkiifz47nb"; + release."4.0.0".sha256 = "1hhih6zmid610l6c8z3x4yzdzw9jniyjiknd1vpkyb2rxvqm3gzp"; + release."3.4.2".sha256 = "07ngix32qarl3pjnm9d0vqc9fdrgm08gy7zp306hwxjyq7h1v7z0"; + release."3.3.0".sha256 = "0lz2hgggzn4cvklvm8rpaxvwaryf37i8mzqajqgdxdbd8f12acsz"; + releaseRev = v: "interval-${v}"; -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 ]; + nativeBuildInputs = [ which autoconf ]; propagatedBuildInputs = [ bignums coquelicot flocq ]; + useMelquiondRemake.logpath = "Interval"; - 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/"; + meta = with lib; { 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/pkgs/development/coq-modules/iris/default.nix b/pkgs/development/coq-modules/iris/default.nix index 6826e07d613e..b46383fa1679 100644 --- a/pkgs/development/coq-modules/iris/default.nix +++ b/pkgs/development/coq-modules/iris/default.nix @@ -1,33 +1,19 @@ -{ stdenv, fetchFromGitLab, coq, stdpp }: +{ lib, mkCoqDerivation, coq, stdpp, version ? null }: -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"; - }; +with lib; mkCoqDerivation rec { + pname = "iris"; + domain = "gitlab.mpi-sws.org"; + owner = "iris"; + inherit version; + defaultVersion = if versions.range "8.9" "8.12" coq.coq-version then "3.3.0" else null; + release."3.3.0".sha256 = "0az4gkp5m8sq0p73dlh0r7ckkzhk7zkg5bndw01bdsy5ywj0vilp"; + releaseRev = v: "iris-${v}"; - 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 ]; + license = licenses.bsd3; + maintainers = [ maintainers.vbgl ]; }; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.9" "8.10" "8.11" "8.12" ]; - }; - } diff --git a/pkgs/development/coq-modules/ltac2/default.nix b/pkgs/development/coq-modules/ltac2/default.nix index 92484f169c15..1d0d03fb7f7c 100644 --- a/pkgs/development/coq-modules/ltac2/default.nix +++ b/pkgs/development/coq-modules/ltac2/default.nix @@ -1,57 +1,28 @@ -{ stdenv, fetchFromGitHub, which, coq }: +{ lib, mkCoqDerivation, which, coq, version ? null }: -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; - }; +with lib; mkCoqDerivation { + pname = "ltac2"; + owner = "coq"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = "8.10"; out = "0.3"; } + { case = "8.9"; out = "0.2"; } + { case = "8.8"; out = "0.1"; } + { case = "8.7"; out = "0.1-8.7"; } + ] null; + release."0.3".sha256 = "0pzs5nsakh4l8ffwgn4ryxbnxdv2x0r1i7bc598ij621haxdirrr"; + release."0.2".sha256 = "0xby1kb26r9gcvk5511wqj05fqm9paynwfxlfqkmwkgnfmzk0x73"; + release."0.1".sha256 = "1zz26cyv99whj7rrpgnhhm9dfqnpmrx5pqizn8ihf8jkq8d4drz7"; + release."0.1-8.7".version = "0.1"; + release."0.1-8.7".rev = "v0.1-8.7"; + release."0.1-8.7".sha256 = "0l6wiwi4cvd0i324fb29i9mdh0ijlxzggw4mrjjy695l2qdnlgg0"; 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}/" ]; + mlPlugin = true; 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; + maintainers = [ maintainers.vbgl ]; + license = licenses.lgpl21; }; } diff --git a/pkgs/development/coq-modules/math-classes/default.nix b/pkgs/development/coq-modules/math-classes/default.nix index 73e420b326d9..c6b0dab0e0a7 100644 --- a/pkgs/development/coq-modules/math-classes/default.nix +++ b/pkgs/development/coq-modules/math-classes/default.nix @@ -1,30 +1,17 @@ -{ stdenv, fetchFromGitHub, coq, bignums }: +{ lib, mkCoqDerivation, coq, bignums, version ? null }: -stdenv.mkDerivation rec { +with lib; mkCoqDerivation { - name = "coq${coq.coq-version}-math-classes-${version}"; - version = "8.11.0"; + pname = "math-classes"; + inherit version; + defaultVersion = if versions.range "8.6" "8.11" coq.coq-version then "8.11.0" else null; + release."8.11.0".sha256 = "1hjgncvm1m46lw6264w4dqsy8dbh74vhmzq52x0fba2yqlvy94sf"; - src = fetchFromGitHub { - owner = "coq-community"; - repo = "math-classes"; - rev = version; - sha256 = "1hjgncvm1m46lw6264w4dqsy8dbh74vhmzq52x0fba2yqlvy94sf"; - }; + extraBuildInputs = [ bignums ]; - buildInputs = [ coq bignums ]; - enableParallelBuilding = true; - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - meta = with stdenv.lib; { + meta = { 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/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix new file mode 100644 index 000000000000..9304335260a9 --- /dev/null +++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix @@ -0,0 +1,27 @@ +{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough, mathcomp-real-closed, + lib, version ? null }: + +with lib; mkCoqDerivation { + + namePrefix = [ "coq" "mathcomp" ]; + pname = "analysis"; + owner = "math-comp"; + + release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8"; + release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966"; + + inherit version; + defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ + { cases = [ (range "8.10" "8.11") "1.11.0" ]; out = "0.3.1"; } + { cases = [ (range "8.8" "8.11") (range "1.8" "1.10") ]; out = "0.2.3"; } + ] null; + + propagatedBuildInputs = + [ mathcomp.ssreflect mathcomp.field + mathcomp-finmap mathcomp-bigenough mathcomp-real-closed ]; + + meta = { + description = "Analysis library compatible with Mathematical Components"; + license = licenses.cecill-c; + }; +} diff --git a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix new file mode 100644 index 000000000000..296bd738928f --- /dev/null +++ b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix @@ -0,0 +1,19 @@ +{ coq, mkCoqDerivation, mathcomp, lib, version ? null }: + +with lib; mkCoqDerivation { + + namePrefix = [ "coq" "mathcomp" ]; + pname = "bigenough"; + owner = "math-comp"; + + release = { "1.0.0".sha256 = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg"; }; + inherit version; + defaultVersion = "1.0.0"; + + propagatedBuildInputs = [ mathcomp.ssreflect ]; + + meta = { + description = "A small library to do epsilon - N reasonning"; + license = licenses.cecill-b; + }; +} diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix new file mode 100644 index 000000000000..c506d07e4574 --- /dev/null +++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix @@ -0,0 +1,36 @@ +{ coq, mkCoqDerivation, mathcomp, lib, version ? null }: + +with lib; mkCoqDerivation { + + namePrefix = [ "coq" "mathcomp" ]; + pname = "finmap"; + owner = "math-comp"; + inherit version; + defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ + { cases = [ (isGe "8.10") (range "1.11" "1.12") ]; out = "1.5.1"; } + { cases = [ (range "8.7" "8.11") "1.11.0" ]; out = "1.5.0"; } + { cases = [ (isEq "8.11") (range "1.8" "1.10") ]; out = "1.4.0+coq-8.11"; } + { cases = [ (range "8.7" "8.11.0") (range "1.8" "1.10") ]; out = "1.4.0"; } + { cases = [ (range "8.7" "8.11.0") (range "1.8" "1.10") ]; out = "1.3.4"; } + { cases = [ (range "8.7" "8.9") "1.7.0" ]; out = "1.1.0"; } + { cases = [ (range "8.6" "8.7") (range "1.6.1" "1.7") ]; out = "1.0.0"; } + ] null; + release = { + "1.5.1".sha256 = "0ryfml4pf1dfya16d8ma80favasmrygvspvb923n06kfw9v986j7"; + "1.5.0".sha256 = "0vx9n1fi23592b3hv5p5ycy7mxc8qh1y5q05aksfwbzkk5zjkwnq"; + "1.4.1".sha256 = "0kx4nx24dml1igk0w0qijmw221r5bgxhwhl5qicnxp7ab3c35s8p"; + "1.4.0+coq-8.11".sha256 = "1fd00ihyx0kzq5fblh9vr8s5mr1kg7p6pk11c4gr8svl1n69ppmb"; + "1.4.0".sha256 = "0mp82mcmrs424ff1vj3cvd8353r9vcap027h3p0iprr1vkkwjbzd"; + "1.3.4".sha256 = "0f5a62ljhixy5d7gsnwd66gf054l26k3m79fb8nz40i2mgp6l9ii"; + "1.2.1".sha256 = "0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf"; + "1.1.0".sha256 = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a"; + "1.0.0".sha256 = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa"; + }; + + propagatedBuildInputs = [ mathcomp.ssreflect ]; + + meta = { + description = "A finset and finmap library"; + license = licenses.cecill-b; + }; +} diff --git a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix new file mode 100644 index 000000000000..dbd1550c6a7a --- /dev/null +++ b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix @@ -0,0 +1,33 @@ +{ coq, mkCoqDerivation, mathcomp, mathcomp-bigenough, + lib, version ? null }: + +with lib; mkCoqDerivation { + + namePrefix = [ "coq" "mathcomp" ]; + pname = "real-closed"; + owner = "math-comp"; + inherit version; + release = { + "1.1.2".sha256 = "0907x4nf7nnvn764q3x9lx41g74rilvq5cki5ziwgpsdgb98pppn"; + "1.1.1".sha256 = "0ksjscrgq1i79vys4zrmgvzy2y4ylxa8wdsf4kih63apw6v5ws6b"; + "1.0.5".sha256 = "0q8nkxr9fba4naylr5xk7hfxsqzq2pvwlg1j0xxlhlgr3fmlavg2"; + "1.0.4".sha256 = "058v9dj973h9kfhqmvcy9a6xhhxzljr90cf99hdfcdx68fi2ha1b"; + "1.0.3".sha256 = "1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb"; + "1.0.1".sha256 = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg"; + }; + + defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ + { cases = [ (isGe "8.10") "1.12.0" ]; out = "1.1.2"; } + { cases = [ (isGe "8.7") "1.11.0" ]; out = "1.1.1"; } + { cases = [ (isGe "8.7") (range "1.9.0" "1.10.0") ]; out = "1.0.4"; } + { cases = [ (isGe "8.7") "1.8.0" ]; out = "1.0.3"; } + { cases = [ (isGe "8.7") "1.7.0" ]; out = "1.0.1"; } + ] null; + + propagatedBuildInputs = [ mathcomp.ssreflect mathcomp.field mathcomp-bigenough ]; + + meta = { + description = "Mathematical Components Library on real closed fields"; + license = licenses.cecill-c; + }; +} diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix index 542fac861c58..5b3501516e15 100644 --- a/pkgs/development/coq-modules/mathcomp/default.nix +++ b/pkgs/development/coq-modules/mathcomp/default.nix @@ -1,265 +1,93 @@ -############################# -# 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. # -######################################################################## +############################################################################ +# 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 passthrough attributes of mathcomp # +# bearing the same names (mathcomp.ssreflect, etc). # +############################################################################ +# Compiling a custom version of mathcomp using `mathcomp.override`. # +# This is the replacement for the former `mathcomp_ config` function. # +# See the documentation at doc/languages-frameworks/coq.section.md. # +############################################################################ -############################################################ -# 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; +{ lib, ncurses, which, graphviz, lua, + mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false, + coqPackages, coq, ocamlPackages, version ? null }@args: +with builtins // lib; let - mathcomp-config-initial = rec { - ####################################################################### - # CONFIGURATION (please edit this), it is exported as mathcomp-config # - ####################################################################### - # sha256 of released mathcomp versions - sha256 = { - "1.12.0" = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp"; - "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.12.0" = flip elem [ "8.13" ]; - "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.12.0" "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; + repo = "math-comp"; + owner = "math-comp"; + withDoc = single && (args.withDoc or false); + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.13"; out = "1.12.0"; } # lower version of coq to 8.10 when all mathcomp packages are ported + { case = range "8.7" "8.12"; out = "1.11.0"; } + { case = range "8.7" "8.11"; out = "1.10.0"; } + { case = range "8.7" "8.11"; out = "1.9.0"; } + { case = range "8.7" "8.9"; out = "1.8.0"; } + { case = range "8.6" "8.9"; out = "1.7.0"; } + { case = range "8.5" "8.7"; out = "1.6.4"; } + ] null; + release = { + "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp"; + "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c"; + "1.10.0".sha256 = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv"; + "1.9.0".sha256 = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r"; + "1.8.0".sha256 = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp"; + "1.7.0".sha256 = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1"; + "1.6.4".sha256 = "09ww48qbjsvpjmy1g9yhm0rrkq800ffq21p6fjkbwd34qvd82raz"; + "1.6.1".sha256 = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i"; }; + releaseRev = v: "mathcomp-${v}"; - ############################################################## - # COMPUTED using the configuration above (edit with caution) # - ############################################################## + # list of core mathcomp packages sorted by dependency order + packages = [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ]; - # 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 + mathcomp_ = package: let + mathcomp-deps = if package == "single" then [] + else map mathcomp_ (head (splitList (pred.equal package) packages)); pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}"; - pkgname = if package == "single" then "mathcomp" else "mathcomp-${package}"; + pname = 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}"; + derivation = mkCoqDerivation ({ + inherit version pname defaultVersion release releaseRev repo owner; - nativeBuildInputs = optionals withDoc [ graphviz ]; - buildInputs = [ ncurses which ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]); - propagatedBuildInputs = [ coq ]; - enableParallelBuilding = true; + nativeBuildInputs = optional withDoc graphviz; + mlPlugin = versions.isLe "8.6" coq.coq-version; + extraBuildInputs = [ ncurses which ] ++ optional withDoc lua; + propagatedBuildInputs = mathcomp-deps; 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}/ - ''; + installTargets = "install" + optionalString withDoc " doc"; - meta = with stdenv.lib; { + meta = { homepage = "https://math-comp.github.io/"; license = licenses.cecill-b; - maintainers = [ maintainers.vbgl maintainers.jwiegley maintainers.cohencyril ]; - platforms = coq.meta.platforms; + maintainers = with maintainers; [ vbgl jwiegley cohencyril ]; }; - - 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); + } // optionalAttrs (package != "single") { passthru = genAttrs packages mathcomp_; }); + patched-derivation1 = derivation.overrideAttrs (o: + optionalAttrs (o.pname != null && o.pname == "mathcomp-all" && + o.version != null && o.version != "dev" && versions.isLt "1.7" o.version) + { preBuild = ""; buildPhase = ""; installPhase = "echo doing nothing"; } + ); + patched-derivation = patched-derivation1.overrideAttrs (o: + optionalAttrs (versions.isLe "8.7" coq.coq-version || + (o.version != "dev" && versions.isLe "1.7" o.version)) + { + installFlags = o.installFlags ++ [ "-f Makefile.coq" ]; + } + ); + in patched-derivation; 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; -} +mathcomp_ (if single then "single" else "all") diff --git a/pkgs/development/coq-modules/mathcomp/extra.nix b/pkgs/development/coq-modules/mathcomp/extra.nix deleted file mode 100644 index 6a2dfcda3456..000000000000 --- a/pkgs/development/coq-modules/mathcomp/extra.nix +++ /dev/null @@ -1,391 +0,0 @@ -########################################################## -# 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/pkgs/development/coq-modules/metalib/default.nix b/pkgs/development/coq-modules/metalib/default.nix index 862184c1460c..3ce3c625d268 100644 --- a/pkgs/development/coq-modules/metalib/default.nix +++ b/pkgs/development/coq-modules/metalib/default.nix @@ -1,33 +1,18 @@ -{ stdenv, fetchFromGitHub, coq }: +{ lib, mkCoqDerivation, coq, version ? null }: -stdenv.mkDerivation rec { - name = "coq${coq.coq-version}-metalib-${version}"; - version = "20200527"; - - src = fetchFromGitHub { - owner = "plclub"; - repo = "metalib"; - rev = "597fd7d0c93eb159274e84a39d554f10f1efccf8"; - sha256 = "0wbypc05d2lqfm9qaw98ynr5yc1p0ipsvyc3bh1rk9nz7zwirmjs"; - }; +with lib; mkCoqDerivation { + pname = "metalib"; + owner = "plclub"; + inherit version; + defaultVersion = if versions.range "8.10" "8.12" coq.coq-version then "20200527" else null; + release."20200527".rev = "597fd7d0c93eb159274e84a39d554f10f1efccf8"; + release."20200527".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"; + meta = { 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/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix new file mode 100644 index 000000000000..4958ad893e92 --- /dev/null +++ b/pkgs/development/coq-modules/multinomials/default.nix @@ -0,0 +1,34 @@ +{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough, + lib, version ? null }: +with lib; mkCoqDerivation { + + namePrefix = [ "coq" "mathcomp" ]; + pname = "multinomials"; + owner = "math-comp"; + inherit version; + defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ + { cases = [ (range "8.7" "8.12") "1.11.0" ]; out = "1.5.2"; } + { cases = [ (range "8.7" "8.11") (range "1.8" "1.10") ]; out = "1.5.0"; } + { cases = [ (range "8.7" "8.10") (range "1.8" "1.10") ]; out = "1.4"; } + { cases = [ "8.6" (range "1.6" "1.7") ]; out = "1.1"; } + ] null; + release = { + "1.5.2".sha256 = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s"; + "1.5.1".sha256 = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3"; + "1.5.0".sha256 = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw"; + "1.5.0".rev = "1.5"; + "1.4".sha256 = "0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p"; + "1.3".sha256 = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4"; + "1.2".sha256 = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq"; + "1.1".sha256 = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s"; + "1.0".sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m"; + }; + + propagatedBuildInputs = + [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap mathcomp-bigenough ]; + + meta = { + description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials"; + license = licenses.cecill-c; + }; +} diff --git a/pkgs/development/coq-modules/paco/default.nix b/pkgs/development/coq-modules/paco/default.nix index ac6eef2f3bd0..900e52f1682b 100644 --- a/pkgs/development/coq-modules/paco/default.nix +++ b/pkgs/development/coq-modules/paco/default.nix @@ -1,42 +1,16 @@ -{stdenv, fetchFromGitHub, coq, unzip}: +{ lib, mkCoqDerivation, coq, version ? null }: -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 ]; +with lib; mkCoqDerivation { + pname = "paco"; + owner = "snu-sf"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.6"; out = "4.0.2"; } + { case = range "8.5" "8.8"; out = "1.2.8"; } + ] null; + release."4.0.2".sha256 = "1q96bsxclqx84xn5vkid501jkwlc1p6fhb8szrlrp82zglj58b0b"; + release."1.2.8".sha256 = "05fskx5x1qgaf9qv626m38y5izichzzqc7g2rglzrkygbskrrwsb"; + releaseRev = v: "v${v}"; preBuild = "cd src"; @@ -46,15 +20,9 @@ stdenv.mkDerivation rec { cp -pR *.vo $COQLIB/user-contrib/Paco ''; - meta = with stdenv.lib; { + meta = { 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/pkgs/development/coq-modules/paramcoq/default.nix b/pkgs/development/coq-modules/paramcoq/default.nix index 12d65bdb3d7b..342e4225a3c2 100644 --- a/pkgs/development/coq-modules/paramcoq/default.nix +++ b/pkgs/development/coq-modules/paramcoq/default.nix @@ -1,58 +1,22 @@ -{ 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; - }; +{ lib, mkCoqDerivation, coq, version ? null }: +with lib; mkCoqDerivation { + pname = "paramcoq"; + inherit version; + defaultVersion = if versions.range "8.7" "8.12" coq.coq-version + then "1.1.2+coq${coq.coq-version}" else null; + displayVersion = { paramcoq = "1.1.2"; }; + release."1.1.2+coq8.12".sha256 = "0qd72r45if4h7c256qdfiimv75zyrs0w0xqij3m866jxaq591v4i"; + release."1.1.2+coq8.11".sha256 = "09c6813988nvq4fpa45s33k70plnhxsblhm7cxxkg0i37mhvigsa"; + release."1.1.2+coq8.10".sha256 = "1lq1mw15w4yky79qg3rm0mpzqi2ir51b6ak04ismrdr7ixky49y8"; + release."1.1.2+coq8.9".sha256 = "1jjzgpff09xjn9kgp7w69r096jkj0x2ksng3pawrmhmn7clwivbk"; + release."1.1.2+coq8.8".sha256 = "0rc4lshqvnfdsph98gnscvpmlirs9wx91qcvffggg73xw0p1g9s0"; + release."1.1.2+coq8.7".sha256 = "09n0ky7ldb24by7yf5j3hv410h85x50ksilf7qacl7xglj4gy5hj"; + releaseRev = v: "v${v}"; + mlPlugin = true; meta = { description = "Coq plugin for parametricity"; - inherit (src.meta) homepage; - license = stdenv.lib.licenses.mit; - maintainers = [ stdenv.lib.maintainers.vbgl ]; - inherit (coq.meta) platforms; + license = licenses.mit; + maintainers = [ maintainers.vbgl ]; }; } diff --git a/pkgs/development/coq-modules/simple-io/default.nix b/pkgs/development/coq-modules/simple-io/default.nix index 82fa215ee9ca..42d4f782f1cf 100644 --- a/pkgs/development/coq-modules/simple-io/default.nix +++ b/pkgs/development/coq-modules/simple-io/default.nix @@ -1,34 +1,21 @@ -{ 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 ]); +{ lib, mkCoqDerivation, coq, coq-ext-lib, version ? null }: +with lib; mkCoqDerivation { + pname = "simple-io"; + owner = "Lysxia"; + repo = "coq-simple-io"; + inherit version; + defaultVersion = if versions.range "8.7" "8.12" coq.coq-version then "1.3.0" else null; + release."1.3.0".sha256 = "1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax"; + extraBuildInputs = (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 ]; + license = licenses.mit; + maintainers = [ maintainers.vbgl ]; }; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; - }; - } diff --git a/pkgs/development/coq-modules/stdpp/default.nix b/pkgs/development/coq-modules/stdpp/default.nix index 28917e73f29f..2caafa9cc555 100644 --- a/pkgs/development/coq-modules/stdpp/default.nix +++ b/pkgs/development/coq-modules/stdpp/default.nix @@ -1,32 +1,17 @@ -{ stdenv, fetchFromGitLab, coq }: +{ lib, mkCoqDerivation, coq, version ? null }: -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}/" ]; +with lib; mkCoqDerivation rec { + pname = "stdpp"; + inherit version; + domain = "gitlab.mpi-sws.org"; + owner = "iris"; + defaultVersion = if versions.range "8.8" "8.12" coq.coq-version then "1.4.0" else null; + release."1.4.0".sha256 = "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r"; + releaseRev = v: "coq-stdpp-${v}"; 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 ]; + license = licenses.bsd3; + maintainers = [ maintainers.vbgl ]; }; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.8" "8.9" "8.10" "8.11" "8.12" ]; - }; - } diff --git a/pkgs/development/coq-modules/tlc/default.nix b/pkgs/development/coq-modules/tlc/default.nix index 816b22050244..6bbad1c6c2b1 100644 --- a/pkgs/development/coq-modules/tlc/default.nix +++ b/pkgs/development/coq-modules/tlc/default.nix @@ -1,41 +1,23 @@ -{ stdenv, fetchurl, fetchFromGitHub, coq }: +{ lib, mkCoqDerivation, coq, version ? null }: -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 ]; +with lib; mkCoqDerivation { + pname = "tlc"; + owner = "charguer"; + inherit version; + displayVersion = { tlc = false; }; + defaultVersion = with versions; switch coq.coq-version [ + { case = range "8.10" "8.12"; out = "20200328"; } + { case = range "8.6" "8.12"; out = "20181116"; } + ] null; + release."20200328".sha256 = "16vzild9gni8zhgb3qhmka47f8zagdh03k6nssif7drpim8233lx"; + release."20181116".sha256 = "032lrbkxqm9d3fhf6nv1kq2z0mqd3czv3ijlbsjwnfh12xck4vpl"; 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" ]; + license = licenses.free; + maintainers = [ maintainers.vbgl ]; }; } diff --git a/pkgs/development/ocaml-modules/elpi/default.nix b/pkgs/development/ocaml-modules/elpi/default.nix index 865c5448c5bd..6f0d355fed5b 100644 --- a/pkgs/development/ocaml-modules/elpi/default.nix +++ b/pkgs/development/ocaml-modules/elpi/default.nix @@ -1,15 +1,19 @@ -{ lib, fetchzip, buildDunePackage, camlp5 +{ stdenv, lib, fetchzip, buildDunePackage, camlp5 , ppxlib, ppx_deriving, re, perl, ncurses +, version ? "1.12.0" }: - +with lib; +let fetched = import ../../../build-support/coq/meta-fetch/default.nix + {inherit stdenv fetchzip; } ({ + release."1.12.0".sha256 = "1agisdnaq9wrw3r73xz14yrq3wx742i6j8i5icjagqk0ypmly2is"; + release."1.11.4".sha256 = "1m0jk9swcs3jcrw5yyw5343v8mgax238cjb03s8gc4wipw1fn9f5"; + releaseRev = v: "v${v}"; + location = { domain = "github.com"; owner = "LPCIC"; repo = "elpi"; }; + }) version; +in buildDunePackage rec { pname = "elpi"; - version = "1.11.4"; - - src = fetchzip { - url = "https://github.com/LPCIC/elpi/releases/download/v${version}/elpi-v${version}.tbz"; - sha256 = "1hmjp2z52j17vwhhdkj45n9jx11jxkdg2dwa0n04yyw0qqy4m7c1"; - }; + inherit (fetched) version src; minimumOCamlVersion = "4.04"; @@ -19,8 +23,8 @@ buildDunePackage rec { meta = { description = "Embeddable λProlog Interpreter"; - license = lib.licenses.lgpl21Plus; - maintainers = [ lib.maintainers.vbgl ]; + license = licenses.lgpl21Plus; + maintainers = [ maintainers.vbgl ]; homepage = "https://github.com/LPCIC/elpi"; }; diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index d56aabd564e0..19d5b9260f6c 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -27426,7 +27426,7 @@ in cadical = callPackage ../applications/science/logic/cadical {}; inherit (callPackage ./coq-packages.nix { - inherit (ocaml-ng) ocamlPackages_4_05 ocamlPackages_4_09; + inherit (ocaml-ng) ocamlPackages_4_05 ocamlPackages_4_09 ocamlPackages_4_10; }) mkCoqPackages coqPackages_8_5 coq_8_5 coqPackages_8_6 coq_8_6 diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index aa7b3c35b82e..c67d489de628 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -1,13 +1,15 @@ { lib, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09 -, compcert -}: - +, ocamlPackages_4_10, compcert +}@args: +let lib = import ../build-support/coq/extra-lib.nix {inherit (args) lib;}; in let mkCoqPackages' = self: coq: let callPackage = self.callPackage; in { - inherit coq; + inherit coq lib; coqPackages = self; + mkCoqDerivation = callPackage ../build-support/coq {}; + contribs = recurseIntoAttrs (callPackage ../development/coq-modules/contribs {}); @@ -22,6 +24,7 @@ let coq-elpi = callPackage ../development/coq-modules/coq-elpi {}; coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {}; coq-haskell = callPackage ../development/coq-modules/coq-haskell { }; + coqeal = callPackage ../development/coq-modules/coqeal {}; coqhammer = callPackage ../development/coq-modules/coqhammer {}; coqprime = callPackage ../development/coq-modules/coqprime {}; coquelicot = callPackage ../development/coq-modules/coquelicot {}; @@ -39,19 +42,20 @@ let iris = callPackage ../development/coq-modules/iris {}; ltac2 = callPackage ../development/coq-modules/ltac2 {}; math-classes = callPackage ../development/coq-modules/math-classes { }; - inherit (callPackage ../development/coq-modules/mathcomp {}) - mathcomp_ mathcomp-config - mathcomp ssreflect - mathcomp-ssreflect mathcomp-fingroup mathcomp-algebra - mathcomp-solvable mathcomp-field mathcomp-character - ; - inherit (callPackage ../development/coq-modules/mathcomp/extra.nix { }) - mathcomp-extra-override mathcomp-extra-config mathcomp-extra - current-mathcomp-extra mathcomp-extra-fast mathcomp-extra-all - mathcomp-finmap mathcomp-bigenough mathcomp-real-closed - mathcomp-analysis multinomials coqeal - ; + mathcomp = callPackage ../development/coq-modules/mathcomp {}; + ssreflect = self.mathcomp.ssreflect; + mathcomp-ssreflect = self.mathcomp.ssreflect; + mathcomp-fingroup = self.mathcomp.fingroup; + mathcomp-algebra = self.mathcomp.algebra; + mathcomp-solvable = self.mathcomp.solvable; + mathcomp-field = self.mathcomp.field; + mathcomp-character = self.mathcomp.character; + mathcomp-analysis = callPackage ../development/coq-modules/mathcomp-analysis {}; + mathcomp-finmap = callPackage ../development/coq-modules/mathcomp-finmap {}; + mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough {}; + mathcomp-real-closed = callPackage ../development/coq-modules/mathcomp-real-closed {}; metalib = callPackage ../development/coq-modules/metalib { }; + multinomials = callPackage ../development/coq-modules/multinomials {}; paco = callPackage ../development/coq-modules/paco {}; paramcoq = callPackage ../development/coq-modules/paramcoq {}; QuickChick = callPackage ../development/coq-modules/QuickChick {}; @@ -64,23 +68,22 @@ let VST = callPackage ../development/coq-modules/VST { compcert = compcert.override { version = "3.7"; }; }; - - filterPackages = filterCoqPackages; + filterPackages = doesFilter: if doesFilter then filterCoqPackages self else self; }; - filterCoqPackages = coq: set: + filterCoqPackages = set: lib.listToAttrs ( - lib.concatMap (name: - let v = set.${name}; in - let p = v.compatibleCoqVersions or (_: true); in - lib.optional (p coq.coq-version) - (lib.nameValuePair name ( - if lib.isAttrs v && v.recurseForDerivations or false - then filterCoqPackages coq v - else v)) + lib.concatMap (name: let v = set.${name} or null; in + lib.optional (! v.meta.coqFilter or false) + (lib.nameValuePair name ( + if lib.isAttrs v && v.recurseForDerivations or false + then filterCoqPackages v + else v)) ) (lib.attrNames set) ); - + mkCoq = version: callPackage ../applications/science/logic/coq { + inherit version ocamlPackages_4_05 ocamlPackages_4_09 ocamlPackages_4_10; + }; in rec { /* The function `mkCoqPackages` takes as input a derivation for Coq and produces @@ -93,41 +96,17 @@ in rec { */ mkCoqPackages = coq: let self = lib.makeScope newScope (lib.flip mkCoqPackages' coq); in - if coq.dontFilter or false then self else filterCoqPackages coq self; + self.filterPackages (! coq.dontFilter or false); - coq_8_5 = callPackage ../applications/science/logic/coq { - ocamlPackages = ocamlPackages_4_05; - version = "8.5pl3"; - }; - coq_8_6 = callPackage ../applications/science/logic/coq { - ocamlPackages = ocamlPackages_4_05; - version = "8.6.1"; - }; - coq_8_7 = callPackage ../applications/science/logic/coq { - ocamlPackages = ocamlPackages_4_09; - version = "8.7.2"; - }; - coq_8_8 = callPackage ../applications/science/logic/coq { - ocamlPackages = ocamlPackages_4_09; - version = "8.8.2"; - }; - coq_8_9 = callPackage ../applications/science/logic/coq { - ocamlPackages = ocamlPackages_4_09; - version = "8.9.1"; - }; - coq_8_10 = callPackage ../applications/science/logic/coq { - ocamlPackages = ocamlPackages_4_09; - version = "8.10.2"; - }; - coq_8_11 = callPackage ../applications/science/logic/coq { - version = "8.11.2"; - }; - coq_8_12 = callPackage ../applications/science/logic/coq { - version = "8.12.2"; - }; - coq_8_13 = callPackage ../applications/science/logic/coq { - version = "8.13+beta1"; - }; + coq_8_5 = mkCoq "8.5"; + coq_8_6 = mkCoq "8.6"; + coq_8_7 = mkCoq "8.7"; + coq_8_8 = mkCoq "8.8"; + coq_8_9 = mkCoq "8.9"; + coq_8_10 = mkCoq "8.10"; + coq_8_11 = mkCoq "8.11"; + coq_8_12 = mkCoq "8.12"; + coq_8_13 = mkCoq "8.13"; coqPackages_8_5 = mkCoqPackages coq_8_5; coqPackages_8_6 = mkCoqPackages coq_8_6;