Rossi v0.2.3

Added

• (parse) Parse infix extension operators as one operator group
• (parse) Resolve prefix and nullary extension operators
• (build) Check runtime suitability of nondeterministic actions
• (lint) Warn on a section written out of order
• (formula) Spell parametric types as type-constructor expressions
• (pretty) Print extended operators by their notation
• (formula) Index a factory's extensions by symbol
• (parse) Accept Rodin's identifier character classes
• (build) Check finiteness in the runtime suitability pass
• (lsp) Serve proof obligations with their proof status
• (build) Check actions, guards and refinement in the runtime pass
• (build) Check what the contexts leave open in the runtime pass
• (build) Register the section-order rule
• (lsp) Let the client cancel the Rodin and animate flows
• (lsp) Tag dead variables as unnecessary
• (lsp) Move the server onto tower-lsp-server
• (lsp) Link duplicate component findings to the other declarations
• (lsp) Go to the carrier sets of a symbol's type
• (lsp) Rename a component when its file is renamed
• (lsp) Format a selected range
• (lsp) Serve semantic tokens for a range
• (lsp) Serve an obligation's sequent as rossi/proofState
• (lsp) Publish the project static check as diagnostics
• (lsp) Go to the events and machines that refine the cursor
• (lsp) Expose the refinement graph as a type hierarchy
• (lsp) Serve pull diagnostics for documents and the workspace
• (lsp) Highlight occurrences of the symbol under the cursor
• (lsp) Offer to move a section written out of order

Changed

• (parse) Thread a formula factory through the AST builder
• (parse) Derive the context and machine section order from the keyword table
• (lsp) Spell URIs through as_str rather than Display

Fixed

• (build) Type axioms, invariants and guards in source order
• (parse) Take one identifier in the basic set comprehension form
• (parse) Require parentheses on the power-set operators
• (parse) Refuse a bare quantifier under negation
• (xml) Keep the first event node when a file repeats an internal name
• (parse) Read integer literals of any size
• (parse) Accept partition with a single argument
• (parse) Restore the parser scopes when a parse unwinds
• (lsp) Publish once on open and push proof status off the handler
• (lsp) Index every workspace folder, and follow folder changes

Documentation

• (lsp) Correct the crate README's feature and diagnostics claims

Rossi v0.2.2

Added

• (cli) Restrict a dump to named components
• (cli) Add the dump subcommand
• (fmt) Add an opt-in private-use-glyph output mode
• (build) Reject a declared name that carries a prime
• (cli) Clean orphaned and broken proofs from a project
• (formula) Expose binder-name resolution
• (xml) Declare UTF-8 encoding in exported Rodin projects
• (pretty) Keep comments where the source put them
• (parse) Give variants a comment field
• (ast) Record where a skip action is written
• (ast) Give a machine variant its source span
• (build) Locate WD conditions by source
• (ast) Identify the source a span indexes
• (formula) Enumerate a predicate's propositional leaves
• (prove) Rewrite a proof file's entries in place
• (build) Keep a previous file's declaration order when regenerating
• (build) Publish the rossi-model JSON schema
• (build) Assemble the checked model into a dump document
• (build) Add the rossi-model formula converter
• (editors) Expose the rossi.rodin.provingPerspective setting
• (lsp) Open Rodin in the Proving perspective on request
• (editors) Expose the rossi.rodin.liveSync setting
• (lsp) Merge Rodin's unsaved edits into the buffer
• (lsp) Receive what the Rodin bridge pushes
• (lsp) Register the Rodin project through its bridge plug-in
• (lsp) Honour privateUseGlyphs across formatting and assistance
• (lsp) Filter operator completions on word aliases

Changed

• (build) Name the component a finding and a severity belong to
• (cli) Share the project-name helpers between build and dump
• (cli) Move the structured-output report to its own module
• (cli) Share the prove command's obligation classification
• (pretty) Thread an output sink through the print helpers
• (lsp) Take a merge's inputs rather than reading them
• (lsp) Resolve document symbols through the line index

Fixed

• (parse) Preserve camille labels verbatim
• (build) Report a primed identifier nothing can declare
• (pretty) Keep a nested same-operator child parenthesized
• (pretty) Space Rodin's binary operators the way its printer does
• (xml) Emit the comment attribute on witnesses
• (parse) Span the primed declarations an action's lowering derives
• (parse) Reject an annotation that does not denote a type
• (formula) Read a type spelling the way Rodin's parser does
• (lsp) Mask names by the grammar's own list and whitespace rules
• (lsp) Keep component and event names out of the operator rewrite
• (parse) Treat bool as the closed operator word it is
• (parse) Reject a math keyword as a predicate-application head
• (build) Ascribe generic atoms the way Rodin's typed printer does
• (build) Place an inherited element in the file that wrote it
• (lsp) Reload Rodin's editors when the lens rebuilds
• (lsp) Keep a Rodin session from deleting derived proof files
• (lsp) Preserve complete label names
• (lsp) Point the variant outline row at the variant
• (lsp) Point declaration symbols at their declaration

