Commit Graph

624 Commits

Author SHA1 Message Date
Weijia Wang
8ff706bad2
Merge pull request #212009 from Shawn8901/remove_with_lib_2
treewide: remove global with lib; statements in pkgs/coq-modules
2023-01-24 01:39:55 +01:00
Weijia Wang
218c4c526e
Merge pull request #212002 from mothsART/feature/replace_http_by_https
treewide: replace http by https when https is a permanent redirection
2023-01-22 03:26:02 +01:00
Ferry Jérémie
65d7e87fdb treewide: replace http by https when https is a permanent redirection 2023-01-22 02:46:49 +01:00
Shawn8901
4dcb03a5c3 treewide: remove global with lib; statements in pkgs/coq-modules 2023-01-21 23:19:48 +01:00
Guillaume Girol
33afbf39f6 treewide: switch to nativeCheckInputs
checkInputs used to be added to nativeBuildInputs. Now we have
nativeCheckInputs to do that instead. Doing this treewide change allows
to keep hashes identical to before the introduction of
nativeCheckInputs.
2023-01-21 12:00:00 +00:00
Vincent Laporte
290df59e84 coqPackages_8_13.smtcoq: fix build by using older make 2023-01-11 08:43:14 +01:00
Vincent Laporte
670a782340 coqPackages_8_13.smtcoq.cvc4: fix build by using older make 2023-01-11 08:43:14 +01:00
Pierre Roux
cc1d830b2a
coq_8_17: init at 8.17+rc1 (#209145) 2023-01-06 15:51:50 +01:00
Théo Zimmermann
d76cdd7b8b
coqPackages.Verdi: preemptive fix for removal of configure in future versions 2022-12-24 17:19:51 +01:00
Théo Zimmermann
365f7f342f
coqPackages.StructTact: preemptive fix for removal of configure in future versions 2022-12-24 17:19:46 +01:00
Théo Zimmermann
6bd604b37c
coqPackages.InfSeqExt: preemptive fix for removal of configure in future versions 2022-12-24 17:19:25 +01:00
Théo Zimmermann
f061c452a6
coqPackages.Cheerios: preemptive fix for removal of configure in future versions 2022-12-24 17:19:04 +01:00
Vincent Laporte
13e0b430e8 coqPackages.VST: 2.10 → 2.11.1 2022-12-22 07:34:58 +01:00
Vincent Laporte
da52ce18b6 coqPackages.VST: add support for Coq 8.16.1 2022-12-05 09:22:59 +01:00
Vincent Laporte
3eb6874bda compcert: add support for Coq 8.16.1 2022-12-05 09:22:59 +01:00
Cyril Cohen
7e5e6625e2 Update HoTT and drop archaic 8.6 specific install 2022-11-29 12:57:11 +01:00
Cyril Cohen
e31777a12c coqPackages.mathcomp-algebra-tactics: init at 1.0.0 2022-11-24 20:41:35 +01:00
Vincent Laporte
6921841682 coqPackages.interval: 4.5.2 → 4.6.0 2022-11-13 15:08:46 +01:00
Martin Weinelt
c728598b84 Merge remote-tracking branch 'origin/staging-next' into staging 2022-10-13 23:29:04 +02:00
Vincent Laporte
5b8ac1bbdc coqPackages.relation-algebra: init at 1.7.8 for Coq 8.16 2022-10-13 21:53:46 +02:00
Vladimír Čunát
00a757ed3f
Merge branch 'master' into staging 2022-10-13 08:27:55 +02:00
Artturi
e66d2fd89d
Merge pull request #194256 from Artturin/treewides2 2022-10-13 00:08:01 +03:00
Vincent Laporte
d451ea73dc coqPackages.coq-elpi: disable OCaml warnings 2022-10-12 20:38:44 +02:00
Pierre Roux
c8aa298134 Adding mathcomp-analysis single 2022-10-11 11:46:46 +02:00
Vincent Laporte
4912687343 coqPackages.VST: enable for Coq 8.16 2022-10-11 07:49:52 +02:00
Vincent Laporte
a861c34a3e coqPackages.compcert: enable for Coq 8.16 2022-10-11 07:49:52 +02:00
Artturin
f4ea1208ec treewide: *Flags convert to list from str
*Flags implies a list

slightly relevant:
> stdenv: start deprecating non-list configureFlags https://github.com/NixOS/nixpkgs/pull/173172

the makeInstalledTests function in `nixos/tests/installed-tests/default.nix` isn't available outside of nixpkgs so
it's not a breaking change
2022-10-10 15:30:59 +03:00
Vincent Laporte
f45bd811fc coqPackages.simple-io: fix & add tests 2022-10-07 07:54:31 +02:00
John Wiegley
a3d3f80c5a
Merge pull request #194539 from vbgl/coq-category-theory-1.0.0 2022-10-05 11:11:03 -04:00
Vincent Laporte
a2c917865f coqPackages.mathcomp-word: 1.1 → 2.0 2022-10-05 13:38:03 +02:00
Vincent Laporte
4076104a38
coqPackages.category-theory: 20211213 → 1.0.0 2022-10-05 06:44:37 +02: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
Cyril Cohen
9ff8c7fd8c coqPackages.hierarchy-builder: 1.3.0 -> 1.4.0 2022-09-29 14:46:20 +02:00
Vincent Laporte
ff346a442d
Merge pull request #192437 from kyoDralliam/metacoq-fix-dev
fix metacoq builds for coq >= 8.16 in dev mode, adds 1.1 release for coq 8.16
2022-09-27 13:39:10 +02:00
Kenji Maillard
fb3c48614f Add metacoq 1.1 release 2022-09-27 11:08:04 +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
Vincent Laporte
60f34d3919 coqPackages.serapi: init at 8.16.0+0.16.0 for Coq 8.16 2022-09-25 18:17:15 +02:00
Kenji Maillard
0ba507689d fix dev metacoq builds for coq >= 8.16 2022-09-22 16:00:43 +02:00
Matthieu Sozeau
3604bfdf5b Support dev version of equations 2022-09-22 14:14:06 +02:00
Vincent Laporte
c5bfd9b4d1 coqPackages.QuickChick: 1.6.2 → 1.6.4 2022-09-20 04:26:37 +02:00
Vincent Laporte
e2abc215de coqPackages.corn: 8.13.0 → 8.16.0 2022-09-19 13:05:52 +02:00
Vincent Laporte
8f87e38995 coqPackages.interval: 4.5.1 → 4.5.2 2022-09-18 16:12:19 +02:00
Théo Zimmermann
5d1ddac949
Merge pull request #183106 from kyoDralliam/metacoq-1.0-8.16
Add the release 1.0 of metacoq for coq 8.16
2022-09-14 18:32:15 +02:00
Vincent Laporte
3a1bec8917
coqPackages.gappalib: 1.5.1 → 1.5.2 2022-09-10 14:29:01 +02:00
Vincent Laporte
9c0b43603a
coqPackages.Verdi: enable for Coq 8.16 2022-09-08 18:07:09 +02:00
Vincent Laporte
0b1099dc6d
coqPackages.aac-tactics: init at 8.16.0 2022-09-08 18:07:02 +02:00
Vincent Laporte
726422b4fe
coqPackages.addition-chains: enable for Coq 8.16 2022-09-08 18:07:00 +02:00
Vincent Laporte
18aa936e06
coqPackages.autosubst: enable for Coq 8.16 2022-09-08 18:06:57 +02:00
Vincent Laporte
0f25d8a02d
coqPackages.coq-bits: enable for Coq 8.16 2022-09-08 18:06:55 +02:00
Vincent Laporte
6791c185dd
coqPackages.coqeal: enable for Coq 8.16 2022-09-08 18:06:52 +02:00