Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix set.mm check #135

Closed
wants to merge 3 commits into from
Closed

Fix set.mm check #135

wants to merge 3 commits into from

Conversation

jkingdon
Copy link
Contributor

First of all, use the develop branch rather than the master branch because the latter is rather old and we haven't been using it.

Second of all, add --verify-markup and --parse-typesetting so that we run more of the checks (including most notably the ones which the set.mm automated checks enable).

First of all, use the develop branch rather than the master branch
because the latter is rather old and we haven't been using it.

Second of all, add --verify-markup and --parse-typesetting so that we
run more of the checks (including most notably the ones which the set.mm
automated checks enable).
@jkingdon
Copy link
Contributor Author

The build is failing, partly due to metamath/set.mm#3527 but also for a few things which changed between set.mm's master and develop.

@digama0
Copy link
Member

digama0 commented Sep 28, 2023

cc: @tirix, the grammar parsing is failing

@digama0 digama0 mentioned this pull request Sep 29, 2023
tirix added a commit to tirix/metamath-knife that referenced this pull request Sep 29, 2023
@tirix tirix mentioned this pull request Sep 29, 2023
@tirix
Copy link
Collaborator

tirix commented Sep 29, 2023

The minimal example provided by @digama0 in #137 helped me to propose one fix in #138.
Unfortunately this is still not enough for successfully parsing set.mm in the develop branch.
The best way would be to do a dichotomy between master and develop, find since when it broke, and what was added at that time. I might have a try this weekend.

@jkingdon
Copy link
Contributor Author

Now that #138 is merged we may be able to unblock this change (let me figure out how to re-open it or if not I'll fall back to making a new one).

@jkingdon jkingdon mentioned this pull request Sep 30, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants