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

Bad minimization with } #147

Open
SkySkimmer opened this issue Mar 8, 2023 · 4 comments
Open

Bad minimization with } #147

SkySkimmer opened this issue Mar 8, 2023 · 4 comments

Comments

@SkySkimmer
Copy link
Contributor

coq/coq#17346 (comment)
The minimized file ends with something like

tac1.
}
 }
          {
tac2.

but in fact only the 1st } is needed to get the error.

@JasonGross
Copy link
Owner

The minimizer does not currently touch the final proof script. This restriction should be dropped, at least in the CI minimization case.

@JasonGross
Copy link
Owner

Duplicate of #105

@JasonGross JasonGross marked this as a duplicate of #105 Mar 15, 2023
@JasonGross
Copy link
Owner

Oh, sorry, I guess this is not a duplicate

@JasonGross JasonGross reopened this Mar 15, 2023
@JasonGross
Copy link
Owner

Ah, maybe this is an issue with our parsing, where we don't recognize that } and { are complete statements and only split statements on periods.

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

No branches or pull requests

2 participants