| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
ocamlPackages.menhir: 20181113 → 20190626
|
| |\
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| | | |
|
| |/
|
|
|
|
|
|
|
| |
treewide replacement of
stdenv.mkDerivation rec {
name = "*-${version}";
version = "*";
to pname
|
| |
|
|
|
|
| |
* treewide: remove unused variables
* making ofborg happy
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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>
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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.
|
| |
|
|
| |
Note that the fix of the VERSION file can likely be removed at the next update.
|
| | |
|
| | |
|
| |
|
|
|
| |
clightgen is a tool for coverting C to C-light.
This patch enable the build of this tool which is added to $out/bin/.
|
| | |
|
| | |
|
| |
|
|
| |
Signed-off-by: Austin Seipp <aseipp@pobox.com>
|
| | |
|
| |
|
|
| |
Also installs the Coq library as a separate output.
|
| |
|
|
|
| |
This is done for the sake of Yosemite, which does not have gcc, and yet
this change is also compatible with Linux.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Signed-off-by: Austin Seipp <aseipp@pobox.com>
|
| |
|
|
| |
Signed-off-by: Austin Seipp <aseipp@pobox.com>
|
| |
|
|
|
|
|
| |
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>
|
|
|
Signed-off-by: Austin Seipp <aseipp@pobox.com>
|