Skip to content

Conversation

jrr6
Copy link
Contributor

@jrr6 jrr6 commented Jun 24, 2025

This PR adds elaboration and a manual page for error explanations.

@jrr6 jrr6 force-pushed the jrr6/preprocess-explanations branch from 523c931 to 5f49d7d Compare June 25, 2025 19:34
@jrr6 jrr6 force-pushed the jrr6/explanations-remainder branch from c3c3a07 to deee512 Compare June 25, 2025 19:35
@jrr6 jrr6 force-pushed the jrr6/preprocess-explanations branch from 5f49d7d to eff8b02 Compare June 25, 2025 19:55
@jrr6 jrr6 force-pushed the jrr6/explanations-remainder branch from deee512 to c132464 Compare June 25, 2025 19:56
Base automatically changed from jrr6/preprocess-explanations to nightly-testing June 25, 2025 20:19
@jrr6 jrr6 marked this pull request as ready for review June 25, 2025 20:20
@jrr6 jrr6 force-pushed the jrr6/explanations-remainder branch from c132464 to 237f71f Compare June 25, 2025 20:23
@jrr6
Copy link
Contributor Author

jrr6 commented Jun 25, 2025

I've changed in core the wording of the error explanation that's currently blocking the build, but it unfortunately won't land until the next nightly.

@david-christiansen
Copy link
Collaborator

I think that we should just disable the prose linter for error explanations. The feedback loop is way too long for it to be worth it. If we want one for them, then we should configure it upstream, in the lean4 CI.

@david-christiansen
Copy link
Collaborator

I can just make the prose linter ignore any HTML that contains an element with class error-example-container

@david-christiansen
Copy link
Collaborator

You haven't enabled the "allow maintainers to edit PR" flag, so I can't push it directly, but I do have a fix for this. Can you enable the flag?

@jrr6
Copy link
Contributor Author

jrr6 commented Jun 26, 2025

You haven't enabled the "allow maintainers to edit PR" flag, so I can't push it directly, but I do have a fix for this. Can you enable the flag?

I think you should be able to commit directly to the jrr6/explanations-remainder branch and have the changes show up here.

@david-christiansen
Copy link
Collaborator

I managed to confuse myself about the role the / was playing here!

@david-christiansen david-christiansen added the HTML available HTML has been generated for this PR label Jun 26, 2025
@jrr6 jrr6 force-pushed the jrr6/explanations-remainder branch from 8f37451 to 0f0d2ce Compare June 27, 2025 00:09
For consistency with the rest of the manual
Copy link
Contributor

Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit d959a6a.

@david-christiansen david-christiansen merged commit 3d8b0f9 into nightly-testing Jun 27, 2025
9 checks passed
@david-christiansen david-christiansen deleted the jrr6/explanations-remainder branch June 27, 2025 04:14
david-christiansen added a commit that referenced this pull request Jun 30, 2025
This PR adds elaboration and a manual page for error explanations.

---------

Co-authored-by: David Thrane Christiansen <[email protected]>
david-christiansen added a commit that referenced this pull request Jun 30, 2025
This PR adds elaboration and a manual page for error explanations.

---------

Co-authored-by: David Thrane Christiansen <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
HTML available HTML has been generated for this PR
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants