Commit Graph

44 Commits

Author SHA1 Message Date
Théo Zimmermann
0235b9517e mkCoqDerivation: make a wrapper on top of mkRocqDerivation 2026-07-10 17:56:53 +02:00
Stefan Frijters
8ad58c00a8 coqPackages.mkCoqDerivation: move env variables into env for structuredAttrs 2026-07-06 14:55:58 +02:00
Théo Zimmermann
6548b1eece mkCoqDerivation: clean up support for Coq <= 8.6
We don't package these old versions anymore.
2026-07-02 16:52:23 +02:00
Théo Zimmermann
301164d8e0 mkCoqDerivation: clean up enableParallelBuilding warning logic
Not necessary anymore.
2026-07-02 16:52:18 +02:00
Théo Zimmermann
7e160edd5d mkCoqDerivation/mkRocqDerivation: update ref to Rocq-community 2026-07-02 15:53:02 +02:00
Aliaksandr
b4e15ead13 mkCoqDerivation: warn on superfluous enableParallelBuilding 2026-01-31 22:36:34 +02:00
Vincent Laporte
72b918494c dune_3: move out of ocamlPackages 2025-12-10 21:51:39 +01:00
Vincent Laporte
dc205f7b4f coqPackages.mkCoqDerivation: add support for release.<version>.hash (#443726) 2025-11-25 14:41:04 +00:00
NAHO
c8d4dabc43 pkgs: remove optional builtins prefixes from prelude functions
Remove optional builtins prefixes from prelude functions by running:

    builtins=(
      abort
      baseNameOf
      break
      derivation
      derivationStrict
      dirOf
      false
      fetchGit
      fetchMercurial
      fetchTarball
      fetchTree
      fromTOML
      import
      isNull
      map
      null
      placeholder
      removeAttrs
      scopedImport
      throw
      toString
      true
    )

    fd \
      --type file \
      . \
      pkgs \
      --exec-batch sed --in-place --regexp-extended "
        s/\<builtins\.($(
          printf '%s\n' "${builtins[@]}" |
            paste --delimiter '|' --serial -
        ))\>/\1/g
      "

    nix fmt
2025-10-04 19:02:37 +02:00
Yifei Sun
f289f9c97f coqPackages.mkCoqDerivation: add support for release.<version>.hash
Per https://github.com/NixOS/nixpkgs/pull/436779 review comment.

This is the first step to support SRI hashes for Rocq packages.

Co-authored-by: Vincent Laporte <Vincent.Laporte@gmail.com>
2025-09-18 10:21:08 +02:00
Arthur Azevedo de Amorim
90db71098f coq: Fix bug when supplying release src.
Because of Nix precedence rules, the previous version of `mkCoqDerivation`
required that the supplied `src` parameter to a package's release were a
function that returned the source.  If an actual source was provided, a
confusing error message was thrown.  This commit fixes this issue.
2025-05-05 21:52:17 +02:00
Silvan Mosberger
374e6bcc40 treewide: Format all Nix files
Format all Nix files using the officially approved formatter,
making the CI check introduced in the previous commit succeed:

  nix-build ci -A fmt.check

This is the next step of the of the [implementation](https://github.com/NixOS/nixfmt/issues/153)
of the accepted [RFC 166](https://github.com/NixOS/rfcs/pull/166).

This commit will lead to merge conflicts for a number of PRs,
up to an estimated ~1100 (~33%) among the PRs with activity in the past 2
months, but that should be lower than what it would be without the previous
[partial treewide format](https://github.com/NixOS/nixpkgs/pull/322537).

Merge conflicts caused by this commit can now automatically be resolved while rebasing using the
[auto-rebase script](8616af08d9/maintainers/scripts/auto-rebase).

If you run into any problems regarding any of this, please reach out to the
[formatting team](https://nixos.org/community/teams/formatting/) by
pinging @NixOS/nix-formatting.
2025-04-01 20:10:43 +02:00
Pierre Roux
b6d12f5938 add overrideRocqDerivation 2025-03-27 08:27:43 +01:00
Peder Bergebakken Sundt
5aba99242e treewide: fix typos in comments
Made with

```shell
git restore .
fd '\.nix$' pkgs/ --type f -j1 -x bash -xc "$(cat <<"EOF"
    typos --no-check-filenames --write-changes "$1"
    git diff --exit-code "$1" && exit
    #( git diff "$1" | grep -qE "^\+ +[^# ]") && git restore "$1"
    count1="$( bat --language nix --diff --style changes "$1" --theme "Monokai Extended" --color always | aha --no-header | grep -E '^<span style="color:olive;">~</span> ' | wc -l )"
    count2="$( bat --language nix --diff --style changes "$1" --theme "Monokai Extended" --color always | aha --no-header | grep -E '^<span style="color:olive;">~</span> (<span style="color:#f8f8f2;"> *</span>)?<span style="color:#75715e;">.*</span>$' | wc -l )"
    [[ $count1 -ne $count2 ]] && git restore "$1"
EOF
)" -- {}
```

and filtered with `GIT_DIFF_OPTS='--unified=15' git -c interactive.singleKey=true add --patch`

I initially tried using the tree-sitter cli, python bindings and even ast-grep through various means, but this is what I ended up with.
2025-02-24 10:44:41 +01:00
Sergei Trofimovich
ef6ac2dd6e coqPackages.metaFetch: fix sort predicate stability
Incorrect sorting predicate was found as part of
https://github.com/NixOS/nix/issues/12106 where `nix` was crashing on
the code like:

    $ nix eval --expr 'builtins.sort (a: b: true) [ 1 2 3 ]'
    ...
    Aborted (core dumped)

Note: the crash happens here because sorting predicate does not
implement `lessThan` and triggers assertion failures for
`std::stable_sort` that backs `builtins.sort`.

The change restores `lessThan` semantic for `version sorting`.
2024-12-26 23:02:04 +00:00
Silvan Mosberger
4f0dadbf38 treewide: format all inactive Nix files
After final improvements to the official formatter implementation,
this commit now performs the first treewide reformat of Nix files using it.
This is part of the implementation of RFC 166.

Only "inactive" files are reformatted, meaning only files that
aren't being touched by any PR with activity in the past 2 months.
This is to avoid conflicts for PRs that might soon be merged.
Later we can do a full treewide reformat to get the rest,
which should not cause as many conflicts.

A CI check has already been running for some time to ensure that new and
already-formatted files are formatted, so the files being reformatted here
should also stay formatted.

This commit was automatically created and can be verified using

    nix-build a08b3a4d19.tar.gz \
      --argstr baseRev b32a094368
    result/bin/apply-formatting $NIXPKGS_PATH
2024-12-10 20:26:33 +01:00
github-actions[bot]
ac34133fb9 Merge master into staging-next 2024-09-23 12:05:36 +00:00
Vincent Laporte
94d0d22817 ocamlPackages.elpi: use release tarball (#343266)
coqPackages.metaFetch: Adding a github artifact option

Co-authored-by: Cyril Cohen <cohen@crans.org>
2024-09-23 09:52:07 +02:00
github-actions[bot]
73cf025711 Merge staging-next into staging 2024-09-17 12:05:50 +00:00
nicoo
633f94fa4a doc/coq: sha256hash 2024-09-17 10:47:31 +02:00
Yueh-Shun Li
5d42a8b38c treewide: handle preConfigurePhases __structuredAttrs-agnostically
Always specify the preConfigurePhases attribute as a list instead of a
string.

Append elements to the preConfigurePhases Bash variable using
appendToVar instead of string or Bash array concatenation.
2024-09-03 05:33:59 +08:00
Vincent Laporte
5d61a87d94 mkCoqDerivation: fix install path of ML plug-in built w/ dune 2024-06-25 21:07:57 +02:00
Philip Taron
c4d420345d Avoid top-level with ...; in pkgs/build-support/coq/extra-lib.nix 2024-03-19 22:31:19 +01:00
Philip Taron
4fc5d50549 Avoid top-level with ...; in pkgs/build-support/coq/meta-fetch/default.nix 2024-03-19 22:31:19 +01:00
Philip Taron
03962f077c Avoid top-level with ...; in pkgs/build-support/coq/default.nix 2024-03-19 22:31:19 +01:00
Felix Buehler
d10e69c86b treewide: deprecate isNull
https://nixos.org/manual/nix/stable/language/builtins.html#builtins-isNull
2023-03-06 22:40:04 +01:00
Vincent Laporte
db0dc68975 mkCoqDerivation: findlib is an optional input 2023-02-28 10:59:42 +00:00
Théo Zimmermann
2dc3552aa1 coqPackages.mkCoqDerivation: upgrade to Dune 3
And remove the version number from the corresponding attributes.
2022-10-02 14:42:28 +02:00
Dennis Gosnell
346454873e coqPackages.lib.overrideCoqDerivation: update documentation for overriding version 2022-09-11 07:41:17 +09:00
Dennis Gosnell
06ece659f0 coqPackages.mkCoqDerivation: add a coqPackages.lib.overrideCoqDerivation function
`overrideCoqDerivation` allows end-users the ability to easily override
arguments to the underlying call to `mkCoqDerivation` for a given Coq
library.

This is similar to `haskell.lib.overrideCabal` for Haskell packages and
`.overridePythonAttrs` for Python packges.
2022-08-29 14:41:03 +09:00
Théo Zimmermann
c6815758ac Do not rely on legacy ocaml passthru value. 2022-07-08 14:33:24 +02:00
Vincent Laporte
af888339b6 mkCoqDerivation: do not set DESTDIR
Fixes #178109
2022-06-18 11:54:21 +02:00
Cyril Cohen
d113661156 coqPackages: etc
- put `findlib` in `buildInputs` of `mkCoqDerivation` to make sure `coq` packages find their ocaml plugin dependencies,
- use `propagatedBuildInputs` to make sure ocaml plugin dependencies are in path,
- updated `coqPackage.heq` (broken url),
- fixed use of `DESTDIR` and `COQMF_COQLIB` in mkCoqDerivation,
- adding `COQCORELIB` environement variable to put ocaml plugin files in the right place,
- make `metaFetch` available from `coqPackages`
2022-05-25 20:00:25 +02:00
Vincent Laporte
1f11888116 Revert "coqPackages: etc"
This reverts commit 7e589a45ef.
2022-05-13 06:47:14 +02:00
Cyril Cohen
7e589a45ef coqPackages: etc
- use propagatedBuildInputs to make sure ocaml plugin stuff is in path
- updated coqPackage.heq (broken url)
- fixed use of `DESTDIR` and `COQMF_COQLIB` in mkCoqDerivation
- adding `COQCORELIB` environement variable to put ocaml plugin files in the right place
- make metaFetch available from `coqPackages`
2022-05-12 06:11:43 +02:00
Ulrik Strid
7e20e9039e coqPackages: tree-wide move packages to nativeBuildInputs and add strictDeps = true
Co-authored-by: Vincent Laporte <vbgl@users.noreply.github.com>
2022-02-25 07:54:17 +01:00
Cyril Cohen
876cd6bcc2 coq: misc
Removing a dangling `let` that went undetected for a while
2022-02-15 10:06:07 +01:00
Théo Zimmermann
20291381c1 coqPackages.mkCoqDerivation: rely on namePrefix to compute default opam-name
As suggested by Cyril Cohen in https://github.com/NixOS/nixpkgs/pull/134362#discussion_r698379405.
2021-09-20 11:10:23 +02:00
Théo Zimmermann
7136060765 mkCoqDerivation: use COQMF_COQLIB for dev versions of Coq 2021-09-08 15:15:28 +02:00
Théo Zimmermann
90654cce7d coqPackages.mkCoqDerivation: fix useDune2
- Reuse build phase from the `buildDunePackage` function.
- Only install the package that was just built (useful for monorepo support).
- Introduces `opam-name` to override the default package name to build with Dune.
2021-08-17 14:38:47 +02:00
Théo Zimmermann
489959099f mkCoqDerivation: fix useDune2 2021-06-10 21:52:03 +02:00
Cyril Cohen
1550a4fe6b coqPackages.multinomials: 1.5.2 -> 1.5.4 (#115427)
- This is the first packages which uses Dune in order to build and install
  so I had to refactor build-support/coq/default.nix in order to support it.
- I added a new feature: one can now release.v.sha256 empty to try to download
  with a fake sha256, hence failures are reported and one can copy paste the
  sha256 given by the error message.
- I updated the documentation of languages-frameworks/coq.section.md accordingly.
2021-03-10 16:25:32 +01:00
Ben Siraphob
82454e9df8 treewide: remove implicit use of stdenv.lib 2021-01-27 20:04:57 +07:00
Cyril Cohen
9ffd16b385 coqPackages: refactor 2021-01-09 11:56:17 +01:00