Skip to content

Support for multiple files in core highlighting and Sterling replies #313

@tnelson

Description

@tnelson

Currently, if an unsatisfiable core references multiple Forge files, the entire core will be projected onto the currently open file in VSCode. (This behavior also seems to exist in Magic Racket with typed Racket's error messages.)

Relatedly, Forge reports the original model back to Sterling along with instances. This is useful for LLM integration, but only includes the top-level file, not any files that it imports. Thus, if file A opens file B, file B is not communicated to Sterling.

Metadata

Metadata

Assignees

Labels

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions