Commit a2f49d26 authored by Vincent Laporte's avatar Vincent Laporte Committed by Vincent Laporte
Browse files

compcert: add support for Coq 8.20.0

parent 031c0e9b

pkgs/development/coq-modules/compcert/default.nix

+7 −2
Original line number Diff line number Diff line
@@ -29,7 +29,7 @@ compcert = mkCoqDerivation { 
  releaseRev = v: "v${v}";



  defaultVersion =  with lib.versions; lib.switch coq.version [

      { case = range "8.14" "8.19"; out = "3.14"; }

      { case = range "8.14" "8.20"; out = "3.14"; }

      { case = isEq "8.13"        ; out = "3.10"; }

      { case = isEq "8.12"       ; out = "3.9"; }

      { case = range "8.8" "8.11"; out = "3.8"; }
@@ -201,13 +201,18 @@ patched_compcert = compcert.overrideAttrs (o: 
          })

        ];

      }

      { cases = [ (isEq "8.19") (isEq "3.14") ];

      { cases = [ (range "8.19" "8.20") (isEq "3.14") ];

        out = [

          # Support for Coq 8.19.2

          (fetchpatch {

            url = "https://github.com/AbsInt/CompCert/commit/8fcfb7d2a6e9ba44003ccab0dfcc894982779af1.patch";

            hash = "sha256-m/kcnDBBPWFriipuGvKZUqLQU8/W1uqw8j4qfCwnTZk=";

          })

          # Support for Coq 8.20.0

          (fetchpatch {

            url = "https://github.com/AbsInt/CompCert/commit/20a5b48758bf8ac18e4c420df67017b371efc237.patch";

            hash = "sha256-TJ87CvLiAv1absGnPsTXsD/HQwKgS82loUTcosulyso=";

          })

        ];

      }

    ] [];

pkgs/top-level/all-packages.nix

+1 −1
Original line number Diff line number Diff line
@@ -14508,7 +14508,7 @@ with pkgs; 
    ocamlPackages = ocaml-ng.ocamlPackages_4_14;

  };













  inherit (coqPackages_8_19) compcert;













  inherit (coqPackages) compcert;





























  computecpp-unwrapped = callPackage ../development/compilers/computecpp { };















  computecpp = wrapCCWith rec {