# Zulip Chat Archive

## Stream: general

### Topic: deterministic timeout

#### Zesen Qian (Jun 28 2018 at 01:32):

In general, how to solve "(deterministic) timeout" error?

#### Zesen Qian (Jun 28 2018 at 01:45):

I have tried increasing the timeout limit, so it must be my code.

#### Simon Hudon (Jun 28 2018 at 03:10):

Yes and it depends on the tactics that you use. Often, `simp`

is the offender. When you give it a list of rules that do not converge, it will just keep going.

#### Jeremy Avigad (Jun 30 2021 at 16:45):

I am working on a program verification project that automatically generates Lean files with large proofs. They use the simplifier in an essential way, and elaboration often takes on the order of 30 seconds or more.

Now I have a large proof that fails with a `deterministic timeout`

. By manually breaking it into smaller proofs, I can get it to elaborate. By commenting out parts of the original proof, I can find the part that puts Lean over the edge.

I tried putting `set_option timeout 300000`

before the proof (and using other big numbers), but it still fails at exactly the same place. Is there anything else I can do to get Lean to try harder? Or is it possible that the `deterministic timeout`

message is standing proxy for some other problem?

#### Gabriel Ebner (Jun 30 2021 at 16:56):

`set_option timeout`

is completely ignored as far I can remember. The timeout setting is set by a command line argument. In vscode you can configure it using the `Lean: Time Limit`

setting.

#### Jeremy Avigad (Jun 30 2021 at 17:10):

That worked! Many thanks.

#### Eric Rodriguez (Mar 20 2022 at 01:12):

getting some in #12836 which adds zero new `simp`

lemmas - does anyone know what's going on? I'm trying to reerun CI as I can't reproduce locally

#### Kyle Miller (Mar 20 2022 at 02:59):

On my machine, `set_option profiler true`

for docs#topological_vector_bundle.trivialization.prod gives

```
662:5: parsing took 373ms
662:5: elaboration of prod took 20.9s
662:5: type checking of prod took 345ms
662:5: decl post-processing of prod took 344ms
```

I don't know how the deterministic timeout system works, but 20.9s is pretty long and maybe you were just unlucky and by chance it timed out.

I wonder if it's worth splitting that definition up somehow so that it elaborates proofs and the definition separately.

#### Eric Rodriguez (Mar 20 2022 at 11:03):

I re-ran and it went away, so it doesn't seem very deterministic :/ but maybe it's worth splitting up that proof anyways

#### Oleksandr Manzyuk (Mar 20 2022 at 23:50):

A Lean n00b here. I'm working through the exercises for LFTCM2020, which are a lot of fun! (I was a mathematician before making a career switch 10 years ago and starting working as a software developer. I've started picking up Lean recently as a hobby at the intersection of mathematics and computer science/type theory/functional programming.) Unfortunately, once I've reached the exercises in category theory, things have become very slow and I often get "(deterministic) timeout", which significantly degrades the experience interacting with the theorem prover making it a lot less responsive and sometimes I simply don't know how to make progress because the obvious thing doesn't work.

For example, here is my attempt at exercise 4. At line 56, the goal is as follows:

```
R : CommRing,
f : (coyoneda.obj (op (CommRing.of (polynomial ℤ)))).obj R
⊢ eval₂ (algebra_map ℤ ↥R) (f.to_fun X) X = f.to_fun X
```

which seems to match the `polynomial.eval₂_X`

lemma, but applying or rewriting with it causes the dreaded deterministic timeout. Does anyone have an idea what might be going on here? Am I missing anything?

#### Thomas Browning (Mar 21 2022 at 00:06):

I have no idea why, but it seems that `hom := { app := λ R, λ r, polynomial.eval₂_ring_hom (algebra_map ℤ R) r },`

is a major contributor to the timeout.

#### Junyan Xu (Mar 21 2022 at 03:24):

If that's the case then probably it's because the tactic that automatically fils in the `naturality'`

