Commit graph

23 commits

Author SHA1 Message Date
Austin Seipp
53fb3bb3ef compcert: clean up expression
- Require Coq 8.6.1+
  - Split substituteInPlace call into patchPhase
  - Constrain platforms correctly to x86_64 Linux/Darwin, which was all
it supported anyway (there was no way to properly configure i686 builds,
nor cross builds. In the future there might be)
  - Minor stylistic cleanups
  - Add new 'man' and 'doc' outputs (the previous attempt to move the
build artifact outputs into $lib no longer worked correctly and they
were installed into 'out' instead, this fixes it completely).
  - Clean up weird binary artifacts left in $out (that were already
in $lib)
  - Wrap ccomp to undefine _FORTIFY_SOURCE; otherwise it causes
annoying warnings on every invocation

Signed-off-by: Austin Seipp <aseipp@pobox.com>
2019-01-12 20:06:28 -06:00
Vincent Laporte
7f2f989d6a
compcert: 3.3 -> 3.4 2018-09-17 18:36:31 +00:00
Vincent Laporte
ec7865cddc compcert: 3.2 -> 3.3 (#44512) 2018-08-05 21:14:55 +02:00
John Wiegley
d8720dd19a compcert: Permit building with Coq 8.7.2 2018-02-16 14:10:45 -08:00
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