[SwayamInSync]

Plan item H3 (a migration guide from 0.1 to 0.2). The release notes describe every change, by area, with examples; a user of 0.1.1 needs the subset that asks something of them, and what to do about each.

Change

New page migrating-to-0.2.rst, listed beside the release notes in the index, in five parts:

• Versions: LLVM 23.1.3 and Z3 4.13.4 unchanged (the Z3 gate keeps 4.13.4, Adopt Z3 releases only through a gate in CI; keep 4.13.4 for 0.2 #135), cvc5 tested from 1.1.2 to 1.4.2, Lean pinned at 4.35.0.
• Source that must change: a clause with two expressions, undefined contracts (with an example and its exact output), verification-only constructs in executable code, trusted declarations and definitions, unsupported member functions, spec templates in hide/reveal, Apple's assertion macros, and clang-format's range footprints.
• Verdicts that change on unchanged source: fixes of wrong results; contracts 0.1.1 ignored that are now verified (members, class invariants, templates, assert, library models, inlined helpers, globals of record and array type, static locals, C++20 rewritten comparisons); one unsupported construct costing only its function; failures that were not real; the warning where facts about specs close a path (which -Werror=cppverify makes an error); budgets; induction after a timeout.
• Command lines: options that select a backend, compiler errors, memory limits, Ctrl-C, archive replay, and the new options.
• Output formats: text (failures as Clang errors, constructs named as C++ names them), compile-time diagnostics and verification before code generation (Verify a compilation before generating its code, never beside it #138), JSON diagnostic/2, archives obligation/6.
• Lean projects: the pin, names by statement hash, a module per function, Lean's precedence, cppverify_auto, and certification.

Also: the release notes' switch entry said [[assume]] was only assumed; it is proved and then assumed, there and in language/functions-loops.rst.

Testing

Every item is taken from release-notes.rst and links the reference page that documents it. The three examples were run with current main (1b4d516) and the guide shows their exact output; docs_examples.test (which checks the verdicts the guide shows) and docs_coverage.test pass with this branch's pages.

#138 (a compilation verifies before generating code) merged, and the guide says so; PRs still open that a user of 0.1 would notice will add their line here when they merge.