mirrors/nixpkgs
1
0
Fork 1
mirror of https://github.com/NixOS/nixpkgs.git synced 2024-12-15 00:54:46 +00:00
Code Issues Wiki Activity
177529 commits 194 branches 125 tags 8.6 GiB
Commit graph

25 commits

Author SHA1 Message Date
Vincent Laporte 338f5208b3
compcert: fix source 2019-03-20 09:54:51 +00:00
Vincent Laporte 3c9bfa32e2 compcert: 3.4 -> 3.5 2019-03-09 05:49:26 -06:00
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