Commit Graph

235 Commits

Author SHA1 Message Date
Vincent Laporte
bafa15f145 coqPackages.mathcomp-finmap: init at 1.1.0 2019-02-09 12:33:02 +01:00
Vincent Laporte
590e07779c coqPackages.mathcomp-bigenough: init at 1.0.0 2019-02-09 12:33:02 +01:00
Vincent Laporte
36e9fe820c coqPackages_8_9: disable a few packages that do not build 2019-02-08 02:01:32 +01:00
Vincent Laporte
59949aa55c
Revert "coq-modules: add default to fix eval"
This reverts commit e20b65156c.
2019-02-01 16:02:42 +00:00
John Wiegley
7239ffcc3c
coqPackages.equations: 1.2-beta-8.9 for coq_8_9 2019-01-31 11:56:07 -08:00
Valentin Robert
f5dbe5de07 coqPackages.coq-extensible-records: init at 1.2.0 2019-01-30 11:30:23 +00:00
Matthew Bauer
82a1153d6d coq-modules: add default to fix eval
We don’t want these to not even evaluate, otherwise we won’t know why
they’re broken. For now, I’ve left these as the latest version for a
default. In the future, maybe we should be smarter about choosing these.

(cherry picked from commit e20b65156c)
2019-01-28 10:16:30 -05:00
Vincent Laporte
85fe73a573 coqPackages.flocq: 2.6.0 -> {2.6.1, 3.0.0} 2019-01-23 07:45:16 +00:00
Vincent Laporte
63383a6db2 coqPackages.QuickChick: init at 1.0.2 for Coq 8.8 2019-01-18 14:53:15 +00:00
Vincent Laporte
10fa10731e coqPackages.category-theory: bound build parallelism 2019-01-11 17:24:45 +00:00
Vincent Laporte
e0561cbadd coqPackages.Verdi: fix build 2018-12-21 12:37:04 +01:00
Vincent Laporte
1d5059c5e6 coqPackages.InfSeqExt: fix build 2018-12-21 12:37:04 +01:00
Vincent Laporte
954bc20786 coqPackages.Cheerios: fix build 2018-12-21 12:37:04 +01:00
Vincent Laporte
5a12bedbfa coqPackages.StructTact: fix build 2018-12-21 12:37:04 +01:00
Vincent Laporte
881bec3238 coqPackages.coqprime: enable for Coq 8.9 2018-12-20 10:43:59 +01:00
Vincent Laporte
655231a612 coqPackages.simple-io: init at 0.2
Purely functional IO for Coq.

homepage: https://github.com/Lysxia/coq-simple-io
2018-12-10 15:35:34 +00:00
Vincent Laporte
e21a5e6035 coqPackages_8_9.coq-ext-lib: init at 0.10.0 2018-12-10 15:33:59 +00:00
Vincent Laporte
2b66c286be coqPackages.corn: init at 8.8.1 2018-12-10 07:56:32 +00:00
Vincent Laporte
e59970e3c4 coqPackages.math-classes: 1.0.7 -> 8.8.1 2018-12-03 08:29:46 +00:00
John Wiegley
a370bd1fed
coqPackages: New expressions: StructTact, InfSeqExt, Cheerios, Verdi 2018-11-20 15:18:12 -08:00
Vincent Laporte
c4cad8cfa7 coqPackages.bignums: enable for Coq version 8.9 2018-11-19 08:47:34 +00:00
Jörg Thalheim
846b2faea1
Merge pull request #49780 from Zimmi48/give-default-version-of-ssreflect
coqPackages.ssreflect: refactor choice of source version
2018-11-06 15:21:19 +00:00
Jörg Thalheim
5b813ebbc4 coqPackages.ssreflect: inherit mathcomp's source/meta attributes 2018-11-06 15:00:45 +00:00
Jörg Thalheim
993bd5df22 coqPackages.mathcomp: use fetchFromGitHub 2018-11-06 13:45:14 +00:00
Vincent Laporte
faea8def19
coqPackages_8_5.fiat_HEAD: fix build 2018-11-06 12:10:09 +00:00
Théo Zimmermann
7cc369c9d5
coqPackages.ssreflect: refactor choice of source version 2018-11-05 18:11:27 +01:00
Vincent Laporte
cd05d5a112
coqPackages.autosubst: fix build 2018-11-05 14:53:19 +00:00
Vincent Laporte
b3f6840d8e coqPackages.ssreflect: refactor 2018-11-04 20:49:38 +00:00
Vincent Laporte
d2c38d1eef coqPackages.mathcomp: refactor 2018-11-04 20:49:38 +00:00
Vincent Laporte
6a449c0742
coqPackages.contribs.zfc: enable for Coq 8.8 2018-11-02 08:51:24 +00:00
Vincent Laporte
ab95faa507 coqPackages.category-theory: fix build 2018-10-24 05:50:04 +00:00
John Wiegley
3c4c4ff051
coqPackages.Velisarios: New expression 2018-10-23 17:09:35 -07:00
Théo Zimmermann
8c399bd6c1
coqPackages: use coq.ocamlPackages instead of coq.ocaml, coq.camlp5, etc. 2018-10-19 10:25:09 +02:00
John Wiegley
1ba4d23c3a
Revert "coqPackages.fiat_HEAD: Update 2016-10-24 -> 2018-02-27"
This reverts commit f5f71c08cd, due to
insufficient testing.
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, which broke
Nixpkgs evaluation.

Ping @jwiegley.
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