3
0
Fork 0
forked from mirrors/nixpkgs
Commit graph

33 commits

Author SHA1 Message Date
Vincent Laporte ee4559129a compcert: remove annoying assertions 2020-11-12 08:20:05 +01:00
Vincent Laporte 9a913b5125 compcert: build with Coq 8.11
And fix installation of development files
(use upstream Makefile rules instead of ad-hoc commands).
2020-10-05 16:39:26 +02:00
R. RyanTM d6aee72a9e compcert: 3.6 -> 3.7 2020-04-01 10:06:48 +00:00
Vincent Laporte 430e5ce04c compcert: 3.5 → 3.6
ocamlPackages.menhir: 20181113 → 20190626
2019-10-19 20:30:48 +00:00
Vladimír Čunát 2e6bf42a22
Merge branch 'master' into staging-next
There ver very many conflicts, basically all due to
name -> pname+version.  Fortunately, almost everything was auto-resolved
by kdiff3, and for now I just fixed up a couple evaluation problems,
as verified by the tarball job.  There might be some fallback to these
conflicts, but I believe it should be minimal.

Hydra nixpkgs: ?compare=1538299
2019-08-24 08:55:37 +02:00
Vincent Laporte 609d408970 coq: make version 8.9 the default one 2019-08-21 12:07:38 +00:00
volth 46420bbaa3 treewide: name -> pname (easy cases) (#66585)
treewide replacement of

stdenv.mkDerivation rec {
  name = "*-${version}";
  version = "*";

to pname
2019-08-15 13:41:18 +01: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 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