Commit 3f042353 authored by Pierre Roux's avatar Pierre Roux
Browse files

coqPackages.validsdp: init at 1.1.0

parent d9b07a71

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

0 → 100644
+120 −0
Original line number Diff line number Diff line 
{

  coq,

  mkCoqDerivation,

  mathcomp,

  bignums,

  flocq,

  coquelicot,

  interval,

  mathcomp-reals-stdlib,

  multinomials,

  coqeal,

  lib,

  version ? null,

}:



let

  repo = "validsdp";

  owner = "validsdp";



  inherit version;

  defaultVersion =

    let

      case = coq: mc: out: {

        cases = [

          coq

          mc

        ];

        inherit out;

      };

    in

    with lib.versions;

    lib.switch

      [ coq.coq-version mathcomp.version ]

      [

        (case (range "9.0" "9.1") (isGe "2.3.0") "1.1.0")

      ]

      null;

  release = {

    "1.1.0".sha256 = "sha256-lbESAFBEBpOShNFh6RZQYPLRhdqYvdKBrxJOMy2L+Ws=";

  };

  releaseRev = v: "v${v}";



  # list of packages sorted by dependency order

  packages = {

    "libvalidsdp" = [ ];

    "validsdp" = [ "libvalidsdp" ];

  };



  validsdp_ =

    package:

    let

      libvalidsdp-deps = [

        mathcomp.field

        bignums

        flocq

        coquelicot

        interval

        mathcomp-reals-stdlib

      ];

      validsdp-deps = [

        mathcomp.field

        bignums

        flocq

        interval

        mathcomp-reals-stdlib

        multinomials

        coqeal

        coq.ocamlPackages.osdp

        coq.ocamlPackages.ocplib-simplex

      ];

      intra-deps = map validsdp_ packages.${package};

      pkgpath = lib.switch package [

        {

          case = "libvalidsdp";

          out = "libvalidsdp";

        }

        {

          case = "validsdp";

          out = ".";

        }

      ] package;

      pname = package;



      derivation = mkCoqDerivation ({

        inherit

          version

          pname

          defaultVersion

          release

          releaseRev

          repo

          owner

          ;



        namePrefix = [

          "coq"

        ];



        mlPlugin = package == "validsdp";



        propagatedBuildInputs =

          intra-deps

          ++ lib.optionals (package == "libvalidsdp") libvalidsdp-deps

          ++ lib.optionals (package == "validsdp") validsdp-deps;



        preBuild = ''

          cd ${pkgpath}

        '';



        meta = {

          description = "ValidSDP";

          license = lib.licenses.lgpl21Plus;

        };



        passthru = lib.mapAttrs (package: deps: validsdp_ package) packages;

      });

    in

    derivation;

in

validsdp_ "validsdp"

pkgs/development/ocaml-modules/osdp/default.nix

0 → 100644
+46 −0
Original line number Diff line number Diff line 
{

  lib,

  buildDunePackage,

  fetchurl,

  ocaml,

  findlib,

  zarith,

  ocplib-simplex,

  csdp,

  autoconf,

}:



lib.throwIf (lib.versionAtLeast ocaml.version "5.0")

  "osdp is not available for OCaml ${ocaml.version}"



  buildDunePackage

  {

    pname = "osdp";

    version = "1.1.1";



    src = fetchurl {

      url = "https://github.com/Embedded-SW-VnV/osdp/releases/download/v1.1.1/osdp-1.1.1.tgz";

      hash = "sha256-X7CS2g+MyQPDjhUCvFS/DoqcCXTEw8SCsSGED64TGKQ=";

    };



    preConfigure = ''

      autoconf

    '';



    nativeBuildInputs = [

      autoconf

      findlib

      csdp

    ];

    propagatedBuildInputs = [

      zarith

      ocplib-simplex

      csdp

    ];



    meta = {

      description = "OCaml Interface to SDP solvers";

      homepage = "https://github.com/Embedded-SW-VnV/osdp";

      license = lib.licenses.lgpl3Plus;

    };

  }

pkgs/top-level/coq-packages.nix

+2 −0
Original line number Diff line number Diff line
@@ -128,6 +128,7 @@ let 
      json = callPackage ../development/coq-modules/json { };

      lemma-overloading = callPackage ../development/coq-modules/lemma-overloading { };

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

      libvalidsdp = self.validsdp.libvalidsdp;

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

      math-classes = callPackage ../development/coq-modules/math-classes { };

      mathcomp = callPackage ../development/coq-modules/mathcomp { };
@@ -211,6 +212,7 @@ let 
      topology = callPackage ../development/coq-modules/topology { };

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

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

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

      vcfloat = callPackage ../development/coq-modules/vcfloat (

        lib.optionalAttrs (lib.versions.range "8.16" "8.18" self.coq.version) {

          interval = self.interval.override { version = "4.9.0"; };

pkgs/top-level/ocaml-packages.nix

+2 −0
Original line number Diff line number Diff line
@@ -1590,6 +1590,8 @@ let 


        ordering = callPackage ../development/ocaml-modules/ordering { };



        osdp = callPackage ../development/ocaml-modules/osdp { };



        oseq = callPackage ../development/ocaml-modules/oseq { };



        otfed = callPackage ../development/ocaml-modules/otfed { };