Commit 71b1f2d9 authored by Pierre Roux's avatar Pierre Roux Committed by Vincent Laporte
Browse files

coqPackages.mtac2: init at 1.4-coq8.19

parent c6ab3b3a

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

0 → 100644
+22 −0
Original line number Diff line number Diff line 
{ lib, mkCoqDerivation, coq, unicoq, version ? null }:



mkCoqDerivation {

  pname = "Mtac2";

  owner = "Mtac2";

  inherit version;

  defaultVersion = with lib.versions; lib.switch coq.version [

    { case = range "8.19" "8.19"; out = "1.4-coq${coq.coq-version}"; }

  ] null;

  release."1.4-coq8.19".sha256 = "sha256-G9eK0eLyECdT20/yf8yyz7M8Xq2WnHHaHpxVGP0yTtU=";

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

  mlPlugin = true;

  propagatedBuildInputs = [ unicoq ];

  meta = with lib; {

    description = "Typed tactic language for Coq";

    license = licenses.mit;

  };

  preBuild = ''

    coq_makefile -f _CoqProject -o Makefile

    patchShebangs tests/sf-5/configure.sh

  '';

}

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

0 → 100644
+20 −0
Original line number Diff line number Diff line 
{ lib, mkCoqDerivation, coq, version ? null }:



mkCoqDerivation {

  pname = "unicoq";

  owner = "unicoq";

  inherit version;

  defaultVersion = with lib.versions; lib.switch coq.version [

    { case = range "8.19" "8.19"; out = "1.6-${coq.coq-version}"; }

  ] null;

  release."1.6-8.19".sha256 = "sha256-fDk60B8AzJwiemxHGgWjNu6PTu6NcJoI9uK7Ww2AT14=";

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

  mlPlugin = true;

  meta = with lib; {

    description = "An enhanced unification algorithm for Coq";

    license = licenses.mit;

  };

  preBuild = ''

    coq_makefile -f _CoqProject -o Makefile

  '';

}

pkgs/top-level/coq-packages.nix

+2 −0
Original line number Diff line number Diff line
@@ -115,6 +115,7 @@ let 
      metacoq-safechecker  = self.metacoq.safechecker;

      metacoq-erasure      = self.metacoq.erasure;

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

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

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

      odd-order = callPackage ../development/coq-modules/odd-order { };

      paco = callPackage ../development/coq-modules/paco {};
@@ -138,6 +139,7 @@ let 
      tlc = callPackage ../development/coq-modules/tlc {};

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

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

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

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