Skip to content

Setup some tracing for ml_translatorLib #1285

@ordinarymath

Description

@ordinarymath

Currently figuring out what is happening internally in ml_translatorLib is pretty much impossible. It would be nice if there's some tracing setup. It should probably be implemented using the Listener api similar to how it's done in the HOL4's simplifier[1].

[1]https://github.com/HOL-Theorem-Prover/HOL/blob/6ee078177f8f5ff059b57fb0d9ba3b090df1d1b9/src/simp/src/Trace.sml

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions