知識マップ: Alire で Ada のプロジェクトを始める ── プロジェクト作成、依存の追加、ビルドプロファイル、GNATproveまで

記事「Alire で Ada のプロジェクトを始める ── プロジェクト作成、依存の追加、ビルドプロファイル、GNATproveまで」の主張を、概念と関係(エッジ)に分解した知識グラフの全体です。各関係には根拠・確認日・確度が付いています。

AlireはAdaとSPARKのパッケージマネージャーで、初回のビルドでGNATとGPRbuildを取得し、GPRbuildでビルドする。依存するクレートはマニフェストalire.tomlにセマンティックバージョニングの範囲で書き、ビルドプロファイルもマニフェストやコマンドのスイッチで選ぶ。既定のDevelopmentでは事前条件などの契約が実行時に検査されず、-gnataを含むValidationで検査される。GNATproveもクレートとして入れ、alr gnatproveで契約を証明できる。WindowsではMSYS2から必要なツールとライブラリを入れる。

flowchart LR
    accTitle: Alireでプロジェクトを始める記事の知識マップ
    accDescr: AlireがGNATとGPRbuildを取得して使い、マニフェストalire.tomlで依存とビルドプロファイルを扱い、Validationプロファイルで契約が実行時に検査され、GNATproveをクレートとして入れて証明できること、WindowsではMSYS2を使うことを示す図。
    alire["Alire"]
    ada["Ada(プログラミング言語)"]
    gnat["GNAT"]
    gprbuild["GPRbuild"]
    alire_manifest["Alireのマニフェスト(alire.toml)"]
    semver["セマンティックバージョニング(semver)"]
    alire_build_profile["ビルドプロファイル(Alire)"]
    design_by_contract["契約による設計(Pre/Post)"]
    gnatprove["GNATprove"]
    spark["SPARK"]
    msys2["MSYS2"]
    ada -.->|"で構成できる"| alire
    gnat -.->|"で構成できる"| alire
    alire -->|"利用する"| gprbuild
    alire -->|"利用する"| alire_manifest
    alire_manifest -->|"利用する"| semver
    alire_build_profile -->|"で構成できる"| alire_manifest
    design_by_contract -.->|"で構成できる"| alire_build_profile
    gnatprove -->|"で構成できる"| alire
    design_by_contract -->|"で確認できる"| gnatprove
    spark -->|"利用する"| gnatprove
    alire -.->|"利用する"| msys2

概念間の関係(全11件)

図と同じ関係を文章でも列挙します。表示している文と機械可読な意味データ(RDFa)は同じ要素に載っています。確度が「確立した関係」のものは直接の関係として、「条件付きの関係」のものは成立条件つきの言明(rdf:Statement)として表現しています。

Ada(プログラミング言語)はAlireで構成できます。AlireはAdaとSPARKのパッケージマネージャーで、プロジェクト(クレート)の作成、依存の取得、ツールチェーンの取得、ビルドと実行をalrコマンドで扱う。Adaの開発環境を作る手段の一つである / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
GNATはAlireで構成できます。ツールチェーンが選ばれていなければ、Alireは最初のビルドでgnat_nativeを選んでダウンロードし、alr toolchain --selectで別のバージョンを選べる。システムにあるGNATを使う構成もある / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典出典
AlireはGPRbuildを利用します。alr buildはGPR_PROJECT_PATHなどの環境変数を整えてからGPRbuildを呼び出してビルドする / 確度: 確立した関係 / 確認日: 2026-11-01 出典
AlireはAlireのマニフェスト(alire.toml)を利用します。Alireはクレートのルートにあるalire.tomlから名前・バージョン・依存するクレートを読み、alr withやalr pinはそこに依存や固定を書き足す / 確度: 確立した関係 / 確認日: 2026-11-01 出典出典
Alireのマニフェスト(alire.toml)はセマンティックバージョニング(semver)を利用します。マニフェストのバージョンはセマンティックバージョニングで、依存は^(同じメジャー番号の中)や~(同じマイナー番号の中)の範囲で書く。1.0より前のバージョンでは^と~に特別な扱いはない / 確度: 確立した関係 / 確認日: 2026-11-01 出典
ビルドプロファイル(Alire)はAlireのマニフェスト(alire.toml)で構成できます。クレートごとのビルドプロファイルはマニフェストの[build-profiles]表で指定でき、ルートのクレートはalr buildの--release・--validation・--developmentでも変えられる / 確度: 確立した関係 / 確認日: 2026-11-01 出典
契約による設計(Pre/Post)はビルドプロファイル(Alire)で構成できます。Alireが生成するスイッチのうち、事前条件・事後条件を有効にする-gnataを含むのはValidationだけで、既定のDevelopmentとReleaseでは契約が実行時に検査されない(alr 2.1で確認) / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典出典
GNATproveはAlireで構成できます。GNATproveはalr with gnatproveでクレートとして依存に加えられ、alrに組み込まれた別名alr gnatprove(alr exec -P1 -- gnatprove)で実行できる / 確度: 確立した関係 / 確認日: 2026-11-01 出典
契約による設計(Pre/Post)はGNATproveで確認できます。Pre/Post契約が満たされることはGNATproveの証明で確認できる。事前条件を満たさない呼び出しは実行せずに指摘される / 確度: 確立した関係 / 確認日: 2026-11-01 出典
SPARKはGNATproveを利用します。SPARKコードの検証には、AdaCoreが提供するGNATproveというツールを使う / 確度: 確立した関係 / 確認日: 2026-11-01 出典
AlireはMSYS2を利用します。Windowsでは、最初にalrを実行するとMSYS2を入れるかを聞かれ、Alireはgitやmakeなどのツールと一部のクレートが使う外部ライブラリをMSYS2から入れる。pacmanがPATHにあれば既存のMSYS2を使う / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典

主要概念の定義

Alire: Ada/SPARKのパッケージマネージャー兼ビルドツールで、ツールチェーン(GNAT)の取得・管理も担う。
Ada(プログラミング言語): 1970年代後半にアメリカ国防総省の主導で標準化された、強い型付けと高信頼性を重視する汎用プログラミング言語。最新標準はAda 2022。
GNAT: GCCに含まれる無償のAdaコンパイラで、Adaの代表的な処理系。
Alireのマニフェスト(alire.toml): クレートのルートに置くTOML形式のファイルで、名前・バージョン・依存するクレート・ビルドプロファイルなど、Alireが扱うクレートの情報を書く。
ビルドプロファイル(Alire): Alireがクレートごとに選ぶコンパイラスイッチの組で、Development・Release・Validationの3つがある。既定ではルートのクレートがDevelopment、依存クレートがReleaseになる。
契約による設計(Pre/Post): サブプログラムの入口での前提条件(Pre)と、出口で保証する性質(Post)を宣言的に記述する、Ada 2012の契約機構である。
GNATprove: AdaCoreが提供する、SPARKコードの契約や表明を自動証明器で検証するコマンドラインツールである。
SPARK: プログラムの性質を数学的に証明できるように設計された、Adaのサブセット(部分言語)とそのツール群。

機械可読データ

JSON-LD / Turtle ── この記事の知識グラフ全体
概念一覧 / 語彙(述語)の定義

このデータセットについて

作成: 合同会社小村ソフト
ライセンス: CC BY 4.0 ── 出典(合同会社小村ソフト)とライセンスへのリンクを明示し、改変した場合はその旨を示すことを条件に、再配布・改変を含めて再利用できます
最終確認日: 2026-11-01 ── 収録する関係のうち、最後に出典と照合した日

このページはサイトの知識グラフ(_data/knowledge/)から自動生成されています。誤りの指摘はお問い合わせからお願いします。