Repository navigation
Conversation
This is a step towards removing `parserInputString`. Upstream `runParserCategory` always starts at `pos := 0` Another option would be to update the upstream function to take this into account, but the idea is that the function will evolve to take a string literal so it should be able to compute the position by itself. I made the types different (the Verso one is monadic) as to help avoid confusion, and increase programming ergonomics. Note that we don't change the parts `in VersoManual.Docstring` as these are code strings that come from the `MD4Lean` and they don't have an attached location.
This is possible after leanprover/lean4#10043 improved upstream parsing API. This replaces the current use of `parserInputString`, which pads the input, and seems clearer overall. There are two main cases for string literals for us to process: - string literals coming from Verso: in this case, `.getPos` and `.getTailPos` do provide the correct start / end of the string, without the quotes. - string literals coming from Lean: in this case, we must account for the quotes and fixup the positions. We have handled this by convention, but `VersoUtils.parseString` takes an optional parameter as it is used in both modes. Eventually we'd like to move Verso-style strings to its own type instead of `StrLit`. Notes: - I couldn't port `VersoBlog.leanInit` as `Parser.parseHeader` always parses from `pos := 0`. This is the last blocker to completely remove `parserInputString`. - In general, it seems like most functions using `mkParserState` upstream could benefit from an update to take positions. - Tests in `UsersGuide.Markup` had to be adapted due to use of `contents.getString.trimAsciiEnd.copy`. I did this to pass CI, must implement a better fix before merging. - Code that depends on MD4Lean hasn't been ported as MD4 doesn't seem to provide the right API for us. - TODO: we should test `canonical := true` and quoting properly. Note special cases such as `` `code ``
Only `Command.State` is needed to thread several example blocks. Note that before we used the parsing state resulting from the last code block, so we did resume from an offset that could be potentially much before the current code block. This worked as the string in that case was empty (produced by `parserInputString`), but would have failed once we have reuse of the input source string.
Keep imports on parseStrLitWith, which now understands the dedicated Verso code-block tokens. Document that the supplied range excludes the fences; the old parseString workaround is superseded by upstream support. Mark the private blog header-padding helper meta for the current elaborator and retain the historical parser-restart changes for design review.
This PR parses blog initialization headers directly from their bounded source spans using the header-start API in leanprover/lean4#15856. Follow up on David Christiansen's leanprover/lean4#10043 and remove the last whitespace-padding helper. Use leadingStartPos? := none for direct command parsing that discards initial trivia. Pin the root and its three dependent test fixtures to the commit-specific CI release for this integration checkout. Validate with lake build (1,302 jobs), lake test (775 passed, zero failures or errors, including all 19 editor/LSP cases), upstream header regressions, and exact UTF-8 and LF/CRLF source-span checks. Breaking changes: require a Lean toolchain containing leanprover/lean4#15856. This integration commit pins leanprover/lean4-pr-releases:pr-release-15856-87576ac.
Document the parser-helper changes and Lean header API dependency in a breaking release note for PR leanprover#750. Include migration paths for source syntax, decoded strings, and structured syntax errors so the draft passes the release-note checks.
Keep the three Errata driver workspaces on the same PR toolchain as Verso, since each requires the root package by path. Retain the demo's diagnostic count of 54 for this compiler snapshot rather than the bump branch's count of 49. Refresh that expectation together with the temporary pins when adopting a regular Lean toolchain containing the API.
Associate the existing migration note with leanprover#1077 while retaining leanprover#750 as the original discussion. Keep the replacement draft eligible for the release-note check.
This branch has not been deployed
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.
This PR parses embedded Lean directly from bounded spans of the original source, replacing whitespace-padded copies while preserving source positions.
Draft: depends on leanprover/lean4#15856 . We temporarily pin Lean and the three root-dependent test projects to
leanprover/lean4-pr-releases:pr-release-15856-87576acso this branch can be reviewed and CI-tested now.We follow up on David's leanprover/lean4#10043 API changes:
leanInitheader-padding helper.syntaxErrordiagnostics.Review focus: the public parser-helper API changes and source provenance for macro-generated syntax.
API changes: require Lean's new header-start and optional leading-trivia APIs. Replace
parserInputStringwith bounded source contexts; use the monadicrunParserCategoryfor source syntax,runParserCategoryStringfor decoded strings, orrunParserCategoryGenwithrunParserCategory.toSyntaxErrorsin place ofrunParserCategory'.Continues #750, which GitHub automatically closed when its
nightly-testingbase branch was deleted. The updated branch policy sends features requiring nightly Lean APIs tobump/v4.37.0.Rebase validation:
lake buildpasses (1,221 jobs); the completelake testrun passes (777 passed, zero failures/errors), including all 19 editor/LSP cases. Align the Errata driver fixtures and the demo's expected diagnostic count with the temporary PR compiler snapshot.