Vincent Laporte
a35e7daa2b
compcert: 3.7 → 3.8
2020-12-09 08:28:04 +01:00
Vincent Laporte
2806eb2743
coq_8_12: 8.12.0 → 8.12.1
2020-11-15 12:03:15 +01:00
Vincent Laporte
d5f1dce6c8
coqPackages.VST: init at 2.6
2020-10-05 16:39:26 +02:00
Vincent Laporte
c8137fc229
coq: default to version 8.11
2020-08-23 08:19:21 +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
d1a7237eee
coqPackages.coq-extensible-records: remove at 1.2.0
2020-07-10 11:26:41 +02:00
Vincent Laporte
a8bb61222f
coq_8_12: init at 8.12+β1
2020-06-19 12:28:42 +02:00
Vincent Laporte
8fb991c7c4
coq: use OCaml 4.09
2020-05-27 10:12:22 +02:00
Vincent Laporte
48f0d8b3c8
coq_8_11: 8.11.1 → 8.11.2
2020-05-20 19:21: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
Vincent Laporte
d6a8d0ca5b
coq_8_11: 8.11.0 → 8.11.1
2020-04-05 15:32:32 +02:00
Cyril Cohen
cf210c082d
coqPackages.hierarchy-builder: init at 0.9.0
2020-03-11 17:15:52 +01:00
Vincent Laporte
229dc013b3
coqPackages.mathcomp_1_10: init at 1.10.0
2020-02-24 15:18:07 +01:00
Vincent Laporte
13dd5844fd
coqPackages_8_11.coq: 8.11+β1 → 8.11.0
2020-01-31 14:09:51 +01:00
Vincent Laporte
2942490c2c
coq_8_11: init at 8.11+β1
2019-12-07 07:58:00 +00:00
Vincent Laporte
3806eff9ca
coq_8_10: 8.10.1 → 8.10.2
2019-12-03 13:51:52 +00:00
Vincent Laporte
a8892b0d76
coq_8_10: 8.10.0 → 8.10.1
2019-10-25 07:58:47 +00:00
Valentin Robert
1bb56de88b
coqPackages.coq-bits: init at 20190812
2019-10-24 06:24:33 +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
8288301636
coq_8_10: 8.10+β2 → 8.10+β3
2019-09-16 11:41:43 -05:00
Vincent Laporte
609d408970
coq: make version 8.9 the default one
2019-08-21 12:07:38 +00:00
Cyril Cohen
52f3c28df2
elpi: 1.4.1 -> 1.6.0, and coq-elpi
2019-08-09 08:47:52 +00:00
Théo Zimmermann
3bc04b576a
coq: 8.10+beta1 -> 8.10+beta2
2019-07-14 14:58:49 +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
37eef9055a
coqPackages.gappalib: init at 1.4.1
...
This is the Coq support library for Gappa.
2019-06-19 09:24:34 +00:00
volth
f3282c8d1e
treewide: remove unused variables ( #63177 )
...
* treewide: remove unused variables
* making ofborg happy
2019-06-16 19:59:05 +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
Vincent Laporte
57c3da07eb
coq_8_9: 8.9.0 -> 8.9.1
2019-05-29 11:24:45 +02:00
Vincent Laporte
c37e00067d
coqPackages.ltac2: init at 0.1
2019-05-23 14:25:07 +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
Cyril Cohen
f7bf3d2239
coqPackages: refactor
...
Coq packages that depend on others need to be recompiled when the dependencies are updated, so we make the whole `coqPackages` overridable by `overrideScope'`, using `lib.makeScope`.
2019-04-10 12:56:57 +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
13e9efbb02
coqPackages.paramcoq: init at 1.1.1
2019-02-17 15:56:43 +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
Valentin Robert
f5dbe5de07
coqPackages.coq-extensible-records: init at 1.2.0
2019-01-30 11:30:23 +00:00
Vincent Laporte
b76961124d
coq_8_9: 8.9+beta1 -> 8.9.0
2019-01-24 09:08:51 +00: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
2b66c286be
coqPackages.corn: init at 8.8.1
2018-12-10 07:56:32 +00:00
Vincent Laporte
83d84c08b9
filterCoqPackages: honor recurseIntoAttrs
2018-12-09 03:08:54 +00:00
Vincent Laporte
527bad18d0
coqPackages: recurse into the attribute set
...
But do not build the packages on hydra.
2018-12-02 21:00:51 +00:00
John Wiegley
a370bd1fed
coqPackages: New expressions: StructTact, InfSeqExt, Cheerios, Verdi
2018-11-20 15:18:12 -08:00
Vincent Laporte
e338d801e2
mkCoqPackages: look for “dontFilter” in coq derivation
2018-11-04 20:49:38 +00:00
Théo Zimmermann
dd21f83950
coq_8_9: init at 8.9+beta1
2018-11-04 07:26:29 +00:00
Jörg Thalheim
8df0ca2bbc
coq_8_4: remove
...
verasco was its only user
2018-10-30 13:31:11 +00:00
John Wiegley
3c4c4ff051
coqPackages.Velisarios: New expression
2018-10-23 17:09:35 -07:00
Théo Zimmermann
2fdd38ed2d
camlp5_transitional: remove in favor of camlp5 (strict)
2018-10-10 19:44:54 +02:00
Théo Zimmermann
34394a38ef
ocamlPackages_3_11_2: remove
...
This requires removing also the Coq 8.3 and Matita 0.5.8 packages.
Coq 8.3 was released 8 years ago (2010) and there is no trace left
of users of this version (contrary to Coq 8.4, released 2012).
It is well over time to remove it.
Matita 0.5.8 was released in 2010 and because this version was still
used for teaching according to the official website, a legacy release
(0.5.9) was released in 5 years later to compile with more recent
OCaml libraries.
Updating to 0.5.9 (or a more recent version like 0.99.3) should allow
getting rid of the dependency on older OCaml but it is hard to test
given that the package is already broken before this update.
2018-10-08 21:10:05 +02:00
