Repository navigation
Conversation
Example output can change between executions because of addresses, clocks, random values or task scheduling. During toolchain updates, these differences can resemble compiler regressions. Add `ada-run-expect-variable-output` as structured metadata so reviewers can distinguish expected variation from regressions when comparing toolchain versions. Extraction produces identical files with and without the annotation. Co-Authored-By: Claude <noreply@anthropic.com> Co-Authored-By: Codex <noreply@openai.com>
GNAT 16 rejects the original literal aspect functions because those declared in `Main` are not primitive operations of `My_Type`. Move the type and literal functions into the `My_Types` package specification and import the package from `Main` in both examples. Both examples build and run with GNAT 16.1, producing unchanged output. Co-Authored-By: Claude <noreply@anthropic.com> Co-Authored-By: Codex <noreply@openai.com>
GNAT 16 rejects positional boxes in the two signature-package examples. Ada RM 12.7 requires named notation for these boxed associations. Use `P => <>` and `Hash => <>` to leave the subprogram actuals unconstrained while binding the formal type to `T`. Both corrected examples pass GNAT 16.1; the positional forms fail with "box requires named notation". Co-Authored-By: Claude <noreply@anthropic.com> Co-Authored-By: Codex <noreply@openai.com>
GNATprove 16 reports that `External_Variable` is not written by `Configuration`, despite its `Initializes` contract. Reading it to initialize `Max` during `Stack` elaboration requires this contract; removing it also fails flow analysis. Initialize the non-imported variable to a valid `Positive` value. `Max` still has variable input and must remain in `The_Stack`'s state refinement. Flow analysis passes with GNATprove 15 and 16. Removing the initializer fails with 16; removing `Max` from the refinement still fails with 16. Co-Authored-By: Claude <noreply@anthropic.com> Co-Authored-By: Codex <noreply@openai.com>
Six container aggregate examples and two SPARK contract examples pass with the GNAT 16 toolchain. Remove their GNAT 14.2 and GNATprove 14.1 pins and restore the run/prove buttons. All eight blocks pass the pipeline checks with GNAT/GNATprove 16.1 and GPRbuild 26, including the expected contract diagnostic. Co-Authored-By: Claude <noreply@anthropic.com> Co-Authored-By: Codex <noreply@openai.com>
GNAT 16 no longer reports the ghost-use diagnostics discussed in the ring-buffer examples 2 and 4. Pin both examples to the GNAT 15 toolchain to preserve their expected errors and the accompanying explanations. Replace compile/prove buttons with classes that keep pipeline checks active while disabling the buttons for the default toolchain. Both examples pass the checks with the pinned GNAT/GNATprove 15 and GPRbuild 25 toolchain. Co-Authored-By: Claude <noreply@anthropic.com> Co-Authored-By: Codex <noreply@openai.com>
Use GNAT and GNATprove 16.1 with GPRbuild 26 for unpinned examples. Keep older versions required by the remaining example pins, and remove unreferenced GNATprove 14.1 and GPRbuild 22/24 releases. Validated 18 files with 537 passing block reports on the updated worktree VM, including all five pinned examples. Co-Authored-By: Claude <noreply@anthropic.com> Co-Authored-By: Codex <noreply@openai.com>
Recognize `ada-run-expect-variable-output` as widget metadata so Sphinx can render examples that mark expected output variation. Preserve the widget's existing buttons and execution behavior. Validated the full HTML build with warnings treated as errors, the existing parser suite, TypeScript tests, and LaTeX/EPUB fixtures. Co-Authored-By: Claude <noreply@anthropic.com> Co-Authored-By: Codex <noreply@openai.com>
Assign `Show_Cat` and `Show_Geo_Forms` to the projects containing their package declarations so extraction includes the required `Animals` and `Geo_Forms` units. The object-oriented chapter check passes with GNAT 16.1 and GPRbuild 26. Co-Authored-By: Claude <noreply@anthropic.com> Co-Authored-By: Codex <noreply@openai.com>
Express `Set`'s dependency as `Ext => Ext`. The volatile objects `X` and `Y` overlay elements of `Ext`, so the contract describes the underlying array read and updated by `Set`. Co-Authored-By: Claude <noreply@anthropic.com> Co-Authored-By: Codex <noreply@openai.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Use GNAT and GNATprove 16.1 with GPRbuild 26 by default, and adapt
the examples to the checks enforced by the updated toolchain.
functions primitive operations, and initialize the volatile
configuration variable to satisfy its
Initializescontract.Pin two ghost-code examples to GNAT 15 to preserve the diagnostics
discussed in their explanations.
ada-run-expect-variable-outputto identifyexpected output variation during toolchain comparisons.
unreferenced versions.
Validation on the VM: covered 18 content files with 537 passing
block reports, plus targeted checks of the revised examples.
Variable-output annotations leave extracted sources unchanged.
Co-Authored-By: Claude noreply@anthropic.com
Co-Authored-By: Codex noreply@openai.com