code generation failed?

Stream: general

[Marianne]

Hello all, I've encountered a confusing error message saying "code generation failed, VM does not have code for 'weeks'", but there is defination existing before. Could anyone understand this error or how to solve it? Much obliged！

[Marianne]

微信图片_20230731155732.png

[Scott Morrison]

As you've written noncomputable theory at the top of the file, Lean doesn't worry if it doesn't know how to compute your functions. As your functions involve real numbers, they noncomputable. (Some functions involving reals are computable, but not many!)

[Scott Morrison]

The solution is essentially: don't use #eval. Note that norm_num still works fine for doing calculations in tactic mode.

[Scott Morrison]

Alternatively you could change to using the rationals rather than the reals.

[Marianne]

Thank you for your help! So … you mean I'd better delete"#eval" and use "norm_num" or rational instead ?

[Kevin Buzzard]

You should update to Lean 4 if at all possible. But yes, #eval will not do real number calculations, you will need to stick to a "computable field" if you want to use Lean like a computer algebra package with things like #eval. It all depends on whether you're going for "let's let Lean compute the answer" or "let's tell Lean the answer and get it to prove that it's the correct answer".

[Marianne]

Thank you for your advice~ But I'm afraid I cannot update to Lean 4. :smiling_face_with_tear: Actually, I'm trying to let Lean compute the answer (learn to solve easy math problems)

[Marianne]

As for the question of real number, I'm not sure what I should do, since I didn't write "noncomputable theory" before, but the error still exists like this:

[Marianne]

微信图片_20230731155448.png

[Kevin Buzzard]

You can't use #eval with reals.

[Kevin Buzzard]

Reals are really complicated objects -- they are equivalence classes of Cauchy sequences and inherently noncomputable. Maybe you want to use floats or rationals?

[Marianne]

Oh! So I should not define 200/50/1000 as reals?

[Kyle Miller]

There's #norm_num for symbolically evaluating numbers, and it works fine with reals.

[Kyle Miller]

You probably have to put @[simp] in front of every definition that you want #norm_num to unfold while it evaluates.

[Kyle Miller]

https://leanprover-community.github.io/mathlib_docs/commands.html##norm_num

[Marianne]

Thanks a lot !!

[Marianne]

image.png

[Notification Bot]

Marianne has marked this topic as resolved.

[Notification Bot]

Marianne has marked this topic as unresolved.

[Notification Bot]

Marianne has marked this topic as unresolved.

[Marianne]

Sorry for bother again...I've just realized that I don't really understand why @[simp] has to be put in front of every definition, what's the function here?

[Siddhartha Gadgil]

What @Kyle Miller said was that you must put @[simp]in front of every definition "that you want #norm_num to unfold while it evaluates".

If you want simp and other tactics like norm_num to simplify a definition when it is encountered (i.e., replace lhs by rhs), you should indicate this by saying @[simp]

[Kyle Miller]

norm_num alternates between looking for numbers it can normalize and using simp to make further progress

[Marianne]

Probably, @[simp] can be regarded as a bridge between finding / computing something ?

[Kyle Miller]

It just adds it to the "simp set", which is a list of lemmas and definitions that simp uses. Here's an overview: https://leanprover-community.github.io/extras/simp.html

[Kyle Miller]

Putting @[simp] on current_savings adds the lemma current_savings = 200 for example. Then whenever simp comes across current_savings it replaces it with 200.

[Marianne]

I see~Thank you so much for your illustration :smile_cat: