Skip to content

chore: use upstream HTML type - #974

Closed
Vtec234 wants to merge 3 commits into
nightly-testingfrom
adapt-html-type
Closed

chore: use upstream HTML type#974
Vtec234 wants to merge 3 commits into
nightly-testingfrom
adapt-html-type

Conversation

@Vtec234

@Vtec234 Vtec234 commented Aug 27, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

This PR switches Verso to use the upcoming core Lean HTML type rather than defining one.

JSX-like syntax and utilites are not changed here.

@Vtec234 Vtec234 mentioned this pull request Aug 27, 2026
Merged
@Vtec234
Vtec234 changed the base branch from main to nightly-testing August 27, 2026 21:44
Vtec234
Vtec234 commented Aug 27, 2026
View reviewed changes
Comment thread doc/UsersGuide/Output/HTML.lean
@david-christiansen

david-christiansen commented Aug 28, 2026

Copy link
Copy Markdown
Collaborator

Given that lots of external codebases use this library, I think we should endeavor to provide deprecated aliases for all the names that point at the Lean versions, to make adaptation less painful.

david-christiansen
david-christiansen reviewed Aug 28, 2026
View reviewed changes
Comment thread src/verso/Verso/Output/Html.lean
david-christiansen
david-christiansen reviewed Aug 28, 2026
View reviewed changes
Comment thread src/verso/Verso/Output/Html.lean Outdated
david-christiansen
david-christiansen reviewed Aug 28, 2026
View reviewed changes
Comment thread src/verso/Verso/Output/Html.lean Outdated
@Vtec234

Vtec234 commented Aug 31, 2026 •
edited
Loading

Copy link
Copy Markdown
Member Author

provide deprecated aliases for all the names that point at the Lean versions

I did this at first, but this mostly results in name resolution failures downstream. For example with @[deprecated] abbrev Verso.Output.Html := Lean.Html, downstream files that open Verso Output and open Lean - which, at least in Verso, most do - end up with 'ambiguous symbol' errors, or the wrong Html type inferred, in ways that make it harder to adapt than when we just break the API, like this PR does. I am open to tricks that would work around this, if you know of any.

UPDATE: I think I have found the optimal thing to do using a combination of export and public/protected abbrev; see the bottom of Verso.Output.Html.

Vtec234
Vtec234 commented Sep 2, 2026
View reviewed changes
Comment thread src/tests/VersoTests/VersoManual/Html/SoftHyphenate.lean
Vtec234
Vtec234 commented Sep 2, 2026
View reviewed changes
Comment thread doc/UsersGuide/Output/HTML.lean
Vtec234
Vtec234 commented Sep 2, 2026
View reviewed changes
Comment thread src/tests/VersoTests/Html.lean
@Vtec234
Vtec234 marked this pull request as ready for review September 2, 2026 20:51
@Vtec234 Vtec234 mentioned this pull request Sep 13, 2026
Open
@Vtec234
Vtec234 added this pull request to stack #988 September 17, 2026 01:29
@Vtec234

Vtec234 commented Oct 1, 2026

Copy link
Copy Markdown
Member Author

Moved to leanprover/downstream-lean4#25.

@Vtec234 Vtec234 closed this Oct 1, 2026
meefs pushed a commit to meefs/lean4 that referenced this pull request Oct 1, 2026
@Vtec234
feat: add Html type (leanprover#14935)
001a6b6 
This PR adds a type `Lean.Data.Html` of HTML forests — aimed primarily
at authoring HTML (as opposed to internal representation in a web
server, etc) — as well as a renderer that produces a `String` object.

Rendering directly into `FS.Stream` is out of scope for this PR.

Downstream *adoption* (not merely adaptation to make CI pass) PRs that
use the new type and renderer:
- leanprover/verso#974
- leanprover/doc-gen4#408
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@david-christiansen david-christiansen david-christiansen approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@Vtec234 @david-christiansen