fields runs too slowly, and you might consider supplying an explicit proof.

You may also split out the individual fields `hom`

, `inv`

etc. as individual `def`

s.

#### Oleksandr Manzyuk (Mar 21 2022 at 08:31):

Thank you. I suspected that the automation was to blame. I'll try providing explicit proofs. I'm curious what the approach to working with the category theory part of the library should be. Should one begin by writing out every proof manually and then try and see which of those could be filled in by automation? Or should one try to leave out as much as possible and only manually fill in the proofs that the automation is failing to provide? I'm leaning towards the former option but I'm curious to hear about other people's experience with the category theory library. (I was a category theorist in the previous life, and I was hoping to eventually contribute something to mathlib, e.g., formalisation of multicategories, so I'm trying to learn and understand how the existing category theory library is structured.)

#### Ruben Van de Velde (Mar 21 2022 at 08:54):

It seems like mostly the latter approach looking in from the outside

#### Oleksandr Manzyuk (Mar 21 2022 at 09:16):

Interesting. Filling in the proof of naturality of `hom`

did indeed allow me to finish the proof of `inv_hom_id'`

and complete the definition of `CommRing_forget_representable`

. At the moment, the proof of naturality also relies on automation but apparently fleshes out enough structure to prune the search? I just did `intros R S f`

, and then the goal is equality of two morphisms, so I used `ext`

, which created two subgoals. I tried to use `simp`

to clean them up a little but it just solved them (after some crunching). Once `simp`

succeeded, is it useful to use `simp?`

to get a list of simplification lemmas used and replace `simp`

with `simp only [...]`

?

#### Arthur Paulino (Mar 21 2022 at 09:22):

Yes, and you can also try `squeeze_simp`

, which might be slower but gets it right more often

#### Oleksandr Manzyuk (Mar 21 2022 at 10:27):

Arthur Paulino said:

Yes, and you can also try

`squeeze_simp`

, which might be slower but gets it right more often

Thank you, I didn't know about `squeeze_simp`

! I tried to use it and something amusing happened: when proving naturality of `hom`

, after `intros R S f, ext r c`

, the first goal is

```
RS: CommRing
f: R ⟶ S
r: (forget CommRing).obj R
c: ℤ
⊢ ⇑(ring_hom.comp (((forget CommRing).map f ≫ λ (r : (forget CommRing).obj S), eval₂_ring_hom (algebra_map ℤ ↥S) r) r) C) c = ⇑(ring_hom.comp (((λ (r : (forget CommRing).obj R), eval₂_ring_hom (algebra_map ℤ ↥R) r) ≫ (coyoneda.obj (op (CommRing.of (polynomial ℤ)))).map f) r) C) c
```

and `squeeze_simp`

suggested `simp only [ring_hom.eq_int_cast]`

. My first thought when looking at that goal was "That's a mouthful, let me clean it up first to see what's going on." So, I tried to insert `dsimp`

before `simp only [ring_hom.eq_int_cast]`

, and the proof stopped working! It took me a while to realise that the original goal was of the form `⇑g c = ⇑h c`

, where `g`

and `h`

are two homomorphisms from `ℤ`

, so that `ring_hom.eq_int_cast`

could be applied directly, whereas `dsimp`

destroyed this property of the goal (even though it made it look simpler).

#### Scott Morrison (Mar 22 2022 at 09:01):

Unless I have some reason to be confident or optimistic that the automation will fill in fields, I tend to fill them in with sorries while I write the data fields (and any proof fields which I know will need human attention). After that, you can try deleting the sorried fields to see if automation handles them.

#### Oleksandr Manzyuk (Mar 22 2022 at 14:33):

Thank you very much, @Scott Morrison I was hoping to hear your take on this.

#### Violeta Hernández (May 30 2022 at 15:33):

I'm getting one on Dedekind domains: https://github.com/leanprover-community/mathlib/pull/14442/files

#### Anne Baanen (May 30 2022 at 15:51):

This is probably related to https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/normalized_factors/near/284291719. I'd like to investigate this, but my schedule the coming week is very full...

#### Violeta Hernández (Jun 04 2022 at 02:03):

Hasn't been fixed, and it's affecting various of my PRs

#### Violeta Hernández (Jun 04 2022 at 02:04):

This is the lemma in question:

```
lemma ideal.count_normalized_factors_eq {p x : ideal R} (hp0 : p ≠ ⊥) [hp : p.is_prime] {n : ℕ}
(hle : x ≤ p^n) (hlt : ¬ (x ≤ p^(n+1))) :
(normalized_factors x).count p = n :=
count_normalized_factors_eq ((ideal.prime_iff_is_prime hp0).mpr hp).irreducible (normalize_eq _)
(ideal.dvd_iff_le.mpr hle) (mt ideal.le_of_dvd hlt)
```

#### Violeta Hernández (Jun 04 2022 at 02:05):

I have no idea how to golf this, it looks very concise?

#### Violeta Hernández (Jun 04 2022 at 02:05):

I have no idea why it's even timing out

#### Violeta Hernández (Jun 04 2022 at 02:08):

This is purely term-mode, right? So why does it take so long?

#### Violeta Hernández (Jun 04 2022 at 04:19):

And why do unrelated changes push it over the edge? It's not like this is calling some simp lemma or whatever

#### Damiano Testa (Jun 04 2022 at 05:15):

I do not know the source of the timeout, but I would start looking at instance searches, if you've added typeclasses.

Regarding term-mode: such proofs tend to be faster, but that is not a rule. I've seen situations where a lemma application form in term mode times out, but `by apply <same lemma>`

works instantly. Again, I think that it usually has to do with instance search.

#### Damiano Testa (Jun 04 2022 at 05:17):

Try seeing if `by apply/exact/convert`

make the lemma faster. Sometimes it works...

#### Violeta Hernández (Jun 04 2022 at 05:27):

None of them seem to make it significantly faster

#### Violeta Hernández (Jun 04 2022 at 05:27):

In fact, `apply`

and `convert`

cause it to time-out on `master`

#### Violeta Hernández (Jun 04 2022 at 05:35):

By testing with a few sorries, it seems like all of the three arguments take up a lot of the runtime

#### Violeta Hernández (Jun 04 2022 at 05:38):

By the way, is it intentional that we have the hypotheses `(hle : x ≤ p^n)`

and `(hlt : ¬ (x ≤ p^(n+1)))`

? These seem to imply `p < 1`

which seems weird, but I don't know what ideal exponentiation nor comparison is supposed to be so...

#### Violeta Hernández (Jun 04 2022 at 05:40):

(not to mention, `hlt`

should be written `p^(n+1) < x`

instead)

#### Ruben Van de Velde (Jun 04 2022 at 05:42):

I \le J means J dvd I, iirc

#### Kevin Buzzard (Jun 04 2022 at 05:44):

What happens if you fill in the hole?

#### Damiano Testa (Jun 04 2022 at 05:44):

Which in turn should mean contain. You can probably interpret the order as containment of sets.

#### Damiano Testa (Jun 04 2022 at 05:46):

If the timeout is due to `zero_le_one_class`

, then I would look for typeclass issues having to do with the order.

#### Damiano Testa (Jun 04 2022 at 05:50):

(not to mention,

`hlt`

should be written`p^(n+1) < x`

instead)

I'm not sure that follows: the order is not linear. It is more like the order on `order_dual (set α)`

.

#### Violeta Hernández (Jun 04 2022 at 19:43):

Yet another one of my PRs, a very big one no less, has succumbed to this same timeout

#### Violeta Hernández (Jun 04 2022 at 19:43):

I wonder if the best solution here is to make the last three arguments into separate private lemmas

#### Violeta Hernández (Jun 04 2022 at 19:43):

