public/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

coqPackages_8_4.contribs: remove

Browse Source
This commit is contained in:
Vincent Laporte
2017-12-02 08:54:19 +00:00
parent 48aa378780
commit da84fab60b
4 changed files with 0 additions and 462 deletions
Download Patch File Download Diff File Expand all files Collapse all files
pkgs/development/coq-modules/contribs/default.nix
-261
View File
@@ -1,261 +0,0 @@
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)
)