pkgs/by-name/ho/hol/package.nix

   1 {lib, stdenv, pkgs, fetchurl, graphviz, fontconfig, liberation_ttf,
   2  experimentalKernel ? true}:
   3
   4 let
   5   pname = "hol4";
   6   vnum = "14";
   7
   8   version = "k.${vnum}";
   9   longVersion = "kananaskis-${vnum}";
  10   holsubdir = "hol-${longVersion}";
  11   kernelFlag = if experimentalKernel then "--expk" else "--stdknl";
  12
  13   polymlEnableShared = with pkgs; lib.overrideDerivation polyml (attrs: {
  14     configureFlags = [ "--enable-shared" ];
  15   });
  16 in
  17
  18 stdenv.mkDerivation {
  19   name = "${pname}-${version}";
  20
  21   src = fetchurl {
  22     url = "mirror://sourceforge/hol/hol/${longVersion}/${holsubdir}.tar.gz";
  23     sha256 = "6Mc/qsEjzxGqzt6yP6x/1Tmqpwc1UDGlwV1Gl+4pMsY=";
  24   };
  25
  26   buildInputs = [polymlEnableShared graphviz fontconfig liberation_ttf];
  27
  28   buildCommand = ''
  29
  30     mkdir chroot-fontconfig
  31     cat ${fontconfig.out}/etc/fonts/fonts.conf > chroot-fontconfig/fonts.conf
  32     sed -e 's@</fontconfig>@@' -i chroot-fontconfig/fonts.conf
  33     echo "<dir>${liberation_ttf}</dir>" >> chroot-fontconfig/fonts.conf
  34     echo "</fontconfig>" >> chroot-fontconfig/fonts.conf
  35
  36     export FONTCONFIG_FILE=$(pwd)/chroot-fontconfig/fonts.conf
  37
  38     mkdir -p "$out/src"
  39     cd  "$out/src"
  40
  41     tar -xzf "$src"
  42     cd ${holsubdir}
  43
  44     substituteInPlace tools/Holmake/Holmake_types.sml \
  45       --replace "\"/bin/" "\"" \
  46
  47
  48     for f in tools/buildutils.sml help/src-sml/DOT;
  49     do
  50       substituteInPlace $f --replace "\"/usr/bin/dot\"" "\"${graphviz}/bin/dot\""
  51     done
  52
  53     #sed -ie "/compute/,999 d" tools/build-sequence # for testing
  54
  55     poly < tools/smart-configure.sml
  56
  57     bin/build ${kernelFlag}
  58
  59     mkdir -p "$out/bin"
  60     ln -st $out/bin  $out/src/${holsubdir}/bin/*
  61     # ln -s $out/src/hol4.${version}/bin $out/bin
  62   '';
  63
  64   meta = with lib; {
  65     broken = (stdenv.hostPlatform.isLinux && stdenv.hostPlatform.isAarch64);
  66     description = "Interactive theorem prover based on Higher-Order Logic";
  67     longDescription = ''
  68       HOL4 is the latest version of the HOL interactive proof
  69       assistant for higher order logic: a programming environment in
  70       which theorems can be proved and proof tools
  71       implemented. Built-in decision procedures and theorem provers
  72       can automatically establish many simple theorems (users may have
  73       to prove the hard theorems themselves!) An oracle mechanism
  74       gives access to external programs such as SMT and BDD
  75       engines. HOL4 is particularly suitable as a platform for
  76       implementing combinations of deduction, execution and property
  77       checking.
  78     '';
  79     homepage = "http://hol.sourceforge.net/";
  80     license = licenses.bsd3;
  81     platforms = platforms.unix;
  82     maintainers = with maintainers; [ mudri ];
  83   };
  84 }