Zulip Chat Archive

Stream: lean4

Topic: Derived Instance not using "extern" attribute

Locria Cyber (Mar 08 2023 at 05:33):

For some reason, the derived Repr is not working correctly.

Raylib/Structures.lean

structure Vector2 where
  mk ::
  x : Float
  y : Float
-- deriving Inhabited

attribute [extern "lean_raylib__Vector2_mk"] Vector2.mk
attribute [extern "lean_raylib__Vector2_x"] Vector2.x
attribute [extern "lean_raylib__Vector2_y"] Vector2.y

set_option trace.Elab.definition true in
deriving instance Repr for Vector2

Locria Cyber (Mar 08 2023 at 05:34):

Main.lean

import Raylib
open Raylib

def main : IO Unit := do
  let a := Vector2.mk 1.0 2.0
  IO.println (repr a)
  IO.println a.x
  IO.println a.y

Locria Cyber (Mar 08 2023 at 05:34):

stdout

{ x := 0.000000, y := 0.000000 }
1.000000
2.000000

Locria Cyber (Mar 08 2023 at 05:37):

When I copy the generated code, it works.

structure Vector2 where
  mk ::
  x : Float
  y : Float
deriving Inhabited

-- from
-- set_option trace.Elab.definition true in
-- deriving instance Repr for Vector2
instance : Repr Vector2 where
  reprPrec :=
    fun x prec =>
      Std.Format.bracket "{ "
        (Std.Format.nil ++ Std.Format.text "x" ++ Std.Format.text " := " ++
                    Std.Format.group (Std.Format.nest 5 (repr x.x)) ++
                  Std.Format.text "," ++
                Std.Format.line ++
              Std.Format.text "y" ++
            Std.Format.text " := " ++
          Std.Format.group (Std.Format.nest 5 (repr x.y)))
        " }"

attribute [extern "lean_raylib__Vector2_mk"] Vector2.mk
attribute [extern "lean_raylib__Vector2_x"] Vector2.x
attribute [extern "lean_raylib__Vector2_y"] Vector2.y

Notification Bot (Mar 08 2023 at 05:41):

Locria Cyber has marked this topic as resolved.

Locria Cyber (Mar 08 2023 at 05:41):

(deleted)

Notification Bot (Mar 08 2023 at 05:43):

Locria Cyber has marked this topic as unresolved.

Locria Cyber (Mar 08 2023 at 06:00):

minimal reproducible https://github.com/locriacyber/debug-lean-derived-repr-extern

Mario Carneiro (Mar 08 2023 at 06:10):

I wonder if the generated instance is using primitive projections (and primitive projections are not going through the extern function definitions)

Mario Carneiro (Mar 08 2023 at 06:12):

Oh, did you put the attribute [extern] before the deriving instance Repr line?

Mario Carneiro (Mar 08 2023 at 06:13):

@Locria Cyber

Mario Carneiro (Mar 08 2023 at 06:14):

The compiler doesn't hot-swap the functions after the fact, so you have to make sure any replacements are set up before functions using the replacements are compiled

Locria Cyber (Mar 08 2023 at 06:29):

Mario Carneiro said:

Oh, did you put the attribute [extern] before the deriving instance Repr line?

it doesn't matter

Locria Cyber (Mar 08 2023 at 06:30):

Either way it's not working

Sebastian Ullrich (Mar 08 2023 at 07:23):

Mario Carneiro said:

I wonder if the generated instance is using primitive projections (and primitive projections are not going through the extern function definitions)

The derive handler creates Syntax, so I'm honestly not sure where the discrepancy could come from

Last updated: Dec 20 2023 at 11:08 UTC