Skip to content

Conversation

@yongweiy
Copy link
Collaborator

gather.c turns

import nki.isa.constants as constants
from nki.isa.constants import oob_mode

def dma_copy(
    dst,
    src,
    dst_rmw_op: np.ufunc = None,
    oob_mode=constants.oob_mode.error,
    dge_mode=dge_mode.unknown,
    name=None,
) -> None: ...

into

nki.isa.neuron_isa.dma_copy(dst,src,dst_rmw_op = None,oob_mode = nki.isa.constants.oob_mode.error,dge_mode = nki.isa.constants.dge_mode.unknown,name = None): ...

nki.isa.dma_copy(dst,src,dst_rmw_op = None,oob_mode = nki.isa.constants.oob_mode.error,dge_mode = dge_mode.unknown,name = None): ...

Default value dge_mode.unknown cannot be resolved later by KLR when the second definition is used.

@yongweiy
Copy link
Collaborator Author

With the update, the globals have the alias:

nki.isa.dma_copy = nki.isa.neuron_isa.dma_copy

Copy link
Collaborator

@govereau govereau left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

lean_object *ref_expr = Python_Expr_mk(Python_Expr_name(target_name, Python_Ctx_load), pos);

def->str = lean_mk_string(alias_name);
def->name = alias_name;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should be:

def->name = lean_string_cstr(def->str);

name and str should refer to the same Lean object.
I think it may not matter, but this is what the comments say is true about this structure.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants