Skip to content

ExtensionAPI is here!#36

Merged
EkanshdeepGupta merged 45 commits intomainfrom
eg/error_credits_ext
Jan 28, 2026
Merged

ExtensionAPI is here!#36
EkanshdeepGupta merged 45 commits intomainfrom
eg/error_credits_ext

Conversation

@EkanshdeepGupta
Copy link
Collaborator

Added

  • Added ExtensionAPI as a way to modularly add and remove front-end features in Raven.
  • Added cmpxchg atomic operation.
  • Added a new cmdline option --extension which (presently) takes one of three values: default, eris, and prophecy. This option can be used to select which extension of Raven are active for a given run.

Changed

  • Upgraded Array interface from an interface to a module.
  • Finished implementation of rdcss
  • Added expr_ext_rewrite_types, stmt_ext_rewrite_types to ExtAPI.
  • Added parser support for auCommit resources; enable 'helping'.
  • Expanded definition of "word-sized" types to more flexible types such as algebraic sums of base types.
  • Overhauled extensions to follow namespace-style convention.
  • Added support for helping by allowing auPred resources to refer to another proc; overhauling parser, type-checking and rewriting.
  • Updated syntax so that commitAU always requires at least two argument: token and a tuple of return values (if function returns nothing then it should be ()); and an optional third argument which is a tuple of the callable args (which goes as the middle argument). This optional argument becomes required if the token refers to a different procedure.

Fixed

  • Fixed bug in ComputeStats functionality with looking up abstract members without entering modules.
  • Fixed bug regarding missing quantifiers for auto lemmas with arguments.
  • Fixed two bugs in type checker related to interface aliasing (Issue with module vs interface type-checking #35)
  • Fixed a bug causing a crash on datatype destructors
  • Sanitizing JSON output in LSP mode.
  • Catch module-level var declarations in type checker rather than parser (Adding semicolon to var declaration changes behaviour #31).
  • Fix type-checking bug that allowed access to members of interfaces from outside of their scopes.

wies and others added 30 commits June 3, 2025 01:38
…ith new stmts and expressions making the infrastructure modular and re-usable. Re-factored atomic commands as an extension. Made parser slightly more modular (more work needed on parser).
…om outside of their scopes; some clean-up along the way
…rophecy features as extensions. General refactoring and clean-up
Added fully fleshed out Extension framework
…nds. Partial implementation of rdcss (`complete()` proc for now).

- Added parser support for auCommit resources; enable 'helping'
- Expanded definition of "word-sized" types
- Overhauled extensions to follow namespace-style convention
- Added support for helping by allowing auPred resources to refer to another proc.
- Updated syntax so that commitAU always requires at least two argument: token and a tuple of return values (if function returns nothing then it should be ()); and an optional third argument which is a tuple of the callable args. This optional argument becomes required if the token refers to a different procedure.
…ed expr_ext_rewrite_types, stmt_ext_rewrite_types to ExtAPI, bugfixes
@EkanshdeepGupta EkanshdeepGupta requested a review from wies January 27, 2026 16:55
Copy link
Collaborator

@wies wies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very minor change in README.md: ExtensionAPI is not a word. Let's just write extension API. Also, you use both ExtensionsAPI and ExtensionAPI.

@EkanshdeepGupta
Copy link
Collaborator Author

Done. Merging the pull request.

@EkanshdeepGupta EkanshdeepGupta merged commit b4131b1 into main Jan 28, 2026
6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants