deterministic timeouts when file is opened

Stream: general

[Koundinya Vajjha]

When I open data.complex.exponential, the lemma cos_add takes a very very long time to compile and I end up getting a deterministic timeout. Does anyone know how I can manually change the timeout value (-T50000?) within VS Code?

[Bryan Gin-ge Chen]

Search for "Lean: Time Limit" in your VS Code settings. Mine seems to be set to 100000.

[Koundinya Vajjha]

Thanks! That worked

[Scott Morrison]

... we should probably fix that lemma, too! I thought someone had already gone through mathlib recently checking these timeouts. Maybe we even need to add this timeout limit to the PR build...