I'm not familiar with the file, so I don't know if these lemmas are anything of standalone interest

#### Junyan Xu (Jun 07 2022 at 13:18):

`convert ideal.dvd_iff_le.mpr hle`

seems faster than `exact`

#### Junyan Xu (Jun 07 2022 at 13:18):

same for `convert mt ideal.le_of_dvd hlt`

#### Junyan Xu (Jun 07 2022 at 13:27):

potential diamond?

```
type mismatch at application
normalize_eq
term
ideal.unique_units
has type
unique (@ideal ?m_1 (@comm_semiring.to_semiring ?m_1 ?m_2))ˣ : Type ?
but is expected to have type
unique (@ideal ?m_1 (@ring.to_semiring ?m_1 (@comm_ring.to_ring ?m_1 ?m_2)))ˣ : Type ?
```

#### Junyan Xu (Jun 07 2022 at 13:27):

from

```
lemma ideal.count_normalized_factors_eq {p x : ideal R} (hp0 : p ≠ ⊥) [hp : p.is_prime] {n : ℕ}
(hle : x ≤ p^n) (hlt : ¬ (x ≤ p^(n+1))) :
(normalized_factors x).count p = n :=
begin
apply count_normalized_factors_eq ((ideal.prime_iff_is_prime hp0).mpr hp).irreducible,
apply @normalize_eq _ ideal.cancel_comm_monoid_with_zero ideal.unique_units,
end
```

#### Junyan Xu (Jun 07 2022 at 13:39):

```
lemma ideal.count_normalized_factors_eq {p x : ideal R} (hp0 : p ≠ ⊥) [hp : p.is_prime] {n : ℕ}
(hle : x ≤ p^n) (hlt : ¬ (x ≤ p^(n+1))) :
(normalized_factors x).count p = n :=
begin
apply count_normalized_factors_eq ((ideal.prime_iff_is_prime hp0).mpr hp).irreducible,
{ haveI : unique (ideal R)ˣ := ideal.unique_units, apply normalize_eq },
convert ideal.dvd_iff_le.mpr hle,
convert mt ideal.le_of_dvd hlt,
end
```

This seems fast enough (1-2s), so I'm gonna PR it! #14590

#### Eric Wieser (Jun 07 2022 at 14:56):

Doesn't look like a diamond in the usual sense, lean just can't guess what ring you're talking about.

#### Yaël Dillies (Jun 11 2022 at 18:48):

Does anyone know what's up with #14683? I'm getting a timeout on docs#intermediate_field.intermediate_field_map. It's `decls post-processing`

that takes 39s and nothing I tried did anything.

#### Yaël Dillies (Jun 11 2022 at 20:33):

Update, I'm htting it in #14686 as well :confused:

#### Junyan Xu (Jun 12 2022 at 12:25):

Remove `@[simps]`

: compiles in an instant

Use `@[simps] noncomputable!`

: decl post-processing of intermediate_field_map took 19.5s

#### Junyan Xu (Jun 12 2022 at 12:25):

@Yaël Dillies

#### Yaël Dillies (Jun 12 2022 at 12:25):

`noncomputable!`

still timed out for me :thinking:

#### Yaël Dillies (Jun 12 2022 at 12:26):

Can you see what `simps`

generates? `simps?`

timed out as well for me.

#### Junyan Xu (Jun 12 2022 at 12:31):

generated with `[simps?] noncomputable!`

```
[simps] > The given definition is not a constructor application:
> e.subalgebra_map E.to_subalgebra
> Retrying with the options { rhs_md := semireducible, simp_rhs := tt}.
[simps] > adding projection intermediate_field.intermediate_field_map_apply_coe:
> ∀ {K : Type u_1} {L : Type u_2} [_inst_1 : field K] [_inst_2 : field L] [_inst_3 : algebra K L]
{L' : Type u_3} [_inst_4 : field L'] [_inst_5 : algebra K L'] (e : L ≃ₐ[K] L') (E : intermediate_field K L)
(ᾰ : ↥(E.to_subalgebra.to_subsemiring)), ↑(⇑(intermediate_field_map e E) ᾰ) = ⇑e ↑ᾰ
[simps] > adding projection intermediate_field.intermediate_field_map_symm_apply_coe:
> ∀ {K : Type u_1} {L : Type u_2} [_inst_1 : field K] [_inst_2 : field L] [_inst_3 : algebra K L]
{L' : Type u_3} [_inst_4 : field L'] [_inst_5 : algebra K L'] (e : L ≃ₐ[K] L') (E : intermediate_field K L)
(ᾰ : ↥(subsemiring.map e.to_ring_equiv.to_ring_hom E.to_subalgebra.to_subsemiring)),
↑(⇑((intermediate_field_map e E).symm) ᾰ) = ⇑(↑↑e.symm) ↑ᾰ
```

#### Junyan Xu (Jun 12 2022 at 12:37):

Sorry, it seems `decl post-processing of intermediate_field_map`

takes 18-20s on my machine no matter whether there's `noncomputable!`

or not, and `[simps?]`

gives the same output. But I do get a deterministic timeout without the `noncomputable!`

. So it seems `@[simps]`

takes 18-20s, and ~~computability related stuff (VM code generation?) takes much longer and yields a timeout~~. But why removing `@[simps]`

makes it instant? There should still be VM code generation, no?

#### Junyan Xu (Jun 12 2022 at 12:40):

Anyway, it's easy enough to add the two auto-generated simp lemmas manually.

#### Junyan Xu (Jun 12 2022 at 13:55):

I increased time limit so that the timeout goes away, and it seems it just take 1-2 more seconds (19-20s total) for the whole declaration to compile.

#### Yaël Dillies (Jun 12 2022 at 14:17):

Do you mind filing the fix as a PR?

#### Junyan Xu (Jun 12 2022 at 15:25):

I'll attend this exhibition this afternoon (leaving in 1 hour) and don't have the time at the moment. You are welcome to submit the PR! So we've decided to go with the manual simp lemmas approach?

#### Junyan Xu (Jun 12 2022 at 16:31):

I've got some time to work out the proper forms of the two auto-generated simp lemmas in the context, but I'm leaving soon!

```
lemma intermediate_field_map_apply_coe (e : L ≃ₐ[K] L') (E : intermediate_field K L) (a : E) :
↑(intermediate_field_map e E a) = e a := rfl
lemma intermediate_field_map_symm_apply_coe (e : L ≃ₐ[K] L') (E : intermediate_field K L)
(a : subsemiring.map e.to_ring_equiv.to_ring_hom E.to_subalgebra.to_subsemiring) :
↑((intermediate_field_map e E).symm a) = e.symm a := rfl
```

#### Yaël Dillies (Jun 12 2022 at 16:33):

Is the second one really ever going to fire?

#### Junyan Xu (Jun 13 2022 at 04:46):

I don't know if it's going to fire but it looks like a reasonable simp lemma. I just pushed to branch#intermediate_field_map_timeout without `simp`

attribute on either lemma to see if and where they fire.

On master, removing the `simps`

from `intermediate_field_map`

also reduces

`decl post-processing of intermediate_field_map`

from 18.3s to 46.4ms on my machine.

#### Junyan Xu (Jun 13 2022 at 04:50):

Seems the build already succeded in 4m 53s...

#### Junyan Xu (Jun 14 2022 at 02:00):

#### Yaël Dillies (Jun 19 2022 at 14:27):

Yet another timeout in file#algebraic_geometry/function_field this time. It's docs#algebraic_geometry.function_field.algebra. Any idea?

#### Junyan Xu (Jun 19 2022 at 15:00):

first observation: `apply structure_sheaf.to_stalk R`

is about 2x faster (11.1s) than `exact structure_sheaf.to_stalk R _`

(29.3s). Will try to speed up it further.

