Formatting and debugging improvements#1114
Closed
keyboardDrummer wants to merge 5 commits intostrata-org:mainfrom
Closed
Formatting and debugging improvements#1114keyboardDrummer wants to merge 5 commits intostrata-org:mainfrom
keyboardDrummer wants to merge 5 commits intostrata-org:mainfrom
Conversation
Formatting improvements:
- Change block formatting to use indent(2) with newlines for vertical layout
instead of single-line '{ ... }' format
- Update semicolon separator to use newlines instead of spaces
Debugging improvements:
- Replace boolean 'coreProgramHasSuperfluousErrors' with 'coreDiagnostics' list
that records why the Core program was suppressed, enabling better error surfacing
- Add source location and reason parameters to 'invalidCoreType' for more
informative diagnostics
- Surface core diagnostics when no other diagnostics explain program suppression
- Add 'processLaurelFileKeepIntermediates' test helper for writing intermediate
pipeline files to Build/ directory
- Add Build/ to .gitignore
Test updates:
- Update all expected outputs to match new block formatting
- Add 'opaque' keyword to test procedures that need it for the new formatting
- Fix #guard_msgs whitespace formatting
Diagnostics with FileRange.unknown are not actionable for users and can arise from pre-existing resolution limitations (e.g., variables in multi-assign with field targets losing their uniqueId). Filter these out when surfacing suppression reasons to avoid spurious errors.
The CodeBuild source location was hardcoded to strata-org/Strata.git, which fails when the commit only exists in keyboardDrummer/Strata. Use github.server_url/github.repository so it resolves to the correct repo dynamically.
The CodeBuild project has credentials for strata-org/Strata only. On forks like keyboardDrummer/Strata, the job cannot access the source. Add an 'if' condition to skip the benchmark on non-upstream repos, and restore the hardcoded source URL that CodeBuild expects.
Contributor
Author
|
@keyboardDrummer-bot please resolve conflicts |
…gging-improvements # Conflicts: # Strata/Languages/Laurel/LaurelToCoreTranslator.lean
Contributor
Author
|
@keyboardDrummer-bot please create the branch of this PR in the strata-org/strata repo, and then recut this PR |
Collaborator
|
Done. Created the branch in |
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.
Summary
Extracts the formatting and debugging improvements from #34 into a standalone PR.
Formatting improvements
{ stmt1; stmt2 }to vertical layout withindent(2):Debugging improvements
coreProgramHasSuperfluousErrorswith acoreDiagnostics : List DiagnosticModelthat records why the Core program was suppressed. When no other diagnostics explain the suppression, these are surfaced to the user.invalidCoreType: Addssourceandreasonparameters so each suppression site provides context about what went wrong.processLaurelFileKeepIntermediatestest helper that writes pipeline intermediate files toBuild/for debugging..gitignore: AddsBuild/directory.Test updates
#guard_msgswhitespace fixes.opaquekeyword where needed for the new formatting to apply correctly.