Vincent Laporte
8d4d822bc0
coqPackages.extructures: enable for Coq 8.17
2023-06-01 05:57:58 +02:00
Vincent Laporte
cba7a1095d
coqPackages.deriving: 0.1.0 → 0.1.1
2023-06-01 05:57:58 +02:00
Vincent Laporte
4a6b131836
coqPackages.corn: enable for Coq 8.17
2023-05-31 11:46:24 +02:00
Vincent Laporte
810f901a4e
coqPackages.math-classes: 8.15.0 → 8.17.0
2023-05-31 11:46:24 +02:00
Vincent Laporte
217bf86dc0
coqPackages.aac-tactics: init at 8.17.0
2023-05-24 10:18:43 +02:00
Vincent Laporte
499cad7a72
Merge pull request #230891 from proux01/update-mathcomp-1.17.0
...
Mathcomp 1.16.0 -> 1.17.0
2023-05-23 17:52:15 +02:00
Vincent Laporte
bec9f57aa5
coqPackages.CoLoR: 1.8.2 → 1.8.3
2023-05-23 12:29:31 +02:00
Vincent Laporte
a68600dc25
coqPackages.coqprime: 8.15 → 8.17
2023-05-22 08:42:07 +02:00
Vincent Laporte
47c722bd77
coqPackages_8_17.dpdgraph: init at 1.0+8.17
2023-05-22 06:40:31 +02:00
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
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
Vincent Laporte
e8598c7982
coqPackages.extructures: enable for Coq 8.16
2022-09-08 18:06:47 +02:00
Vincent Laporte
0e6ea7d975
coqPackages.deriving: enable for Coq 8.16
2022-09-08 18:06:44 +02:00
Vincent Laporte
bdc09cc2e1
coqPackages.gaia-hydras: enable for Coq 8.16
2022-09-08 18:06:41 +02:00
Vincent Laporte
ac447c9772
coqPackages.goedel: enable for Coq 8.16
2022-09-08 18:06:37 +02:00
Vincent Laporte
9ad12d1d8c
coqPackages.graph-theory: enable for Coq 8.16
2022-09-08 18:06:35 +02:00
Vincent Laporte
1b0eaf4d3a
coqPackages.itauto: init at 8.16.0
2022-09-08 18:06:32 +02:00
Vincent Laporte
d8318a75d5
coqPackages.coquelicot: enable for Coq 8.16
2022-09-08 18:06:29 +02:00
Vincent Laporte
215ba1b3d3
coqPackages.mathcomp-tarjan: enable for Coq 8.16
2022-09-08 18:06:26 +02:00
Vincent Laporte
2611f23722
coqPackages.mathcomp-word: enable for Coq 8.16
2022-09-08 18:06:24 +02:00
Vincent Laporte
4bdd2be574
coqPackages.mathcomp-zify: enable for Coq 8.16
2022-09-08 18:06:21 +02:00
Vincent Laporte
3359e6ba27
coqPackages.reglang: enable for Coq 8.16
2022-09-08 18:06:18 +02:00
Vincent Laporte
557f5ee714
coqPackages.trakt: enable for Coq 8.16
2022-09-08 18:05:52 +02:00
Enrico Tassi
e50697278b
mathcomp: 1.14.0 -> 1.15.0
2022-08-31 19:00:56 +02:00
Vincent Laporte
fcfa7a704a
coqPackages.mathcomp-analysis: 0.3.13 → 0.5.3
2022-08-31 09:29:48 +02:00
Vincent Laporte
0079deac1f
coqPackages.stdpp: 1.7.0 → 1.8.0
...
coqPackages.iris: 3.6.0 → 4.0.0
2022-08-27 08:54:26 +02:00
Vincent Laporte
e54bfd3ed3
coqPackages.coq-record-update: 0.3.0 → 0.3.1
2022-08-18 10:50:56 +02:00
Vincent Laporte
ab223b256d
coqPackages.coq-ext-lib: 0.11.6 → 0.11.7
2022-08-17 14:44:05 +02:00
Vincent Laporte
91706b1a3f
coqPackages_8_13.smtcoq: build cvc4 with gcc10
2022-08-02 21:50:58 +02:00
Vincent Laporte
454617cad6
coqPackages_8_16.dpdgraph: init at 1.0+8.16
2022-07-28 09:00:29 +02:00
Kenji Maillard
a1b40785e4
add the release 1.0 of metacoq for coq 8.16
2022-07-27 16:06:38 +02:00
Vincent Laporte
0ab119a6cf
coqPackages.mathcomp-abel: 1.2.0 → 1.2.1
2022-07-26 16:32:49 +02:00
Vincent Laporte
da15d8f43e
coqPackages.hierarchy-builder: enable for Coq 8.16
2022-07-26 16:32:49 +02:00
Vincent Laporte
097b07f427
coqPackages.hydra-battles: enable for Coq 8.16
2022-07-25 16:28:59 +02:00
Vincent Laporte
81a0991e2d
coqPackages_8_16.equations: init at 1.3+8.16
2022-07-25 16:28:59 +02:00
Kenji Maillard
b9da0d3852
first release of Metacoq
2022-07-20 16:52:11 +02:00
Ben Siraphob
239f2a4be4
Merge pull request #181910 from vbgl/coq-fourcolor-1.2.5
...
coqPackages.fourcolor: 1.2.4 → 1.2.5
2022-07-20 06:46:50 -07:00
Aaron L. Zeng
50d9adfa8a
Fix coqPackages.serapi version 8.15 for ocamlPackages.janeStreet version 0.15
...
This is a follow-up to #166033 adding a patch for coqPackages.serapi
so that it builds successfully with the new Jane Street OCaml
packages. I did not upstream this patch because
upstream (coq-serapi-v8.16) already includes commits mentioning Jane
Street 0.15 compatibility with a similar patch.
2022-07-20 06:56:35 +02:00
Pierre Roux
c8585bf4a8
coqPackages.coq-elpi 1.14.0 -> 1.15.1
2022-07-19 13:03:25 +02:00
Vincent Laporte
fa3c3c1a33
coqPackages.flocq: 3.4.3 → 4.1.0
...
compcert: 3.10 → 3.11
coqPackages.VST: 2.9 → 2.10
2022-07-19 06:52:13 +02:00
Vincent Laporte
f201cf5f78
coqPackages.fourcolor: 1.2.4 → 1.2.5
2022-07-17 21:04:43 +02:00
Vincent Laporte
773140e96d
coqPackages.mathcomp-finmap: 1.5.1 → 1.5.2
2022-07-17 08:06:19 +02:00
Ben Siraphob
68c9333eb4
Merge pull request #176321 from siraben/smtcoq-fix
2022-07-16 09:27:57 -07:00
Vincent Laporte
f2dba019c6
coqPackages.gaia: 1.13 → 1.14
2022-07-16 14:06:14 +02:00
Vincent Laporte
2d123c3c4b
coqPackages.coqeal: 1.1.0 → 1.1.1
2022-07-13 09:20:44 +02:00
Théo Zimmermann
3ea8ed7d7e
Split out CoqIDE by default when Coq >= 8.14.
2022-07-10 15:49:44 +02:00
Théo Zimmermann
0898779c39
Do not rely on coq-version when coq.version works just fine.
2022-07-08 14:33:24 +02:00
Vincent Laporte
23127e71da
coqPackages_8_16.paramcoq: init at 1.1.3+coq8.16
2022-06-23 09:23:06 +02:00
Vincent Laporte
af888339b6
mkCoqDerivation: do not set DESTDIR
...
Fixes #178109
2022-06-18 11:54:21 +02:00
Vincent Laporte
61d8986385
coqPackages.{hierarchy-builder,trakt}: disable for Coq ≥ 8.16
...
They depend on elpi (not yet available in nixpkgs)
2022-06-13 11:29:20 +02:00
Vincent Laporte
10f159ffd1
coqPackages.mathcomp: disable for Coq ≥ 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
476cb5b0c7
coqPackages.simple-io: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
31648f5f8e
coqPackages.StructTact: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
bd84a72970
coqPackages.coqprime: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
e488c3e834
coqPackages.coq-record-update: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
7d14828292
coqPackages.LibHyps: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
e09c29e9e6
coqPackages.ITree: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
8bdc101414
coqPackages.math-classes: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
577c99884d
coqPackages.metalib: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
80fd9ab13e
coqPackages.parsec: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
b03dc538a3
coqPackages.semantics: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
082dc9aba9
coqPackages.iris: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
591f280978
coqPackages.stdpp: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
ecb1e2a99b
coqPackages.CoLoR: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
a8392b2ee4
coqPackages.tlc: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
b8e366f1a4
coqPackages.paco: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Vincent Laporte
3d80ca27c0
coqPackages.coq-ext-lib: enable for Coq 8.16
2022-06-13 11:29:20 +02:00
Pierre Roux
ecf2791d8b
coq_8_16: init at 8.16+rc1
2022-06-08 18:42:10 +02:00
Vincent Laporte
66a532257d
coqPackages.coq-elpi: 1.13.0 → 1.14.0
2022-06-08 09:46:41 +02:00
Ben Siraphob
3de12b0987
smtcoq: fix cvc4 dependency
2022-06-06 00:03:11 -07:00
Ben Siraphob
91dde6efd2
coqPackages.smtcoq: itp22 -> 2021-09-17
2022-06-05 23:22:07 -07:00
Vincent Laporte
73812431fb
compcert: add support for Coq 8.15.2
2022-06-03 10:45:45 +02:00
Vincent Laporte
595e59d4b0
coqPackages.VST: fix build with Coq 8.15.2
2022-06-03 10:45:45 +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
Ben Siraphob
f150888da6
coqPackages.interval: 4.4.0 -> 4.5.1
2022-05-16 22:37:13 +02:00
Vincent Laporte
1f11888116
Revert "coqPackages: etc"
...
This reverts commit 7e589a45ef
.
2022-05-13 06:47:14 +02:00
Vincent Laporte
215235cce5
Revert "moving findlib to propagedNativeBuildInputs"
...
This reverts commit 82440c9374
.
2022-05-13 06:47:14 +02:00
Cyril Cohen
82440c9374
moving findlib to propagedNativeBuildInputs
2022-05-12 06:11:43 +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
38dc75293d
coqPackages.mathcomp-tarjan: enable with Coq 8.15
2022-05-07 07:29:45 +02:00
Vincent Laporte
a1cb58e4cf
coqPackages.semantics: enable with Coq 8.15
2022-05-07 07:29:42 +02:00
Vincent Laporte
7711b57784
coqPackages.smpl: init at 8.14 & 8.15
2022-05-07 07:29:39 +02:00
Vincent Laporte
e34f56ce98
coqPackages.itauto: init at 8.14.0 & 8.15.0
2022-05-07 07:29:36 +02:00
Vincent Laporte
f393892bb3
coqPackages.smtcoq: disable for Coq > 8.13
2022-05-07 07:29:33 +02:00
Vincent Laporte
e9d3fe8f28
coqPackages.goedel: enable with Coq 8.15
2022-05-07 07:29:30 +02:00
Vincent Laporte
4847e4382c
coqPackages.category-theory: enable with Coq 8.15
2022-05-07 07:29:25 +02:00
Vincent Laporte
d317484de1
coqPackages.graph-theory: enable for Coq 8.15
2022-05-07 07:29:18 +02:00
Vincent Laporte
94c97dfa94
coqPackages.QuickChick: 1.5.0 → 1.6.2
2022-05-07 07:20:43 +02:00
Kenji Maillard
86a6908045
coqPackages.metacoq: create package ( #162639 )
2022-05-03 09:26:34 +02:00
Vladimír Čunát
c480cc2895
Merge branch 'master' into staging-next-2022-04-23
2022-04-30 23:02:28 +02:00
Vincent Laporte
10b2632716
coqPackages.simple-io: 1.3.0 → 1.7.0
2022-04-29 20:59:11 +02:00
Vincent Laporte
95261182f0
coqPackages.parsec: 0.1.0 → 0.1.1
2022-04-29 07:11:26 +02:00
Vincent Laporte
52dfc053d0
coqPackages.tlc: 20210316 → 20211215
2022-04-28 20:56:01 +02:00
Vladimír Čunát
51554cbbdb
Merge branch 'master' into staging-next-2022-04-23
2022-04-27 22:50:17 +02:00
Vincent Laporte
a231ab1096
coqPackages.coqtail-math: 20201124 → 8.14
2022-04-27 19:15:35 +02:00
Vincent Laporte
5e718d7071
coqPackages.metalib: clean & init at 8.15
2022-04-27 11:36:20 +02:00
github-actions[bot]
e7703dd154
Merge master into staging-next
2022-04-26 12:04:22 +00:00
Vincent Laporte
68322e1297
coqPackages.mathcomp-word: 1.0 → 1.1
2022-04-26 13:11:29 +02:00
Artturi
785373a76f
Merge pull request #166605 from siraben/remove-redundant-stdenv
2022-04-22 20:25:38 +03:00
Vincent Laporte
834faa24b4
coqPackages.Verdi: 20210524 → 20211026
2022-04-19 21:35:05 +02:00
Ben Siraphob
259fa13d53
treewide: remove nativeBuildInputs that are in stdenv
2022-04-16 21:46:46 +03:00
Ben Siraphob
a1244414d5
coqPackages.smtcoq: init at itp22
2022-04-13 19:38:01 -05:00
Ben Siraphob
8566253746
coqPackages.trakt: init at 1.0
2022-04-13 19:38:00 -05:00
Vincent Laporte
72f3b1a4d1
coqPackages.CoLoR: 1.8.1 → 1.8.2
2022-04-12 18:57:15 +02:00
Vincent Laporte
ffe759bb5b
coqPackages.gappalib: 1.5.0 → 1.5.1
2022-04-11 21:07:00 +02:00
Ben Siraphob
e121b4b732
Merge pull request #167193 from vbgl/coq-coqprime-8.15
2022-04-04 17:36:54 -05:00
Vincent Laporte
1ea4550773
coqPackages.coqprime: 8.14.1 → 8.15
2022-04-04 17:08:31 +02:00
Vincent Laporte
bee11786f6
coqPackages.relation-algebra: 1.7.6, 1.7.7
2022-04-04 11:24:27 +02:00
Vincent Laporte
ff32bb3cf2
coqPackages.aac-tactics: 8.13.2, 8.14.1, 8.15.1
2022-04-04 11:21:01 +02:00
Vincent Laporte
ff83e827b5
coqPackages.VST: fix build with Coq 8.15.1
2022-03-24 10:17:42 +01:00
Vincent Laporte
9e4d58db80
compcert: add support for Coq 8.15.1
2022-03-24 10:17:42 +01: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
Vincent Laporte
3b50449992
coqPackages.iris: 3.5.0 → 3.6.0
...
coqPackages.stdpp: 1.6.0 → 1.7.0
2022-02-23 21:14:14 +01:00
Vincent Laporte
df5c6e08b8
coqPackages_8_15.coqhammer: enable at 1.3.2
2022-02-23 09:04:09 +01:00
Théo Zimmermann
61ac416992
coqPackages.hydra-battles: fix version checking logic
...
With this change, the derivation can be relied on without overlay in the upstream project.
2022-02-21 16:20:04 +01:00
Théo Zimmermann
450eab2ca7
coqPackages_8_14.gaia-hydras: 0.5 -> 0.6
2022-02-20 14:32:30 +01:00
Théo Zimmermann
8208c3eec8
coqPackages.addition-chains: 0.5 -> 0.6
2022-02-20 14:32:30 +01:00
Théo Zimmermann
d0bb08b5cc
coqPackages.hydra-battles: 0.5 -> 0.6
2022-02-20 14:32:30 +01:00
Théo Zimmermann
7fa2a7232d
coqPackages.LibHyps: init at 2.0.4.1
2022-02-20 14:14:40 +01:00
Enrico Tassi
15d1c96f91
coq-elpi: 1.12.1 -> 1.13.0
2022-02-16 17:57:06 +01:00
Vincent Laporte
6d5e3764dd
coqPackages.VST: 2.8 → 2.9
2022-02-16 08:03:02 +01:00
Vincent Laporte
dd09b52700
coqPackages.ITree: enable for Coq 8.15
2022-02-16 08:03:02 +01:00