Commit Graph

164 Commits

Author SHA1 Message Date
Pierre Roux
9134617536 coqPackages.coinduction: init at 1.9 2024-08-07 15:44:13 +02:00
Pierre Roux
a69fe54c49 coqPackages.stalmarck: init at 8.20.0 2024-08-07 12:15:20 +02:00
Vincent Laporte
ee96b8a3cf
Merge pull request #329695 from definfo/coq-high-school-geometry-8.16
coqPackages.high-school-geometry: init at 8.16
2024-07-31 09:52:37 +02:00
Martin Weinelt
852453aae1
coqPackages: restor recurseIntoAttrs
Fixes: 0213840 ("pythonPackages: move __attrsFailEvaluation to allo...")
2024-07-26 18:01:21 +02:00
definfo
b1d0e56bc4 coqPackages.high-school-geometry: init at 8.16 2024-07-24 23:57:23 +08:00
Philip Taron
4640ede492
coqPackages: allow one level of introspection before applying __attrsFailEvaluation 2024-07-04 14:02:42 -07:00
Pierre Roux
971ef0c694
coq_8_20: init at 8.20+rc1 (#323105) 2024-06-28 15:47:38 +02:00
Vincent Laporte
90e35645fc coqPackages.coq-hammer: init at 1.3.2 2024-06-27 07:09:32 +02:00
Vincent Laporte
b8a048b959 coqPackages.coq-hammer-tactics: init at 1.3.2 2024-06-27 07:09:32 +02:00
Vincent Laporte
9c479cf090
compcert: 3.13.1 → 3.14 (#308752) 2024-05-03 14:47:10 +00:00
Sebastian Ertel
ea51404f4e
coqPackages.ssprove: init at 0.2.0 (#306981) 2024-05-03 11:32:09 +02:00
Vincent Laporte
0a379ae698
coq: default to version 8.19 2024-04-29 20:45:04 +02:00
Vincent Laporte
e976fa8f49 coqPackages.vcfloat: enable for Coq 8.18 & 8.19 2024-04-02 22:41:01 +02:00
Vincent Laporte
cffe0a32af coqPackages.interval: 4.9.0 → 4.10.0 2024-04-02 22:41:01 +02:00
Vincent Laporte
453b69da7a coqPackages.VplTactic: init at 0.5 2024-03-15 10:24:58 +01:00
Vincent Laporte
4027ca26b9 coqPackages.Vpl: init at 0.5 2024-03-15 10:24:58 +01:00
Cyril Cohen
4116f0379e
coqPackages.vscoq-language-server: init at 2.0.3 (#256515) 2024-02-01 10:10:43 +01:00
Vincent Laporte
7ff0562792 coqPackages.compcert: use OCaml 4.14 2024-01-22 08:36:01 +01:00
Pierre Roux
d77d8f69f7 coq_8_19: init at 8.19+rc1 2023-12-19 14:41:20 +01:00
Adam Joseph
80472e3754 treewide: add __attrsFailEvaluation and __recurseIntoDerivationForReleaseJobs 2023-12-15 05:13:46 -08:00
Vincent Laporte
2ec2d68238 coqPackages.VST: 2.12 → 2.13
coqPackages.compcert: 3.13 → 3.13.1
2023-11-27 03:57:47 +01:00
ineol
6a63b4a97a
coqPackages.iris-named-props: new expression (#263100) 2023-11-10 08:37:23 +01:00
Vincent Laporte
42bea51aa7 coqPackages.VST: 2.11.1 → 2.12 2023-11-01 07:07:41 +01:00
Quinn Dougherty
c7634cf59a coqPackages.vcfloat: init at 2.1.1 2023-09-29 23:57:07 +02:00
Vincent Laporte
2abfae9e9b coq: 8.17.1 -> 8.18.0 2023-09-21 11:02:55 +02:00
Vincent Laporte
02643fe422 coq_8_18: init at 8.18+rc1 2023-09-04 10:02:59 +02:00
Vincent Laporte
84821b9769 coqPackages.paco: 4.1.2 → 4.2.0 2023-08-03 04:30:34 +02:00
Vincent Laporte
055d78335d coqPackages.bignums: 8.17.0 → 9.0.0+coq8.17 2023-07-25 03:45:12 +02:00
affeldt-aist
8a92dd9a9a
mathcomp-infotheo: init at 0.5.1 (#231077) 2023-05-11 23:09:28 +02:00
Vincent Laporte
e11ba0e7e1
coq: default to version 8.17 2023-04-13 14:23:20 +02:00
Pierre Roux
2fb1078369 Put mathcomp packages in alphabetical order 2023-03-30 13:55:40 +02:00
Pierre Roux
25c631cc0e Add coqPackages.mathcomp-apery 2023-03-30 13:55:40 +02:00
Théo Zimmermann
f89354c12f coqPackages_8_13.VST: fix by using compatible version of ITree
Co-authored-by: Vincent Laporte <Vincent.Laporte@gmail.com>
2023-03-30 10:37:16 +02:00
Vincent Laporte
82d2212d29 compcert: 3.11 → 3.12 2023-03-01 09:45:31 +00:00
Mario Rodas
ca97b34a97 coqPackages_8_16.coq-lsp: init at 0.1.6.1+8.16 2023-02-21 04:20:00 +00:00
Pierre Roux
cc1d830b2a
coq_8_17: init at 8.17+rc1 (#209145) 2023-01-06 15:51:50 +01:00
Cyril Cohen
e31777a12c coqPackages.mathcomp-algebra-tactics: init at 1.0.0 2022-11-24 20:41:35 +01:00
Vincent Laporte
1101dfae20 coq: default to version 8.16 2022-10-12 20:38:44 +02:00
Vincent Laporte
661ee3a269 coq_8_16: use OCaml 4.14 2022-10-12 20:38:44 +02:00
Pierre Roux
4610844682 Split coqPackages.mathcomp-analysis
In preparation of https://github.com/math-comp/analysis/pull/600
2022-09-26 09:46:37 +02:00
Dennis Gosnell
a3f5759e53
Merge pull request #188766 from cdepillabout/overrideCoqDerivation
coqPackages.mkCoqDerivation: add a lib.overrideCoqDerivation function
2022-09-11 08:41:55 -04:00
Kenji Maillard
c91790e21c add attributes for metacoq subpackages 2022-09-06 15:55:48 +02: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
3ea8ed7d7e Split out CoqIDE by default when Coq >= 8.14. 2022-07-10 15:49:44 +02:00
Pierre Roux
ecf2791d8b coq_8_16: init at 8.16+rc1 2022-06-08 18:42:10 +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
Vincent Laporte
a7241ea207
coq: default to 8.15 2022-05-07 07:29:49 +02:00
Kenji Maillard
86a6908045
coqPackages.metacoq: create package (#162639) 2022-05-03 09:26:34 +02:00