Pierre Roux
ed1f52d4c2
Mathcomp 1.16.0 -> 1.17.0
2023-05-17 16:26:09 +02:00
Pierre Roux
52c9e5c8f9
coqPackages.coqeal: 1.1.1 -> 1.1.3
2023-05-17 16:24:06 +02:00
Pierre Roux
7a3bc4f18f
coqPackages.multinomials: 1.5.6 -> 1.6.0
2023-05-17 16:24:06 +02:00
Pierre Roux
e5264e45b7
coqPackages.coquelicot: 3.3.0 -> 3.3.1
2023-05-17 16:24:06 +02:00
Pierre Roux
a0ca431141
Add coqPackages.mathcomp 2.0.0
2023-05-15 11:26:42 +02:00
affeldt-aist
8a92dd9a9a
mathcomp-infotheo: init at 0.5.1 ( #231077 )
2023-05-11 23:09:28 +02:00
Vincent Laporte
0697e32ae1
coqPackages_8_17: enable a few packages for Coq 8.17
2023-04-13 14:23:14 +02:00
Pierre Roux
6302147d48
coqPackages.mathcomp-algebra-tactics 1.0.0 -> 1.1.1
2023-04-13 14:21:59 +02:00
Ali Caglayan
6462ef85d8
coqPackages.coq-lsp: 0.1.6.1 for Coq 8.17
...
Signed-off-by: Ali Caglayan <alizter@gmail.com>
2023-04-04 13:23:51 +02:00
Ali Caglayan
21131995d9
coqPackages.serapi: 8.16.0+0.16.3 -> 8.17.0+0.17.0
...
Signed-off-by: Ali Caglayan <alizter@gmail.com>
2023-04-04 13:23:51 +02:00
Ali Caglayan
463643afa8
coqPackages.HoTT: 8.16 -> 8.17
...
We bump the HoTT library to 8.17 and switch to using Dune for the
build.
I attempted to include the 8.10 - 8.13 builds but I couldn't get
autoconf to work the way I wanted so I gave up in the end.
Signed-off-by: Ali Caglayan <alizter@gmail.com>
2023-03-30 20:05:15 +02:00
Pierre Roux
25c631cc0e
Add coqPackages.mathcomp-apery
2023-03-30 13:55:40 +02:00
Cyril Cohen
a601e65967
coqPackages_8_17.stdpp: init at 1.8.0
2023-03-27 16:56:32 +02:00
Vincent Laporte
9d8a066fd4
coqPackages.ITree: 4.0.0 → 5.1.0
2023-03-15 09:14:01 +01:00
Vincent Laporte
265f0cae75
coqPackages.paco: enable for Coq 8.17
2023-03-15 09:14:01 +01:00
Vincent Laporte
73bc86dc9c
coqPackages.coq-ext-lib: enable for Coq 8.17
2023-03-15 09:14:01 +01:00
Pierre Roux
2959062362
coqPackages: various 8.16 -> 8.17
2023-03-09 13:13:00 +01:00
Vincent Laporte
d8cc4e215d
coqPackages.mathcomp-analysis: 0.6.0 → 0.6.1
2023-03-03 21:17:02 +00:00
Vincent Laporte
c81f6065c5
coqPackages.mathcomp-analysis: 0.5.3 → 0.6.0
2023-03-03 21:17:02 +00:00
Vincent Laporte
1662bbb5fb
coqPackages.smtcoq.cvc4: fix build with bash 5.2
...
See: 4d85cedf5a
2023-03-01 10:02:09 +00:00
Vincent Laporte
82d2212d29
compcert: 3.11 → 3.12
2023-03-01 09:45:31 +00:00
Vincent Laporte
0cad0fd119
coqPackages.coq-elpi: propagate findlib
2023-02-28 10:59:42 +00:00
Vincent Laporte
a18a7e5ff8
coqPackages.coqhammer: fix src URL
2023-02-28 10:59:42 +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
Mario Rodas
46f9a706c9
coqPackages_8_16.serapi: 8.16.0+0.16.0 -> 8.16.0+0.16.3
2023-02-21 04:20:00 +00:00
Ulrik Strid
376e9ceead
treewide: add strictDeps = true to most packages depending on ocaml
2023-02-03 08:59:34 +01:00
Nick Cao
37878b459d
Merge pull request #213855 from vbgl/coq-coquelicot-3.3
...
coqPackages.coquelicot: 3.2.0 → 3.3.0
2023-02-03 10:49:30 +08:00
Vincent Laporte
4664292ca1
coqPackages_8_17.paramcoq: init at 1.1.3+coq8.17
2023-02-02 08:12:32 +01:00
Vincent Laporte
5aa7222940
coqPackages_8_17.equations: init at 1.3+8.17
2023-02-01 07:41:17 +01:00
Vincent Laporte
d8fbdbc0c4
coqPackages.coquelicot: 3.2.0 → 3.3.0
2023-01-31 21:25:44 +01:00
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