From 225d915e5c4766281fa3d11a7dfe603c0adc963b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bj=C3=B8rn=20Forsman?= Date: Sat, 1 May 2021 15:15:01 +0200 Subject: [PATCH 01/21] nixos/atd: prefer 'install' over 'mkdir/chmod/chown' I don't think there was a security issue here, but using 'install' is preferred. Ref #121293. --- nixos/modules/services/scheduling/atd.nix | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/nixos/modules/services/scheduling/atd.nix b/nixos/modules/services/scheduling/atd.nix index cefe72b0e999..37f6651ec4cf 100644 --- a/nixos/modules/services/scheduling/atd.nix +++ b/nixos/modules/services/scheduling/atd.nix @@ -81,14 +81,9 @@ in jobdir=/var/spool/atjobs etcdir=/etc/at - for dir in "$spooldir" "$jobdir" "$etcdir"; do - if [ ! -d "$dir" ]; then - mkdir -p "$dir" - chown atd:atd "$dir" - fi - done - chmod 1770 "$spooldir" "$jobdir" - ${if cfg.allowEveryone then ''chmod a+rwxt "$spooldir" "$jobdir" '' else ""} + install -dm755 -o atd -g atd "$etcdir" + spool_and_job_dir_perms=${if cfg.allowEveryone then "1777" else "1770"} + install -dm"$spool_and_job_dir_perms" -o atd -g atd "$spooldir" "$jobdir" if [ ! -f "$etcdir"/at.deny ]; then touch "$etcdir"/at.deny chown root:atd "$etcdir"/at.deny From b58f6f6b515e0bd8a739df7ee49541db52ea0b6e Mon Sep 17 00:00:00 2001 From: ajs124 Date: Sun, 9 May 2021 15:19:15 +0200 Subject: [PATCH 02/21] mariadb-galera: remove unused code --- pkgs/servers/sql/mariadb/galera/default.nix | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/pkgs/servers/sql/mariadb/galera/default.nix b/pkgs/servers/sql/mariadb/galera/default.nix index 165b92162407..cbee434d89b9 100644 --- a/pkgs/servers/sql/mariadb/galera/default.nix +++ b/pkgs/servers/sql/mariadb/galera/default.nix @@ -2,13 +2,7 @@ , asio, boost, check, openssl, cmake }: -let - galeraLibs = buildEnv { - name = "galera-lib-inputs-united"; - paths = [ openssl.out boost check ]; - }; - -in stdenv.mkDerivation rec { +stdenv.mkDerivation rec { pname = "mariadb-galera"; version = "26.4.8"; From 59eba3aa9c97a55ecf60c86cfa263d9cb38ddbda Mon Sep 17 00:00:00 2001 From: ajs124 Date: Sun, 9 May 2021 15:41:55 +0200 Subject: [PATCH 03/21] mariadb-galera: don't produce symlink loop as sugested by Izorkin --- pkgs/servers/sql/mariadb/galera/default.nix | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pkgs/servers/sql/mariadb/galera/default.nix b/pkgs/servers/sql/mariadb/galera/default.nix index cbee434d89b9..2b387db66cdc 100644 --- a/pkgs/servers/sql/mariadb/galera/default.nix +++ b/pkgs/servers/sql/mariadb/galera/default.nix @@ -23,7 +23,8 @@ stdenv.mkDerivation rec { postInstall = '' # for backwards compatibility - ln -s . $out/lib/galera + mkdir $out/lib/galera + ln -s $out/lib/libgalera_smm.so $out/lib/galera/libgalera_smm.so ''; meta = with lib; { From 0677bf37095e12a8ad84ec03668dde1581fbe0b4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?St=C3=A9phan=20Kochen?= Date: Sun, 9 May 2021 21:31:25 +0200 Subject: [PATCH 04/21] cargo-deb: fix build on darwin --- pkgs/tools/package-management/cargo-deb/default.nix | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pkgs/tools/package-management/cargo-deb/default.nix b/pkgs/tools/package-management/cargo-deb/default.nix index 6a71189314d7..4ed3b21b64b8 100644 --- a/pkgs/tools/package-management/cargo-deb/default.nix +++ b/pkgs/tools/package-management/cargo-deb/default.nix @@ -3,6 +3,7 @@ , fetchFromGitHub , rustPlatform , rust +, libiconv , Security }: @@ -17,7 +18,7 @@ rustPlatform.buildRustPackage rec { sha256 = "sha256-2eOWhxKZ+YPj5oKTe5g7PyeakiSNnPz27dK150GAcVQ="; }; - buildInputs = lib.optionals stdenv.isDarwin [ Security ]; + buildInputs = lib.optionals stdenv.isDarwin [ libiconv Security ]; cargoSha256 = "sha256-QmchuY+4R7w0zMOdReH1m8idl9RI1hHE9VtbwT2K9YM="; From 0cde88f4b13ae8ac7efd7b245a98dab0e8f4ac9d Mon Sep 17 00:00:00 2001 From: Fabian Affolter Date: Sun, 9 May 2021 22:48:29 +0200 Subject: [PATCH 05/21] nuclei: 2.3.6 -> 2.3.7 --- pkgs/tools/security/nuclei/default.nix | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pkgs/tools/security/nuclei/default.nix b/pkgs/tools/security/nuclei/default.nix index 42dc9db651e9..2e32940657bb 100644 --- a/pkgs/tools/security/nuclei/default.nix +++ b/pkgs/tools/security/nuclei/default.nix @@ -5,16 +5,16 @@ buildGoModule rec { pname = "nuclei"; - version = "2.3.6"; + version = "2.3.7"; src = fetchFromGitHub { owner = "projectdiscovery"; repo = pname; rev = "v${version}"; - sha256 = "sha256-9C/r1B+lEveRHRLgD0ay9xhi6100c/SGfUaiP7qwstc="; + sha256 = "sha256-loViPW84KdAOJbL8oUJeiON1f6vrZTcYXRP2VBMNkGk="; }; - vendorSha256 = "sha256-GAJxEBLZmbSmCeuAEYIHQ4xEzbTJYlJU+JCAL5hlVzY="; + vendorSha256 = "sha256-HBpKaRI7gcWp13GVxTlnZvvTyRncfLmu0NmwAUyQ4hQ="; modRoot = "./v2"; subPackages = [ From 76833b12065cb7f48b40b6c4320974b517cb66c2 Mon Sep 17 00:00:00 2001 From: pacien Date: Sun, 9 May 2021 23:51:26 +0200 Subject: [PATCH 06/21] beamerpresenter: 0.1.3 -> 0.2.0 --- .../office/beamerpresenter/default.nix | 39 +++++++++++-------- 1 file changed, 22 insertions(+), 17 deletions(-) diff --git a/pkgs/applications/office/beamerpresenter/default.nix b/pkgs/applications/office/beamerpresenter/default.nix index 4e8bcaee019e..e9543a095933 100644 --- a/pkgs/applications/office/beamerpresenter/default.nix +++ b/pkgs/applications/office/beamerpresenter/default.nix @@ -1,39 +1,44 @@ { lib, mkDerivation, fetchFromGitHub, installShellFiles, - qmake, qtbase, poppler, qtmultimedia }: + qmake, qtbase, qtmultimedia, + poppler, mupdf, jbig2dec, openjpeg, gumbo, + renderer ? "mupdf" }: -mkDerivation rec { +let + renderers = { + mupdf.buildInputs = [ mupdf jbig2dec openjpeg gumbo ]; + poppler.buildInputs = [ poppler ]; + }; + +in mkDerivation rec { pname = "beamerpresenter"; - version = "0.1.3"; + version = "0.2.0"; src = fetchFromGitHub { owner = "stiglers-eponym"; repo = "BeamerPresenter"; rev = "v${version}"; - sha256 = "1nbcqrfdjcsc6czqk1v163whka4x1w883b1298aws8yi7vac4f1i"; + sha256 = "10i5nc5b5syaqvsixam4lmfiz3b5cphbjfgfqavi5jilq769792a"; }; nativeBuildInputs = [ qmake installShellFiles ]; - buildInputs = [ qtbase qtmultimedia poppler ]; + buildInputs = [ qtbase qtmultimedia ] ++ renderers.${renderer}.buildInputs; + + qmakeFlags = [ "RENDERER=${renderer}" ]; postPatch = '' - # Fix location of poppler-*.h shopt -s globstar - for f in **/*.{h,cpp}; do - substituteInPlace $f --replace '#include Date: Mon, 10 May 2021 08:27:30 +0200 Subject: [PATCH 07/21] beamerpresenter: fix darwin build --- .../office/beamerpresenter/default.nix | 18 ++++++++++++------ pkgs/top-level/all-packages.nix | 9 ++++++++- 2 files changed, 20 insertions(+), 7 deletions(-) diff --git a/pkgs/applications/office/beamerpresenter/default.nix b/pkgs/applications/office/beamerpresenter/default.nix index e9543a095933..351609d8c058 100644 --- a/pkgs/applications/office/beamerpresenter/default.nix +++ b/pkgs/applications/office/beamerpresenter/default.nix @@ -1,15 +1,17 @@ -{ lib, mkDerivation, fetchFromGitHub, installShellFiles, - qmake, qtbase, qtmultimedia, - poppler, mupdf, jbig2dec, openjpeg, gumbo, +{ lib, stdenv, fetchFromGitHub, installShellFiles, + qmake, qtbase, qtmultimedia, wrapQtAppsHook, + poppler, mupdf, freetype, jbig2dec, openjpeg, gumbo, renderer ? "mupdf" }: let renderers = { - mupdf.buildInputs = [ mupdf jbig2dec openjpeg gumbo ]; + mupdf.buildInputs = [ mupdf freetype jbig2dec openjpeg gumbo ]; poppler.buildInputs = [ poppler ]; }; -in mkDerivation rec { +in + +stdenv.mkDerivation rec { pname = "beamerpresenter"; version = "0.2.0"; @@ -20,7 +22,7 @@ in mkDerivation rec { sha256 = "10i5nc5b5syaqvsixam4lmfiz3b5cphbjfgfqavi5jilq769792a"; }; - nativeBuildInputs = [ qmake installShellFiles ]; + nativeBuildInputs = [ qmake installShellFiles wrapQtAppsHook ]; buildInputs = [ qtbase qtmultimedia ] ++ renderers.${renderer}.buildInputs; qmakeFlags = [ "RENDERER=${renderer}" ]; @@ -35,6 +37,10 @@ in mkDerivation rec { done ''; + postInstall = lib.optionalString stdenv.isDarwin '' + wrapQtApp "$out"/bin/beamerpresenter.app/Contents/MacOS/beamerpresenter + ''; + meta = with lib; { description = "Modular multi screen pdf presentation software respecting your window manager"; homepage = "https://github.com/stiglers-eponym/BeamerPresenter"; diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 0334a03c75f6..74152f3fd51d 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -3214,7 +3214,14 @@ in bdsync = callPackage ../tools/backup/bdsync { }; - beamerpresenter = libsForQt5.callPackage ../applications/office/beamerpresenter { }; + beamerpresenter = libsForQt5.callPackage ../applications/office/beamerpresenter { + # developed for a compiler with C++20 support + stdenv = + if stdenv.isDarwin then + overrideCC stdenv clang_10 + else + stdenv; + }; beanstalkd = callPackage ../servers/beanstalkd { }; From 99a7c0ac777f6df12bd7c0d84d9ad561f7796534 Mon Sep 17 00:00:00 2001 From: Dave Gallant Date: Sun, 9 May 2021 21:58:26 -0400 Subject: [PATCH 08/21] awscrt: init at 0.11.13 --- .../python-modules/awscrt/default.nix | 33 +++++++++++++++++++ pkgs/top-level/python-packages.nix | 2 ++ 2 files changed, 35 insertions(+) create mode 100644 pkgs/development/python-modules/awscrt/default.nix diff --git a/pkgs/development/python-modules/awscrt/default.nix b/pkgs/development/python-modules/awscrt/default.nix new file mode 100644 index 000000000000..2c0180eb4a29 --- /dev/null +++ b/pkgs/development/python-modules/awscrt/default.nix @@ -0,0 +1,33 @@ +{ lib, buildPythonPackage, fetchPypi, cmake, perl, stdenv, gcc10, darwin }: + +buildPythonPackage rec { + pname = "awscrt"; + version = "0.11.13"; + + buildInputs = lib.optionals stdenv.isDarwin + (with darwin.apple_sdk.frameworks; [ Security ]); + + # Required to suppress -Werror + # https://github.com/NixOS/nixpkgs/issues/39687 + hardeningDisable = lib.optional stdenv.cc.isClang "strictoverflow"; + + nativeBuildInputs = [ cmake ] ++ lib.optionals stdenv.isAarch64 ([ gcc10 perl ]); + + dontUseCmakeConfigure = true; + + # Unable to import test module + # https://github.com/awslabs/aws-crt-python/issues/281 + doCheck = false; + + src = fetchPypi { + inherit pname version; + sha256 = "sha256-G/bf2AzWp8AHL4of0zfX3jIYyTtmTLBIC2ZKiMi19c0="; + }; + + meta = with lib; { + homepage = "https://github.com/awslabs/aws-crt-python"; + description = "Python bindings for the AWS Common Runtime"; + license = licenses.asl20; + maintainers = with maintainers; [ davegallant ]; + }; +} diff --git a/pkgs/top-level/python-packages.nix b/pkgs/top-level/python-packages.nix index 620b2238ae61..13dbda61552e 100644 --- a/pkgs/top-level/python-packages.nix +++ b/pkgs/top-level/python-packages.nix @@ -665,6 +665,8 @@ in { aws-xray-sdk = callPackage ../development/python-modules/aws-xray-sdk { }; + awscrt = callPackage ../development/python-modules/awscrt { }; + awsiotpythonsdk = callPackage ../development/python-modules/awsiotpythonsdk { }; awslambdaric = callPackage ../development/python-modules/awslambdaric { }; From cee71902e30979aaaf87ed0acb402f2c457ae7a6 Mon Sep 17 00:00:00 2001 From: Dave Gallant Date: Sun, 9 May 2021 22:35:19 -0400 Subject: [PATCH 09/21] awscli2: 2.1.35 -> 2.2.1 --- pkgs/tools/admin/awscli2/default.nix | 30 +++++++++++++++++++++------- 1 file changed, 23 insertions(+), 7 deletions(-) diff --git a/pkgs/tools/admin/awscli2/default.nix b/pkgs/tools/admin/awscli2/default.nix index a2ea7bb35db3..eeb511cd31c1 100644 --- a/pkgs/tools/admin/awscli2/default.nix +++ b/pkgs/tools/admin/awscli2/default.nix @@ -3,12 +3,12 @@ let py = python3.override { packageOverrides = self: super: { botocore = super.botocore.overridePythonAttrs (oldAttrs: rec { - version = "2.0.0dev103"; + version = "2.0.0dev109"; src = fetchFromGitHub { owner = "boto"; repo = "botocore"; - rev = "e30d580042687a79776fdf93264e80746e08d21f"; - sha256 = "sha256-+cTQQO6dPctvf3WZOk8Mgo1eQUdqRdGCcz7jcVhEvNo="; + rev = "b006ff741d12608a9187b873e276abd1fd8eb707"; + sha256 = "sha256-uU3XVQiwtbBt7cdSwAeHkv6NUbL8kK2Ro44h1GYyA1A="; }; }); prompt_toolkit = super.prompt_toolkit.overridePythonAttrs (oldAttrs: rec { @@ -18,19 +18,26 @@ let sha256 = "1nr990i4b04rnlw1ghd0xmgvvvhih698mb6lb6jylr76cs7zcnpi"; }; }); + s3transfer = super.s3transfer.overridePythonAttrs (oldAttrs: rec { + version = "0.4.2"; + src = oldAttrs.src.override { + inherit version; + sha256 = "sha256-ywIvSxZVHt67sxo3fT8JYA262nNj2MXbeXbn9Hcy4bI="; + }; + }); }; }; in with py.pkgs; buildPythonApplication rec { pname = "awscli2"; - version = "2.1.35"; # N.B: if you change this, change botocore to a matching version too + version = "2.2.1"; # N.B: if you change this, change botocore to a matching version too src = fetchFromGitHub { owner = "aws"; repo = "aws-cli"; rev = version; - sha256 = "sha256-YgzagbbVLlGSPIhck0YaJg3gQGEdoqXtLapN04Q6hLw="; + sha256 = "sha256-TafYBkRlPCqewGBMgTfcX8kLtDhSCdiUYK1xXofKrLk="; }; postPatch = '' @@ -41,10 +48,10 @@ with py.pkgs; buildPythonApplication rec { substituteInPlace setup.py --replace "wcwidth<0.2.0" "wcwidth" ''; - # No tests included - doCheck = false; + checkInputs = [ jsonschema mock nose ]; propagatedBuildInputs = [ + awscrt bcdoc botocore colorama @@ -62,6 +69,15 @@ with py.pkgs; buildPythonApplication rec { wcwidth ]; + checkPhase = '' + export PATH=$PATH:$out/bin + + # https://github.com/NixOS/nixpkgs/issues/16144#issuecomment-225422439 + export HOME=$TMP + + AWS_TEST_COMMAND=$out/bin/aws python scripts/ci/run-tests + ''; + postInstall = '' mkdir -p $out/${python3.sitePackages}/awscli/data ${python3.interpreter} scripts/gen-ac-index --index-location $out/${python3.sitePackages}/awscli/data/ac.index From c9e9814cde101c18cf0bf93ff2ebc55d41ecedf8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Robert=20Sch=C3=BCtz?= Date: Mon, 10 May 2021 00:20:56 +0200 Subject: [PATCH 10/21] python3Packages.pytube: 10.7.2 -> 10.8.1 https://github.com/pytube/pytube/releases/tag/v10.8.1 --- pkgs/development/python-modules/pytube/default.nix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pkgs/development/python-modules/pytube/default.nix b/pkgs/development/python-modules/pytube/default.nix index 8bcfa8b6c7d9..dd6ece2163c0 100644 --- a/pkgs/development/python-modules/pytube/default.nix +++ b/pkgs/development/python-modules/pytube/default.nix @@ -7,7 +7,7 @@ buildPythonPackage rec { pname = "pytube"; - version = "10.7.2"; + version = "10.8.1"; disabled = pythonOlder "3.6"; @@ -15,7 +15,7 @@ buildPythonPackage rec { owner = "pytube"; repo = "pytube"; rev = "v${version}"; - sha256 = "sha256-85pHzfQYyqwX8mQ5msIojM/0FSfeaC12KJw4mXmji3g="; + sha256 = "sha256-QPYu6UA0CEf/FSFoN+OfjhbDgkrMOjxaxNpFcDQzAz0="; }; checkInputs = [ From 8c52ec99a2b7f79027fddcd650e6bc4b90ddd8ab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?St=C3=A9phan=20Kochen?= Date: Sun, 9 May 2021 21:55:53 +0200 Subject: [PATCH 11/21] cargo-limit: fix build on darwin --- pkgs/development/tools/rust/cargo-limit/default.nix | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/pkgs/development/tools/rust/cargo-limit/default.nix b/pkgs/development/tools/rust/cargo-limit/default.nix index 7d63b7adcea7..76f766685ab4 100644 --- a/pkgs/development/tools/rust/cargo-limit/default.nix +++ b/pkgs/development/tools/rust/cargo-limit/default.nix @@ -2,6 +2,8 @@ , rustPlatform , fetchFromGitHub , nix-update-script +, stdenv +, libiconv }: rustPlatform.buildRustPackage rec { @@ -17,6 +19,8 @@ rustPlatform.buildRustPackage rec { cargoSha256 = "sha256-LxqxRtMKUKZeuvk1caoYy8rv1bkEOQBM8i5SXMF4GXc="; + buildInputs = lib.optionals stdenv.isDarwin [ libiconv ]; + passthru = { updateScript = nix-update-script { attrPath = pname; From 0e13b2c44e3a4df8d0f43681d40d30e4822ac906 Mon Sep 17 00:00:00 2001 From: Evils Date: Sat, 5 Sep 2020 15:06:13 +0200 Subject: [PATCH 12/21] python3.pkgs.pytomlpp: init at 0.3.5 --- .../python-modules/pytomlpp/default.nix | 53 +++++++++++++++++++ pkgs/top-level/python-packages.nix | 2 + 2 files changed, 55 insertions(+) create mode 100644 pkgs/development/python-modules/pytomlpp/default.nix diff --git a/pkgs/development/python-modules/pytomlpp/default.nix b/pkgs/development/python-modules/pytomlpp/default.nix new file mode 100644 index 000000000000..19edd7057eb4 --- /dev/null +++ b/pkgs/development/python-modules/pytomlpp/default.nix @@ -0,0 +1,53 @@ +{ lib +, buildPythonPackage +, fetchFromGitHub +, pythonOlder +, pybind11 +, pytestCheckHook +, dateutil +, doxygen +, python +, pelican +, matplotlib +}: + +buildPythonPackage rec { + pname = "pytomlpp"; + version = "0.3.5"; + + src = fetchFromGitHub { + owner = "bobfang1992"; + repo = pname; + rev = version; + fetchSubmodules = true; + sha256 = "1h06a2r0f5q4mml485113mn7a7585zmhqsk2p1apcybyydllcqda"; + }; + + buildInputs = [ pybind11 ]; + + checkInputs = [ + pytestCheckHook + + dateutil + doxygen + python + pelican + matplotlib + ]; + + # pelican requires > 2.7 + doCheck = !pythonOlder "3.6"; + + preCheck = '' + cd tests + ''; + + pythonImportsCheck = [ "pytomlpp" ]; + + meta = with lib; { + description = "A python wrapper for tomlplusplus"; + homepage = "https://github.com/bobfang1992/pytomlpp"; + license = licenses.mit; + maintainers = with maintainers; [ evils ]; + }; +} diff --git a/pkgs/top-level/python-packages.nix b/pkgs/top-level/python-packages.nix index 13dbda61552e..8e24f152e30f 100644 --- a/pkgs/top-level/python-packages.nix +++ b/pkgs/top-level/python-packages.nix @@ -6728,6 +6728,8 @@ in { pytoml = callPackage ../development/python-modules/pytoml { }; + pytomlpp = callPackage ../development/python-modules/pytomlpp { }; + pytools = callPackage ../development/python-modules/pytools { }; pytorch = callPackage ../development/python-modules/pytorch { From e7d5862f4e12b0c6c093a257a25add014f98bb4c Mon Sep 17 00:00:00 2001 From: Ben Siraphob Date: Sat, 8 May 2021 23:55:56 +0700 Subject: [PATCH 13/21] coqPackages.hydra-battles: init at 0.3 --- .../coq-modules/hydra-battles/default.nix | 29 +++++++++++++++++++ pkgs/top-level/coq-packages.nix | 1 + 2 files changed, 30 insertions(+) create mode 100644 pkgs/development/coq-modules/hydra-battles/default.nix diff --git a/pkgs/development/coq-modules/hydra-battles/default.nix b/pkgs/development/coq-modules/hydra-battles/default.nix new file mode 100644 index 000000000000..a74eec4b64fc --- /dev/null +++ b/pkgs/development/coq-modules/hydra-battles/default.nix @@ -0,0 +1,29 @@ +{ lib, mkCoqDerivation, coq, mathcomp, equations, paramcoq, version ? null }: +with lib; + +mkCoqDerivation { + pname = "hydra-battles"; + owner = "coq-community"; + + release."0.3".rev = "v0.3"; + release."0.3".sha256 = "sha256-rXP/vJqVEg2tN/I9LWV13YQ1+C7M6lzGu3oI+7pSZzg="; + + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.11"; out = "0.3"; } + ] null; + + propagatedBuildInputs = [ mathcomp equations paramcoq ]; + + meta = { + description = "Variations on Kirby & Paris' hydra battles and other entertaining math in Coq"; + longDescription = '' + Variations on Kirby & Paris' hydra battles and other + entertaining math in Coq (collaborative, documented, includes + exercises) + ''; + maintainers = with maintainers; [ siraben ]; + license = licenses.mit; + platforms = platforms.unix; + }; +} diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index 6da0598c6ace..2a6c9d42377b 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -39,6 +39,7 @@ let heq = callPackage ../development/coq-modules/heq {}; hierarchy-builder = callPackage ../development/coq-modules/hierarchy-builder {}; HoTT = callPackage ../development/coq-modules/HoTT {}; + hydra-battles = callPackage ../development/coq-modules/hydra-battles {}; interval = callPackage ../development/coq-modules/interval {}; InfSeqExt = callPackage ../development/coq-modules/InfSeqExt {}; iris = callPackage ../development/coq-modules/iris {}; From ddc71c80de78f35e4035354603cca221f523c11b Mon Sep 17 00:00:00 2001 From: Ben Siraphob Date: Sun, 9 May 2021 00:01:39 +0700 Subject: [PATCH 14/21] coqPackages.pocklington: init at 8.12.0 --- .../coq-modules/pocklington/default.nix | 22 +++++++++++++++++++ pkgs/top-level/coq-packages.nix | 1 + 2 files changed, 23 insertions(+) create mode 100644 pkgs/development/coq-modules/pocklington/default.nix diff --git a/pkgs/development/coq-modules/pocklington/default.nix b/pkgs/development/coq-modules/pocklington/default.nix new file mode 100644 index 000000000000..111bffeca2c9 --- /dev/null +++ b/pkgs/development/coq-modules/pocklington/default.nix @@ -0,0 +1,22 @@ +{ lib, mkCoqDerivation, coq, version ? null }: +with lib; + +mkCoqDerivation { + pname = "pocklington"; + owner = "coq-community"; + + release."8.12.0".rev = "v8.12.0"; + release."8.12.0".sha256 = "sha256-0xBrw9+4g14niYdNqp0nx00fPJoSSnaDSDEaIVpPfjs="; + + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.7"; out = "8.12.0"; } + ] null; + + meta = { + description = "Pocklington's criterion for primality in Coq"; + maintainers = with maintainers; [ siraben ]; + license = licenses.mit; + platforms = platforms.unix; + }; +} diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index 2a6c9d42377b..e8737753652a 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -64,6 +64,7 @@ let odd-order = callPackage ../development/coq-modules/odd-order { }; paco = callPackage ../development/coq-modules/paco {}; paramcoq = callPackage ../development/coq-modules/paramcoq {}; + pocklington = callPackage ../development/coq-modules/pocklington {}; QuickChick = callPackage ../development/coq-modules/QuickChick {}; simple-io = callPackage ../development/coq-modules/simple-io { }; stdpp = callPackage ../development/coq-modules/stdpp { }; From 7209ede743cea82096696525acae32babba20748 Mon Sep 17 00:00:00 2001 From: Ben Siraphob Date: Sun, 9 May 2021 00:17:50 +0700 Subject: [PATCH 15/21] coqPackages.goedel: init at 8.12.0 --- .../coq-modules/goedel/default.nix | 24 +++++++++++++++++++ pkgs/top-level/coq-packages.nix | 1 + 2 files changed, 25 insertions(+) create mode 100644 pkgs/development/coq-modules/goedel/default.nix diff --git a/pkgs/development/coq-modules/goedel/default.nix b/pkgs/development/coq-modules/goedel/default.nix new file mode 100644 index 000000000000..f6ed9491e98c --- /dev/null +++ b/pkgs/development/coq-modules/goedel/default.nix @@ -0,0 +1,24 @@ +{ lib, mkCoqDerivation, coq, hydra-battles, pocklington, version ? null }: +with lib; + +mkCoqDerivation { + pname = "goedel"; + owner = "coq-community"; + + release."8.12.0".rev = "v8.12.0"; + release."8.12.0".sha256 = "sha256-4lAwWFHGUzPcfHI9u5b+N+7mQ0sLJ8bH8beqQubfFEQ="; + + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.11"; out = "8.12.0"; } + ] null; + + propagatedBuildInputs = [ hydra-battles pocklington ]; + + meta = { + description = "The Gödel-Rosser 1st incompleteness theorem in Coq"; + maintainers = with maintainers; [ siraben ]; + license = licenses.mit; + platforms = platforms.unix; + }; +} diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index e8737753652a..9884553c9e05 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -36,6 +36,7 @@ let flocq = callPackage ../development/coq-modules/flocq {}; fourcolor = callPackage ../development/coq-modules/fourcolor {}; gappalib = callPackage ../development/coq-modules/gappalib {}; + goedel = callPackage ../development/coq-modules/goedel {}; heq = callPackage ../development/coq-modules/heq {}; hierarchy-builder = callPackage ../development/coq-modules/hierarchy-builder {}; HoTT = callPackage ../development/coq-modules/HoTT {}; From 9622485d70a52f32a10972d0b913bfc99e6fe440 Mon Sep 17 00:00:00 2001 From: "Robert T. McGibbon" Date: Sun, 9 May 2021 11:35:38 -0400 Subject: [PATCH 16/21] python39Packages.python-toolbox: unbreak --- .../python-modules/python-toolbox/default.nix | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/pkgs/development/python-modules/python-toolbox/default.nix b/pkgs/development/python-modules/python-toolbox/default.nix index bdf09fdf2c79..a310736c7492 100644 --- a/pkgs/development/python-modules/python-toolbox/default.nix +++ b/pkgs/development/python-modules/python-toolbox/default.nix @@ -3,8 +3,7 @@ , docutils , fetchFromGitHub , isPy27 -, nose -, pytest +, pytestCheckHook }: buildPythonPackage rec { @@ -21,7 +20,13 @@ buildPythonPackage rec { checkInputs = [ docutils - pytest + pytestCheckHook + ]; + + disabledTestPaths = [ + # file imports 'dummy_threading', which was deprecated since py37 + # and removed in py39 + "test_python_toolbox/test_cute_profile/test_cute_profile.py" ]; meta = with lib; { From b593afbfb62334472d35f117a17ba76c826add3e Mon Sep 17 00:00:00 2001 From: Emery Hemingway Date: Sat, 8 May 2021 10:28:06 +0200 Subject: [PATCH 17/21] nicotine-plus: 1.4.1 -> 3.0.6 --- .../soulseek/nicotine-plus/default.nix | 39 ++++++++----------- pkgs/top-level/all-packages.nix | 4 +- 2 files changed, 17 insertions(+), 26 deletions(-) diff --git a/pkgs/applications/networking/soulseek/nicotine-plus/default.nix b/pkgs/applications/networking/soulseek/nicotine-plus/default.nix index 045120813f0d..fbf742c5e2a2 100644 --- a/pkgs/applications/networking/soulseek/nicotine-plus/default.nix +++ b/pkgs/applications/networking/soulseek/nicotine-plus/default.nix @@ -1,44 +1,37 @@ -{ lib, fetchFromGitHub, python27Packages, geoip }: +{ lib, fetchFromGitHub, python3Packages, gettext, gdk-pixbuf +, gobject-introspection, gtk3, wrapGAppsHook }: with lib; -python27Packages.buildPythonApplication { +python3Packages.buildPythonApplication rec { pname = "nicotine-plus"; - version = "1.4.1"; + version = "3.0.6"; src = fetchFromGitHub { owner = "Nicotine-Plus"; repo = "nicotine-plus"; - rev = "4e057d64184885c63488d4213ade3233bd33e67b"; - sha256 = "11j2qm67sszfqq730czsr2zmpgkghsb50556ax1vlpm7rw3gm33c"; + rev = version; + sha256 = "sha256-NL6TXFRB7OeqNEfdANkEqh+MCOF1+ehR+6RO1XsIix8="; }; - propagatedBuildInputs = with python27Packages; [ - pygtk - miniupnpc - mutagen - notify - (GeoIP.override { inherit geoip; }) - ]; + nativeBuildInputs = [ gettext wrapGAppsHook ]; - # Insert real docs directory. - # os.getcwd() is not needed - postPatch = '' - substituteInPlace ./pynicotine/gtkgui/frame.py \ - --replace "paths.append(os.getcwd())" "paths.append('"$out"/doc')" - ''; + propagatedBuildInputs = [ gtk3 gdk-pixbuf gobject-introspection ] + ++ (with python3Packages; [ pygobject3 ]); - postFixup = '' - mkdir -p $out/doc/ - mv ./doc/NicotinePlusGuide $out/doc/ + postInstall = '' mv $out/bin/nicotine $out/bin/nicotine-plus + substituteInPlace $out/share/applications/org.nicotine_plus.Nicotine.desktop \ + --replace "Exec=nicotine" "Exec=$out/bin/nicotine-plus" ''; + doCheck = false; + meta = { description = "A graphical client for the SoulSeek peer-to-peer system"; homepage = "https://www.nicotine-plus.org"; - license = licenses.gpl3; - maintainers = with maintainers; [ klntsky ]; + license = licenses.gpl3Plus; + maintainers = with maintainers; [ ehmry klntsky ]; platforms = platforms.unix; }; } diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 74152f3fd51d..ac3e1d41390b 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -24952,9 +24952,7 @@ in newsflash = callPackage ../applications/networking/feedreaders/newsflash { }; - nicotine-plus = callPackage ../applications/networking/soulseek/nicotine-plus { - geoip = geoipWithDatabase; - }; + nicotine-plus = callPackage ../applications/networking/soulseek/nicotine-plus { }; nice-dcv-client = callPackage ../applications/networking/remote/nice-dcv-client { }; From e612d0e09a033c4c51d466a6ced0b17616fa61e4 Mon Sep 17 00:00:00 2001 From: Lancelot SIX Date: Mon, 10 May 2021 09:22:57 +0100 Subject: [PATCH 18/21] gnuchess: 6.2.7 -> 6.2.8 See https://lists.gnu.org/archive/html/info-gnu/2021-05/msg00006.html for release information. --- pkgs/games/gnuchess/default.nix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pkgs/games/gnuchess/default.nix b/pkgs/games/gnuchess/default.nix index 69ec574a644f..9f7d1684a5c4 100644 --- a/pkgs/games/gnuchess/default.nix +++ b/pkgs/games/gnuchess/default.nix @@ -3,10 +3,10 @@ let s = # Generated upstream information rec { baseName="gnuchess"; - version="6.2.7"; + version="6.2.8"; name="${baseName}-${version}"; url="mirror://gnu/chess/${name}.tar.gz"; - sha256="0ilq4bfl0lwyzf11q7n2skydjhalfn3bgxhrp5hjxs5bc5d6fdp5"; + sha256="0irqb0wl30c2i1rs8f6mm1c89l7l9nxxv7533lr408h1m36lc16m"; }; buildInputs = [ flex From 0b973eaa9441f894c65e5008a042b21025f6ff44 Mon Sep 17 00:00:00 2001 From: Peter Hoeg Date: Wed, 5 May 2021 19:04:07 +0800 Subject: [PATCH 19/21] audacity-gtk3: re-introduce at 3.0.2 --- pkgs/applications/audio/audacity/default.nix | 52 +++++++++----------- pkgs/top-level/all-packages.nix | 4 +- 2 files changed, 27 insertions(+), 29 deletions(-) diff --git a/pkgs/applications/audio/audacity/default.nix b/pkgs/applications/audio/audacity/default.nix index 1a47451ad76b..0fee289021e4 100644 --- a/pkgs/applications/audio/audacity/default.nix +++ b/pkgs/applications/audio/audacity/default.nix @@ -30,24 +30,26 @@ , soundtouch , pcre /*, portaudio - given up fighting their portaudio.patch */ , linuxHeaders -, at-spi2-core ? null -, dbus ? null -, epoxy ? null -, libXdmcp ? null -, libXtst ? null -, libpthreadstubs ? null -, libselinux ? null -, libsepol ? null -, libxkbcommon ? null -, utillinux ? null +, at-spi2-core +, dbus +, epoxy +, libXdmcp +, libXtst +, libpthreadstubs +, libselinux +, libsepol +, libxkbcommon +, util-linux }: # TODO -# - as of 3.0.2, GTK2 is still the recommended version ref https://www.audacityteam.org/download/source/ check if that changes in future versions -# - detach sbsms +# 1. as of 3.0.2, GTK2 is still the recommended version ref https://www.audacityteam.org/download/source/ check if that changes in future versions +# 2. detach sbsms let - wxGTK-audacity = wxGTK.overrideAttrs (oldAttrs: rec { + inherit (lib) optionals; + + wxGTK' = wxGTK.overrideAttrs (oldAttrs: rec { src = fetchFromGitHub { owner = "audacity"; repo = "wxWidgets"; @@ -56,6 +58,7 @@ let fetchSubmodules = true; }; }); + in stdenv.mkDerivation rec { pname = "audacity"; @@ -70,28 +73,21 @@ stdenv.mkDerivation rec { patches = [ (fetchpatch { - url = "https://github.com/audacity/audacity/commit/007852e51fcbb5f1f359d112f28b8984a604dac6.patch"; + url = "https://github.com/audacity/audacity/pull/831/commits/007852e51fcbb5f1f359d112f28b8984a604dac6.patch"; sha256 = "0zp2iydd46analda9cfnbmzdkjphz5m7dynrdj5qdnmq6j3px9fw"; name = "audacity_xdg_paths.patch"; }) ]; - # this file *should* be generated by cmake but as of 2.4.2 isn't yet postPatch = '' touch src/RevisionIdent.h - ''; - preConfigure = '' - substituteInPlace src/FileNames.cpp --replace /usr/include/linux/magic.h ${linuxHeaders}/include/linux/magic.h + substituteInPlace src/FileNames.cpp \ + --replace /usr/include/linux/magic.h ${linuxHeaders}/include/linux/magic.h ''; - # workaround for a broken cmake. Drop it with a later version to see if it works. - # https://github.com/NixOS/nixpkgs/issues/94905 - cmakeFlags = lib.optional stdenv.isLinux "-DCMAKE_OSX_ARCHITECTURES="; - # audacity only looks for ffmpeg at runtime, so we need to link it in manually NIX_LDFLAGS = toString [ - # ffmpeg "-lavcodec" "-lavdevice" "-lavfilter" @@ -108,7 +104,7 @@ stdenv.mkDerivation rec { gettext pkg-config python3 - ] ++ lib.optionals stdenv.isLinux [ + ] ++ optionals stdenv.isLinux [ linuxHeaders ]; @@ -135,9 +131,9 @@ stdenv.mkDerivation rec { sratom suil twolame - wxGTK-audacity - wxGTK-audacity.gtk - ] ++ lib.optionals stdenv.isLinux [ + wxGTK' + wxGTK'.gtk + ] ++ optionals stdenv.isLinux [ at-spi2-core dbus epoxy @@ -147,7 +143,7 @@ stdenv.mkDerivation rec { libxkbcommon libselinux libsepol - utillinux + util-linux ]; doCheck = false; # Test fails diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index ac3e1d41390b..e59e1caeee38 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -22207,7 +22207,9 @@ in audacious = libsForQt5.callPackage ../applications/audio/audacious { }; audaciousQt5 = audacious; - audacity = callPackage ../applications/audio/audacity { wxGTK = wxGTK31-gtk2; }; + audacity-gtk2 = callPackage ../applications/audio/audacity { wxGTK = wxGTK31-gtk2; }; + audacity-gtk3 = callPackage ../applications/audio/audacity { wxGTK = wxGTK31-gtk3; }; + audacity = audacity-gtk2; audio-recorder = callPackage ../applications/audio/audio-recorder { }; From c72048d1a4fc1877f3bdef96dfb036662e0d8108 Mon Sep 17 00:00:00 2001 From: Ben Siraphob Date: Sat, 8 May 2021 21:38:12 +0700 Subject: [PATCH 20/21] coqPackages.interval: 4.1.0 -> 4.1.1 --- pkgs/development/coq-modules/interval/default.nix | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix index 8671eba67241..cdb904523651 100644 --- a/pkgs/development/coq-modules/interval/default.nix +++ b/pkgs/development/coq-modules/interval/default.nix @@ -1,6 +1,4 @@ -{ lib, mkCoqDerivation, which, autoconf -, coq, coquelicot, flocq, mathcomp -, bignums ? null, version ? null }: +{ lib, mkCoqDerivation, which, autoconf, coq, coquelicot, flocq, bignums ? null, version ? null }: with lib; mkCoqDerivation { pname = "interval"; @@ -8,12 +6,12 @@ with lib; mkCoqDerivation { domain = "gitlab.inria.fr"; inherit version; defaultVersion = with versions; switch coq.coq-version [ - { case = isGe "8.8" ; out = "4.1.0"; } + { case = isGe "8.8" ; out = "4.1.1"; } { 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.1.1".sha256 = "sha256-h2NJ6sZt1C/88v7W2xyuftEDoyRt3H6kqm5g2hc1aoU="; release."4.0.0".sha256 = "1hhih6zmid610l6c8z3x4yzdzw9jniyjiknd1vpkyb2rxvqm3gzp"; release."3.4.2".sha256 = "07ngix32qarl3pjnm9d0vqc9fdrgm08gy7zp306hwxjyq7h1v7z0"; release."3.3.0".sha256 = "0lz2hgggzn4cvklvm8rpaxvwaryf37i8mzqajqgdxdbd8f12acsz"; From 92c5a672b322afd85342423871883a02936f42d7 Mon Sep 17 00:00:00 2001 From: Ben Siraphob Date: Sun, 9 May 2021 23:25:47 +0700 Subject: [PATCH 21/21] coqPackages.autosubst: 5b40a32e -> 1.7 and fix build --- .../0001-changes-to-work-with-Coq-8.6.patch | 134 ------------------ .../coq-modules/autosubst/default.nix | 27 ++-- 2 files changed, 14 insertions(+), 147 deletions(-) delete mode 100644 pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch diff --git a/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch b/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch deleted file mode 100644 index dde0e2e03eb6..000000000000 --- a/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch +++ /dev/null @@ -1,134 +0,0 @@ -From 5b40a32e35fe446cda20ed34c756a010856f39ce Mon Sep 17 00:00:00 2001 -From: Theo Giannakopoulos -Date: Wed, 5 Apr 2017 15:48:55 -0400 -Subject: [PATCH] changes to work with Coq 8.6 - ---- - theories/Autosubst_Derive.v | 12 ++++++++++++ - theories/Autosubst_MMap.v | 3 ++- - 2 files changed, 14 insertions(+), 1 deletion(-) - -diff --git a/theories/Autosubst_Derive.v b/theories/Autosubst_Derive.v -index 61995de..cf87f67 100644 ---- a/theories/Autosubst_Derive.v -+++ b/theories/Autosubst_Derive.v -@@ -18,6 +18,7 @@ Hint Extern 0 (Ids _) => derive_Ids : derive. - - Ltac derive_Rename := - match goal with [ |- Rename ?term ] => -+ let inst := fresh "inst" in - hnf; fix inst 2; change _ with (Rename term) in inst; - intros xi s; change (annot term s); destruct s; - match goal with -@@ -66,6 +67,7 @@ Ltac has_var s := - Ltac derive_Subst := - match goal with [ |- Subst ?term ] => - require_instance (Rename term); -+ let inst := fresh "inst" in - hnf; fix inst 2; change _ with (Subst term) in inst; - intros sigma s; change (annot term s); destruct s; - match goal with -@@ -107,6 +109,7 @@ Hint Extern 0 (Subst _) => derive_Subst : derive. - Ltac derive_HSubst := - match goal with [ |- HSubst ?inner ?outer ] => - require_instance (Subst inner); -+ let inst := fresh "inst" in - hnf; fix inst 2; change _ with (HSubst inner outer) in inst; - intros sigma s; change (annot outer s); destruct s; - match goal with -@@ -327,6 +330,7 @@ Ltac derive_SubstLemmas := - assert (up_upren_n : - forall xi n, upn n (ren xi) = ren (iterate upren n xi)) by - (apply up_upren_n_internal, up_upren); -+ let ih := fresh "ih" in - fix ih 2; intros xi s; destruct s; try reflexivity; simpl; f_equal; - try apply mmap_ext; intros; rewrite ?up_upren, ?up_upren_n; apply ih); - -@@ -337,6 +341,7 @@ Ltac derive_SubstLemmas := - (apply up_id_internal; reflexivity); - assert (up_id_n : forall n, upn n ids = ids) by - (apply up_id_n_internal, up_id); -+ let ih := fresh "ih" in - fix ih 1; intros s; destruct s; simpl; f_equal; try reflexivity; - rewrite ?up_id, ?up_id_n; try apply mmap_id_ext; intros; apply ih); - -@@ -344,6 +349,7 @@ Ltac derive_SubstLemmas := - - assert (ren_subst_comp : - forall xi sigma (s : term), (rename xi s).[sigma] = s.[xi >>> sigma]) by( -+ let ih := fresh "ih" in - fix ih 3; intros xi sigma s; destruct s; try reflexivity; simpl; f_equal; - rewrite ?up_comp_ren_subst, ?up_comp_ren_subst_n, ?mmap_comp; - try apply mmap_ext; intros; apply ih); -@@ -357,6 +363,7 @@ Ltac derive_SubstLemmas := - assert (up_comp_subst_ren_n : - forall sigma xi n, upn n (sigma >>> rename xi) = upn n sigma >>> rename (iterate upren n xi)) - by (apply up_comp_subst_ren_n_internal; apply up_comp_subst_ren); -+ let ih := fresh "ih" in - fix ih 3; intros sigma xi s; destruct s; try reflexivity; simpl; - f_equal; rewrite ?up_comp_subst_ren, ?up_comp_subst_ren_n, ?mmap_comp; - try (rewrite hcomp_ren_internal; [|apply rename_subst]); -@@ -368,6 +375,7 @@ Ltac derive_SubstLemmas := - by (apply up_comp_internal; [reflexivity|apply ren_subst_comp|apply subst_ren_comp]); - assert (up_comp_n : forall sigma tau n, upn n (sigma >> tau) = upn n sigma >> upn n tau) - by (apply up_comp_n_internal; apply up_comp); -+ let ih := fresh "ih" in - fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal; - rewrite ?up_comp, ?up_comp_n, ?mmap_comp, ?hcomp_dist_internal; - try apply mmap_ext; intros; apply ih); -@@ -382,6 +390,7 @@ Ltac derive_HSubstLemmas := - let ids := constr:(ids : var -> inner) in - - assert (hsubst_id : forall (s : outer), s.|[ids] = s) by ( -+ let ih := fresh "ih" in - fix ih 1; intros s; destruct s; try reflexivity; simpl; f_equal; - rewrite ?up_id, ?up_id_n; try apply mmap_id_ext; intros; - (apply subst_id || apply ih) -@@ -390,6 +399,7 @@ Ltac derive_HSubstLemmas := - assert (hsubst_comp : forall (theta eta : var -> inner) (s : outer), - s.|[theta].|[eta] = s.|[theta >> eta]) - by ( -+ let ih := fresh "ih" in - fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal; - rewrite <- ?up_comp, <- ?up_comp_n, ?mmap_comp; try apply mmap_ext; intros; - (apply subst_comp || apply ih) -@@ -405,6 +415,7 @@ Ltac derive_SubstHSubstComp := - assert (ren_hsubst_comp : forall xi (theta : var -> inner) (s : outer), - rename xi s.|[theta] = (rename xi s).|[theta] - ) by ( -+ let ih := fresh "ih" in - fix ih 3; intros xi theta s; destruct s; try reflexivity; simpl; f_equal; - rewrite ?mmap_comp; try apply mmap_ext; intros; simpl; apply ih - ); -@@ -421,6 +432,7 @@ Ltac derive_SubstHSubstComp := - apply up_hcomp_n_internal; apply up_hcomp - ); - -+ let ih := fresh "ih" in - fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal; - rewrite ?up_hcomp, ?up_hcomp_n, ?hcomp_lift_n_internal, ?mmap_comp; - try apply mmap_ext; intros; apply ih -diff --git a/theories/Autosubst_MMap.v b/theories/Autosubst_MMap.v -index f8387e7..7af7902 100644 ---- a/theories/Autosubst_MMap.v -+++ b/theories/Autosubst_MMap.v -@@ -23,7 +23,7 @@ Arguments mmap {A B _} f !s /. - Class MMapExt (A B : Type) `{MMap A B} := - mmap_ext : forall f g, - (forall t, f t = g t) -> forall s, mmap f s = mmap g s. --Arguments mmap_ext {A B _ _ f g} H s. -+Arguments mmap_ext {A B H' _ f g} H s : rename. - - Class MMapLemmas (A B : Type) `{MMap A B} := { - mmap_id x : mmap id x = x; -@@ -123,6 +123,7 @@ Tactic Notation "msimpl" "in" "*" := (in_all msimplH); msimpl. - - Ltac derive_MMap := - hnf; match goal with [ |- (?A -> ?A) -> ?B -> ?B ] => -+ let map := fresh "map" in - intros f; fix map 1; intros xs; change (annot B xs); destruct xs; - match goal with - | [ |- annot _ ?ys ] => --- -2.13.2 - diff --git a/pkgs/development/coq-modules/autosubst/default.nix b/pkgs/development/coq-modules/autosubst/default.nix index b2609d5dfc32..a5f7cbb2f0b1 100644 --- a/pkgs/development/coq-modules/autosubst/default.nix +++ b/pkgs/development/coq-modules/autosubst/default.nix @@ -1,22 +1,23 @@ -{ lib, mkCoqDerivation, coq, mathcomp, version ? null }: +{ lib, mkCoqDerivation, coq, mathcomp-ssreflect, version ? null }: +with lib; + +mkCoqDerivation { + pname = "autosubst"; + + release."1.7".rev = "v1.7"; + release."1.7".sha256 = "sha256-qoyteQ5W2Noxf12uACOVeHhPLvgmTzrvEo6Ts+FKTGI="; -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; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.10"; out = "1.7"; } + ] null; - release."5b40a32e".rev = "1c3bb3bbf5477e3b33533a0fc090399f45fe3034"; - release."5b40a32e".sha256 = "1wqfzc9az85fvx71xxfii502jgc3mp0r3xwfb8vnb03vkk625ln0"; - - propagatedBuildInputs = [ mathcomp.ssreflect ]; - - patches = [./0001-changes-to-work-with-Coq-8.6.patch]; + propagatedBuildInputs = [ mathcomp-ssreflect ]; meta = { homepage = "https://www.ps.uni-saarland.de/autosubst/"; description = "Automation for de Bruijn syntax and substitution in Coq"; - maintainers = with maintainers; [ jwiegley ]; + maintainers = with maintainers; [ siraben jwiegley ]; + license = licenses.mit; }; }