Interestingly `convert structure_sheaf.to_stalk R _`

(11.3s) is similar to `apply`

(but probably bad for building data instance).

#### Junyan Xu (Jun 19 2022 at 15:46):

```
ring_hom.to_algebra $ by { change CommRing.of R ⟶ _, apply structure_sheaf.to_stalk }
```

about 0.4s now!

#### Junyan Xu (Jun 19 2022 at 15:57):

#### Violeta Hernández (Jun 22 2022 at 02:23):

One of my PRs is getting a timeout on docs#exterior_algebra.graded_algebra

#### Violeta Hernández (Jun 22 2022 at 02:23):

@Eric Wieser

#### Eric Wieser (Jun 22 2022 at 10:39):

Which PR?

#### Violeta Hernández (Jun 22 2022 at 11:13):

#### Violeta Hernández (Jun 25 2022 at 15:37):

Got this on #14707 too

#### Violeta Hernández (Jun 25 2022 at 15:37):

I'm not at all familiar with this API or even the math here

#### Eric Wieser (Jun 25 2022 at 16:47):

I guess this might have been made worse by the `exterior_algebra R M = clifford_algebra 0`

refactor

#### Eric Wieser (Jun 25 2022 at 16:49):

Does replacing either begin/end block with sorry help?

#### Junyan Xu (Jun 26 2022 at 05:14):

No, it's typechecking `graded_algebra.ι R M`

that is slow.

```
by { fapply graded_algebra.of_alg_hom, apply lift _ _, fsplit, convert graded_algebra.ι R M }
```

is very fast, but we certainly don't want to convert data ...

#### Junyan Xu (Jun 26 2022 at 05:16):

It's weird that the types look exactly the same but `exact`

takes so long (10+ seconds) ...

#### Junyan Xu (Jun 26 2022 at 06:04):

It seems Lean is spending time checking the following defeq:

```
import algebra.direct_sum.algebra
import algebra.direct_sum.internal
open_locale direct_sum
example {S R} [comm_semiring S] [semiring R] [algebra S R] (p : submodule S R) :
non_unital_non_assoc_semiring.to_add_comm_monoid (⨁ i : ℕ, ↥(p ^ i)) =
direct_sum.add_comm_monoid _ _ := rfl
```

This `rfl`

is fast (typechecking 15ms, elaboration 200ms), but maybe Lean is unfolding too much in the exterior algebra situation.

