「‍」 Lingenic

lingenic_text

(⤓.gpr ◇.gpr); γ ≜ [2026-07-12T135544.192, 2026-07-12T135544.192] ∧ |γ| = 1

--  Copyright © 2026 Lingenic LLC. All rights reserved.
--  Licensed under the Lingenic Source-Available License v2.3.
--  Production use requires a separate license from Licensor.
--  See LICENSE.md and COPYRIGHT in the project root.
--

project Lingenic_Text is

   for Source_Dirs use ("src");
   for Object_Dir use "obj";
   for Library_Name use "lingenic_text";
   for Library_Dir use "lib";
   for Library_Kind use "static";

   --  Mode: "prove" for gnatprove, "build" for gprbuild (default)
   type Mode_Type is ("prove", "build");
   Mode : Mode_Type := external ("MODE", "build");

   package Compiler is
      for Default_Switches ("Ada") use
         ("-gnat2022",       --  Ada 2022 standard
          "-gnatwa",         --  All warnings
          "-gnatwe",         --  Warnings as errors
          "-gnatVa",         --  All validity checks
          "-gnato13",        --  Overflow checks (eliminate, strict)
          "-gnatp",          --  Suppress all checks (proved by gnatprove)
          "-O2");            --  Optimization
   end Compiler;

   package Prove is
      for Proof_Switches ("Ada") use
         ("--level=4",
          "--timeout=60",
          "--steps=0",
          "--counterexamples=on",
          "--proof=progressive");
   end Prove;

   package Builder is
      case Mode is
         when "prove" =>
            for Global_Configuration_Pragmas use "gnatprove.adc";
         when others =>
            for Global_Configuration_Pragmas use "build.adc";
      end case;
      for Default_Switches ("Ada") use ("-j0");
   end Builder;

end Lingenic_Text;