camlp5_transitional: remove in favor of camlp5 (strict)
This commit is contained in:
parent
eaf0de5985
commit
2fdd38ed2d
@ -27,7 +27,6 @@ let
|
|||||||
"8.8.2" = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd";
|
"8.8.2" = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd";
|
||||||
}."${version}";
|
}."${version}";
|
||||||
coq-version = builtins.substring 0 3 version;
|
coq-version = builtins.substring 0 3 version;
|
||||||
camlp5 = ocamlPackages.camlp5_strict;
|
|
||||||
ideFlags = if buildIde then "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
|
ideFlags = if buildIde then "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
|
||||||
csdpPatch = if csdp != null then ''
|
csdpPatch = if csdp != null then ''
|
||||||
substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
|
substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
|
||||||
@ -37,8 +36,8 @@ self = stdenv.mkDerivation {
|
|||||||
name = "coq-${version}";
|
name = "coq-${version}";
|
||||||
|
|
||||||
passthru = {
|
passthru = {
|
||||||
inherit coq-version camlp5;
|
inherit coq-version;
|
||||||
inherit (ocamlPackages) ocaml findlib num;
|
inherit (ocamlPackages) ocaml camlp5 findlib num;
|
||||||
emacsBufferSetup = pkgs: ''
|
emacsBufferSetup = pkgs: ''
|
||||||
; Propagate coq paths to children
|
; Propagate coq paths to children
|
||||||
(inherit-local-permanent coq-prog-name "${self}/bin/coqtop")
|
(inherit-local-permanent coq-prog-name "${self}/bin/coqtop")
|
||||||
@ -93,7 +92,7 @@ self = stdenv.mkDerivation {
|
|||||||
};
|
};
|
||||||
|
|
||||||
nativeBuildInputs = [ pkgconfig ];
|
nativeBuildInputs = [ pkgconfig ];
|
||||||
buildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib camlp5 ncurses ocamlPackages.num ]
|
buildInputs = [ ncurses ] ++ (with ocamlPackages; [ ocaml findlib camlp5 num ])
|
||||||
++ stdenv.lib.optional buildIde ocamlPackages.lablgtk;
|
++ stdenv.lib.optional buildIde ocamlPackages.lablgtk;
|
||||||
|
|
||||||
postPatch = ''
|
postPatch = ''
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
{ stdenv, fetchFromGitHub, ocaml, findlib, camlp5_strict
|
{ stdenv, fetchFromGitHub, ocaml, findlib, camlp5
|
||||||
, ppx_tools_versioned, ppx_deriving, re
|
, ppx_tools_versioned, ppx_deriving, re
|
||||||
}:
|
}:
|
||||||
|
|
||||||
@ -14,7 +14,7 @@ stdenv.mkDerivation rec {
|
|||||||
|
|
||||||
buildInputs = [ ocaml findlib ppx_tools_versioned ];
|
buildInputs = [ ocaml findlib ppx_tools_versioned ];
|
||||||
|
|
||||||
propagatedBuildInputs = [ camlp5_strict ppx_deriving re ];
|
propagatedBuildInputs = [ camlp5 ppx_deriving re ];
|
||||||
|
|
||||||
createFindlibDestdir = true;
|
createFindlibDestdir = true;
|
||||||
|
|
||||||
|
@ -21277,9 +21277,7 @@ with pkgs;
|
|||||||
|
|
||||||
libpoly = callPackage ../applications/science/logic/poly {};
|
libpoly = callPackage ../applications/science/logic/poly {};
|
||||||
|
|
||||||
prooftree = ocamlPackages.callPackage ../applications/science/logic/prooftree {
|
prooftree = ocamlPackages.callPackage ../applications/science/logic/prooftree { };
|
||||||
camlp5 = ocamlPackages.camlp5_strict;
|
|
||||||
};
|
|
||||||
|
|
||||||
prover9 = callPackage ../applications/science/logic/prover9 { };
|
prover9 = callPackage ../applications/science/logic/prover9 { };
|
||||||
|
|
||||||
|
@ -56,8 +56,7 @@ in rec {
|
|||||||
filterCoqPackages coq self;
|
filterCoqPackages coq self;
|
||||||
|
|
||||||
coq_8_4 = callPackage ../applications/science/logic/coq/8.4.nix {
|
coq_8_4 = callPackage ../applications/science/logic/coq/8.4.nix {
|
||||||
inherit (ocamlPackages_4_02) ocaml findlib lablgtk;
|
inherit (ocamlPackages_4_02) ocaml findlib lablgtk camlp5;
|
||||||
camlp5 = ocamlPackages_4_02.camlp5_transitional;
|
|
||||||
};
|
};
|
||||||
coq_8_5 = callPackage ../applications/science/logic/coq {
|
coq_8_5 = callPackage ../applications/science/logic/coq {
|
||||||
ocamlPackages = ocamlPackages_4_05;
|
ocamlPackages = ocamlPackages_4_05;
|
||||||
|
@ -88,15 +88,10 @@ let
|
|||||||
then callPackage ../development/tools/ocaml/camlp4 { }
|
then callPackage ../development/tools/ocaml/camlp4 { }
|
||||||
else null;
|
else null;
|
||||||
|
|
||||||
camlp5_6_strict = callPackage ../development/tools/ocaml/camlp5 { };
|
camlp5 = callPackage ../development/tools/ocaml/camlp5 { };
|
||||||
|
|
||||||
camlp5_6_transitional = callPackage ../development/tools/ocaml/camlp5 {
|
# Compatibility alias
|
||||||
transitional = true;
|
camlp5_strict = camlp5;
|
||||||
};
|
|
||||||
|
|
||||||
camlp5_strict = camlp5_6_strict;
|
|
||||||
|
|
||||||
camlp5_transitional = camlp5_6_transitional;
|
|
||||||
|
|
||||||
camlpdf = callPackage ../development/ocaml-modules/camlpdf { };
|
camlpdf = callPackage ../development/ocaml-modules/camlpdf { };
|
||||||
|
|
||||||
@ -1042,10 +1037,7 @@ let
|
|||||||
enableX11 = config.unison.enableX11 or true;
|
enableX11 = config.unison.enableX11 or true;
|
||||||
};
|
};
|
||||||
|
|
||||||
hol_light = callPackage ../applications/science/logic/hol_light {
|
hol_light = callPackage ../applications/science/logic/hol_light { };
|
||||||
inherit num;
|
|
||||||
camlp5 = camlp5_strict;
|
|
||||||
};
|
|
||||||
|
|
||||||
};
|
};
|
||||||
in (ocamlPackages.janeStreet // ocamlPackages);
|
in (ocamlPackages.janeStreet // ocamlPackages);
|
||||||
|
Loading…
x
Reference in New Issue
Block a user