(cf. docs#submodule.nat_power_graded_monoid, docs#direct_sum.algebra )

#### Junyan Xu (Jun 26 2022 at 06:07):

Wow, `let := graded_algebra.ι R M, exact this, `

is also super fast! Why is it different from `exact graded_algebra.ι R M`

??

I see the produced term is different:

```
exact let this : M →ₗ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i) := graded_algebra.ι R M
in this
```

#### Kevin Buzzard (Jun 26 2022 at 06:08):

With the `let`

version, laan is free to let the type be whatever it wants, so unification is happening in a different order

#### Junyan Xu (Jun 26 2022 at 06:10):

I hope terms lilke `exact let this : ... in this`

won't pose much an annoyance? If so then maybe that's the solution to be PR'd...

#### Junyan Xu (Jun 26 2022 at 06:12):

Or maybe there's some easy `change`

that can be inserted ..

#### Junyan Xu (Jun 26 2022 at 06:27):

OK, `apply`

works, as easy as that!

#### Junyan Xu (Jun 26 2022 at 06:59):

Another fix needs to be applied to the proofs: `graded_algebra.ι_apply`

needs to be replaced by `graded_algebra.ι_apply R M`

at two places (reduces from 10-12s to 3s).

#### Junyan Xu (Jun 26 2022 at 07:38):

#### Eric Wieser (Jun 26 2022 at 08:18):

Thanks!

#### Eric Wieser (Jun 29 2022 at 22:47):

A new one in file#number_theory/cyclotomic/primitive_roots here (and some other builds): https://github.com/leanprover-community/mathlib/runs/7120067385?check_suite_focus=true#step:6:12

#### Riccardo Brasca (Jun 29 2022 at 23:14):

I am going to sleep now, but I bet this is caused by `simps`

.

#### Paul Lezeau (Jun 30 2022 at 09:54):

I'm running into a timeout on #15000 when working with polynomial rings. An mwe would be something like

```
import ring_theory.dedekind_domain.ideal
import ring_theory.ideal.operations
import ring_theory.polynomial.basic
import ring_theory.unique_factorization_domain
open ideal polynomial unique_factorization_monoid
open_locale classical
variables {R : Type*} [comm_ring R] [is_domain R] [is_dedekind_domain R]
noncomputable instance {I: ideal R} [hI : is_maximal] : field (R ⧸ I) :=
((ideal.quotient.maximal_ideal_iff_is_field_quotient I).mp hI).to_field
--deterministic timeout
def problematic_definition {I : ideal R} (f : polynomial R)
(hI : is_maximal I) :
{J : ideal (polynomial $ R ⧸ I ) |
J ∈ normalized_factors (ideal.span ({ map I^.quotient.mk f } : set (polynomial $ R ⧸ I))) }
:= sorry
```

The issue seems to come from `normalized_factors`

, since removing it makes the statement work fine.

For context, I am trying to construct an `equiv`

of the form

```
def normalized_factors_equiv [is_domain R] [is_dedekind_domain R] (f : polynomial R) (I : ideal R)
(hI : is_prime I) (hI' : I ≠ ⊥ ) :
{J : ideal S | J ∈ normalized_factors (I.map (algebra_map R S)) } ≃
{J : ideal (polynomial $ R ⧸ I ) |
J ∈ normalized_factors (ideal.span ({ map I^.quotient.mk f } : set (polynomial $ R ⧸ I))) }
:= sorry
```

#### Paul Lezeau (Jun 30 2022 at 09:57):

Does anyone know what might be causing this?

#### Alex J. Best (Jun 30 2022 at 10:21):

Did you try adding `noncomputable! def`

?

#### Paul Lezeau (Jun 30 2022 at 10:50):

I'll try that now!

#### Riccardo Brasca (Jun 30 2022 at 11:05):

You can also make it a `lemma`

until it is `sorry`

free, this sometimes helps.

#### Paul Lezeau (Jun 30 2022 at 11:10):

The `noncomputable! def`

fix worked, thanks !

#### Paul Lezeau (Jun 30 2022 at 11:11):

Riccardo Brasca said:

You can also make it a

`lemma`

until it is`sorry`

free, this sometimes helps.

I'll keep that in mind!

#### Moritz Doll (Nov 04 2022 at 04:45):

Sorry, stupid question time: how do I increase the time limit in VSCode, the tips and tricks say there is a setting Lean Time Limit, but `ctrl+shift+p`

and `Lean: Time Limit`

does not work

#### Moritz Doll (Nov 04 2022 at 04:46):

less stupid question: why does `squeeze_simp`

take so much longer than `simp`

?

#### Moritz Doll (Nov 04 2022 at 04:51):

answer to first question is `ctrl+,`

and then searching for lean time limit

#### Floris van Doorn (Nov 04 2022 at 08:38):

It should be "Settings (`ctrl+,`

) -> search for `lean time limit`

"

#### Floris van Doorn (Nov 04 2022 at 08:39):

(please also make a PR to tips and tricks fixing the tip)

#### Floris van Doorn (Nov 04 2022 at 08:40):

I believe `squeeze_simp`

does some work after the `simp`

is done minimizing the list lemmas it found (maybe it rewrote with `foo`

, but the `simp`

will result in the same state if `foo`

was never applied).

#### Floris van Doorn (Nov 04 2022 at 08:40):

Oh, I should have read your third message before answering your first :-)

Last updated: Aug 03 2023 at 10:10 UTC