nixpkgs/pkgs/development/ada-modules/gnatprove/default.nix

{
  stdenv,
  lib,
  fetchFromGitHub,
  gnat,
  gnatcoll-core,
  gprbuild,
  python3,
  ocamlPackages,
  makeWrapper,
  gpr2,
}:
let
  gnat_version = lib.versions.major gnat.version;

  # gnatprove fsf-14 requires gpr2 from a special branch
  gpr2_24_2_next =
    (gpr2.override {
      # pregenerated kb db is not included
      gpr2kbdir = "${gprbuild}/share/gprconfig";
    }).overrideAttrs
      (old: rec {
        version = "24.2.0-next";
        src = fetchFromGitHub {
          owner = "AdaCore";
          repo = "gpr";
          rev = "v${version}";
          hash = "sha256-Tp+N9VLKjVWs1VRPYE0mQY3rl4E5iGb8xDoNatEYBg4=";
        };
      });

  # TODO:
  # Build why3 (github.com/AdaCore/why3) as separate package and not as submodule.
  # The relevant tags on why3 may get changed without the submodule pointer being updated.

  fetchSpark2014 =
    { rev, hash }:
    fetchFromGitHub {
      owner = "AdaCore";
      repo = "spark2014";
      fetchSubmodules = true;
      inherit rev hash;
    };

  spark2014 = {
    "12" = {
      src = fetchSpark2014 {
        rev = "ab34e07080a769b63beacc141707b5885c49d375"; # branch fsf-12
        hash = "sha256-7pe3eWitpxmqzjW6qEIEuN0qr2IR+kJ7Ssc9pTBcCD8=";
      };
      commit_date = "2022-05-25";
    };
    "13" = {
      src = fetchSpark2014 {
        rev = "12db22e854defa9d1c993ef904af1e72330a68ca"; # branch fsf-13
        hash = "sha256-mZWP9yF1O4knCiXx8CqolnS+93bM+hTQy40cd0HZmwI=";
      };
      commit_date = "2023-01-05";
      patches = [
        # Changes to the GNAT frontend: https://github.com/AdaCore/spark2014/issues/58
        ./0003-Adjust-after-category-change-for-N_Formal_Package_De.patch
      ];
    };
    "14" = {
      src = fetchSpark2014 {
        rev = "ce5fad038790d5dc18f9b5345dc604f1ccf45b06"; # branch fsf-14
        hash = "sha256-WprJJIe/GpcdabzR2xC2dAV7kIYdNTaTpNYoR3UYTVo=";
      };
      patches = [
        # Disable Coq related targets which are missing in the fsf-14 branch
        ./0001-fix-install-fsf-14.patch

        # Suppress warnings on aarch64: https://github.com/AdaCore/spark2014/issues/54
        ./0002-mute-aarch64-warnings.patch

        # Changes to the GNAT frontend: https://github.com/AdaCore/spark2014/issues/58
        ./0003-Adjust-after-category-change-for-N_Formal_Package_De.patch
      ];
      commit_date = "2024-01-11";
    };
    "15" = {
      src = fetchSpark2014 {
        rev = "22bf1510e0829ba74f9d8d686badb65c7365ee91";
        hash = "sha256-KjAWMgMT3Tp/s/DQ20ZZajty9Zrv8aPFocwgv5LkjSw=";
      };
      patches = [
        # Disable Coq related targets which are missing in the fsf-15 branch
        ./0001-fix-install-fsf-15.patch
      ];
      commit_date = "2025-06-10";
    };
  };

  thisSpark =
    spark2014.${gnat_version}
      or (throw "GNATprove depends on a specific GNAT version and can't be built using GNAT ${gnat_version}.");

in
stdenv.mkDerivation {
  pname = "gnatprove";
  version = "fsf-${gnat_version}_${thisSpark.commit_date}";

  src = thisSpark.src;

  patches = thisSpark.patches or [ ];

  nativeBuildInputs = [
    gnat
    gprbuild
    python3
    makeWrapper
  ]
  ++ (with ocamlPackages; [
    ocaml
    findlib
    menhir
  ]);

  buildInputs = [
    gnatcoll-core
  ]
  ++ (with ocamlPackages; [
    ocamlgraph
    zarith
    ppx_deriving
    ppx_sexp_conv
    camlzip
    menhirLib
    num
    re
    sexplib
    yojson
  ])
  ++ (lib.optionals (gnat_version == "14") [
    gpr2_24_2_next
  ])
  ++ (lib.optionals (gnat_version == "15") [
    gpr2
  ]);

  propagatedBuildInputs = [
    gprbuild
  ];

  postPatch = ''
    # gnat2why/gnat_src points to the GNAT sources
    tar xf ${gnat.cc.src} --wildcards 'gcc-*/gcc/ada'
    mv gcc-*/gcc/ada gnat2why/gnat_src
  '';

  configurePhase = ''
    runHook preConfigure
    make setup
    runHook postConfigure
  '';

  installPhase = ''
    runHook preInstall
    make install-all
    cp -a ./install/. $out
    mkdir $out/share/gpr
    ln -s $out/lib/gnat/* $out/share/gpr/
    runHook postInstall
  '';

  meta = with lib; {
    description = "Software development technology specifically designed for engineering high-reliability applications";
    homepage = "https://github.com/AdaCore/spark2014";
    maintainers = [ maintainers.jiegec ];
    license = licenses.gpl3;
    platforms = platforms.all;
  };
}