nixpkgs/pkgs/applications/science/logic/hol/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

89 lines
2.6 KiB
Nix

{lib, stdenv, pkgs, fetchurl, graphviz, fontconfig, liberation_ttf,
experimentalKernel ? true}:
let
pname = "hol4";
vnum = "10";
in
let
version = "k.${vnum}";
longVersion = "kananaskis-${vnum}";
holsubdir = "hol-${longVersion}";
kernelFlag = if experimentalKernel then "-expk" else "-stdknl";
in
let
polymlEnableShared = with pkgs; lib.overrideDerivation polyml (attrs: {
configureFlags = [ "--enable-shared" ];
});
in
stdenv.mkDerivation {
name = "${pname}-${version}";
src = fetchurl {
url = "mirror://sourceforge/hol/hol/${longVersion}/${holsubdir}.tar.gz";
sha256 = "0x2wxksr305h1lrbklf6p42lp09rbhb4rsh74g0l70sgapyiac9b";
};
buildInputs = [polymlEnableShared graphviz fontconfig liberation_ttf];
buildCommand = ''
mkdir chroot-fontconfig
cat ${fontconfig.out}/etc/fonts/fonts.conf > chroot-fontconfig/fonts.conf
sed -e 's@</fontconfig>@@' -i chroot-fontconfig/fonts.conf
echo "<dir>${liberation_ttf}</dir>" >> chroot-fontconfig/fonts.conf
echo "</fontconfig>" >> chroot-fontconfig/fonts.conf
export FONTCONFIG_FILE=$(pwd)/chroot-fontconfig/fonts.conf
mkdir -p "$out/src"
cd "$out/src"
tar -xzf "$src"
cd ${holsubdir}
substituteInPlace tools/Holmake/Holmake_types.sml \
--replace "\"/bin/mv\"" "\"mv\"" \
--replace "\"/bin/cp\"" "\"cp\""
for f in tools/buildutils.sml help/src-sml/DOT;
do
substituteInPlace $f --replace "\"/usr/bin/dot\"" "\"${graphviz}/bin/dot\""
done
#sed -ie "/compute/,999 d" tools/build-sequence # for testing
poly < tools/smart-configure.sml
bin/build ${kernelFlag} -symlink
mkdir -p "$out/bin"
ln -st $out/bin $out/src/${holsubdir}/bin/*
# ln -s $out/src/hol4.${version}/bin $out/bin
'';
meta = with lib; {
description = "Interactive theorem prover based on Higher-Order Logic";
longDescription = ''
HOL4 is the latest version of the HOL interactive proof
assistant for higher order logic: a programming environment in
which theorems can be proved and proof tools
implemented. Built-in decision procedures and theorem provers
can automatically establish many simple theorems (users may have
to prove the hard theorems themselves!) An oracle mechanism
gives access to external programs such as SMT and BDD
engines. HOL4 is particularly suitable as a platform for
implementing combinations of deduction, execution and property
checking.
'';
homepage = "http://hol.sourceforge.net/";
license = licenses.bsd3;
maintainers = with maintainers; [ mudri ];
platforms = with platforms; linux;
broken = true;
};
}