Vincent Laporte
93f8365824
compcert: 3.1 -> 3.2
2018-02-13 22:26:39 +00:00
Théo Zimmermann
8fde5790b4
compcert: fix license
...
The license of CompCert is not a generic "INRIA" license. It is "INRIA Non-Commercial
Agreement for the CompCert verified compiler". As unfortunate as it may seem, this
is a non-free license (clearly mentioned as such in its preamble). See also #20256 .
2017-09-21 15:24:17 +02:00
Théo Zimmermann
3370615a7f
compcert: 3.0.1 -> 3.1
...
Note that the fix of the VERSION file can likely be removed at the next update.
2017-09-21 15:06:51 +02:00
John Wiegley
f130ecdd30
coqPackages.compcert: Recent compcert supports 64-bit architectures
2017-07-17 11:21:20 -04:00
Vincent Laporte
b634622be0
compcert: 2.7.1 -> 3.0.1
2017-02-20 20:09:53 +00:00
Russell O'Connor
8ba82f28bc
compcert: adding clightgen to the build
...
clightgen is a tool for coverting C to C-light.
This patch enable the build of this tool which is added to $out/bin/.
2017-02-01 08:37:34 +01:00
Vincent Laporte
7c53518663
compcert: patch to build with Coq-8.5pl3
2016-11-02 19:23:15 +01:00
Kirill Boltaev
e61663a233
treewide: move to ocaml-ng system
2016-09-26 02:36:49 +03:00
Austin Seipp
f277185b48
nixpkgs: compcert 2.6 -> 2.7.1
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2016-08-13 23:07:01 +00:00
Vincent Laporte
c0691a0659
compcert: 2.5 -> 2.6
2016-01-25 11:48:47 +01:00
Vincent Laporte
475527adb7
compcert: 2.4 -> 2.5
...
Also installs the Coq library as a separate output.
2015-07-15 19:14:18 +02:00
John Wiegley
28b6fb61e6
Change occurrences of gcc to the more general cc
...
This is done for the sake of Yosemite, which does not have gcc, and yet
this change is also compatible with Linux.
2014-12-26 11:06:21 -06:00
Vincent Laporte
579e74549d
CompCert: update to 2.4
2014-10-05 23:38:16 +01:00
John Wiegley
f666bf4ddf
compcert: Correct syntax used in default.nix
2014-07-01 17:01:11 -05:00
John Wiegley
8d5c4e8b4b
compcert: build with 64-bit compiler, add darwin support
2014-07-01 16:43:27 -05:00
Austin Seipp
8155e5d119
compcert: fix build by adding menhir dependency
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-06-09 01:25:27 -05:00
Austin Seipp
8c0b63162b
compcert: 2.2 -> 2.3pl2
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-06-06 23:09:47 -05:00
Austin Seipp
27a0d56514
compcert: Fix Hydra platforms
...
Copy-pasta error, and compcert doesn't really make sense on Darwin or
64bit linux (it's callPackage_i686 anyway).
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-05-02 14:07:36 -05:00
Austin Seipp
0c51a4ac98
nixpkgs: add CompCert
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-05-01 19:11:46 -05:00