John Wiegley
1ba4d23c3a
Revert "coqPackages.fiat_HEAD: Update 2016-10-24 -> 2018-02-27"
...
This reverts commit f5f71c08cd
2018-10-10 10:00:23 -07:00
Matthew Bauer
0421891aaa
Merge pull request #47589 from vbgl/coq-coqprime-init
...
coqPackages.coqprime: init at 8.7.2 & 8.8
2018-10-05 22:33:15 -05:00
John Wiegley
df48060e4c
coqPackages.coq-haskell: Support building with Coq 8.8
2018-10-04 17:13:41 -07:00
Vincent Laporte
c71cc0b98b
coqPackages.coqprime: init at 8.7.2 & 8.8
2018-10-01 10:11:24 +00:00
Janne Heß
9ef77854f7
treewide: Use http/https for homepages
2018-09-08 18:30:00 +02:00
Vladimír Čunát
5b0398dc36
Merge branch 'master' into staging-next
...
Conflicts: gobby and libinfinity - I took the hand-edited versions
instead of those resuting from the mass-replacement.
Hydra: ?compare=1473190
2018-08-13 20:43:59 +02:00
Vincent Laporte
3811efb347
coqPackages.coq-ext-lib: 0.9.5 -> {0.9.7,0.9.8}
2018-08-08 11:24:09 +00:00
John Ericson
db965063b3
treewide: Make configureFlags lists
2018-08-03 17:06:03 -04:00
Peter Simons
6d6522d30d
coqPackages.category-theory: revert "Add equations as a buildInput"
...
This reverts commit 08bf0b7630
2018-07-28 09:16:37 +02:00
John Wiegley
08bf0b7630
coqPackages.category-theory: Add equations as a buildInput
2018-07-27 16:17:09 -07:00
John Wiegley
368cca9f19
coqPackages.category-theory: Update to Git version as of 20180709
2018-07-27 16:11:52 -07:00
volth
52f53c69ce
pkgs/*: remove unreferenced function arguments
2018-07-21 02:48:04 +00:00
Vincent Laporte
3f41f6c5fa
coqPackages.equations: enable for Coq 8.8
2018-07-08 11:13:27 +00:00
John Wiegley
1459b2dffa
coqPackages.equations: Add support for Coq 8.8
2018-07-05 15:17:22 -07:00
Vincent Laporte
44659fcbe1
coqPackages.contribs.aac-tactics: enable for Coq 8.7 and 8.8 ( #41351 )
2018-06-01 19:31:02 +02:00
Vincent Laporte
042790832e
coqPackages.tlc: 20171206 -> 20180316 ( #40927 )
2018-05-22 20:55:57 +02:00
Vincent Laporte
571a1e19e9
coqPackages.iris: init at 3.1.0 ( #40909 )
2018-05-22 19:26:32 +02:00
Vincent Laporte
42462d7b66
coqPackages.stdpp: init at 1.1
2018-05-15 20:55:53 +00:00
Vincent Laporte
1276e82c2e
coqPackages.dpdgraph: init at 0.6.3 for Coq 8.8
2018-05-09 08:03:10 +02:00
Matthew Justin Bauer
738f9a9673
Merge pull request #39469 from vbgl/coq-contribs-containers-8.8
...
coqPackages.contribs.containers: make available for Coq 8.8
2018-05-01 10:21:58 -05:00
Vincent Laporte
b4d0647752
coqPackages.mathcomp: 1.6.4 -> 1.7.0
2018-05-01 11:06:04 +02:00
Vincent Laporte
72ec248eda
coqPackages.contribs.containers: make available for Coq 8.8
2018-04-25 06:27:21 +00:00
Vincent Laporte
f3c8036a70
coqPackages.bignums: make it available for Coq 8.8
2018-03-27 16:19:33 +00:00
John Wiegley
bee172501d
Merge pull request #37591 from vbgl/coq-88beta1
...
coq: init at 8.8+beta1
2018-03-23 22:09:06 -07:00
Vincent Laporte
6845b248d9
coq: init at 8.8+beta1
2018-03-21 18:06:28 +00:00
Vincent Laporte
1ce37ab8a9
coqPackages.contribs.containers: make available for Coq 8.7
2018-03-21 09:27:50 +01:00
John Wiegley
4bd69fd249
coqPackages.bignums: Change expression to match other Coq packages
...
Without this change, it's impossible to override bignums, or ignore it when
creating custom datasets for other versions of Coq (such as 8.8+alpha).
2018-03-06 07:46:51 -08:00
John Wiegley
9186aa1bf8
coqPackages.QuickChick: use fetchFromGitHub
2018-03-06 07:46:51 -08:00
John Wiegley
f5f71c08cd
coqPackages.fiat_HEAD: Update 2016-10-24 -> 2018-02-27
2018-03-05 13:07:16 -08:00
Vincent Laporte
a9d066a990
coqPackages.tlc: init at 20171206
...
TLC is a general purpose Coq library that provides an alternative to Coq's
standard library.
Homepage: http://www.chargueraud.org/softs/tlc/
2017-12-28 08:19:54 +01:00
Vincent Laporte
24474528e4
coqPackages.contribs.containers: fix url
2017-12-22 17:07:25 +00:00
John Wiegley
2134543064
coqPackages.contribs: new set with all packages from coq-contribs
2017-12-21 10:26:56 -08:00
John Wiegley
60a6b81e2d
coqPackages.equations: -> 1.0
2017-12-21 01:06:14 -08:00
Vincent Laporte
fcb89df111
coqPackages.multinomials: init at 1.0
2017-12-18 15:30:38 +00:00
Vincent Laporte
d9f41a5bce
coqPackages: move to a separate file and filter the package set
2017-12-18 15:30:36 +00:00
John Wiegley
8123bc7942
coqPackages.coq-haskell: Update to add Hask.Ssr module
2017-12-15 08:53:49 -08:00
John Wiegley
d1532bc6c6
coqPackages.category-theory: New expression
2017-12-14 23:32:37 -08:00
John Wiegley
0042a343b4
coqPackages.coq-haskell: New expression
2017-12-14 23:32:37 -08:00
John Wiegley
dc6f3e3c7b
coqPackages_8_7.QuickChick: update to latest master
2017-12-12 11:37:17 -08:00
Vincent Laporte
da84fab60b
coqPackages_8_4.contribs: remove
2017-12-02 08:54:19 +00:00
Vincent Laporte
48aa378780
coqPackages_8_4.ynot: remove
2017-12-02 08:53:14 +00:00
Vincent Laporte
e8a316f17f
coqPackages_8_4.unimath: remove
2017-12-02 08:52:38 +00:00
Vincent Laporte
c1efbbab96
coqPackages_8_4.tlc: remove
2017-12-02 08:52:01 +00:00
Vincent Laporte
f6284c76da
coqPackages_8_4.ssreflect: remove
2017-12-02 08:51:36 +00:00
Vincent Laporte
f307634f9d
coqPackages_8_4.QuickChick: remove
2017-12-02 08:51:02 +00:00
Vincent Laporte
5b7e3de309
coqPackages_8_4.mathcomp: remove
2017-12-02 08:49:36 +00:00
Vincent Laporte
00a6d849f8
coqPackages_8_4.interval: remove
2017-12-02 08:48:41 +00:00
Vincent Laporte
5a043e24da
coqPackages_8_4.fiat: remove
2017-12-02 08:46:16 +00:00
Vincent Laporte
13573cf129
coqPackages_8_4.domains: remove
2017-12-02 08:45:14 +00:00
Vincent Laporte
017321a91c
coqPackages_8_4.coquelicot: remove
2017-12-02 08:44:29 +00:00
Vincent Laporte
5add451ee3
coqPackages_8_4.coqeal: remove
2017-12-02 08:42:29 +00:00
Vincent Laporte
7a12b3de44
coqPackages_8_4.coqExtLib: remove
2017-12-02 08:41:40 +00:00
Vincent Laporte
1ada9f8283
coqPackages_8_4.bedrock: remove
2017-12-02 08:40:42 +00:00
Vincent Laporte
d7e84159f8
coqPackages.interval: make bignums optional and propagated
2017-11-13 08:42:52 +00:00
John Wiegley
9ea242c617
coqPackages.interval: Add bignums, now a required dependency
2017-11-12 10:21:56 -08:00
John Wiegley
a41478cebb
coqPackages.CoLoR: 1.3.0 -> 1.4.0, which now supports Coq 8.7
2017-11-12 10:03:32 -08:00
John Wiegley
bb038283c4
coqPackages.metalib: New expression
2017-11-12 09:34:06 -08:00
John Wiegley
7d6d4af1d1
Add missing default.nix for coqPackages.equations
2017-11-12 09:33:40 -08:00
John Wiegley
dcab51c6f4
coqPackages.QuickChick: Update build for Coq 8.6 and 8.7
2017-11-12 09:17:48 -08:00
John Wiegley
f1fc74359f
coqPackages.ssreflect: Build version 0.6.4 for Coq 8.6 and 8.7
2017-11-12 08:50:37 -08:00
John Wiegley
b2418ca598
coqPackages.dpdgraph: Build version 0.6.2 for Coq 8.7
2017-11-12 08:50:36 -08:00
John Wiegley
462b5e0d21
coqPackages.mathcomp: 1.6.1 -> 1.6.4, for Coq versions 8.6 and 8.7
2017-11-11 09:44:55 -08:00
Tim Steinbach
198fd526ca
Revert "coqPackages.{ssreflect,mathcomp}: 1.6.1 -> 1.6.4"
2017-11-07 17:15:09 +00:00
Maxime Dénès
90d33e4eaa
coqPackages.ssreflect: 1.6.1 -> 1.6.4
2017-11-07 13:26:13 +01:00
Maxime Dénès
5a43ac2c60
coqPackages.mathcomp: 1.6.1 -> 1.6.4
2017-11-07 13:26:10 +01:00
Théo Zimmermann
1ddadc6b1c
coqPackages.math-classes: 1.0.6 -> 1.0.7
...
This version introduces compatibility with Coq 8.7.
2017-11-05 16:59:23 +01:00
Théo Zimmermann
f4914d4eb4
bignums: init at various versions
...
Bignums used to be part of the standard library of Coq.
We provide a version for Coq 8.6, and one for Coq 8.7.
2017-11-05 16:59:23 +01:00
Maxime Dénès
51e68732f9
coqPackages.dpdgraph: remove support for coq 8.7
...
coqPackages_8_7.dpdgraph won't build since Coq 8.7.0 is not yet supported
upstream.
2017-10-30 02:02:19 +01:00
John Wiegley
79aa720020
Merge pull request #30708 from maximedenes/fix-quickchick
...
coqPackages.QuickChick: remove support for coq 8.7
2017-10-26 10:18:53 -07:00
Maxime Dénès
41df85dd1b
coqPackages.QuickChick: remove support for coq 8.7
...
coqPackages_8_7.QuickChick won't build since Coq 8.7.0 is not yet supported
upstream.
2017-10-23 22:40:29 +02:00
Vincent Laporte
4ace0daa21
coqPackages.fiat_HEAD: mark as broken with Coq ≥ 8.6
2017-10-22 20:48:18 +00:00
John Wiegley
89720d851a
coqPackages_8_7: New expression, but don't make it the default yet
2017-10-22 12:43:27 -07:00
Vincent Laporte
43ebfb5016
coqPackages.flocq: 2.5.2 -> 2.6.0
2017-10-18 23:21:37 +00:00
Langston Barrett
48a49fc12e
coqPackages.HoTT: init at 20170921
2017-10-11 02:51:16 +02:00
Vladimír Čunát
ef41fc7f51
Merge branch 'master' into staging
...
Hydra: ?compare=1399476
2017-10-07 10:17:42 +02:00
Vincent Laporte
5728b8d4e6
coqPackages.coquelicot: 2.1.2 -> 3.0.1
...
coqPackages.interval: 3.1.1 -> 3.3.0
2017-10-06 21:16:06 +00:00
John Ericson
531e4b80c9
misc pkgs: Basic sed to get fix pkgconfig and autoreconfHook buildInputs
...
Only acts on one-line dependency lists.
2017-09-21 15:49:53 -04:00
Vincent Laporte
ebce795c5c
coqPackages: remove duplication in mkCoqPackages
2017-09-04 02:39:49 +00:00
Vincent Laporte
9b9d3743ce
coqPackages.QuickChick: fix
...
Use the most recent versions of branches coq8.4pl6 and coq8.5-legacy
with the corresponding versions of Coq.
Use a two month old version with Coq-8.6 to avoid issue #45 :
https://github.com/QuickChick/QuickChick/issues/45
2017-09-02 15:33:16 +00:00
Vincent Laporte
6f9d84fe64
coqPackages.interval: fix URL
2017-08-11 16:29:14 +00:00
Vincent Laporte
0f94ac9296
coqPackages.autosubst: fix hash
2017-07-28 06:45:31 +00:00
John Wiegley
0bf019c99a
coqPackages_8_6.CoLoR: Fix installPhase
2017-07-18 20:22:03 -04:00
John Wiegley
006a512e8f
coqPackages_8_6.math-classes: New expression (for 8.6) 1.0.6
2017-07-18 19:12:52 -04:00
John Wiegley
53d1eb0fc6
coqPackages_8_6.CoLoR: new expression 1.3.0
2017-07-18 19:12:51 -04:00
John Wiegley
399dee93ae
coqPackages.autosubst: New expression
2017-07-10 18:35:56 -07:00
John Wiegley
d40dd2c70d
coqPackages.QuickChick: 20170422 -> 20170710
2017-07-10 18:35:56 -07:00
John Wiegley
e78b9a68a0
coqPackages.paco: 1.2.7 -> 1.2.8
2017-07-10 18:35:55 -07:00
rht
31b0e34d1d
Use consistent package naming for HEAD.nix files
2017-05-09 10:31:15 +07:00
John Wiegley
2df7f1b5b5
coq.QuickChick: Update to latest version that works with Coq 8.6
2017-04-23 21:53:21 -07:00
Vincent Laporte
8bfce24045
coqPackages.interval: 2.2.1 -> 3.1.1
2017-02-11 14:02:19 +01:00
Vincent Laporte
dedba2a32d
coqPackages.coquelicot: 2.1.1 -> 2.1.2
...
keeping old 2.1.1 version for Coq-8.4,
as newer versions of the library do not support older Coq versions
2017-02-11 14:02:19 +01:00
Vincent Laporte
5712ac6a72
coqPackages.{ssreflect,mathcomp}: 1.6 -> 1.6.1
2017-02-11 14:02:19 +01:00
Langston Barrett
d486fb053b
coqPackages.math-classes: init at 2016-06-08
2017-01-27 11:16:30 +00:00
Vincent Laporte
42bf99ef44
coqPackages.{ssreflect,mathcomp}: fix build with Coq-8.6
...
by adding `findlib` as a build input.
Also clean `default.nix` a little bit.
2017-01-25 13:06:11 +00:00
Vincent Laporte
f537f842d6
coqPackages.flocq: 2.5.1 -> 2.5.2
2017-01-14 15:53:03 +01:00
Vincent Laporte
7d75dd71dc
coqPackages.coq-ext-lib: 0.9.3 -> 0.9.{4,5}
2017-01-14 15:36:02 +01:00
Vincent Laporte
befc29454b
coqPackages.dpdgraph: 0.5 -> 0.6{,.1}
2017-01-12 21:23:18 +00:00
John Wiegley
4888bfecc2
coq_8_6: 8.6 is now default, 8.4 optional, updated mathcomp/ssreflect
...
Addresses #14829
2016-12-22 10:35:56 -08:00
John Wiegley
a12f3d232d
coqPackages.fiat_HEAD: New package for Coq 8.4pl6 and 8.5pl2
2016-10-31 16:22:04 -07:00
Tuomas Tynkkynen
bac26e08db
Fix lots of fetchgit hashes (fallout from #15469 )
2016-06-03 17:17:08 +03:00
Vincent Laporte
a42f845925
coq-dpdgraph: init at 0.5
2016-05-03 09:27:16 +02:00
Vincent Laporte
618b336808
coq-ext-lib: 0.9.0-beta3 -> 0.9.3
2016-04-12 19:43:49 +02:00
Robin Gloster
9afe794f5e
coqPackages.contribs.Bertrand: fix hash
2016-02-08 10:10:38 +00:00
Tobias Geerinckx-Rice
32d40f0f98
Remove no longer (or never) referenced patches
...
55 files changed, 6041 deletions. Tested with `nix-build -A tarball`.
2016-01-24 02:02:21 +01:00
Vincent Laporte
ca8ef0fa1d
coq-interval: 2.1.0 -> 2.2.1
2016-01-06 09:35:05 +01:00
Vincent Laporte
e182ddf008
coqPackages.coquelicot: init at 2.1.1
...
Coquelicot is a Coq library for Reals.
Homepage: http://coquelicot.saclay.inria.fr/
2016-01-06 09:13:38 +01:00
Vincent Laporte
2027caa875
coq-flocq: 2.5.0 -> 2.5.1
2016-01-04 23:37:40 +01:00
Vincent Laporte
3553258b1d
Revert "coqPackages.flocq: 2.4.0 -> 2.5.0"
...
This reverts commit db9bc6875f
2016-01-04 23:37:40 +01:00
Vincent Laporte
7462d96a65
ssreflect, mathcomp: fix build
2016-01-04 23:37:40 +01:00
John Wiegley
e582c41482
coqPackages.mathcomp,ssreflect: 1.5 -> 1.6
...
See the INSTALL file in the mathcomp package for instructions on
upgrading projects from 1.5 to 1.6. The 1.6 version works with both Coq
8.4 and 8.5.
2015-12-20 11:12:23 -08:00
John Wiegley
db9bc6875f
coqPackages.flocq: 2.4.0 -> 2.5.0
2015-12-16 14:10:14 -08:00
Vincent Laporte
dc6b4e7fdd
coq-flocq: 2.4.0 -> 2.5.0; coq-interval: 2.0.0 -> 2.1.0
2015-12-03 19:30:19 +01:00
Vincent Laporte
2bc3965bb7
coq-ext-lib: 1.0.0-beta2 -> 0.9.0-beta3
2015-11-21 04:18:14 +01:00
John Wiegley
8f97ad7b3c
coqPackages.ssreflect: add ncurses as a dependency
...
This is needed in the Darwin pure environment, where ncurses is not
available within the sandbox. The exact error was:
coqmktop -coqlib `coqtop -where` -o bin/ssrcoq.byte -I +threads src/ssrmatching.cmo src/ssreflect.cmo
ld: warning: directory not found for option '-L/nix/store/wlf8pb7gz5alzbhdxwayxx0x4as3rnw8-coq-8.5b2/lib/coq/kernel/byterun'
ld: library not found for -lncurses
2015-10-31 09:33:05 -07:00
Vincent Laporte
6a238d4b3e
coq-ext-lib: c2c71a2a -> 0.9.0 & 1.0.0-beta2
2015-09-27 10:24:25 +02:00
Vincent Laporte
7e80417fa8
coq-QuickChick: 21f50a02 -> 20150605
2015-08-18 21:28:33 +02:00
Vincent Laporte
22bc910c1a
coq-fiat: do not run tests on i686
...
as they require too much memory
2015-07-09 00:15:24 +02:00
Vincent Laporte
cd3a7d5be6
ssreflect, mathcomp: better package names
2015-06-19 18:11:33 +02:00
Vincent Laporte
01571ab2d7
coq-mathcomp: refactor
2015-06-19 18:11:33 +02:00
Vincent Laporte
524b7fe178
coq-ssreflect: refactor
2015-06-19 18:11:33 +02:00
Vincent Laporte
0f6b981fba
coq-mathcomp: also build and install the documentation
2015-06-19 18:11:33 +02:00
Vincent Laporte
e6b29c024b
coq-ssreflect: also build and install the documentation
2015-06-19 18:11:33 +02:00
Pascal Wittmann
6fa0db5a31
coqPackages.fiat: disable parallel build to fix build
2015-06-10 16:14:11 +02:00
Vincent Laporte
d5a4c3d21d
coq-tlc: fix package
2015-06-02 13:53:17 +02:00
Vincent Laporte
dfbef0d770
coq-coqeal: fix installation
2015-05-29 11:42:45 +02:00
John Wiegley
7d4b5d04c8
bedrock: Change build to use "src native"
2015-05-21 10:55:17 -05:00
John Wiegley
1da4d8b5c9
coqPackages.QuickChick: New expression
2015-05-08 11:35:23 -05:00
Joachim Fasting
bf7ad2d84f
meta.description fixups
...
Mostly scripted substitutions with a couple of subjective enhancements.
2015-04-30 18:17:42 +02:00
Pascal Wittmann
f99d5cf2fc
Fixed some descriptions
2015-04-28 10:55:20 +02:00
John Wiegley
9402a56620
coq_8_5: New expression
2015-04-26 22:29:15 -05:00
John Wiegley
86bead829a
bedrock: Don't bulid Cito without the platform
2015-04-10 14:13:54 -05:00
Vincent Laporte
587f127e93
coq-contribs: fix various packages
2015-03-01 17:53:51 +01:00
Vincent Laporte
88d31f6db0
coqPackages: add contribs ( close #5242 )
...
The Coq Users' Contributions
Homepage: http://www.lix.polytechnique.fr/coq/pylons/contribs/index
2015-01-25 07:36:10 +01:00
Vincent Laporte
833800aeba
coq-containers: remove
2015-01-25 07:35:45 +01:00
John Wiegley
753539800e
coqPackages.fiat: enable building the examples as a test
2015-01-09 15:20:17 -06:00
John Wiegley
443301ec8c
coqPackages.fiat: correct installation directory
2015-01-09 14:21:08 -06:00
John Wiegley
2aec1b0f31
coqPackages.fiat: new expression
2015-01-09 14:07:39 -06:00
Vincent Laporte
6a69a25c56
Adds coq-interval
...
This library provides vernacular files containing tactics for
simplifying the proofs of inequalities on expressions of real numbers
for the Coq proof assistant.
Homepage: http://coq-interval.gforge.inria.fr/
2014-12-08 09:15:13 +01:00
Vincent Laporte
7893825613
coq-flocq: license
2014-12-07 13:14:33 +01:00
John Wiegley
e5d92d45b7
coqPackages.coqeal: new expression
2014-12-04 14:15:30 -06:00
John Wiegley
38ab111dd7
coqPackages.unimath: new expression
2014-11-12 14:37:25 -06:00
John Wiegley
89e68ee32e
coqPackages.flocq: new expression
2014-10-21 00:23:36 -05:00
John Wiegley
f78f2a90d6
coqPackages.ssreflect, more: build ssrcoq binary, add maintainer
2014-10-13 16:11:33 -05:00
John Wiegley
7821d15299
coqPackages.domains: new expression
2014-10-11 22:01:46 -05:00
John Wiegley
f300c68977
coqPackages.ynot: remove broken tag
2014-10-11 19:32:16 -05:00
John Wiegley
904bee0c46
coqPackages.[coq-ext-lib,heq,paco,ynot]: new expressions
2014-10-11 17:24:59 -05:00
John Wiegley
382badfefb
coqPackages.bedrock: new expression
2014-10-11 16:22:15 -05:00
John Wiegley
814961f37a
coqPackages.tlc: new expression
2014-10-11 13:29:45 -05:00
John Wiegley
f310d73ac1
coqPackages.containers: set broken to false
2014-10-11 13:02:22 -05:00
John Wiegley
a064080d8c
coqPackages.containers: correct sha256 for the tarball
2014-10-11 13:00:22 -05:00
Vincent Laporte
01c6d8569f
coq-containers: package is broken
2014-10-01 18:39:31 +01:00
Vincent Laporte
c30c5f7cf3
Adds three coq libraries: containers, mathcomp, ssreflect
...
Containers is a reimplementation of the FSets/FMaps library from the
standard library, using typeclasses.
Homepage: http://coq.inria.fr/pylons/pylons/contribs/view/Containers/v8.4
The Mathematical Components (mathcomp) contains advanced theory files
covering a wide spectrum of mathematics.
Homepage: http://ssr.msr-inria.inria.fr/
Ssreflect is a proof language (plugin for Coq) and a small set of core
theory libraries about boolean, natural numbers, sequences, decidable
equality and finite types.
Homepage: http://ssr.msr-inria.inria.fr/
2014-09-28 14:03:15 +01:00
