mirrors/nixpkgs
1
0
Fork 1
mirror of https://github.com/NixOS/nixpkgs.git synced 2024-11-18 19:51:17 +00:00
Code Issues Wiki Activity
664484 commits 271 branches 124 tags 6.1 GiB
Commit graph

852 commits

Author SHA1 Message Date
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
Vincent Laporte c845a272a5 coqPackages.compcert: enable for Coq 8.15 
and make version 3.9 the default for Coq 8.12
 2022-02-16 08:03:02 +01:00
Vincent Laporte 8199da6293
coqPackages_8_15.dpdgraph: init at 1.0+8.15 2022-02-06 12:16:43 +01:00
Pierre Roux ced4ffe645 Add odd-order 1.13.0 2022-02-02 08:56:55 +01:00
Pierre Roux 2768c9d4cb Adapt to Coq 8.15 and MathCOmp 1.14 2022-02-02 08:56:55 +01:00
Pierre Roux 7846d0278e mathcomp-abel compiles with Coq 8.15 2022-02-02 08:56:55 +01:00
Cyril Cohen dffe2434ae coqPackages.mathcomp: 1.13.0 -> 1.14.0 2022-02-02 08:56:55 +01:00
Théo Zimmermann 51d92e5c6e coqPackages_8_15.paramcoq: init at 1.1.3+coq8.15 2022-01-27 08:49:00 +01:00
Théo Zimmermann 4632498895 coqPackages.gaia: mark as compatible with Coq 8.15 2022-01-27 08:49:00 +01:00
Théo Zimmermann 247cc00c9e coqPackages.mathcomp-zify: mark as compatible with Coq 8.15 2022-01-27 08:49:00 +01:00
Théo Zimmermann eb1b39787f coqPackages_8_15.serapi: init at 8.15.0+0.15.0 
And also clean up rc version for Coq 8.15.
 2022-01-27 08:11:31 +01:00
