Update SSReflect to version 1.4
This commit is contained in:
parent
ef649da119
commit
46d9146d64
@ -6,7 +6,7 @@
|
|||||||
|
|
||||||
let
|
let
|
||||||
pname = "ssreflect";
|
pname = "ssreflect";
|
||||||
version = "1.3pl4";
|
version = "1.4";
|
||||||
name = "${pname}-${version}";
|
name = "${pname}-${version}";
|
||||||
webpage = http://www.msr-inria.inria.fr/Projects/math-components;
|
webpage = http://www.msr-inria.inria.fr/Projects/math-components;
|
||||||
in
|
in
|
||||||
@ -15,22 +15,16 @@ stdenv.mkDerivation {
|
|||||||
inherit name;
|
inherit name;
|
||||||
|
|
||||||
src = fetchurl {
|
src = fetchurl {
|
||||||
url = "${webpage}/${name}.tar.gz";
|
url = "${webpage}/${name}-coq8.4.tar.gz";
|
||||||
sha256 = "1ha3iiqq79pgll5ra9z0xdi3d3dr3wb9f5vsm4amy884l5anva02";
|
sha256 = "1ysx29xw09i86lq0d92z9cnyx133jfgq4qddy3501000fn7xwi7h";
|
||||||
};
|
};
|
||||||
|
|
||||||
buildInputs = [ ocaml camlp5 coq makeWrapper ];
|
buildInputs = [ ocaml camlp5 coq makeWrapper ];
|
||||||
|
|
||||||
patches = [ ./static.patch ];
|
patches = [ ./static.patch ];
|
||||||
|
|
||||||
postBuild = ''
|
|
||||||
cd src
|
|
||||||
coqmktop -ide -opt ssreflect.cmx -o ../bin/ssrcoqide
|
|
||||||
cd ..
|
|
||||||
'';
|
|
||||||
|
|
||||||
installPhase = ''
|
installPhase = ''
|
||||||
COQLIB=$out/lib/coq make -f Makefile.coq install -e
|
COQLIB=$out/lib/coq/ make -f Makefile.coq install -e
|
||||||
mkdir -p $out/bin
|
mkdir -p $out/bin
|
||||||
cp bin/* $out/bin
|
cp bin/* $out/bin
|
||||||
for i in $out/bin/*; do
|
for i in $out/bin/*; do
|
||||||
@ -39,6 +33,7 @@ stdenv.mkDerivation {
|
|||||||
--add-flags "$out/lib/coq/user-contrib/Ssreflect" \
|
--add-flags "$out/lib/coq/user-contrib/Ssreflect" \
|
||||||
--add-flags "Ssreflect"
|
--add-flags "Ssreflect"
|
||||||
done
|
done
|
||||||
|
makeWrapper "${coq}/bin/coqide" "$out/bin/ssrcoqide" --add-flags "-coqtop" --add-flags "$out/bin/ssrcoq"
|
||||||
'';
|
'';
|
||||||
|
|
||||||
meta = {
|
meta = {
|
||||||
|
@ -1,33 +1,21 @@
|
|||||||
--- ssreflect1.3pl4/Make (revision 3823)
|
--- ssreflect1.4-coq8.4/Make (revision 3823)
|
||||||
+++ ssreflect1.3pl4/Make (working copy)
|
+++ ssreflect1.4-coq8.4/Make (working copy)
|
||||||
@@ -1,18 +1,18 @@
|
@@ -1,10 +1,10 @@
|
||||||
## Uncomment for static linking
|
-### Uncomment for static linking
|
||||||
## <static>
|
-##
|
||||||
-#
|
-#-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -opt -o bin/ssrcoq src/ssrmatching.cmx src/ssreflect.cmx" "src/ssrmatching.cmx src/ssreflect.cmx" bin/ssrcoq
|
||||||
-#-custom "$(COQBIN)coqmktop -opt -o bin/ssrcoq src/ssreflect.cmx" "src/ssreflect.cmx" bin/ssrcoq
|
-#-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -o bin/ssrcoq.byte src/ssrmatching.cmo src/ssreflect.cmo" "src/ssrmatching.cmo src/ssreflect.cmo" bin/ssrcoq.byte
|
||||||
-#-custom "$(COQBIN)coqmktop -o bin/ssrcoq.byte src/ssreflect.cmo" "src/ssreflect.cmo bin/ssrcoq" bin/ssrcoq.byte
|
|
||||||
-#-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo"
|
-#-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo"
|
||||||
-#SSRCOQ = bin/ssrcoq
|
-#SSRCOQ = bin/ssrcoq
|
||||||
-#
|
-##
|
||||||
+
|
+## Uncomment for static linking
|
||||||
+-custom "$(COQBIN)coqmktop -opt -o bin/ssrcoq src/ssreflect.cmx" "src/ssreflect.cmx" bin/ssrcoq
|
+#
|
||||||
+-custom "$(COQBIN)coqmktop -o bin/ssrcoq.byte src/ssreflect.cmo" "src/ssreflect.cmo bin/ssrcoq" bin/ssrcoq.byte
|
+-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -opt -o bin/ssrcoq src/ssrmatching.cmx src/ssreflect.cmx" "src/ssrmatching.cmx src/ssreflect.cmx" bin/ssrcoq
|
||||||
|
+-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -o bin/ssrcoq.byte src/ssrmatching.cmo src/ssreflect.cmo" "src/ssrmatching.cmo src/ssreflect.cmo" bin/ssrcoq.byte
|
||||||
+-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo"
|
+-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo"
|
||||||
+SSRCOQ = bin/ssrcoq
|
+SSRCOQ = bin/ssrcoq
|
||||||
+
|
|
||||||
## </static>
|
|
||||||
|
|
||||||
## Uncomment for dynamic linking
|
|
||||||
## <dynamic>
|
|
||||||
-
|
|
||||||
--I src
|
|
||||||
-
|
|
||||||
+#
|
+#
|
||||||
+#-I src
|
|
||||||
+#
|
|
||||||
## </dynamic>
|
|
||||||
|
|
||||||
## What follows should be left untouched by the final user of ssreflect
|
## What follows should be left untouched by the final user of ssreflect
|
||||||
Common subdirectories: old/src and new/src
|
-R theories Ssreflect
|
||||||
Common subdirectories: old/test and new/test
|
|
||||||
Common subdirectories: old/theories and new/theories
|
|
||||||
|
@ -8575,7 +8575,6 @@ let
|
|||||||
spass = callPackage ../applications/science/logic/spass {};
|
spass = callPackage ../applications/science/logic/spass {};
|
||||||
|
|
||||||
ssreflect = callPackage ../applications/science/logic/ssreflect {
|
ssreflect = callPackage ../applications/science/logic/ssreflect {
|
||||||
coq = coq_8_3;
|
|
||||||
camlp5 = ocamlPackages.camlp5_transitional;
|
camlp5 = ocamlPackages.camlp5_transitional;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user