Commit 087ded31 authored by vbgl's avatar vbgl
Browse files

Merge pull request #8044 from vbgl/coqdoc 

Ssreflect: install the documentation
parents 8def3d69 cd3a7d5b

pkgs/development/coq-modules/mathcomp/default.nix

+16 −18
Original line number Diff line number Diff line 
{stdenv, fetchurl, coq, ssreflect}:

{ callPackage, coq, fetchurl }:



stdenv.mkDerivation {

let src = 

  if coq.coq-version == "8.4" then



  name = "coq-mathcomp-1.5";



  src = fetchurl {

    fetchurl {

      url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.tar.gz;

      sha256 = "1297svwi18blrlyd8vsqilar2h5nfixlvlifdkbx47aljq4m5bam";

  };

    }



  propagatedBuildInputs = [ coq ssreflect ];

  else if coq.coq-version == "8.5" then



  enableParallelBuilding = true;

    fetchurl {

      url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.coq85beta2.tar.gz;

      sha256 = "03bnq44ym43x8shi7whc02l0g5vy6rx8f1imjw478chlgwcxazqy";

    }



  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";

  else throw "No mathcomp package for Coq version ${coq.coq-version}";



  meta = with stdenv.lib; {

    homepage = http://ssr.msr-inria.inria.fr/;

    license = licenses.cecill-b;

    maintainers = [ maintainers.vbgl maintainers.jwiegley ];

    platforms = coq.meta.platforms;

    hydraPlatforms = [];

  };

in



callPackage ./generic.nix {

  inherit src;

}

pkgs/development/coq-modules/mathcomp/1.5.nix→pkgs/development/coq-modules/mathcomp/generic.nix

+33 −0
Original line number Diff line number Diff line 
{stdenv, fetchurl, coq, ssreflect}:

{ stdenv, fetchurl, coq, ssreflect

, graphviz, ocamlPackages, withDoc ? true

, src

}:



stdenv.mkDerivation {



  name = "coq-mathcomp-1.5-8.5b2";

  name = "coq-mathcomp-1.5-${coq.coq-version}";



  src = fetchurl {

    url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.coq85beta2.tar.gz;

    sha256 = "03bnq44ym43x8shi7whc02l0g5vy6rx8f1imjw478chlgwcxazqy";

  };

  inherit src;



  propagatedBuildInputs = [ coq ssreflect ];

  nativeBuildInputs = stdenv.lib.optionals withDoc

    ([ graphviz ] ++ (with ocamlPackages; [ ocaml camlp5_transitional ]));

  propagatedBuildInputs = [ ssreflect ];



  enableParallelBuilding = true;



  buildFlags = stdenv.lib.optionalString withDoc "doc";



  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";



  postInstall = stdenv.lib.optionalString withDoc ''

    make -f Makefile.coq install-doc DOCDIR=$out/share/coq/${coq.coq-version}/

  '';



  meta = with stdenv.lib; {

    homepage = http://ssr.msr-inria.inria.fr/;

    license = licenses.cecill-b;

    maintainers = [ maintainers.vbgl maintainers.jwiegley ];

    platforms = coq.meta.platforms;

    hydraPlatforms = [];

  };



}

pkgs/development/coq-modules/ssreflect/default.nix

+13 −26
Original line number Diff line number Diff line 
{stdenv, fetchurl, coq}:

{ callPackage, fetchurl, coq }:



assert coq.coq-version == "8.4";

if coq.coq-version == "8.4" then



stdenv.mkDerivation {



  name = "coq-ssreflect-1.5";

callPackage ./generic.nix {



  src = fetchurl {

    url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.tar.gz;

    sha256 = "0hm1ha7sxqfqhc7iwhx6zdz3nki4rj5nfd3ab24hmz8v7mlpinds";

  };



  buildInputs = [ coq.ocaml coq.camlp5 ];

  propagatedBuildInputs = [ coq ];



  enableParallelBuilding = true;



  patchPhase = ''

    # Permit building of the ssrcoq statically-bound executable

    sed -i 's/^#-custom/-custom/' Make

    sed -i 's/^#SSRCOQ/SSRCOQ/' Make

  '';

}



  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";

else if coq.coq-version == "8.5" then



  postInstall = ''

    mkdir -p $out/bin

    cp -p bin/ssrcoq $out/bin

    cp -p bin/ssrcoq.byte $out/bin

  '';

callPackage ./generic.nix {



  meta = with stdenv.lib; {

    homepage = http://ssr.msr-inria.inria.fr/;

    license = licenses.cecill-b;

    maintainers = with maintainers; [ vbgl jwiegley ];

    platforms = coq.meta.platforms;

  src = fetchurl {

    url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.coq85beta2.tar.gz;

    sha256 = "084l9xd5vgb8jml0dkm66g8cil5rsf04w821pjhn2qk9mdbwaagf";

  };



  patches = [ ./threads.patch ];



}



else throw "No ssreflect package for Coq version ${coq.coq-version}"

pkgs/development/coq-modules/ssreflect/1.5.nix→pkgs/development/coq-modules/ssreflect/generic.nix

+13 −9
Original line number Diff line number Diff line 
{stdenv, fetchurl, coq}:



assert coq.coq-version == "8.5";

{ stdenv, fetchurl, coq

, graphviz, withDoc ? true

, src, patches ? []

}:



stdenv.mkDerivation {



  name = "coq-ssreflect-1.5-8.5b2";

  name = "coq-ssreflect-1.5-${coq.coq-version}";



  src = fetchurl {

    url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.coq85beta2.tar.gz;

    sha256 = "084l9xd5vgb8jml0dkm66g8cil5rsf04w821pjhn2qk9mdbwaagf";

  };

  inherit src;



  nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];

  buildInputs = [ coq.ocaml coq.camlp5 ];

  propagatedBuildInputs = [ coq ];



  enableParallelBuilding = true;



  patches = [ ./threads.patch ];

  inherit patches;



  postPatch = ''

    # Permit building of the ssrcoq statically-bound executable
@@ -24,12 +23,17 @@ stdenv.mkDerivation { 
    sed -i 's/^#SSRCOQ/SSRCOQ/' Make

  '';



  buildFlags = stdenv.lib.optionalString withDoc "doc";



  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";



  postInstall = ''

    mkdir -p $out/bin

    cp -p bin/ssrcoq $out/bin

    cp -p bin/ssrcoq.byte $out/bin

  '' + stdenv.lib.optionalString withDoc ''

    mkdir -p $out/share/doc/coq/${coq.coq-version}/user-contrib/Ssreflect/

    cp -r html $out/share/doc/coq/${coq.coq-version}/user-contrib/Ssreflect/

  '';



  meta = with stdenv.lib; {

pkgs/top-level/all-packages.nix

+9 −8
Original line number Diff line number Diff line
@@ -14048,6 +14048,8 @@ let 


  mkCoqPackages_8_4 = self: let callPackage = newScope self; in {



    inherit callPackage;



    bedrock = callPackage ../development/coq-modules/bedrock {};



    contribs =
@@ -14090,19 +14092,18 @@ let 


  mkCoqPackages_8_5 = self: let callPackage = newScope self; in rec {



    mathcomp = callPackage ../development/coq-modules/mathcomp/1.5.nix {

      coq = coq_8_5;

      ssreflect = ssreflect;

    };

    inherit callPackage;



    ssreflect = callPackage ../development/coq-modules/ssreflect/1.5.nix {

    coq = coq_8_5;

    };



    mathcomp = callPackage ../development/coq-modules/mathcomp { };



    ssreflect = callPackage ../development/coq-modules/ssreflect { };



  };



  coqPackages = recurseIntoAttrs (mkCoqPackages_8_4 coqPackages);

  coqPackages_8_5 = recurseIntoAttrs (mkCoqPackages_8_5 coqPackages);

  coqPackages_8_5 = recurseIntoAttrs (mkCoqPackages_8_5 coqPackages_8_5);



  cvc3 = callPackage ../applications/science/logic/cvc3 {};

  cvc4 = callPackage ../applications/science/logic/cvc4 {};