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):
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
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: Aug 03 2023 at 10:10 UTC