nixpkgs/pkgs/applications/science/logic/hol_light/default.nix
Profpatsch 4a7f99d55d treewide: with stdenv.lib; in meta -> with lib;
Part of: https://github.com/NixOS/nixpkgs/issues/108938

meta = with stdenv.lib;

is a widely used pattern. We want to slowly remove
the `stdenv.lib` indirection and encourage people
to use `lib` directly. Thus let’s start with the meta
field.

This used a rewriting script to mostly automatically
replace all occurances of this pattern, and add the
`lib` argument to the package header if it doesn’t
exist yet.

The script in its current form is available at
https://cs.tvl.fyi/depot@2f807d7f141068d2d60676a89213eaa5353ca6e0/-/blob/users/Profpatsch/nixpkgs-rewriter/default.nix
2021-01-11 10:38:22 +01:00

56 lines
1.6 KiB
Nix

{ lib, stdenv, runtimeShell, fetchFromGitHub, fetchpatch, ocaml, num, camlp5 }:
let
load_num =
if num == null then "" else
''
-I ${num}/lib/ocaml/${ocaml.version}/site-lib/num \
-I ${num}/lib/ocaml/${ocaml.version}/site-lib/top-num \
-I ${num}/lib/ocaml/${ocaml.version}/site-lib/stublibs \
'';
start_script =
''
#!${runtimeShell}
cd $out/lib/hol_light
exec ${ocaml}/bin/ocaml \
-I \`${camlp5}/bin/camlp5 -where\` \
${load_num} \
-init make.ml
'';
in
stdenv.mkDerivation {
name = "hol_light-2019-10-06";
src = fetchFromGitHub {
owner = "jrh13";
repo = "hol-light";
rev = "5c91b2ded8a66db571824ecfc18b4536c103b23e";
sha256 = "0sxsk8z08ba0q5aixdyczcx5l29lb51ba4ip3d2fry7y604kjsx6";
};
patches = [(fetchpatch {
url = "https://salsa.debian.org/ocaml-team/hol-light/-/raw/master/debian/patches/0004-Fix-compilation-with-camlp5-7.11.patch";
sha256 = "180qmxbrk3vb1ix7j77hcs8vsar91rs11s5mm8ir5352rz7ylicr";
})];
buildInputs = [ ocaml camlp5 ];
propagatedBuildInputs = [ num ];
installPhase = ''
mkdir -p "$out/lib/hol_light" "$out/bin"
cp -a . $out/lib/hol_light
echo "${start_script}" > "$out/bin/hol_light"
chmod a+x "$out/bin/hol_light"
'';
meta = with lib; {
description = "Interactive theorem prover based on Higher-Order Logic";
homepage = "http://www.cl.cam.ac.uk/~jrh13/hol-light/";
license = licenses.bsd2;
platforms = platforms.unix;
maintainers = with maintainers; [ thoughtpolice maggesi vbgl ];
};
}