sparklib_internal.gpr

with "sparklib_common";

project SPARKlib_Internal is

   for Externally_Built use SPARKlib_common.SPARKlib_Installed;

   -- This project is not supposed to be used directly. Instead, copy
   -- sparklib.gpr.templ as sparklib.gpr in your code and provide
   -- appropriate values for the object directory Object_Dir (so that
   -- compilation and artifacts are generated in directories under your
   -- control) and the list of excluded source files Excluded_Source_Files
   -- (so that you only compile and analyse files from the library that
   -- you need).

   case SPARKlib_common.SPARKlib_Installed is
      when "True" =>
         for Source_Dirs use (SPARKlib_Internal'Project_Dir & "/../../include/spark");
      when others =>
         for Source_Dirs use (SPARKlib_Internal'Project_Dir & "/src");
         for Object_Dir use "obj";
   end case;

   SPARK_Body_Mode : SPARKlib_common.SPARK_Body_Mode_T := SPARKlib_common.SPARK_Body_Mode;

   package Compiler is
      --  Enforce GNAT style checks, except for multiple blank lines which does
      --  not work for preprocessed files, and alphabetical ordering of
      --  subprogram bodies (although not applicable to null subprograms).
      for Default_Switches ("Ada") use
         ("-gnat2022", "-gnatygo-u", "-gnata",
	  "-gnatwI",  --  disable warnings about SPARKlib using GNAT internal units
          "-gnateDSPARK_BODY_MODE=" & SPARK_Body_Mode);
   end Compiler;

   package Prove renames SPARKlib_common.Prove;

   Common_Excluded_Source_Files :=
     ("spark-big_integers__light.ads",
      "spark-big_integers__light.adb",
      "spark-big_intervals__light.ads",
      "spark-big_reals__light.adb",
      "spark-big_reals__light.ads",
      "spark-containers-functional-base__light.ads",
      "spark-containers-functional-infinite_sequences__light.ads",
      "spark-containers-functional-maps__light.ads",
      "spark-containers-functional-multisets__light.ads",
      "spark-containers-functional-sets__light.ads",
      "spark-containers-functional-vectors__light.ads",
      "spark-containers-types__light.ads");

   case SPARK_Body_Mode is
      when "On" =>
         for Excluded_Source_Files use Common_Excluded_Source_Files
                                       & ("spark.ads");
      when "Off" =>
         for Excluded_Source_Files use Common_Excluded_Source_Files
                                       & ("spark__exec.ads");
   end case;

   package Naming is
      case SPARK_Body_Mode is
         when "On" =>
            for Spec ("SPARK") use "spark__exec.ads";
         when "Off" =>
            null;
      end case;
   end Naming;

end SPARKlib_Internal;