From 962d8fb3ed9d715fcefc7b831056ca18b08e1896 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Mon, 6 Jul 2026 13:23:13 +0200 Subject: [PATCH] mkRocqDerivation: document new parameters useCoq and useCoqifVersion --- doc/languages-frameworks/rocq.section.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/languages-frameworks/rocq.section.md b/doc/languages-frameworks/rocq.section.md index f2ba50312807..056394056797 100644 --- a/doc/languages-frameworks/rocq.section.md +++ b/doc/languages-frameworks/rocq.section.md @@ -74,6 +74,8 @@ The recommended way of defining a derivation for a Rocq library, is to use the ` * `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 variables `COQLIBINSTALL` and `COQPLUGININSTALL` so as to install in the proper subdirectory. Indeed Rocq libraries should be installed in `$(out)/lib/coq/${rocq-core.rocq-version}/user-contrib/`. Such directories are automatically added to the `$ROCQPATH` environment variable by the hook defined in the Rocq derivation. * `setROCQBIN` (optional, defaults to `true`), by default, the environment variable `$ROCQBIN` is set to the current Rocq's binary, but one can disable this behavior by setting it to `false`, +* `useCoq` (optional, defaults to `false`), adds the Coq compatibility binaries to the build environment, which is necessary for some packages that still depend on them and sets `COQBIN` to the path of the `coqc` binary (if `setROCQBIN` is also set to `true`). A wrapper `mkCoqDerivation` is provided that sets this option to `true`. +* `useCoqifVersion` (optional, defaults to `(x: false)`), adds the Coq compatibility binaries to the build environment if the provided predicate evaluates to true on the version. This can be useful for supporting old package versions that need the Coq compatibility binaries, while newer versions do not. * `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`.