···3333* `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.
3434* `useDune2ifVersion` (optional, default to `(x: false)` uses Dune2 to build the package if the provided predicate evaluates to true on the version, e.g. `useDune2if = versions.isGe "1.1"` will use dune if the version of the package is greater or equal to `"1.1"`,
3535* `useDune2` (optional, defaults to `false`) uses Dune2 to build the package if set to true, the presence of this attribute overrides the behavior of the previous one.
3636+* `opam-name` (optional, defaults to `coq-` followed by the value of `pname`), name of the Dune package to build.
3637* `enableParallelBuilding` (optional, defaults to `true`), since it is activated by default, we provide a way to disable it.
3738* `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.
3839* `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`,
···172172 </para>
173173 </listitem>
174174 </itemizedlist>
175175+ <itemizedlist spacing="compact">
176176+ <listitem>
177177+ <para>
178178+ <link xlink:href="https://www.navidrome.org/">navidrome</link>,
179179+ a personal music streaming server with subsonic-compatible
180180+ api. Available as
181181+ <link linkend="opt-services.navidrome.enable">navidrome</link>.
182182+ </para>
183183+ </listitem>
184184+ </itemizedlist>
175185 </section>
176186 <section xml:id="sec-release-21.11-incompatibilities">
177187 <title>Backward Incompatibilities</title>
+3
nixos/doc/manual/release-notes/rl-2111.section.md
···5353- [isso](https://posativ.org/isso/), a commenting server similar to Disqus.
5454 Available as [isso](#opt-services.isso.enable)
55555656+* [navidrome](https://www.navidrome.org/), a personal music streaming server with
5757+subsonic-compatible api. Available as [navidrome](#opt-services.navidrome.enable).
5858+5659## Backward Incompatibilities {#sec-release-21.11-incompatibilities}
57605861- The `staticjinja` package has been upgraded from 1.0.4 to 3.0.1
···828828 };
829829 challengeResponsePath = mkOption {
830830 default = null;
831831- type = types.path;
831831+ type = types.nullOr types.path;
832832 description = ''
833833 If not null, set the path used by yubico pam module where the challenge expected response is stored.
834834
···11-{ lib, mkCoqDerivation, coq, mathcomp, equations, paramcoq, version ? null }:
11+{ lib, mkCoqDerivation, coq, equations, version ? null }:
22with lib;
3344mkCoqDerivation {
55 pname = "hydra-battles";
66 owner = "coq-community";
7788- release."0.3".rev = "v0.3";
99- release."0.3".sha256 = "sha256-rXP/vJqVEg2tN/I9LWV13YQ1+C7M6lzGu3oI+7pSZzg=";
88+ release."0.4".sha256 = "sha256:1f7pc4w3kir4c9p0fjx5l77401bx12y72nmqxrqs3qqd3iynvqlp";
99+ releaseRev = (v: "v${v}");
10101111 inherit version;
1212 defaultVersion = with versions; switch coq.coq-version [
1313- { case = isGe "8.11"; out = "0.3"; }
1313+ { case = isGe "8.11"; out = "0.4"; }
1414 ] null;
15151616- propagatedBuildInputs = [ mathcomp equations paramcoq ];
1616+ propagatedBuildInputs = [ equations ];
1717+1818+ useDune2 = true;
17191820 meta = {
1919- description = "Variations on Kirby & Paris' hydra battles and other entertaining math in Coq";
2121+ description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq";
2022 longDescription = ''
2121- Variations on Kirby & Paris' hydra battles and other
2222- entertaining math in Coq (collaborative, documented, includes
2323- exercises)
2323+ An exploration of some properties of Kirby and Paris' hydra
2424+ battles, with the help of the Coq Proof assistant. This
2525+ development includes the study of several representations of
2626+ ordinal numbers, and a part of the so-called Ketonen and Solovay
2727+ machinery (combinatorial properties of epsilon0).
2428 '';
2525- maintainers = with maintainers; [ siraben ];
2929+ maintainers = with maintainers; [ siraben Zimmi48 ];
2630 license = licenses.mit;
2731 platforms = platforms.unix;
2832 };
+1-1
pkgs/development/coq-modules/mathcomp/default.nix
···1919 owner = "math-comp";
2020 withDoc = single && (args.withDoc or false);
2121 defaultVersion = with versions; switch coq.coq-version [
2222- { case = isGe "8.13"; out = "1.12.0"; } # lower version of coq to 8.10 when all mathcomp packages are ported
2222+ { case = isGe "8.10"; out = "1.12.0"; }
2323 { case = range "8.7" "8.12"; out = "1.11.0"; }
2424 { case = range "8.7" "8.11"; out = "1.10.0"; }
2525 { case = range "8.7" "8.11"; out = "1.9.0"; }