Michael Reilly
84cf00f980
treewide: Per RFC45, remove all unquoted URLs
2020-04-10 17:54:53 +01:00
Benjamin Hipple
ef2995988a
Merge pull request #83343 from vbgl/coq-coqhammer-1.1.1
...
coqPackages.coqhammer: 1.1 → 1.1.1
2020-03-28 23:20:37 -04:00
Vincent Laporte
2773498fc0
coqPackages.paramcoq: 1.1.1 → 1.1.2
2020-03-27 18:15:11 +01:00
Vincent Laporte
db5bde2342
coqPackages.coqhammer: 1.1 → 1.1.1
2020-03-25 08:44:34 +01:00
Cyril Cohen
cf210c082d
coqPackages.hierarchy-builder: init at 0.9.0
2020-03-11 17:15:52 +01:00
Vincent Laporte
659e89e21b
coqPackages.dpdgraph: enable for Coq ≥ 8.9
2020-03-10 17:46:15 +01:00
Vincent Laporte
e8243467b9
coqPackages_8_10.QuickChick: init at 1.2.0
2020-03-06 07:28:26 +01:00
Vincent Laporte
4f8ea1e02e
coqPackages.simple-io: enable for Coq 8.10
2020-03-06 07:28:26 +01:00
Vincent Laporte
b01052f138
coqPackages.paco: enable for Coq 8.10 and 8.11
2020-03-04 07:12:02 +01:00
Cyril Cohen
66a7f5d4e2
elpi: 1.7.0 -> 1.10.2; coq-elpi: 1.1 -> 1.3
2020-03-03 14:57:42 +01:00
Vincent Laporte
229dc013b3
coqPackages.mathcomp_1_10: init at 1.10.0
2020-02-24 15:18:07 +01:00
Valentin Robert
40376f1724
coqPackages.coq-ext-lib: 0.10.3 -> 0.11.1
2020-02-20 18:13:11 +01:00
Vincent Laporte
f2cd2ee0e0
coqPackages.bignums: enable for Coq 8.11
2020-02-07 10:26:26 +01:00
Vincent Laporte
fa709922f3
coqPackages.tlc: disable for Coq > 8.10
2020-01-31 14:09:51 +01:00
Jarrod Pas
b25a192755
coqPackages.CoLoR support for Coq 8.10
2020-01-26 09:37:22 -06:00
Jarrod Pas
bebbc486d0
Keeps older CoLoR available for older Coq
2020-01-25 16:38:04 -06:00
Jarrod Pas
4339f5803d
coqPackages.CoLoR 1.4.0 -> 1.6.0
...
The package is now developed on GitHub, so fetchurl was replace with
fetchFromGithub.
2020-01-22 02:05:22 -06:00
Robin Gloster
2157dcd141
treewide: installFlags is a list
2019-12-30 13:22:43 +01:00
Robin Gloster
ac8eaa8507
treewide: fix *Flags
2019-12-30 04:50:37 +01:00
c0bw3b
69b393ace5
Treewide: update some problematic homepages
...
These URLs are reported as problematic by Repology.
It could be a permanent redirection
or the page does not exist anymore
2019-12-08 10:21:29 -08:00
Valentin Robert
b937c4c734
coqPackages.coq-ext-lib: 0.10.1 -> 0.10.3
2019-11-08 09:42:01 +00:00
Valentin Robert
ea8e3f5979
coqPackages.paco: 1.2.8 -> 4.0.0
2019-11-08 09:41:30 +00:00
Valentin Robert
b76193a336
coqPackages.coq-extensible-records: support for coq 8.9 and 8.10
2019-10-29 12:42:22 +00:00
Valentin Robert
1bb56de88b
coqPackages.coq-bits: init at 20190812
2019-10-24 06:24:33 +00:00
Vincent Laporte
7044058ef7
coqPackages_8_10.ltac2: init at 0.3
2019-10-24 06:20:59 +00:00
Vincent Laporte
b4db381443
coq_8_10: 8.10+β3 → 8.10.0
...
coqPackages.coq-elpi: master → 1.1.0
2019-10-16 02:43:46 +00:00
Vincent Laporte
1f365f9d26
coqPackages_8_7.contribs.additions: remove
2019-10-11 07:58:42 +02:00
volth
7b8fb5c06c
treewide: remove redundant quotes
2019-09-08 23:38:31 +00:00
Jan Tojnar
f9237f3152
Merge branch 'master' into staging-next
2019-09-06 16:55:11 +02:00
Vincent Laporte
5b3dc48f19
coqPackages.stdpp: 1.1 -> 1.2.1; coqPackages.iris: 3.1.0 -> 3.2.0
...
Ensures compatibility with Coq ≥ 8.9
2019-09-06 11:51:34 +00:00
volth
08f68313a4
treewide: remove redundant rec
2019-08-28 11:07:32 +00:00
volth
35d68ef143
treewide: remove redundant quotes
2019-08-26 21:40:19 +00:00
Vincent Laporte
4018a4cddf
coqPackages.interval: 3.4.0 -> 3.4.1
2019-08-12 09:05:16 +00:00
Cyril Cohen
52f3c28df2
elpi: 1.4.1 -> 1.6.0, and coq-elpi
2019-08-09 08:47:52 +00:00
Vincent Laporte
5b0fdad5df
coqPackages.flocq: fetch sources from gitlab
2019-08-05 09:21:02 +00:00
Vincent Laporte
bc1417c557
coqPackages.flocq: 3.1.0 -> 3.2.0
...
Ensures compatibility with Coq 8.10
2019-08-05 09:21:02 +00:00
Vincent Laporte
58e0c7b8ce
coqPackages.coquelicot: 3.0.2 -> 3.0.3
...
Ensures compatibility with Coq 8.10
2019-08-03 06:16:54 +00:00
Vincent Laporte
f9486ce114
coqPackages.equations: 1.2beta2 -> 1.2 ( #65281 )
...
* coqPackages.equations: 1.2beta2 -> 1.2
* coqPackages.category-theory: 20181016 -> 20190414
2019-07-23 22:27:55 +02:00
Théo Zimmermann
fd20e227a0
coqPackages.math-classes: 8.8.1 -> 8.9.1
...
Introduces compatibility with Coq 8.10.
2019-07-22 11:37:37 +00:00
Cyril Cohen
d80148928b
coqPackages: fix + add multinomials 1.3 + coqeal 1.0.0
2019-07-02 12:01:36 +00:00
Vincent Laporte
5f78fa399d
coqPackages.gappalib: disable for Coq 8.10
2019-06-27 13:59:02 +00:00
Vincent Laporte
37eef9055a
coqPackages.gappalib: init at 1.4.1
...
This is the Coq support library for Gappa.
2019-06-19 09:24:34 +00:00
Vincent Laporte
5e241a691b
coqPackages.coqprime: enable for Coq 8.10
2019-06-18 07:29:11 +00:00
Vincent Laporte
dbb6f70006
coqPackages.bignums: enable for Coq 8.10
2019-06-18 07:29:11 +00:00
volth
f3282c8d1e
treewide: remove unused variables ( #63177 )
...
* treewide: remove unused variables
* making ofborg happy
2019-06-16 19:59:05 +00:00
Vincent Laporte
7af35549ed
coqPackages.simple-io: 1.0.0 -> 1.2.0
2019-06-06 15:06:08 +00:00
Vincent Laporte
281b26533d
coqPackages.QuickChick: init at 1.1.0 for Coq 8.9
...
Removes QuickChick for Coq 8.7 as it is broken
(probably due to a too recent ssreflect).
2019-06-06 15:06:02 +00:00
Cyril Cohen
547466064e
coqPackages.mathcomp: 1.8.0 -> 1.9.0 and adding real-closed
2019-06-03 15:23:35 +00:00
Cyril Cohen
c96ef6fc44
updating packages coqPackages.bignums and coqPackages.equations
2019-05-23 15:05:15 +02:00
Vincent Laporte
c37e00067d
coqPackages.ltac2: init at 0.1
2019-05-23 14:25:07 +02:00
Cyril Cohen
d16a78b512
several fixes in coq and coqPackages.mathcomp (and extras)
2019-05-21 08:55:38 +02:00
Cyril Cohen
b71c308591
coqPackages: refactor mathcomp packages
...
Closes #61456
2019-05-15 14:11:21 +00:00
Vincent Laporte
b72daf7117
coq: init at 8.10+β1
2019-05-15 10:30:03 +02:00
Vincent Laporte
e3a03659e5
coqPackages.Verdi: 20181102 -> 20190202
2019-04-25 08:35:20 +02:00
Vincent Laporte
f61cadb624
coqPackages.tlc: 20180316 -> 20181116
2019-04-24 08:54:56 +02:00
Vincent Laporte
f09a13899d
coqPackages.mathcomp: 1.7.0 -> 1.8.0
...
coqPackages.mathcomp-finmap: 1.1.0 -> 1.2.0
coqPackages.mathcomp-analysis: 0.1.0 -> 0.2.0
2019-04-23 09:35:38 +02:00
Vincent Laporte
823107038b
coqPackages.coqhammer: init at 1.1
...
CoqHammer is a general-purpose automated reasoning hammer tool for Coq.
Homepage: http://cl-informatik.uibk.ac.at/cek/coqhammer/
2019-03-29 09:07:27 +01:00
Vincent Laporte
f23e6ec166
coqPackages.contribs.containers: enable for Coq 8.9
2019-03-18 10:25:58 +01:00
Vincent Laporte
2923bd5d06
coqPackages.coq-simple-io: 0.2 -> 1.0.0
...
coqPackages.QuickChick: 1.0.2 -> 20190311
2019-03-18 09:52:01 +01:00
Vincent Laporte
fc32780cdf
coqPackages.coq-ext-lib: 0.10.0 -> 0.10.1
2019-03-15 18:45:01 +01:00
Théo Zimmermann
b6a6f7ac98
coqPackages.contribs.zorns-lemma: 8.6.0 -> 8.9.0
2019-03-12 06:59:51 +00:00
Vincent Laporte
4a21043578
coqPackages.mathcomp-analysis: enable for Coq 8.9
2019-02-18 08:54:11 +01:00
Vincent Laporte
13e9efbb02
coqPackages.paramcoq: init at 1.1.1
2019-02-17 15:56:43 +01:00
Vincent Laporte
86db60f3f3
coqPackages.flocq: 3.0.0 -> 3.1.0
2019-02-15 10:03:39 +01:00
Vincent Laporte
1613f3db27
coqPackages.interval: 3.3.0 -> 3.4.0
2019-02-15 10:03:39 +01:00
Vincent Laporte
9461a108bc
coqPackages.coquelicot: 3.0.1 -> 3.0.2
2019-02-15 10:03:39 +01:00
Vincent Laporte
5d3e350536
coqPackages.mathcomp-analysis: init at 0.1.0
2019-02-09 12:33:02 +01:00
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