Zulip Chat Archive

Stream: general

Topic: surprising "failed to generate bytecode" warning


Kevin Buzzard (Nov 18 2021 at 15:06):

Ashvni showed me a surprising warning: here's a MWE:

import number_theory.padics.ring_homs

variables (p : ) [fact (nat.prime p)]

def sets (H : Type*) := {s : set H // true}

def foo : sets (ℤ_[p]) :=
⟨(set.preimage (padic_int.appr) {id}), by trivial

/-
failed to generate bytecode for 'foo'
code generation failed, VM does not have code for 'classical.choice'
-/

Both the fact that it's a subtype and the fact that we're using padic_int.appr seem to be relevant. Can this be fixed? Should she worry if it can't? It's beyond me!

Floris van Doorn (Nov 18 2021 at 15:09):

Did you try adding noncomputable def and/or noncomputable theory?

Floris van Doorn (Nov 18 2021 at 15:11):

Ah, that doesn't seem to fix it...

Reid Barton (Nov 18 2021 at 15:12):

I have the feeling that this mostly happens because something should be a lemma not a def or vice versa

Reid Barton (Nov 18 2021 at 15:13):

however, I don't see how that could apply here...

Kevin Buzzard (Nov 18 2021 at 15:23):

Indeed, noncomputable def complains that it should be computable. appr is defined noncomputably in number_theory.padics_ring_homs and then made irreducible on line 383, I wondered if that had anything to do with it.

Floris van Doorn (Nov 18 2021 at 15:34):

It somehow also has to do with the fact that set is a function into Sort*:

import number_theory.padics.ring_homs

variables (p : ) [fact (nat.prime p)]

def foo {α β : Type} (f : α  β) : unit  Type := λ _, unit

def bar : {s : unit  Type // true} :=
foo (@padic_int.appr p _), trivial -- error

but

import number_theory.padics.ring_homs

variables (p : ) [fact (nat.prime p)]

def foo {α β : Type} (f : α  β) : Type := unit

def bar : {s : Type // true} :=
foo (@padic_int.appr p _), trivial -- no error

and

import number_theory.padics.ring_homs

variables (p : ) [fact (nat.prime p)]

def foo {α β : Type} (f : α  β) : unit   := λ _, 0

noncomputable def bar : {s : unit   // true} :=
foo (@padic_int.appr p _), trivial -- no error (but noncomputable is mandatory)

Eric Wieser (Nov 18 2021 at 17:33):

Is it possible my PR to remove noncomputable lemma from docs#classical.dec is to blame?

Eric Wieser (Nov 18 2021 at 17:33):

I thought we were safe because mathlib was happy

Kyle Miller (Mar 07 2022 at 10:48):

Kevin Buzzard said:

/-
failed to generate bytecode for 'foo'
code generation failed, VM does not have code for 'classical.choice'
-/

Both the fact that it's a subtype and the fact that we're using padic_int.appr seem to be relevant. Can this be fixed? Should she worry if it can't? It's beyond me!

I've just found a strange fix for this:

import number_theory.padics.ring_homs

variables (p : ) [fact (nat.prime p)]

def sets (H : Type*) := {s : set H // true}

local attribute [inline] set.preimage

def foo : sets (ℤ_[p]) :=
⟨(set.preimage (padic_int.appr) {id}), by trivial

I think it's got to do with the fact that the vm doesn't see that padic_int.appr is computationally irrelevant for some reason. But once it's expanded out to

def foo' : sets (ℤ_[p]) :=
⟨{x | padic_int.appr x  ({id} : set (  ))}, by trivial

then it's happy.


Last updated: Dec 20 2023 at 11:08 UTC