Documentation

• Correct the subcommand tables
• Describe rossi clean in the READMEs
• (lsp) Document the documentSymbol and settings contract

Rossi v0.2.1

Added

• (import) Merge components in dependency order
• (parse) Require a label on every predicate and action
• (lint) Warn on separators stock Camille cannot read (EB031)
• (cli) Report an empty clause and a clause order as EB029 and EB030
• (lint) Warn when a declared name spells a structural keyword
• (build) Compute proof statuses in repack by default
• (cli) Replay proofs in the prove command
• (cli) Add a prove command reporting proof status
• (deps) Order components for a single merged document
• (lsp) Offer to remove an empty clause and to move a misplaced one
• (parse) Report an event clause written out of order
• (parse) Report an empty clause and a bare label where they are
• (parse) Summarize a parse error's expected set by category
• (lsp) Flag ASCII operator spellings behind rossi.format.enforceUnicode
• (lsp) Add a source.fixAll.rossi operator normalization action
• (prove) Auto-rewrite driver and type rewrites
• (prove) Stream .bpr proof files into stored proofs
• (ast) Parse canonical type strings back into Type
• (prove) The small remaining reasoners
• (prove) Negation and membership removal
• (prove) Override splits, image goals and the one-point rule
• (prove) Domain, image and bounded-goal reasoners
• (prove) Partition rewrites and the manual-rewrite shape
• (prove) The generalized modus ponens reasoner
• (prove) The level-5 auto rewriter
• (prove) Input-bearing inference reasoners
• (prove) Core structural reasoners
• (prove) Proof builder with reuse, replay, and rebuild
• (prove) Proof status verdicts and the .bps model
• (prove) Load .bpo sequents into prover sequents
• (prove) Proof dependency analysis and the reuse predicate
• (prove) Reasoner descriptors and the versioned registry
• (prove) Proof rules, hyp actions, and proof trees
• (prove) Scaffold the crate with sequents and confidence
• (build) Register the missing-label rule
• (build) Register the empty-clause and clause-order rules
• (lsp) Refresh the workspace index on watched-file changes
• (build) Compute proof statuses at the reconcile boundary
• (lsp) Offer to write the label an item is missing
• (lsp) Report components duplicated within one file
• (lsp) Register the .eventb file watcher with the client

Changed

• (cli) Allocate through mimalloc
• (lsp) Keep the index off the edit path when nothing moved
• (cli) Walk source trees through the shared walker
• (cli) Check components in parallel in prove
• (cli) Reuse the proof-file walkers in prove's collection
• (parse) Move span clearing into the AST
• (parse) Derive event-clause boundary sets from the grammar follow-set
• (prove) Share type-checked intern entries across a file's proofs
• (prove) Share type environments across a proof's intern entries
• (ast) Parse canonical type strings without the formula parser
• (ast) Move type-ascription stripping into the formula layer
• (prove) Edit owned sequents in place across an antecedent's actions
• (prove) Copy only the hypothesis sets a proof step changes
• (prove) Parse each distinct intern formula once per proof file
• (prove) Hand out proofs as the .bpr streams
• (prove) Read only the intern entries the dependencies name
• (prove) Load each hypothesis set once per project
• (prove) Drop constant plumbing and share the crate's helpers
• (build) Share one Event-B source predicate
• (build) Update statuses per component in parallel
• (build) Classify through the shared bucket type
• (lsp) Give the cross-reference index disk and open layers
• (lsp) Record every file that declares a component name
• (lsp) Key both workspace indexes by canonical URI

Fixed

• (cli) Match the Rodin XML build gate to the project loader
• (cli) Single-source the prove command's confidence classification
• (build) Discover only direct-child sources as components
• (xml) Name an element that carries no label
• (parse) Read an implicit comprehension's member in a closed scope
• (parse) Reject a set comprehension that binds nothing
• (lsp) Keep label text intact when converting operators
• (parse) Bind unary minus at additive precedence
• (prove) Resolve parent-set handles inside the referring file's directory
• (lsp) Read eventb-animate's v4 report
• (lsp) Hover a declared name that spells a keyword as the name
• (lsp) Let a declared name that spells a keyword be renamed

Documentation

• Describe rossi-prove in the READMEs
• (lsp) Record why the project rebuild skips the status update

Rossi v0.2.0

Added

