BUILDING

BUILDING AND VERIFICATION
=========================

This document covers building the library, running formal verification,
and executing conformance tests.


TOOLCHAIN REQUIREMENTS
----------------------

  GNAT       15.1.2 or later   Ada 2022 compiler
  GPRBuild   25.0.1 or later   Project-based build system
  GNATprove  15.1.0 or later   SPARK formal verifier

All three are available through Alire (Ada Library Repository).

Toolchain paths (if installed via Alire):

  export PATH="$HOME/.local/share/alire/toolchains/gprbuild_25.0.1_c2b4ada4/bin:$HOME/.local/share/alire/toolchains/gnat_native_15.1.2_60748c54/bin:$HOME/.local/share/alire/toolchains/gnatprove_15.1.0_a4a9bb7c/bin:$PATH"


UCD FILES
---------

Unicode Character Database files must be present in the ucd/ directory.
They are read at runtime by the library's Initialize procedures.

To download UCD files from unicode.org:

  scripts/fetch-ucd.sh

Or manually place the following files in ucd/:

  UnicodeData.txt               Core character data
  Scripts.txt                   Script property
  ScriptExtensions.txt          Script extensions
  GraphemeBreakProperty.txt     Grapheme cluster break
  WordBreakProperty.txt         Word break
  SentenceBreakProperty.txt     Sentence break
  LineBreak.txt                 Line break
  EastAsianWidth.txt            East Asian width
  DerivedBidiClass.txt          Bidi class
  DerivedGeneralCategory.txt    General category
  DerivedJoiningType.txt        Joining type
  DerivedCoreProperties.txt     Core derived properties
  DerivedNormalizationProps.txt Normalization properties
  CaseFolding.txt               Case folding
  SpecialCasing.txt             Special casing
  BidiBrackets.txt              Bidi bracket pairs
  allkeys.txt                   DUCET (collation)
  emoji-data.txt                Emoji properties
  IdnaMappingTable.txt          IDNA mapping table
  PropertyValueAliases.txt      Property value names

Conformance test files (for test programs):

  GraphemeBreakTest.txt
  WordBreakTest.txt
  SentenceBreakTest.txt
  LineBreakTest.txt
  NormalizationTest.txt
  BidiCharacterTest.txt
  emoji-test.txt
  IdnaTestV2.txt
  CollationTest/                Directory with collation test files


BUILDING THE LIBRARY
--------------------

  gprbuild -P lingenic_text.gpr

This produces a static library at lib/lingenic_text.a and object files
in obj/.

Compiler switches (set in lingenic_text.gpr):

  -gnat2022     Ada 2022 standard
  -gnatwa       All warnings enabled
  -gnatwe       Warnings treated as errors
  -gnatVa       All validity checks
  -gnato13      Overflow checks (eliminate, strict)
  -gnatp        Suppress runtime checks (proved by GNATprove)
  -O2           Optimization level 2

Configuration pragmas (build.adc):

  pragma SPARK_Mode (On);
  pragma Assertion_Policy (Ignore);

Assertions are not checked at runtime because the prover has already
verified them.  Runtime checks are suppressed for the same reason.


FORMAL VERIFICATION
-------------------

  gnatprove -P lingenic_text.gpr -XMODE=prove -j0

This runs GNATprove on all source files with the following settings
(from the Prove package in lingenic_text.gpr):

  --level=4             Highest proof effort
  --timeout=60          60-second timeout per verification condition
  --steps=0             No step limit (timeout governs)
  --counterexamples=on  Show counterexamples for failed proofs
  --proof=progressive   Progressive proof strategy

Configuration pragmas for prove mode (gnatprove.adc):

  pragma SPARK_Mode (On);
  pragma Assertion_Policy (Check);

The -j0 flag uses all available CPU cores for parallel proving.

All verification conditions must discharge.  A failed proof means the
code does not build -- there is no "suppress and ship" path.


BUILDING TESTS
--------------

Each test program has its own GPR project file in tests/:

  gprbuild -P tests/test_graphemes.gpr
  gprbuild -P tests/test_words.gpr
  gprbuild -P tests/test_sentences.gpr
  gprbuild -P tests/test_line_break.gpr
  gprbuild -P tests/test_normalization.gpr
  gprbuild -P tests/test_case_mapping.gpr
  gprbuild -P tests/test_collation.gpr
  gprbuild -P tests/test_bidi.gpr
  gprbuild -P tests/test_emoji.gpr
  gprbuild -P tests/test_properties.gpr
  gprbuild -P tests/test_idna.gpr
  gprbuild -P tests/test_grapheme_props.gpr

Test binaries are placed in tests/obj/.


RUNNING TESTS
-------------

Each test program reads UCD conformance test files and compares the
library's output against expected results:

  ./tests/obj/test_graphemes
  ./tests/obj/test_words
  ./tests/obj/test_sentences
  ./tests/obj/test_line_break
  ./tests/obj/test_normalization
  ./tests/obj/test_case_mapping
  ./tests/obj/test_collation
  ./tests/obj/test_bidi
  ./tests/obj/test_emoji
  ./tests/obj/test_properties
  ./tests/obj/test_idna
  ./tests/obj/test_grapheme_props

Each test reports pass/fail counts and exits with status 0 on full pass.

The test programs expect UCD files to be in ucd/ relative to the
current working directory, so run them from the project root.


USING THE LIBRARY
-----------------

To use Lingenic-Text in your own project, add a "with" clause in your
GPR project file:

  with "path/to/lingenic_text.gpr";

Then in your Ada code:

  with Lingenic_Text.Properties;
  with Lingenic_Text.Graphemes;
  with Lingenic_Text.Normalization;
  -- etc.

Initialize modules before use:

  Properties.Initialize ("ucd", Success);
  if Success then
     Normalization.Initialize ("ucd", N_Success);
     -- Use the library...
  end if;

See API_REFERENCE.txt for the full public API.


UPDATING UNICODE VERSION
------------------------

Lingenic-Text reads UCD files at runtime.  To update to a new Unicode
version:

  1. Download new UCD files from https://unicode.org/Public/
  2. Place them in the ucd/ directory (replacing old files)
  3. Rebuild: gprbuild -P lingenic_text.gpr
  4. Re-prove: gnatprove -P lingenic_text.gpr -XMODE=prove -j0
  5. Re-run conformance tests

If the Unicode standard introduces new property values or rule changes,
the ghost specifications may need updating.