diff options
73 files changed, 1740 insertions, 2385 deletions
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 <archive-url>` to find it, where `<archive-url>` 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/nixos/modules/virtualisation/podman.nix b/nixos/modules/virtualisation/podman.nix index f554aeffb451..36c0ca8dfea3 100644 --- a/nixos/modules/virtualisation/podman.nix +++ b/nixos/modules/virtualisation/podman.nix @@ -1,6 +1,8 @@ { config, lib, pkgs, utils, ... }: let cfg = config.virtualisation.podman; + toml = pkgs.formats.toml { }; + nvidia-docker = pkgs.nvidia-docker.override { containerRuntimePath = "${pkgs.runc}/bin/runc"; }; inherit (lib) mkOption types; @@ -53,6 +55,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 +88,37 @@ in }; - config = lib.mkIf cfg.enable { - - 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"; - - # Enable common /etc/containers configuration - virtualisation.containers.enable = true; - - assertions = [{ - assertion = cfg.dockerCompat -> !config.virtualisation.docker.enable; - message = "Option dockerCompat conflicts with docker"; - }]; - - }; + config = lib.mkIf cfg.enable (lib.mkMerge [ + { + 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"; + + 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 [ nvidia-docker ]}" ]; + runtimes.nvidia = [ "${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 = "${nvidia-docker}/etc/podman-config.toml"; + }) + ]); } 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/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"; 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; 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; |