bytecode?

Stream: general

[Sebastien Gouezel]

In a file with noncomputable theory, I get the trace message

failed to generate bytecode for 'locally_compact_of_compact'
code generation failed, VM does not have code for 'locally_compact_of_compact_nhds'

What does this mean, and should I worry?

[Bryan Gin-ge Chen]

I got that message before when I had accidentally labeled a def as a theorem / lemma. Not sure if that applies in your case or not.

[Reid Barton]

Usually it means there is a lemma whose type is not a Prop, yes. In this case it is because I forgot to mark locally_compact_space as a Prop.

[Sebastien Gouezel]

Indeed, it solves the problem. Thanks!

[Johannes Hölzl]

I have a fix for mathlib

[Reid Barton]

Thanks :+1: