Zulip Chat Archive

Stream: general

Topic: Meta weirdness (was: `norm_num` question)

Notification Bot (Sep 02 2022 at 20:33):

Michael Stoll has marked this topic as unresolved.

Michael Stoll (Sep 02 2022 at 20:37):

Here is something weird: When I additionally import analysis.normed.field.basic in the example above, then I get an error message rec_fn_macro only allowed in meta definitions at the line meta def prove_test : ....
This does not occur when I instead import one of the files imported by analysis.normed.field.basic. What is going on here?
In a similar situation, I get an error message missing 'noncomputable' modifier, definition 'prove_foo' depends on 'rat.normed_field', which seems to be triggered by the use of norm_num.prove_ne. This is quite annoying...

Kevin Buzzard (Sep 02 2022 at 22:03):

Coincidentally this came up within the last day or two on the Discord. You can fix it with instance : ring ℚ := division_ring.to_ring ℚ. See #16349 which probably @Mario Carneiro should be alerted to...(and which will fix the problem if the PR is accepted, but the PR might cause other issues)

Michael Stoll (Sep 03 2022 at 07:54):

Thanks, Kevin!
Can you also explain how this error arises? (Just out of curiosity.)

Kevin Buzzard (Sep 03 2022 at 08:38):

The part I understand: the import makes the ring structure on the rationals noncomputable, because the typeclass inference system can find a new way to prove Q is a ring after the import, via normed_ring which is noncomputable, and by chance this is the preferred way after the import. The fix is to explicitly make the computable construction and explicitly add it into the system, which then prefers this choice and all of a sudden it's computable again. The part I don't understand is the rec_fn_macro error, I searched for it on this site and found several other occurrences, which all seemed to be to do with computability, but I can't say I understand the problem properly. The reason I tagged Mario in the previous post was two-fold; firstly to point out the PR to him (becuase there might be reasons against the change) but secondly to alert him to your error (which I think he understands quite well).

Mario Carneiro (Sep 03 2022 at 08:40):

The issue is when some auxiliary definition mistakenly gets marked computable when it shouldn't be, there is some edge case here that results in bad error messages

Kevin Buzzard (Sep 03 2022 at 08:41):

I was hoping that I could fix everything by adding noncomputable! all over the place but I couldn't get rid of the error.

Mario Carneiro (Sep 03 2022 at 08:43):

IIRC if you put noncomputable theory too you can get noncomputable on that pesky internal definition

Michael Stoll (Sep 03 2022 at 08:51):

It looked like analysis.normed.field.basic uses noncomputable theory, but I didn't look at it too closely.

Yaël Dillies (Sep 03 2022 at 15:04):

Yeah, we can make rat.normed_field computable using some trickery. I can do that if you want.

Michael Stoll (Sep 03 2022 at 17:45):

For now, I am happy with the workaround that Kevin mentioned. But it would be nice, of course, if the error would not show up in the first place.

Last updated: Dec 20 2023 at 11:08 UTC