quote4

Stream: nightly-testing

[Kim Morrison]

@Eric Wieser, would you be able to look at this test failure in quote4?

https://github.com/leanprover-community/quote4/pull/48

[Kim Morrison]

This is me trying to bring quote4 up to the latest nightly; I have no idea at what point along the way this example stopped working, because we don't regularly update quote4.

[Eric Wieser]

Can you make a PR to bump to 4.10.0 or 4.11.0rc1, just to rule out the error being there?

[Kim Morrison]

Any chance you could? quote4 is pretty low priority for me, so if it's working for mathlib I'm happy. :-)

[Eric Wieser]

Just tested in the web editor; this test is already broken in the (version of Qq used by the) latest mathlib

[Eric Wieser]

run_cmd Elab.Command.lintersRef.set #[] fixes it

[Eric Wieser]

So the crash is coming from a core linter

[Eric Wieser]

So a feature request: can linters catch all error messages and prefix them with "the foo linter crashed:" before re-raising?

[Eric Wieser]

set_option linter.constructorNameAsVariable false

fixes it

[Eric Wieser]

Interestingly set_option linter.all false does not

[Eric Wieser]

Eric Wieser said:

Can you make a PR to bump to 4.10.0 or 4.11.0rc1, just to rule out the error being there?

Done in https://github.com/leanprover-community/quote4/pull/49, along with a temporary workaround that should unblock your nightly bump

[Kim Morrison]

Thanks!

[Kim Morrison]

The remaining things here are:

• feature request for the linter framework to prefix errors from linters
• finding a quote4-free minimization for the constructorNameAsVariable crash

[Kim Morrison]

Interested in doing either? :-)

[Eric Wieser]

Is the linter.all thing a bug too?

[Kim Morrison]

Oh, yes, possibly!

[Eric Wieser]

I might at some point get to 2; can you handle 1 and 3?

[Kim Morrison]

linter.all fix is #4966

[Eric Wieser]

lean4#4966

[Kim Morrison]

And prefixing the name is done at lean#4967