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
Théo Zimmermann
290b16bfe5
coqPackages.zorns-lemma: fix build of versions pre-9.0
...
The source was fetched from the wrong location and thus did not match the provided sha.
2021-10-18 12:01:37 +02:00
Théo Zimmermann
8797af5eb7
coqPackages.gaia-hydras: init at 0.5
2021-10-18 11:42:52 +02:00
Théo Zimmermann
589393a08b
coqPackages.hydra-battles: 0.4 -> 0.5
2021-10-18 11:42:02 +02:00
Théo Zimmermann
856da48b65
coqPackages.addition-chains: 0.4 -> 0.5
2021-10-18 11:41:25 +02:00
Théo Zimmermann
3c6e3c742f
coqPackages.mathcomp-zify: 1.0.0+1.12+8.13 -> 1.1.0+1.12+8.13
2021-10-16 09:31:55 +02:00
Théo Zimmermann
4b26811cdd
coqPackages.gaia: mark as compatible with Coq 8.14
2021-10-16 09:28:48 +02:00
Théo Zimmermann
b946b0f9bb
coqPackages.goedel: 8.12.0 -> 8.13.0
2021-10-15 21:04:46 +02:00
Théo Zimmermann
e7735f2252
coqPackages_8_14.serapi: init at 8.14+rc1+0.14.0
2021-10-13 10:44:09 +02:00
Théo Zimmermann
3437b543fd
coq_8_14: init at 8.14+rc1
2021-10-13 10:44:09 +02:00
Vincent Laporte
9f4ccabc7e
coqPackages.Verdi: 20200131 → 20210524
2021-10-05 07:38:05 +02:00
Vincent Laporte
05845bd429
coqPackages.StructTact: 20181102 → 20210328
2021-10-05 07:38:05 +02:00
Vincent Laporte
63df91f789
coqPackages.coq-ext-lib: 0.11.3 → 0.11.4
2021-10-04 20:33:53 +02:00
Cyril Cohen
4f762132b0
coqPackages.multinomials: fix
2021-10-04 11:35:53 +02:00
Vincent Laporte
97fe835b44
coqPackages.gappalib: 1.4.5 → 1.5.0
2021-10-03 21:57:48 +02:00
Vincent Laporte
4b5042caf3
coqPackages.paramcoq: 1.1.2 → 1.1.3
2021-10-01 07:50:55 +02:00
Vincent Laporte
6c3324e245
coqPackages.flocq: 3.3.1 → 3.4.2
2021-09-24 21:39:00 +02:00
Théo Zimmermann
20291381c1
coqPackages.mkCoqDerivation: rely on namePrefix to compute default opam-name
...
As suggested by Cyril Cohen in https://github.com/NixOS/nixpkgs/pull/134362#discussion_r698379405 .
2021-09-20 11:10:23 +02:00
Théo Zimmermann
ddbbf5d80b
coqPackages.parsec: init at 0.1.0
2021-09-15 14:23:46 +02:00
Théo Zimmermann
28bf99d3cf
coqPackages.ceres: init at 0.4.0
2021-09-15 14:23:46 +02:00
Ben Siraphob
228f8bed64
Merge pull request #136938 from siraben/mathcomp-analysis-update
...
coqPackages.mathcomp-analysis: 0.3.9 -> 0.3.10
2021-09-08 13:32:41 -05:00
Théo Zimmermann
1eebd96344
coqPackages.corn: c366d3f01ec1812b145117a4da940518b092d3a6 -> 8.13.0
...
Fix to use a released version.
2021-09-08 13:15:48 +02:00
Ben Siraphob
714c90ee5f
coqPackages.mathcomp-analysis: 0.3.9 -> 0.3.10
2021-09-07 11:50:49 -05:00
Théo Zimmermann
a864b59ef1
coqPackage.topology: 8.12.0 -> 9.0.0
...
First release with Zorns-lemma and Topology in a monorepo.
Each individual package is built with Dune.
2021-08-22 16:11:42 +02:00
Ben Siraphob
fb56026541
Merge pull request #134456 from Zimmi48/mathcomp-1.12
...
coqPackages.mathcomp: change default version for Coq 8.10+
2021-08-17 10:56:28 -05:00
Théo Zimmermann
0c7e82e299
coqPackages.serapi: init at multiple versions
2021-08-17 16:45:04 +02:00
Théo Zimmermann
839354e312
coqPackages.mathcomp: change default version for Coq 8.10+
...
Fix the build of mathcomp-analysis with Coq 8.12 (by selecting a version which is compatible with HB 1.1.0).
2021-08-17 15:59:06 +02:00
Théo Zimmermann
58c1ab9158
coqPackages.addition-chains: init at 0.4
2021-08-17 14:44:10 +02:00
Théo Zimmermann
ff96901dbd
coqPackages.hydra-battles: 0.3 -> 0.4
2021-08-17 14:44:10 +02:00
Théo Zimmermann
98e2339545
coqPackages.gaia: init at 1.11 and 1.12
2021-08-17 14:44:10 +02:00
Théo Zimmermann
90654cce7d
coqPackages.mkCoqDerivation: fix useDune2
...
- Reuse build phase from the `buildDunePackage` function.
- Only install the package that was just built (useful for monorepo support).
- Introduces `opam-name` to override the default package name to build with Dune.
2021-08-17 14:38:47 +02:00
Vincent Laporte
49a6254362
coqPackages.coqeal: 1.0.5 → 1.0.6
2021-08-06 11:42:07 +02:00
Sandro Jäckel
a8f2d2ca78
QuickChick: format
2021-08-02 10:58:47 +02:00
Sandro Jäckel
7db52ad591
interval: format
2021-08-02 10:58:46 +02:00
Vincent Laporte
6dac1b7a09
coqPackages.VST: build and install more modules from floyd/
...
Fixes #131203
2021-07-31 21:44:44 +02:00
Ben Siraphob
95f1154f99
coqPackages.interval: 4.1.1 -> 4.3.0 ( #131818 )
2021-07-31 09:31:23 +02:00
John Wiegley
c8ff5bc6f7
coqPackages.category-theory: v20210730, for Coq versions 8.10-8.13
2021-07-30 21:38:30 -07:00
Théo Zimmermann
b8315c660b
coqPackages.QuickChick: add optional version parameter
...
This is the only package in coqPackages for which it was forgotten.
2021-07-30 17:00:15 +02:00
Ben Siraphob
2f3c29cc68
coqPackages.graph-theory: init at 0.9
2021-07-29 09:33:21 +02:00
Lars Rasmusson
23ea64cd81
coqPackages.corn: 8.12.0 → 8.13.0
2021-07-28 12:53:29 +02:00
Ben Siraphob
a22cd19910
Merge pull request #130023 from siraben/hierarchy-builder-update
...
coqPackages.hierarchy-builder: 1.0.0 -> 1.1.0
2021-07-18 00:57:39 +07:00
larsr
dfbc940137
coqPackages.math-classes: 8.12.0 -> 8.13.0
2021-07-17 16:25:34 +02:00
Ben Siraphob
492e12cd2d
coqPackages.mathcomp-analysis: 0.3.6 -> 0.3.9
...
For compatibility with hierarchy-builder
2021-07-16 22:04:25 +07:00
Ben Siraphob
7ded69f4c4
coqPackages.hierarchy-builder: 1.0.0 -> 1.1.0
2021-07-16 22:04:25 +07:00
Ben Siraphob
9fd32c9121
coqPackages.itauto: init at 8.13+no
2021-07-01 21:46:19 +07:00
Ben Siraphob
be76644735
coqPackages.semantics: init
2021-06-29 11:04:42 +02:00
Ben Siraphob
c1cb31af6b
coqPackages.VST: 2.7.1 -> 2.8
2021-06-18 10:39:33 +02:00
Théo Zimmermann
2bbf6c8687
Move CompCert into coqPackages. ( #126214 )
...
* compcert: preparation to move in coqPackages
* compcert: move into coqPackages
* compcert: remove version 3.7
As a consequence, also remove VST version 2.6
These were broken.
2021-06-14 14:21:41 +02:00
Ben Siraphob
f637d1b632
coqPackages.reglang: init at 1.1.2
2021-06-08 16:48:28 +02:00
Ben Siraphob
fb4061c6f1
coqPackages.topology: init
2021-06-01 12:38:18 +02:00
Ben Siraphob
25edb8c2ca
coqPackages.zorns-lemma: init
2021-06-01 12:38:18 +02:00
Enrico Tassi
6fb5325d5c
coq-elpi: clarify license
2021-05-28 03:15:23 +02:00
Enrico Tassi
abc154793a
coq-elpi: 1.9.7 -> 1.10.1
2021-05-28 03:15:23 +02:00
Ben Siraphob
8ff27c0c09
coqPackages.relation-algebra: init
2021-05-17 10:17:18 +02:00
Ben Siraphob
915abd3f08
coqPackages.aac-tactics: init
2021-05-17 10:17:18 +02:00
Vincent Laporte
bcbf6aafbd
coqPackages.metalib: enable for Coq 8.13
2021-05-10 18:57:58 +02:00
Vincent Laporte
67dfd53485
coqPackages.coqprime: enable for Coq 8.13
2021-05-10 18:57:58 +02:00
Cyril Cohen
0aa521e3a0
coqPackages.mathcomp-zify: init at 1.0.0+1.12+8.13
2021-05-10 15:59:48 +02:00
Ben Siraphob
92c5a672b3
coqPackages.autosubst: 5b40a32e -> 1.7 and fix build
2021-05-10 12:40:32 +02:00
Ben Siraphob
c72048d1a4
coqPackages.interval: 4.1.0 -> 4.1.1
2021-05-10 12:35:41 +02:00
Ben Siraphob
7209ede743
coqPackages.goedel: init at 8.12.0
2021-05-10 09:08:55 +02:00
Ben Siraphob
ddc71c80de
coqPackages.pocklington: init at 8.12.0
2021-05-10 09:08:55 +02:00
Ben Siraphob
e7d5862f4e
coqPackages.hydra-battles: init at 0.3
2021-05-10 09:08:55 +02:00
Vincent Laporte
4fb15bc739
coqPackages.VST: 2.6 → 2.7.1
2021-05-07 08:35:13 +02:00
Vincent Laporte
86878f63f9
coqPackages.CoLoR: 1.7.0 → 1.8.1
2021-05-07 01:06:52 +02:00
Vincent Laporte
cc6e48c8ba
coqPackages.coqeal: 1.0.4 → 1.0.5
2021-04-29 08:24:35 +02:00
Vincent Laporte
1437eee5bb
coqPackages.paramcoq: enable for Coq 8.13
2021-04-28 09:18:42 +02:00
Vincent Laporte
674de725cb
coqPackages.coqhammer: 1.3 → 1.3.1
2021-04-26 16:28:32 +02:00
Vincent Laporte
d4f48c8547
coqPackages.tlc: 20200328 → 20210316
2021-04-25 11:51:38 +02:00
Vincent Laporte
276cb2ad23
coqPackages_8_13.QuickChick: init at 1.5.0
2021-04-24 07:43:54 +02:00
Enrico Tassi
38cef0ba3b
coq-elpi: 1.6.2 -> 1.6.3
2021-04-18 06:09:28 +02:00
Enrico Tassi
5feab34f2e
coq-elpi: 1.8.2 -> 1.8.3
2021-04-18 06:09:28 +02:00
Enrico Tassi
9400e49ddf
coq-elpi: 1.9.5 -> 1.9.7
2021-04-18 06:09:28 +02:00
Lars Rasmusson
316db3a129
coqPackages.ITree: changed pname to InteractionTrees
2021-04-14 14:42:01 +02:00
Lars Rasmusson
7e73508a5f
ITree: init at 4.0.0
2021-04-14 13:45:56 +02:00
Lars Rasmusson
cba2770893
coqPackages.simple-io: enable for Coq 8.13
2021-04-14 13:45:56 +02:00
Lars Rasmusson
38c34b4304
coqPackages.coq-ext-lib: add Coq 8.13
2021-04-14 13:45:56 +02:00
Lars Rasmusson
7fc935db12
coqPackages.equations: 1.2.3 → 1.2.4
2021-04-14 13:45:56 +02:00
Enrico Tassi
7d51a0cdb0
coq-elpi: 1.6.1_8.11 -> 1.6.2_8.11
2021-04-12 21:52:06 +02:00
Enrico Tassi
8b22df9883
coq-elpi: 1.8.0 -> 1.8.2_8.12
2021-04-12 21:52:06 +02:00
Enrico Tassi
031da79988
coq-elpi: 1.9.4 -> 1.9.5
2021-04-12 21:52:06 +02:00
Vincent Laporte
c87714a040
coqPackages.stdpp: 1.4.0 → 1.5.0
...
coqPackages.iris: 3.3.0 → 3.4.0
2021-04-12 13:58:30 +02:00
Ben Siraphob
970b82e7d0
coqtail-math: init at 20201124
2021-04-09 10:05:32 +02:00
Ben Siraphob
80d5498aa2
coqPackages.odd-order: init at 1.12.0
2021-03-31 08:31:08 +02:00
Ben Siraphob
2341ffeeaa
coqPackages.fourcolor: init at 1.2.3
2021-03-26 10:55:48 +01:00
Cyril Cohen
6c5ca9c3eb
coqPackages.coq-elpi: 1.6.0 -> 1.6.1
2021-03-22 11:40:34 +01:00
Cyril Cohen
0f98db39af
coqPackages.coq-elpi: 1.9.3 -> 1.9.4
2021-03-17 21:54:53 +01:00
Cyril Cohen
18f9a74a18
coqPackages.mathcomp: etc ( #115417 )
...
* Fixing doc generation for mathcomp
* Update pkgs/development/coq-modules/mathcomp/default.nix
Co-authored-by: Sandro <sandro.jaeckel@gmail.com>
* More robust patchShebangs directives
Co-authored-by: Sandro <sandro.jaeckel@gmail.com>
2021-03-15 12:59:05 +01:00
Cyril Cohen
163ffe2fe4
coqPackages.mathcomp-analysis: 0.3.1 -> 0.3.6
2021-03-12 10:40:18 +01:00
Cyril Cohen
1550a4fe6b
coqPackages.multinomials: 1.5.2 -> 1.5.4 ( #115427 )
...
- This is the first packages which uses Dune in order to build and install
so I had to refactor build-support/coq/default.nix in order to support it.
- I added a new feature: one can now release.v.sha256 empty to try to download
with a fake sha256, hence failures are reported and one can copy paste the
sha256 given by the error message.
- I updated the documentation of languages-frameworks/coq.section.md accordingly.
2021-03-10 16:25:32 +01:00
Cyril Cohen
268e43a005
elpi: 1.12.0 -> 1.13.0
2021-02-18 22:26:10 +01:00
Vincent Laporte
9dfa33f610
coqPackages.dpdgraph: init at 0.6.9 for Coq 8.13
2021-02-14 14:36:18 +01:00
Vincent Laporte
c174292ec7
coqPackages.corn: 8.8.1 → 8.12.0
2021-01-28 10:28:51 +01:00
Théo Zimmermann
33fc9b1c6d
coqPackages.math-classes: 8.11.0 -> 8.12.0
2021-01-21 16:39:59 +01:00
Sandro
65aca46e9e
Merge pull request #109330 from CohenCyril/mathcomp-abel
...
coqPackages.mathcomp-abel: init at 1.0.0
2021-01-15 10:53:53 +01:00
Cyril Cohen
f06be1bcf9
coqPackages.mathcomp-abel: init at 1.0.0
2021-01-14 19:51:30 +01:00
Cyril Cohen
7c10cce9f3
coqPackages.mathcomp-analysis: add maintainers
2021-01-14 14:27:55 +01:00
Cyril Cohen
9ffd16b385
coqPackages: refactor
2021-01-09 11:56:17 +01:00
Vincent Laporte
de8205f8bb
coq_8_13: init at 8.13+β1
2020-12-15 21:13:40 +01:00
Vincent Laporte
4569be3b21
coqPackages.coq-ext-lib: 0.11.2 → 0.11.3
2020-12-01 22:02:08 +01:00
Vincent Laporte
9366259691
coqPackages.coq-ext-lib: refactor
2020-12-01 22:02:08 +01:00
Vincent Laporte
423dd60f07
coqPackages.paco: 4.0.0 → 4.0.2
2020-10-12 09:41:45 +02:00
Vincent Laporte
ddb2c7779e
coqPackages.coq-ext-lib: clean dependencies
2020-10-09 16:32:48 +02:00
Vincent Laporte
13126ce0a0
coqPackages.dpdgraph: do not depend on camlp5 for recent versions of Coq
2020-10-09 16:32:48 +02:00
Vincent Laporte
488d73f045
coqPackages.bignums: do not depend on camlp5 for recent versions of Coq
2020-10-09 16:32:48 +02:00
Vincent Laporte
d5f1dce6c8
coqPackages.VST: init at 2.6
2020-10-05 16:39:26 +02:00
Vincent Laporte
a1f8e0b4a1
coqPackages.metalib: 20170713 → 20200527
2020-09-22 21:53:29 +02:00
Vincent Laporte
5f3be6b669
coqPackages.Verdi: enable for Coq 8.12
2020-09-10 22:10:02 +02:00
Vincent Laporte
7f797b9521
coqPackages.paco: enable for Coq 8.12
2020-09-10 22:10:02 +02:00
Vincent Laporte
6e08d23707
coqPackages.paramcoq: init at 1.1.2 for Coq 8.12
2020-09-09 22:26:06 +02:00
Vincent Laporte
607b0ae7ae
coqPackages.coqprime: init at 8.12 for Coq 8.12
2020-09-09 06:32:25 +02:00
Vincent Laporte
60d0746a84
coqPackages.dpdgraph: init at 0.6.8 for Coq 8.12
2020-09-01 08:53:19 +02:00
Vincent Laporte
b3beb74d7c
coqPackages.gappalib: 1.4.3 → 1.4.4
2020-08-30 07:26:32 +02:00
Cyril Cohen
0a29f8c620
ocamlPackages.elpi: 1.11.2 -> 1.11.4
...
and fixing dependencies
2020-08-28 08:35:32 +02:00
Vincent Laporte
1875d9bfd5
coqPackages.coqprime: enable for Coq 8.11
2020-08-23 08:19:21 +02:00
Vincent Laporte
f839441f09
coqPackages.coqhammer: 1.2 → 1.3
2020-08-20 08:37:24 +02:00
Vincent Laporte
6f83faf70b
coqPackages.QuickChick: 1.3.1 → 1.3.2, 1.4.0
2020-08-19 08:08:37 +02:00
Vincent Laporte
6a1d98ecc4
coqPackages.simple-io: enable for Coq 8.12
2020-08-19 08:08:37 +02:00
Vincent Laporte
59d48ade22
coqPackages.coq-ext-lib: 0.11.1 → 0.11.2
2020-08-19 08:08:37 +02:00
Vincent Laporte
d0bb8ca41b
coqPackages.interval: 3.4.2 → 4.0.0
2020-08-17 07:05:35 +02:00
Vincent Laporte
a379617057
coqPackages.stdpp: 1.2.1 → 1.4.0
...
coqPackages.iris: 3.2.0 → 3.3.0
2020-08-16 08:22:55 +02:00
Cyril Cohen
084d5c0b8c
coq-elpi: 1.4.1 -> 1.5.1
2020-08-11 13:49:51 +02:00
Vincent Laporte
b8dfca143c
coq_8_12: 8.12+β1 → 8.12.0
...
coqPackages.equations: 1.2.2 → 1.2.3
2020-08-08 06:33:08 +02:00
Vincent Laporte
3541e8b4fb
coqPackages.bignums: init at 8.12.0 for Coq 8.12
2020-08-01 18:04:52 +02:00
Vincent Laporte
f2df7cd34f
coqPackages.math-classes: 8.9.1 → 8.11.0
2020-07-19 18:41:00 +02:00
Vincent Laporte
5adadd1466
coqPackages.tlc: 20181116 → 20200328
2020-07-17 19:43:34 +02:00
Vincent Laporte
d1a7237eee
coqPackages.coq-extensible-records: remove at 1.2.0
2020-07-10 11:26:41 +02:00
Vincent Laporte
473519a25d
coqPackages.coq-extensible-records: enable for Coq 8.11 and 8.12
2020-07-10 11:26:41 +02:00
Vincent Laporte
f6db90a389
coqPackages.coq-bits: enable for Coq 8.11 and 8.12
2020-07-09 08:17:49 +02:00
Vincent Laporte
60940d7dde
coqPackages.QuickChick: 1.2.0 → 1.2.1, 1.3.1
2020-07-05 10:43:06 +02:00
Vincent Laporte
4e0164cbb3
coqPackages.equations: 1.2.1 → 1.2.2
2020-06-30 08:51:15 +02:00
Vincent Laporte
5dfcb77a8e
coqPackages.interval: 3.4.1 → 3.4.2
2020-06-29 07:41:28 +02:00
Vincent Laporte
05eefe5ef8
coqPackages.simple-io: 1.2.0 → 1.3.0
2020-06-23 08:07:29 +02:00
Vincent Laporte
a4de542abe
coqPackages.coquelicot: 3.0.3 → 3.1.0
2020-06-21 10:05:15 +02:00
Vincent Laporte
5293575e85
coqPackages.mathcomp: enable 1.11.0 for Coq 8.12
2020-06-19 12:28:42 +02:00
Vincent Laporte
2d50195be2
coqPackages.flocq: 3.2.0 → 3.3.1
2020-06-14 09:51:00 +02:00
Cyril Cohen
b7f55b30f5
coqPackages.mathcomp: 1.11.0
2020-06-12 14:37:40 +02:00
Cyril Cohen
c60e2bee7c
coqPackages.coq-elpi: 1.4.0 -> 1.4.1
2020-06-12 10:12:02 +02:00
Cyril Cohen
cc1f954bc4
ocamlPackages.elpi: 1.10.2 -> 1.11.0
...
coqPackages.coq-elpi: 1.3.1 -> 1.4.0
coqPackages.hierarchy-builder: 0.9.0 -> 0.9.1
2020-06-04 10:25:19 +02:00
Vincent Laporte
f0d985cf9c
coqPackages.Verdi: 20190202 → 20200131
2020-06-02 09:18:29 +02:00
Vincent Laporte
6f9d12460b
coqPackages.Cheerios: 20181102 → 20200201
2020-06-02 09:18:29 +02:00
Vincent Laporte
550533171d
coqPackages.InfSeqExt: 20180918 → 20200131
2020-06-02 09:18:29 +02:00
Vincent Laporte
19dab239bb
coqPackages.CoLoR: enable for Coq 8.11
2020-06-01 15:04:17 +02:00
Cyril Cohen
147aded7df
coqPackages.mathcomp-extra: refactor
...
- removing broken packages
- taking into account fixpoint coqPackages in mathcomp-extra-config
2020-05-27 09:22:42 +02:00
Cyril Cohen
8d05e53561
Coq: refactoring of mathcomp packages ( #86088 )
...
- fixed bignum version
- fixed coq-bits version
- fixed coqprime version
- fixed mathcomp and mathcomp extra packages
(reworked building scheme and removed unused ssreflect directory)
- giving the user access to function filterCoqPackages, because overrideScope' does not re-apply it.
2020-05-09 07:47:47 +02:00
Andrew Miloradovsky
7397d8421e
coq-zorns-lemma: 8.9.0 -> 8.11.0
2020-05-08 07:40:32 +02:00
Vincent Laporte
95b35a2514
coqPackages.gappalib: 1.4.1 → 1.4.3
2020-04-29 06:56:14 +02:00
Damien Cassou
5eb2125cb4
Merge pull request #86058 from vbgl/coq-coqhammer-1.2
...
coqPackages.coqhammer: 1.1.1 → 1.2
2020-04-26 21:02:09 +02:00
Vincent Laporte
ef964a801e
coqPackages.coqhammer: 1.1.1 → 1.2
...
Add support for Coq 8.11
2020-04-26 15:51:20 +02:00
Vincent Laporte
a4adb1f75b
coqPackages.equations: 1.2 → 1.2.1
2020-04-23 18:03:04 +02:00
Vincent Laporte
f2eeeb83f2
coqPackages.dpdgraph: fix build with OCaml ≥ 4.08
2020-04-13 11:04:26 +02:00
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