nixpkgs/pkgs/development/coq-modules/contribs/default.nix

contribs:

let
  mkContrib = import ./mk-contrib.nix;
  all = import ./all.nix;
  overrides = {
    Additions = self: {
      patchPhase = ''
        for p in binary_strat dicho_strat generation log2_implementation shift
        do
          substituteInPlace $p.v \
          --replace 'Require Import Euclid.' 'Require Import Coq.Arith.Euclid.'
        done
      '';
    };
    BDDs = self: {
      buildInputs = self.buildInputs ++ [ contribs.IntMap ];
      patchPhase = ''
        patch Make <<EOF
        2d1
        < -R ../../Cachan/IntMap IntMap
        32d30
        < extraction
        EOF
        coq_makefile -f Make -o Makefile
      '';
      postInstall = ''
        mkdir -p $out/bin
        cp extraction/dyade $out/bin
      '';
    };
    CanonBDDs = self: {
      patchPhase = ''
        patch Make <<EOF
        17d16
        < rauzy/algorithme1/extraction
        EOF
        coq_makefile -f Make -o Makefile
      '';
      postInstall = ''
        mkdir -p $out/bin
        cp rauzy/algorithme1/extraction/suresnes $out/bin
      '';
    };
    CoinductiveReals = self: {
      buildInputs = self.buildInputs ++ [ contribs.QArithSternBrocot ];
      patchPhase = ''
        patch Make <<EOF
        2d1
        < -R ../QArithSternBrocot QArithSternBrocot
        EOF
        coq_makefile -f Make -o Makefile
      '';
    };
    CoRN = self: {
      buildInputs = self.buildInputs ++ [ contribs.MathClasses ];
      patchPhase = ''
        patch Make <<EOF
        2d1
        < -R ../MathClasses/ MathClasses
        EOF
        coq_makefile -f Make -o Makefile.coq
      '';
      enableParallelBuilding = true;
      installFlags = self.installFlags + " -f Makefile.coq";
    };
    Counting = self: {
      postInstall = ''
        for ext in cma cmxs
        do
          cp src/counting_plugin.$ext $out/lib/coq/8.4/user-contrib/Counting/
        done
      '';
    };
    Ergo = self: {
      buildInputs = self.buildInputs ++ (with contribs; [ Containers Counting Nfix ]);
      patchPhase = ''
        patch Make <<EOF
        4,9d3
        < -I ../Containers/src
        < -R ../Containers/theories Containers
        < -I ../Nfix/src
        < -R ../Nfix/theories Nfix
        < -I ../Counting/src
        < -R ../Counting/theories Counting
        EOF
        coq_makefile -f Make -o Makefile
      '';
    };
    FingerTree = self: {
      patchPhase = ''
        patch Make <<EOF
        21d20
        < extraction
        EOF
        coq_makefile -f Make -o Makefile
      '';
    };
    FOUnify = self: {
      patchPhase = ''
        patch Make <<EOF
        8c8
        < -custom "\$(CAMLOPTLINK) -pp '\$(CAMLBIN)\$(CAMLP4)o' -o unif unif.mli unif.ml main.ml" unif.ml unif
        ---
        > -custom "\$(CAMLOPTLINK) -pp 'camlp5o' -o unif unif.mli unif.ml main.ml" unif.ml unif
        EOF
        coq_makefile -f Make -o Makefile
      '';
      postInstall = ''
        mkdir -p $out/bin
        cp unif $out/bin/
      '';
    };
    Goedel = self: {
      buildInputs = self.buildInputs ++ [ contribs.Pocklington ];
      patchPhase = ''
        patch Make <<EOF
        2d1
        < -R ../../Eindhoven/Pocklington Pocklington
        EOF
        coq_makefile -f Make -o Makefile
      '';
    };
    Graphs = self: {
      buildInputs = self.buildInputs ++ [ contribs.IntMap ];
      patchPhase = ''
        patch Make <<EOF
        2d1
        < -R ../../Cachan/IntMap IntMap
        EOF
        coq_makefile -f Make -o Makefile
      '';
      postInstall = ''
        mkdir -p $out/bin
        cp checker $out/bin/
      '';
    };
    IntMap = self: { configurePhase = "coq_makefile -f Make -o Makefile"; };
    LinAlg = self: {
      buildInputs = self.buildInputs ++ [ contribs.Algebra ];
      patchPhase = ''
        patch Make <<EOF
        2d1
        < -R ../../Sophia-Antipolis/Algebra/ Algebra
        EOF
        coq_makefile -f Make -o Makefile
      '';
    };
    Markov = self: { configurePhase = "coq_makefile -o Makefile -R . Markov markov.v"; };
    Nfix = self: {
      postInstall = ''
        for ext in cma cmxs
        do
          cp src/nfix_plugin.$ext $out/lib/coq/8.4/user-contrib/Nfix/
        done
      '';
    };
    OrbStab = self: {
      buildInputs = self.buildInputs ++ (with contribs; [ LinAlg Algebra ]);
      patchPhase = ''
        patch Make <<EOF
        2,3d1
        < -R ../../Sophia-Antipolis/Algebra Algebra
        < -R ../../Nijmegen/LinAlg LinAlg
        EOF
        coq_makefile -f Make -o Makefile
      '';
    };
    PTSF = self: {
      buildInputs = self.buildInputs ++ [ contribs.PTSATR ];
      patchPhase = ''
        patch Make <<EOF
        1d0
        < -R ../../Paris/PTSATR/ PTSATR
        EOF
        coq_makefile -f Make -o Makefile
      '';
    };
    RelationExtraction = self: {
      patchPhase = ''
        patch Make <<EOF
        31d30
        < test
        EOF
        coq_makefile -f Make -o Makefile
      '';
    };
    Semantics = self: {
      patchPhase = ''
        patch Make <<EOF
        18a19
        > interp.mli
        EOF
      '';
      configurePhase = ''
        coq_makefile -f Make -o Makefile
        make extract_interpret.vo
        rm -f str_little.ml.d
      '';
    };
    SMC = self: {
      buildInputs = self.buildInputs ++ [ contribs.IntMap ];
      patchPhase = ''
        patch Make <<EOF
        2d1
        < -R ../../Cachan/IntMap IntMap
        EOF
        coq_makefile -f Make -o Makefile
      '';
    };
    Ssreflect = self: {
      patchPhase = ''
        substituteInPlace Makefile \
        --replace "/bin/mkdir" "mkdir"
      '';
    };
    Stalmarck = self: {
      configurePhase = "coq_makefile -R . Stalmarck *.v staltac.ml4 > Makefile";
    };
    Topology = self: {
      buildInputs = self.buildInputs ++ [ contribs.ZornsLemma ];
      patchPhase = ''
        patch Make <<EOF
        2d1
        < -R ../ZornsLemma ZornsLemma
        EOF
        coq_makefile -f Make -o Makefile
      '';
    };
    TreeAutomata = self: {
      buildInputs = self.buildInputs ++ [ contribs.IntMap ];
      patchPhase = ''
        patch Make <<EOF
        2d1
        < -R ../../Cachan/IntMap IntMap
        EOF
        coq_makefile -f Make -o Makefile
      '';
    };
  };
in

callPackage: extra:

builtins.listToAttrs (
map
(name:
  let
    sha256 = builtins.getAttr name all;
    override =
      if builtins.hasAttr name overrides
      then builtins.getAttr name overrides
      else x: { };
  in
  {
    inherit name;
    value = callPackage (mkContrib { inherit name sha256 override; }) extra;
  }
)
(builtins.attrNames all)
)