Commit 01571ab2 authored by Vincent Laporte's avatar Vincent Laporte
Browse files

coq-mathcomp: refactor

parent 524b7fe1

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

+16 −27
Original line number Diff line number Diff line 
{ stdenv, fetchurl, coq, ssreflect

, graphviz, ocaml, withDoc ? true

}:

{ 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";

  };



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

  propagatedBuildInputs = [ coq ssreflect ];



  enableParallelBuilding = true;

    }



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

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



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

    fetchurl {

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

      sha256 = "03bnq44ym43x8shi7whc02l0g5vy6rx8f1imjw478chlgwcxazqy";

    }



  postInstall = stdenv.lib.optionalString withDoc ''

    make -f Makefile.coq install-doc DOCDIR=$out/share/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-${coq.coq-version}-mathcomp-1.5";



  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/top-level/all-packages.nix

+3 −1
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 =
@@ -14094,7 +14096,7 @@ let 


    coq = coq_8_5;



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

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



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