mathport issues in data.int.least_greatest

Stream: mathlib4

[Arien Malec]

I have an initial port in mathlib4#1003 that's all green (modulo some docu cleanup) but the mathlib3port file that it's based on has a bunch of PrettyPrinter.parenthesize stack trace dumps in it. It looks like the resulting file has all the input from mathlib.data.int.least_greatest but it would be good for someone to look at the porting stack trace to see if there are any issues I need to be aware of.

[Arien Malec]

the PR was merged, but did anyone look at the mathlib3port file to see if the PrettyPrinter.parenthesize garbage there was indicative of anything?

[Kevin Buzzard]

Yikes! @Mario Carneiro do you know what's going on here? here is the mathlib3port opinion of this mathlib3 lemma [edit : fixed link]. Remark: the docstring contains P : ℤ → Prop and {m : P m} and [decidable_pred P] , all quoted with ` in the docstring. Could this be anything to do with it?

[Mario Carneiro]

parenthesize errors in mathport are bugs in mathport, usually because some mathlib4 syntax has changed and mathport is generating ill formed syntax objects

[Mario Carneiro]

the main question is, what bit of unusual syntax is used in this file? Usually this kind of error appears in every use of the bad syntax construction

[Mario Carneiro]

looks like (Mathlib.Tactic.tacticClassical_ (Tactic.skip "skip")) is the culprit, this is ill formed

[Arien Malec]

Good to hear, wasn't necessary to the proof.

[Mario Carneiro]

to be clear, the issue is not in least_of_bdd but in the declaration after that, exists_least_of_bdd

[Mario Carneiro]

the problem is classical; exact, which has to be translated in a complicated way because classical is now a tactic combinator like try and it seems that it isn't handling the case classical <;> tac => classical tac correctly

[Kevin Buzzard]

Mario Carneiro said:

to be clear, the issue is not in least_of_bdd but in the declaration after that, exists_least_of_bdd

yeah sorry, I fixed the link.

[Kevin Buzzard]

But is the long and short of it that if Arien managed to get a mathlib4 proof working then we don't have to worry about anything in this file in mathlib4, and it's just a bug in mathport?

[Mario Carneiro]

well, it should hopefully be a similar proof as the lean 3 one

[Mario Carneiro]

you will have to do the mathporting manually in this case

[Mario Carneiro]

at least until the bug is fixed

[Kevin Buzzard]

OK that's great, indeed that was what was done in this case. Thanks!