name = "lingenic_text"
version = "1.1.0"
description = "Formally verified Unicode 17.0 text processing library in SPARK/Ada"
long-description = """
Lingenic-Text implements the Unicode 17.0 standard in SPARK/Ada with \
machine-checked correctness proofs on every subprogram. Fourteen algorithm \
modules -- UTF-8 (RFC 3629), grapheme/word/sentence segmentation (UAX #29), \
line breaking (UAX #14), normalization (UAX #15), case mapping, \
collation (UTS #10), the Bidirectional Algorithm (UAX #9), East Asian width \
(UAX #11), emoji (UTS #51), identifiers (UAX #31), and IDNA with Punycode \
(UTS #46) -- each with postconditions verified by GNATprove at Level 4. \
9,214 verification conditions discharged. No pragma Assume. No heap allocation. \
No runtime exceptions. 504,634 conformance test cases passed."""
authors = ["Danslav Slavenskoj <[email protected]>"]
maintainers = ["Danslav Slavenskoj <[email protected]>"]
maintainers-logins = ["Lingenics"]
licenses = "custom-lingenic-source-available-2.3"
website = "https://lingenic.com"
tags = ["unicode", "spark", "verified", "utf8", "text",
"normalization", "segmentation", "bidi", "collation", "idna"]
project-files = ["lingenic_text.gpr"]
[gpr-externals]
MODE = ["build", "prove"]
[gpr-set-externals]
MODE = "build"
[[depends-on]]
gnat = ">=15"