• (cli) Serve the language server only from eventb-language-server
• (cli) Wrap at 120 columns by default
• (fmt) Wrap formulas at a configurable maximum line width
• (fmt) Make camille the default formatting style
• (cli) Expose the formatter style preset and toggles
• (fmt) Add the camille formatting style to the pretty printer
• (fmt) Expose wrapped formula-level predicate printing
• (build) Expose a static-check-only entry point with the typed model
• (lsp) Log animate failures and shorten the tool-failure toast
• (lsp) Publish the static errors behind the animate build gate
• (lsp) Turn animate verdict errors into diagnostics
• (lsp) Render PO counterexamples one binding per line
• (lsp) Render animate counterexample states one binding per line
• (lsp) Mark well-definedness conditions with inlay hints
• (lsp) Serve declaration type inlay hints
• (lsp) Map rossi.format.maxLineWidth to the formatter
• (lsp) Map rossi.format style settings to the formatter

Changed

• (build) Move Rodin workspace helpers from eventb-lsp
• (build) Return structured well-definedness conditions
• (lsp) Collect document-link source lines once

Fixed

• (cli) End formatted text with exactly one newline
• (fmt) Print one-per-line any parameters without requiring comments
• (lsp) Wrap WD inlay-hint tooltips at the configured width
• (lsp) Resolve benchmark sites from the AST, not printed text

Rossi v0.1.9

Added

• (build) Stamp a .project descriptor into text-built source archives
• (cli) Import proof files next to the generated text
• (cli) Add export --build and --proofs
• (cli) Preserve proof state in directory and flat-archive builds
• (build) Emit proof-obligation files from the build
• (validate) Surface proof status in text, JSON and SARIF output
• (validate) Surface EB010 with --show-info
• (parse) Accept multiple event refinement targets
• (parse) Accept labeled and repeatable machine variants
• (formula) Derive before-after and feasibility predicates for assignments
• (wd) Emit EB010 from checked formulas
• (lsp) Sync Rodin model edits back into the sources automatically
• (build) Preserve proofs and carry stamps when repacking archives
• (pog) Reconcile regenerated obligations with previous proof state
• (pog) Parse obligation stamps and expose semantic equality in the po view
• (pog) Emit merged guard-strengthening obligations
• (build) Check merged events statically
• (pog) Emit lexicographic variant obligations
• (build) Check every labeled variant
• (pog) Emit convergence obligations
• (pog) Emit guard strengthening and simulation obligations
• (pog) Emit witness obligations and refined-event invariants
• (pog) Emit action and invariant preservation obligations
• (pog) Build event hypotheses and guard obligations
• (pog) Build machine hypotheses, invariant and variant obligations
• (pog) Emit context proof obligations
• (pog) Model proof-obligation files and hypothesis chains
• (build) Add typed closure lookups to the checked model
• (build) Report proof status from Rodin proof files
• (lsp) Mirror workspace proofs back beside the sources when Rodin exits
• (lsp) Seed text-adjacent proof files into the Rodin project at lens start
• (lsp) Catch up on Rodin model edits at watcher startup
• (lsp) Rebuild the shared Rodin project on save
• (lsp) Watch the Rodin workspace and surface proof status live
• (lsp) Serve Open in Rodin as CodeLens + executeCommand
• (lsp) Add the Rodin workspace build, launch, and lock core

Changed

• (lsp) Host the .rossi/rodin reverse lookup beside its naming convention
• (build) Route export --build through the text-to-project doors
• (cli) Hoist the shared build pipeline into build_common
• (build) Share the text-to-project assembly between the CLI and the LSP
• (parse) Tighten the AST layer after review
• (build) Simplify the checker and generator internals
• (lsp) Derive the pretty-printer from one FormatConfig mapping

Fixed

• (cli,lsp) Skip dot-directories when collecting source files
• (parse) Reject nonstandard set declarations
• (build) Keep theorem guards over variables disappearing here
• (lsp) Hold the Open in Rodin single-flight until Rodin takes the lock
• (lsp) Seed Rodin workspace preferences without clobbering foreign keys
• (lsp) Harden and streamline the Rodin sync loop
• (lsp) Create the Rodin workspace watcher off the request path

Documentation

• (cli) Document the proof round-trip through import and export

Rossi v0.1.8

Added

• (pretty) Render the new formula model
• (validate) Expose joined path in JSON output
• (ast) Lower parsed formulas onto the typed model
• (ast) Scope-aware occurrence walker for the new formula model
• (ast) Add datatype extensions with constructors and destructors
• (ast) Add operator extension mechanism with dynamic tags
• (ast) Simplify well-definedness lemmas by antecedent subsumption
• (ast) Add well-definedness lemma computation
• (ast) Add two-pass type checking with unification
• (ast) Add path-based subformula positions
• (ast) Add fresh-name resolution for bound identifiers
• (ast) Add formula rewriter and substitution infrastructure
• (ast) Synthesize node types bottom-up at construction
• (ast) Add immutable formula nodes with factory construction
• (ast) Add mathematical type hierarchy and type environments
• (ast) Add formula tag constants and operator kind enums
• (build) Expose typed formulas through the checked model
• (build) Gate formulas through the two-pass checker
• (build) Type declarations with the two-pass checker

