86 Commits

Author SHA1 Message Date
Yifei Sun 5e2c21a18f coqPackages.mathcomp: modernize mkCoqDerivation release hash format 2026-06-17 22:36:59 +02:00
Pierre Roux 30b1c85e66 rocqPackages.mathcomp-algebra: master depends on micromega-plugin 2026-05-06 11:57:10 +02:00
Pierre Roux 96af9f8acf rocqPackages.mathcomp: rename fingroup -> finite-group and character -> group-representation 2026-05-05 14:11:16 +02:00
Pierre Roux a4d52834af rocqPackages.mathcomp: init at 2.5.0 2026-01-12 11:43:45 +01:00
Pierre Roux 65fb0bd613 coqPackages.mathcomp: 2.4.0 -> 2.5.0 2025-11-12 17:43:56 +01:00
Wolfgang Walther 5a0711127c treewide: run nixfmt 1.0.0 2025-07-24 13:55:40 +02:00
Pierre Roux 6bb4f60316 coqPackages.*: 9.0 -> 9.1 2025-07-09 07:27:19 +02:00
Pierre Roux 19e4869241 coqPackages.*: better formatting fix 2025-06-30 10:10:31 +02:00
Pierre Roux 0ddb075c4d coqPackages.*: fix formatting 2025-06-21 17:23:27 +02:00
Pierre Roux 42dba13fa6 coqPackages.mathcomp: 2.3.0 -> 2.4.0 2025-05-10 12:06:21 +02:00
Pierre Roux 0401f9a22a coqPackages.mathcomp-boot: init at master (future 2.5.0) 2025-05-05 15:16:10 +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](https://github.com/NixOS/nixpkgs/tree/8616af08d915377bd930395f3b700a0e93d08728/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 873cceaf59 coqPackages.mathcomp*: update stdlib dependencies 2025-02-24 21:02:24 +01:00
Pierre Roux c407726f4f coqPackages.mathcomp: remove Stdlib dependency
Adapting to https://github.com/math-comp/math-comp/pull/1343
2025-02-14 14:21:56 +01:00
Pierre Roux c683a77656 coq_9_0: init at 9.0+rc1 2025-01-26 16:32:07 +01:00
Pierre Roux 04133be9c7 coqPackages.mathcomp: adapt to https://github.com/math-comp/math-comp/pull/1329 2025-01-23 13:48:52 +01:00
Pierre Roux a5a738b092 coqPackages.mathcomp: 2.2.0 -> 2.3.0 2025-01-08 12:55:42 +01:00
Pierre Roux 629830c8ff Add coqPackages.stdlib 2024-12-13 11:42:53 +01:00
h7x4 574f430583 Merge pull request #331530 from proux01/mc2-default
coqPackages.mathcomp: 1 -> 2
2024-08-20 08:10:55 +02:00
Sigmanificient 63d05d989e pkgs/development: remove unused arguments 2024-08-03 17:18:20 +02:00
Pierre Roux a06a5415bb coqPackages.mathcomp: 1 -> 2 2024-08-01 17:13:09 +02:00
Pierre Roux 383e9b5696 coq-elpi: 2.0.1 -> 2.2.0 (#323590)
elpi: 1.18.1 -> 1.19.2
2024-07-01 08:04:15 +02:00
Pierre Roux 971ef0c694 coq_8_20: init at 8.20+rc1 (#323105) 2024-06-28 15:47:38 +02:00
Philip Taron 94112e3ae5 coqPackages.mathcomp: avoid top-level with ...; 2024-06-25 09:04:21 -07:00
Pierre Roux 2c7c560330 coqPackages.mathcomp: 2.1.0 -> 2.2.0 2024-01-17 15:40:16 +01:00
Pierre Roux e1f1b5bcd2 coqPackages.mathcomp: 1.18.0 -> 1.19.0 2024-01-16 10:34:25 +01:00
Pierre Roux d77d8f69f7 coq_8_19: init at 8.19+rc1 2023-12-19 14:41:20 +01:00
Pierre Roux c2892b3fc9 coqPackages.mathcomp: 1.17.0 -> 1.18.0 (#265046)
* coqPackages.mathcomp: 1.17.0 -> 1.18.0

* coqPackages.mathcomp-analysis: 0.6.5 -> 0.6.6
2023-11-15 13:22:46 +01:00
Pierre Roux c0c7836116 Add mathcomp 2.1.0 2023-10-25 17:45:56 +02:00
Pierre Roux ae24e3e528 Add a few packages for Coq 8.18 and MathComp 2.0 2023-09-04 10:02:59 +02:00
Felix Buehler bec27fabee treewide: use lib.optional instead of 'then []' 2023-07-12 09:36:28 +01:00
Pierre Roux ed1f52d4c2 Mathcomp 1.16.0 -> 1.17.0 2023-05-17 16:26:09 +02:00
Pierre Roux a0ca431141 Add coqPackages.mathcomp 2.0.0 2023-05-15 11:26:42 +02:00
Pierre Roux 2959062362 coqPackages: various 8.16 -> 8.17 2023-03-09 13:13:00 +01:00
Shawn8901 4dcb03a5c3 treewide: remove global with lib; statements in pkgs/coq-modules 2023-01-21 23:19:48 +01:00
Enrico Tassi e50697278b mathcomp: 1.14.0 -> 1.15.0 2022-08-31 19:00:56 +02:00
Vincent Laporte 10f159ffd1 coqPackages.mathcomp: disable for Coq ≥ 8.16 2022-06-13 11:29:20 +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 dffe2434ae coqPackages.mathcomp: 1.13.0 -> 1.14.0 2022-02-02 08:56:55 +01:00
Cyril Cohen c5c34f6be1 coqPackages.mathcomp: 1.12.0 -> 1.13.0 2021-10-29 21:05:07 +02:00
Théo Zimmermann 839354e312 coqPackages.mathcomp: change default version for Coq 8.10+
Fix the build of mathcomp-analysis with Coq 8.12 (by selecting a version which is compatible with HB 1.1.0).
2021-08-17 15:59:06 +02:00
Cyril Cohen 18f9a74a18 coqPackages.mathcomp: etc (#115417)
* Fixing doc generation for mathcomp

* Update pkgs/development/coq-modules/mathcomp/default.nix

Co-authored-by: Sandro <sandro.jaeckel@gmail.com>

* More robust patchShebangs directives

Co-authored-by: Sandro <sandro.jaeckel@gmail.com>
2021-03-15 12:59:05 +01:00
Cyril Cohen 9ffd16b385 coqPackages: refactor 2021-01-09 11:56:17 +01:00
Vincent Laporte de8205f8bb coq_8_13: init at 8.13+β1 2020-12-15 21:13:40 +01:00
Vincent Laporte 5293575e85 coqPackages.mathcomp: enable 1.11.0 for Coq 8.12 2020-06-19 12:28:42 +02:00
Cyril Cohen b7f55b30f5 coqPackages.mathcomp: 1.11.0 2020-06-12 14:37:40 +02:00
Cyril Cohen 147aded7df coqPackages.mathcomp-extra: refactor
- removing broken packages
- taking into account fixpoint coqPackages in mathcomp-extra-config
2020-05-27 09:22:42 +02:00