José Romildo Malaquias a01cad0d0f
ocamlPackages.ppx_import: 1.8.0 -> 1.9.1 (#156399) 
* ocamlPackages.ppx_import: 1.8.0 -> 1.9.1

* coqPackages.serapi: fix compilation with ppx_import-1.9.1
 2022-01-26 13:16:24 +01:00
Théo Zimmermann 7e149abe9d coqPackages.reglang: mark as compatible with Coq 8.15 2022-01-25 15:24:08 +01:00
Théo Zimmermann 4b7398fe10 coqPackages_8_15.equations: init at 1.3+8.15 2022-01-25 15:24:08 +01:00
Théo Zimmermann f18e742079 coqPackages.deriving: mark as compatible with Coq 8.15 2022-01-25 15:24:08 +01:00
Théo Zimmermann ec85449f80 coqPackages.coq-record-update: mark as compatible with Coq 8.15 2022-01-25 15:24:08 +01:00
Théo Zimmermann e290bc12f7 coqPackages.coq-ext-lib: 0.11.4 -> 0.11.6 
Compatibility with Coq 8.15.
 2022-01-25 15:24:08 +01:00
Théo Zimmermann 075b606ef9 coqPackages.corn: mark as compatible with Coq 8.15 2022-01-25 12:59:07 +01:00
Théo Zimmermann e40a892f11 coqPackages.math-classes: 8.13.0 -> 8.15.0 
Compatibility with Coq 8.15.
 2022-01-25 12:59:07 +01:00
Ben Siraphob 28d7cd8c46
coqPackages.CoLoR: update homepage 2022-01-07 16:45:54 +07:00
Ben Siraphob fc8e7c963d
coqPackages.semantics: add 8.14.0 2021-12-29 21:21:02 +07:00
Vincent Laporte e99619604d coqPackages.mathcomp-word: init at 1.0 2021-12-24 11:59:00 +01:00
Vincent Laporte a2aaaee3d9 coqPackages.ITree: enable for Coq 8.14 2021-12-22 19:10:10 +01:00
Vincent Laporte 3f4f5ee591 coqPackages.paco: 4.1.1 → 4.1.2 2021-12-22 19:10:10 +01:00
Bobby Rong 281e50cad8
Merge pull request #147386 from ineol/update-coq-paco 
coqPackages.paco: 4.0.2 -> 4.1.1
 2021-12-17 15:13:26 +08:00
John Wiegley 11f5352bbe
coqPackages.category-theory: Set highest compatibility to coq 8.14 (#150559) 
* coqPackages.category-theory: Set highest compatibility to coq 8.14

* coqPackages.category-theory: 20210730 → 20211213

Co-authored-by: Vincent Laporte <Vincent.Laporte@gmail.com>
 2021-12-16 10:00:31 +01:00
Vincent Laporte 9ec8e46141
coqPackages.serapi: init at 8.14.0+0.14.0 for Coq 8.14 & OCaml < 4.12 (#148775) 2021-12-12 20:41:49 +01:00
Vincent Laporte a2b044154f coqPackages.iris: disable for Coq 8.15 2021-12-09 15:46:06 +01:00
Vincent Laporte 5401acff06 coqPackages.stdpp: disable for Coq 8.15 2021-12-09 15:46:06 +01:00
Vincent Laporte 69bba1dc67 coqPackages.interval: disable for Coq 8.15 2021-12-09 15:46:06 +01:00
Vincent Laporte b62ea74e97 coqPackages.graph-theory: disable for Coq 8.15 2021-12-09 15:46:06 +01:00
Vincent Laporte a73d01cf07 coqPackages.gappalib: disable for Coq 8.15 2021-12-09 15:46:06 +01:00
Vincent Laporte edd5950d12 coqPackages.coqeal: disable for Coq 8.15 2021-12-09 15:46:06 +01:00
Vincent Laporte a0240d5415 coqPackages.bignums: enable for Coq 8.15 2021-12-09 15:46:06 +01:00
Vincent Laporte 2b51eb99d2 coqPackages.StructTac: enable for Coq 8.15 2021-12-09 15:46:06 +01:00
Vincent Laporte f5ca72dcf3
coqPackages.mathcomp-bigenough: 1.0.0 → 1.0.1 2021-12-08 13:37:58 +01:00
Vincent Laporte 2db21cf063 coqPackages.equations: 1.2.4 → 1.3 (for Coq 8.13) 2021-12-03 12:54:58 +01:00
Vincent Laporte d24027a684 coqPackages.coqprime: 8.12 → 8.14.1 2021-12-02 13:16:44 +01:00
Vincent Laporte 3b1c4a732f compcert: fix for Coq 8.14.1 2021-12-01 15:43:53 +01:00
Vincent Laporte 4f51fae5bb coqPackages.serapi: remove with Coq 8.14 2021-12-01 13:46:15 +01:00
Vincent Laporte 041de05c3d coqPackages.coqhammer: 1.3.1 → 1.3.2 2021-11-29 10:33:36 +01:00
Vincent Laporte 5b861824b3 compcert: 3.9 → 3.10 
Enable for Coq 8.14

Use default version of OCaml (instead of 4.05)

VST is not ready for CompCert 3.10, so it still uses 3.9
 2021-11-29 08:45:34 +01:00
Léo Stefanesco f127992f86 coqPackages.paco: 4.0.2 -> 4.1.1 2021-11-25 18:48:21 +01:00
Léo Stefanesco 7c52900af1 coqPackages.coq-record-update: init 2021-11-25 17:20:16 +00:00
Valentin Robert 30c56e2e10 coq-bits: 1.0.0 -> 1.1.0 2021-11-16 13:43:32 -08:00
Ben Siraphob d4ca3899e9
Merge pull request #145711 from siraben/coq-smpl-init 
coqPackages.smpl: init
 2021-11-15 19:49:58 -06:00
Léo Stefanesco 58bdfc529b iris: 3.4.0 -> 3.5.0; stdpp: 1.5.0 -> 1.6.0 2021-11-14 15:26:37 +01:00
Vincent Laporte 3e84e0fd7d coqPackages.graph-theory: enable for Coq 8.14 2021-11-13 13:17:20 +01:00
Ben Siraphob c513f1ed91
coqPackages.smpl: init 2021-11-12 22:22:35 -06:00
xaverdh 03a257e5a3
treewide: quote urls according to rfc 0045 (#145260) 
Co-authored-by: Sandro <sandro.jaeckel@gmail.com>
 2021-11-10 11:37:56 +01:00
Pierre Roux aeb8fae646 coqPackages.coqeal: 1.0.6 -> 1.1.0 2021-11-05 14:37:53 +01:00
Pierre Roux 3e66c4013f coqPackages.coqeal: master, add dependency 
In order to include matrix normal forms in
CoqEAL (https://github.com/coq-community/coqeal/pull/54)
we add a dependency to mathcomp-real-closed.
 2021-11-02 11:36:09 +01:00
Vincent Laporte a2445c740e coqPackages.dpdgraph: 0.6.9 → 1.0 2021-10-31 07:06:14 +01:00
Ben Siraphob 054bac1eca
Merge pull request #143793 from CohenCyril/fixHB-coq8.12 
coqPackages.hierarchy-builder: etc
 2021-10-30 14:01:19 -05:00
Ben Siraphob dbe6b53a93
Merge pull request #142072 from Zimmi48/fix-zorns-lemma-before-9.0 
Fix zorns-lemma before 9.0.
 2021-10-30 11:44:46 -05:00
Cyril Cohen 314e64e467 coqPackages.hierarchy-builder: etc 2021-10-30 05:30:44 +02:00
Cyril Cohen c5c34f6be1 coqPackages.mathcomp: 1.12.0 -> 1.13.0 2021-10-29 21:05:07 +02:00
Cyril Cohen b46055e928 coqPackages.coq-elpi: 1.10 -> 1.11 2021-10-27 13:19:57 +02:00
Vincent Laporte c7671c1853 coqPackages.paramcoq: 1.1.2 → 1.1.3 (for Coq 8.10–8.12) 2021-10-21 13:29:12 +02:00
Théo Zimmermann 170128a5a7 coqPackages.serapi: patch to fix COQPATH issue 
SerAPI was interpreting paths as relative to the Coq root.
 2021-10-21 11:55:12 +02:00
Vincent Laporte 44745d496c coqPackages.extructures: init at 0.3.0 2021-10-21 10:03:03 +02:00
Vincent Laporte 78085b01ef coqPackages.deriving: init at 0.1.0 2021-10-21 10:03:03 +02:00