Changed

• (parser) Build the formula model directly and drop the legacy tree
• (ast) Make the legacy formula tree parser-internal
• (ast) Route all formulas through the typed model
• (build) Render canonical text from typed formulas
• (ast) Move the legacy formula types behind an ast::legacy module
• (ast) Allow multiple targets in membership assignments
• (build) Type extended-event scopes from inherited decls
• (build) Derive canonical formula text at render time
• (build) Adopt the core mathematical types throughout
• (build) Drop the superseded inference and enrichment passes
• (build) Retire the well-typedness façade
• (build) Funnel identifier typing through a single seam

Fixed

• (validate) Retain ruleless failures in SARIF
• (validate) Reject directories without components
• (ast) Scope implicit comprehension binders everywhere they bind

Rossi v0.1.7

Added

• (validate) Fail on advisory lints with --deny-warnings
• (validate) Tag SARIF runs with --sarif-category
• (validate) Write the report to --output

Fixed

• (validate) Report directory parse failures per component file
• (validate) Render directory members as real paths
• (build) Validate inherited event render state

Rossi v0.1.6

Added

• (build) Expose project archive entry classification

Fixed

• (build) Decode checked project names

Rossi v0.1.5

Added

• (parse) Add Rodin-canonical formula spacing
• (parse) Expose shared syntax snapshot queries

Changed

• (lsp) Unify component cursor resolution
• (lint) Reuse dependency graph identities
• (parse) Shift spans through AST visitors
• (xml) Share ZIP entry parsing
• (parse) Encode single-argument applications
• Remove dead code
• (build) Emit canonical formulas during printing
• (build) Group event check state
• (lsp) Share candidate dependency environments
• (lsp) Extract component occurrence service

Fixed

• (build) Reject ill-typed expressions before emission
• (cli) Reject colliding fmt output paths
• (parse) Enforce parallel assignment arity
• (cli) Handle structured output failures
• (cli) Show errors in quiet continue mode
• (cli) Raw-copy retained formatted ZIP entries
• (cli) Contain loose build output paths
• (cli) Propagate recursive input scan errors
• (build) Reject inherited event label conflicts
• (parse) Reset prefix depth across connective operands
• (lsp) Make component rename and references syntax-aware
• (parse) Shift sliced errors to absolute locations
• (lsp) Scope keyword completions structurally
• (lsp) Centralize dependency environments
• (parse) Align recovery identifier validation
• (xml) Parse project names with quick-xml
• (xml) Emit Rodin operator glyphs in source files
• (build) Retain enriched machine formula ASTs
• (build) Journal insert-if-absent bindings
• (build) Enrich predicates inside bool expressions
• (build) Raw-copy retained ZIP entries
• (build) Propagate project directory scan errors
• (build) Reject conflicting event parameters
• (build) Mask outer types during binder inference
• (build) Preserve Rodin checked element identities
• (lsp) Derive signature help from shared syntax
• (lsp) Batch selection ranges on shared syntax
• (lsp) Index workspace symbols from disk
• (lsp) Make document analysis snapshots atomic
• (lsp) Offload blocking workspace operations
• (lsp) Keep failed workspace scans incomplete

Rossi v0.1.4

Added

• (build) Enforce EB021/EB022 in the static checker
• (cli) Report EB026 assignment-in-predicate in validate
• (parse) Detect misplaced assignment in predicate (EB026)
• (build) Register EB026 assignment-in-predicate rule
• (lsp) Surface EB026 as a diagnostic with an operator quick-fix

Changed

• (build) Extract duplicate-name detection into a shared module

Fixed

• (build) Align EB006/EB009 severities with Rodin
• (cli) Fail rossi build on any error diagnostic
• (lint) Repartition the variable-usage lints (EB011/EB012)
• (build) Fail the build on duplicate component names (EB019)
• (lint) Remove the EB013 dead-constant lint
• (lint) Report duplicate component names as errors (EB019)
• (parse) Drop the misleading strict error when recovery reports EB026
• (build) Closure and closure1 are not Event-B built-ins
• (lint) Skip variable reference lints on unresolvable refinement chains
• (lint) Key the cross-component index by component, not name
• (lint) Count inherited invariants as references (EB011/EB012)
• (lint) Check extended INITIALISATION against the inherited chain (EB014)
• (lint) Count extended events' inherited clauses in EB011/EB012