Lean3 reduction on eq.refl operating on string

Stream: general

[loki der quaeler]

Using 3.4.2 stable, i get a deterministic time out on reducing stringEqRefl below, but natEqRefl reduces as anticipated. Why is this?

def natEqRefl : 23 = 23 := eq.refl 23
#reduce natEqRefl

def stringEqRefl : "foo" = "foo" := eq.refl "foo"
#reduce stringEqRefl

[Eric Wieser]

3.4.2 is very old

[Eric Rodriguez]

(this happens in 3.40.0)

[Eric Rodriguez]

probably linked to lean#144

[Eric Rodriguez]

by this, even #eval stringEqRefl should be really slow for you, but it's blazing fast in modern versions

[Eric Rodriguez]

Lean tends to use the VM far more than the kernel

[loki der quaeler]

Another gremlin in the system "related" to this is that in VS Code, the line following the string flavored def gets indented one column, which not the def for ℕ (nor an equivalent for type bool).

#eval stringEqRefl returns quickly (in 3.40.0) with a:

result type does not have an instance of type class 'has_repr', dumping internal representation

[Eric Rodriguez]

I don't know what you mean. And yes, that's expected - Props get erased in the VM

[loki der quaeler]

(The #eval returns (to my human senses) equivalently quickly in 3.4.2 as well.) WRT the VS Code thing, it's two columns, not one:
lean-vscode-string-column-indent.gif

[Eric Rodriguez]

huh, that is odd. also, I guess the #eval is only slow for large strings; I wonder how a 4000 char string would perform,a s mentioned in that issue

[Eric Wieser]

Is there any reason you're using 3.4.2 and not something closer to 3.40.0?

[loki der quaeler]

purely because i'm not too bright. (i had asked elan to pull leanprover/lean:stable not realizing that stable pulled a newer version of 3)

[Eric Wieser]

You likely want to be using leanprover-community/lean instead