Metadata-Version: 2.1
Name: lean-lldb
Version: 0.1.0
Summary: An LLDB extension for debugging Lean programs
Home-page: https://github.com/ydewit/lean-lldb
License: Apache-2.0
Keywords: debugging,lldb,lean
Author: Yuri de Wit
Author-email: ydewit@gmail.com
Requires-Python: >=3.7,<4.0
Classifier: License :: OSI Approved :: Apache Software License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.7
Classifier: Programming Language :: Python :: 3.8
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Requires-Dist: six (>=1.0.0,<2.0.0)
Project-URL: Repository, https://github.com/ydewit/lean-lldb
Description-Content-Type: text/markdown

# lean-lldb

[![License](https://img.shields.io/badge/license-Apache%202.0-blue.svg)](LICENSE)

`lean-lldb` is a set of custom LLDB formatters for Lean4 runtime objects. These formatters are designed to make debugging Lean4 programs more intuitive by providing meaningful representations of Lean4 objects in the LLDB debugger.

## Installation

1. Clone the repository:

   ```bash
   git clone https://github.com/ydewit/lean-lldb.git
   ```

2. Navigate to the project directory:

   ```bash
   cd lean-lldb
   ```

3. Source the formatters in your LLDB session:

   ```bash
   command script import lean_lldb.py
   ```

   Alternatively, you can add this command to your `~/.lldbinit` file for automatic loading:

   ```bash
   echo "command script import /path/to/lean_lldb.py" >> ~/.lldbinit
   ```

## Usage

Once the formatters are loaded, LLDB will automatically use them when displaying Lean4 runtime objects. You can inspect the values of variables and expressions in your Lean4 programs as usual, but with the enhanced, readable output provided by `lean-lldb`.

For example, when you inspect a Lean4 object:

```lldb
(lldb) p myLeanObject
```

The output will now show a more user-friendly representation of `myLeanObject`, making it easier to understand the state of your program.

## Contributing

Contributions are welcome! If you have ideas for improvements or encounter any issues, feel free to open a pull request or issue on the GitHub repository.

## License

This project is licensed under the MIT License - see the [LICENSE](LICENSE) file for details.

## Acknowledgments

Special thanks to the Lean4 community for their support and contributions.

## References

- [How to create LLDB type summaries and synthetic children for your custom types](https://melatonin.dev/blog/how-to-create-lldb-type-summaries-and-synthetic-children-for-your-custom-types/)
- [Examples from the LLDB repo](https://github.com/llvm/llvm-project/tree/main/lldb/examples/synthetic)
- [JUCE C++ LLDB formatters](https://melatonin.dev/blog/how-to-create-lldb-type-summaries-and-synthetic-children-for-your-custom-types/)
- [Tips for writing LLDB pretty printers](https://offlinemark.com/tips-for-writing-lldb-pretty-printers/)
- [Rust LLDB formatters](https://github.com/vadimcn/codelldb/blob/master/formatters/rust.py)
- [LLDB - Variable Formatting](https://lldb.llvm.org/varformats.html)
- [LLDB - Python Reference](https://lldb.llvm.org/use/python-reference.html)
- 
#   3. https://lldb.llvm.org/python_reference/lldb.formatters.cpp.libcxx-pysrc.html
#   4. https://github.com/llvm-mirror/lldb/tree/master/examples/summaries/cocoa
lldb.frame.get_locals()[0].GetChildMemberWithName('m_tag').GetValueAsUnsigned()
>>> lldb.frame.get_locals()[0].CreateValueFromAddress("test", lldb.frame.get_locals()[0].GetValueAsAddress() + 8, lldb.target.FindFirstType('size_t'))


var = lldb.frame.get_locals()[0]
var_size = var.GetType().GetByteSize()
size_t_size = lldb.target.FindFirstType('size_t').GetByteSize()
size_t = lldb.target.FindFirstType('size_t')
char = lldb.target.FindFirstType('char')

m_size = var.CreateValueFromAddress("m_size", var.GetValueAsAddress() + var_size, size_t)
m_capacity = var.CreateValueFromAddress("m_capacity", var.GetValueAsAddress() + var_size + size_t_size, size_t)
m_length = var.CreateValueFromAddress("m_length", var.GetValueAsAddress() + var_size + size_t_size + size_t_size, size_t)
m_data = var.CreateValueFromAddress("m_data", var.GetValueAsAddress() + var_size + size_t_size + size_t_size + size_t_size, char)

m_data.AddressOf()

typedef struct {
    lean_object m_header;
    size_t      m_size;     /* byte length including '\0' terminator */
    size_t      m_capacity;
    size_t      m_length;   /* UTF8 length */
    char        m_data[0];
} lean_string_object;


