diff options
Diffstat (limited to 'nixpkgs/pkgs/development/coq-modules')
6 files changed, 93 insertions, 25 deletions
diff --git a/nixpkgs/pkgs/development/coq-modules/VST/default.nix b/nixpkgs/pkgs/development/coq-modules/VST/default.nix new file mode 100644 index 000000000000..a625aa54c148 --- /dev/null +++ b/nixpkgs/pkgs/development/coq-modules/VST/default.nix @@ -0,0 +1,43 @@ +{ stdenv, fetchFromGitHub, coq, compcert }: + +stdenv.mkDerivation rec { + pname = "coq${coq.coq-version}-VST"; + version = "2.6"; + + src = fetchFromGitHub { + owner = "PrincetonUniversity"; + repo = "VST"; + rev = "v${version}"; + sha256 = "00bf9hl4pvmsqa08lzjs1mrxyfgfxq4k6778pnldmc8ichm90jgk"; + }; + + buildInputs = [ coq ]; + propagatedBuildInputs = [ compcert ]; + + preConfigure = "patchShebangs util"; + + makeFlags = [ + "BITSIZE=64" + "COMPCERT=inst_dir" + "COMPCERT_INST_DIR=${compcert.lib}/lib/coq/${coq.coq-version}/user-contrib/compcert" + "INSTALLDIR=$(out)/lib/coq/${coq.coq-version}/user-contrib/VST" + ]; + + postInstall = '' + for d in msl veric floyd sepcomp progs64 + do + cp -r $d $out/lib/coq/${coq.coq-version}/user-contrib/VST/ + done + ''; + + enableParallelBuilding = true; + + passthru.compatibleCoqVersions = stdenv.lib.flip builtins.elem [ "8.11" ]; + + meta = { + description = "Verified Software Toolchain"; + homepage = "https://vst.cs.princeton.edu/"; + inherit (compcert.meta) platforms; + }; + +} diff --git a/nixpkgs/pkgs/development/coq-modules/bignums/default.nix b/nixpkgs/pkgs/development/coq-modules/bignums/default.nix index 88d7e461a317..f0434c4ae471 100644 --- a/nixpkgs/pkgs/development/coq-modules/bignums/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/bignums/default.nix @@ -29,6 +29,10 @@ let params = { rev = "V8.12.0"; sha256 = "14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8"; }; + "8.13" = { + rev = "V8.13.0"; + sha256 = "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y"; + }; }; param = params.${coq.coq-version}; in @@ -43,7 +47,9 @@ stdenv.mkDerivation { inherit (param) rev sha256; }; - buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ]; + buildInputs = with coq.ocamlPackages; [ ocaml findlib coq ] + ++ stdenv.lib.optional (!stdenv.lib.versionAtLeast coq.coq-version "8.10") camlp5 + ; installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; diff --git a/nixpkgs/pkgs/development/coq-modules/coq-ext-lib/default.nix b/nixpkgs/pkgs/development/coq-modules/coq-ext-lib/default.nix index 9cf30e277f3c..e0ca52086206 100644 --- a/nixpkgs/pkgs/development/coq-modules/coq-ext-lib/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/coq-ext-lib/default.nix @@ -1,17 +1,35 @@ -{ stdenv, fetchFromGitHub, coq }: - -let params = - { - "8.5" = { version = "0.9.4"; sha256 = "1y66pamgsdxlq2w1338lj626ln70cwj7k53hxcp933g8fdsa4hp0"; }; - "8.6" = { version = "0.9.5"; sha256 = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg"; }; - "8.7" = { version = "0.9.7"; sha256 = "00v4bm4glv1hy08c8xsm467az6d1ashrznn8p2bmbmmp52lfg7ag"; }; - "8.8" = { version = "0.11.2"; sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; }; - "8.9" = { version = "0.11.2"; sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; }; - "8.10" = { version = "0.11.2"; sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; }; - "8.11" = { version = "0.11.2"; sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; }; - "8.12" = { version = "0.11.2"; sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; }; +{ stdenv, fetchFromGitHub, coq, ...}@args: + +let + hashes = { + "0.9.4" = "1y66pamgsdxlq2w1338lj626ln70cwj7k53hxcp933g8fdsa4hp0"; + "0.9.5" = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg"; + "0.9.7" = "00v4bm4glv1hy08c8xsm467az6d1ashrznn8p2bmbmmp52lfg7ag"; + "0.10.0" = "1kxi5bmjwi5zqlqgkyzhhxwgcih7wf60cyw9398k2qjkmi186r4a"; + "0.10.1" = "0r1vspad8fb8bry3zliiz4hfj4w1iib1l2gm115a94m6zbiksd95"; + "0.10.2" = "1b150rc5bmz9l518r4m3vwcrcnnkkn9q5lrwygkh0a7mckgg2k9f"; + "0.10.3" = "0795gs2dlr663z826mp63c8h2zfadn541dr8q0fvnvi2z7kfyslb"; + "0.11.1" = "0dmf1p9j8lm0hwaq0af18jxdwg869xi2jm8447zng7krrq3kvkg5"; + "0.11.2" = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; + "0.11.3" = "1w99nzpk72lffxis97k235axss5lmzhy5z3lga2i0si95mbpil42"; }; - param = params.${coq.coq-version}; + + default-versions = { + "8.5" = "0.9.4"; + "8.6" = "0.9.5"; + "8.7" = "0.9.7"; + "8.8" = "0.11.3"; + "8.9" = "0.11.3"; + "8.10" = "0.11.3"; + "8.11" = "0.11.3"; + "8.12" = "0.11.3"; + }; + + param = rec { + version = args.version or default-versions.${coq.coq-version}; + sha256 = hashes.${version}; + }; + in stdenv.mkDerivation rec { @@ -20,14 +38,13 @@ stdenv.mkDerivation rec { inherit (param) version; src = fetchFromGitHub { - owner = "coq-ext-lib"; + owner = "coq-community"; repo = "coq-ext-lib"; - rev = "v${param.version}"; + rev = "v${version}"; inherit (param) sha256; }; - buildInputs = with coq.ocamlPackages; [ ocaml camlp5 ]; - propagatedBuildInputs = [ coq ]; + buildInputs = [ coq ]; enableParallelBuilding = true; @@ -41,6 +58,6 @@ stdenv.mkDerivation rec { }; passthru = { - compatibleCoqVersions = v: builtins.hasAttr v params; + compatibleCoqVersions = v: builtins.hasAttr v default-versions; }; } diff --git a/nixpkgs/pkgs/development/coq-modules/dpdgraph/default.nix b/nixpkgs/pkgs/development/coq-modules/dpdgraph/default.nix index 54654f37bac8..195a1c4eada5 100644 --- a/nixpkgs/pkgs/development/coq-modules/dpdgraph/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/dpdgraph/default.nix @@ -53,7 +53,8 @@ stdenv.mkDerivation { nativeBuildInputs = [ autoreconfHook ]; buildInputs = [ coq ] - ++ (with coq.ocamlPackages; [ ocaml camlp5 findlib ocamlgraph ]); + ++ (with coq.ocamlPackages; [ ocaml findlib ocamlgraph ] + ++ stdenv.lib.optional (!stdenv.lib.versionAtLeast coq.coq-version "8.10") camlp5); # dpd_compute.ml uses deprecated Pervasives.compare # Versions prior to 0.6.5 do not have the WARN_ERR build flag diff --git a/nixpkgs/pkgs/development/coq-modules/mathcomp/default.nix b/nixpkgs/pkgs/development/coq-modules/mathcomp/default.nix index 8cf502a1943b..542fac861c58 100644 --- a/nixpkgs/pkgs/development/coq-modules/mathcomp/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/mathcomp/default.nix @@ -66,6 +66,7 @@ let ####################################################################### # sha256 of released mathcomp versions sha256 = { + "1.12.0" = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp"; "1.11.0" = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c"; "1.11+beta1" = "12i3zznwajlihzpqsiqniv20rklj8d8401lhd241xy4s21fxkkjm"; "1.10.0" = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv"; @@ -76,6 +77,7 @@ let }; # versions of coq compatible with released mathcomp versions coq-versions = { + "1.12.0" = flip elem [ "8.13" ]; "1.11.0" = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; "1.11+beta1" = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; "1.10.0" = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" ]; @@ -96,7 +98,7 @@ let # mathcomp preferred versions by decreasing order # (the first version in the list will be tried first) version-preferences = - [ "1.10.0" "1.11.0" "1.9.0" "1.8.0" "1.7.0" "1.6.1" ]; + [ "1.12.0" "1.10.0" "1.11.0" "1.9.0" "1.8.0" "1.7.0" "1.6.1" ]; # list of core mathcomp packages sorted by dependency order packages = _version: # unused in current versions of mathcomp diff --git a/nixpkgs/pkgs/development/coq-modules/paco/default.nix b/nixpkgs/pkgs/development/coq-modules/paco/default.nix index e8958fa1ada5..ac6eef2f3bd0 100644 --- a/nixpkgs/pkgs/development/coq-modules/paco/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/paco/default.nix @@ -9,8 +9,8 @@ let }; post_8_6 = rec { rev = "v${version}"; - version = "4.0.0"; - sha256 = "1ncrdyijkgf0s2q4rg1s9r2nrcb17gq3jz63iqdlyjq3ylv8gyx0"; + version = "4.0.2"; + sha256 = "1q96bsxclqx84xn5vkid501jkwlc1p6fhb8szrlrp82zglj58b0b"; }; }; params = { @@ -36,8 +36,7 @@ stdenv.mkDerivation rec { repo = "paco"; }; - buildInputs = with coq.ocamlPackages; [ ocaml camlp5 unzip ]; - propagatedBuildInputs = [ coq ]; + buildInputs = [ coq ]; preBuild = "cd src"; |