Overview
========
[](LICENSE)
`lean_lldb` is an LLDB extension for debugging Lean programs.
It can be useful for debugging and troubleshooting stuck threads and crashes in Lean programs. Unlike most popular languages, Lean does not have *yet* (note that this is part of the roadmap) a debugger and without this extension we are stuck inspecting the lower-level Lean runtime in C.
When analyzing the state of a Lean process, normally you would only have
access to Lean "runtime-level" information: most variables would be of type
`lean_object*`, and stack traces would only contain Lean internal calls and
calls to library functions. Unless you are a Lean developer troubleshooting
the a Lean progream, that is typically not very useful. This extension,
however, allows you to view a more compact and accessible representation of the same runtime information about the execution of
a program. At this point the only thing this extension provides is printing the values of variables, but it could also list the source code, display Lean
stack traces, etc.
While Lean already provides a similar extension for gdb [out of the box](
https://github.com/leanprover/lean4/blob/38288ae07a24f469a85fd10e93cbbb130f0e9f6c/src/bin/lean-gdb.py),
LLDB might be the debugger of choice on some operating systems, e.g.
on Mac OS.
This extension requires Lean programs to be built with debugging symbols enabled (see `buildType := .debug` in Lake). For now, a debugging build of the Lean runtime is not required, but that may change when we provide the ability to list Lean source code and Lean stack traces.
Features
========
`lean_lldb` targets CPython 3.5+ and supports the following features:
* pretty-priting of runtime values:
* `lean_ctor_object`
* `lean_closure_object`
* `lean_array_object`
* `lean_scalararray_object`
* `lean_string_object`
* `lean_mpz_object`
* `lean_thunk_object`
* `lean_task_object`
* `lean_ref_object`
* `lean_external_object`
Some interesting ideas to consider:
* printing of local variables
* printing of Lean-level stack traces
* listing the Lean source code
* walking up and down the Lean call stack
*
**NOTE**: Although it may be interesting to push this project further and implement these additional features, a better use of time would be to look into generating DWARF symbols for a future, first-class debugger for Lean.
Installation
============
If your version of LLDB is linked against system libpython, it's recommended
that you install the extension to the user site packages directory and allow
it to be loaded automatically on start of a new LLDB session:
```shell
$ python -m pip install --user lean-lldb
$ echo "command script import lean_lldb" >> ~/.lldbinit
$ chmod +x ~/.lldbinit
```
Alternatively, you can install the extension to some other location and tell LLDB
to load it from there, e.g. ~/.lldb:
```shell
$ mkdir -p ~/.lldb/lean_lldb
$ python -m pip install --target ~/.lldb/lean_lldb lean-lldb
$ echo "command script import ~/.lldb/lean_lldb/lean_lldb.py" >> ~/.lldbinit
$ chmod +x ~/.lldbinit
```
MacOS
-----
LLDB bundled with MacOS is linked with the system version of CPython which may not even
be in your PATH. To locate the right version of the interpreter, use:
```shell
$ lldb --print-script-interpreter-info
```
The output of the command above is a JSON with the following structure:
```
{
"executable":"/Library/.../Python3.framework/Versions/3.9/bin/python3",
"language":"python",
"lldb-pythonpath":"/Library/.../LLDB.framework/Resources/Python",
"prefix":"/Library/.../Python3.framework/Versions/3.9"
}
```
Where the value for "executable" is the CPython version that should be used to install
`lean_lldb` for LLDB to be able to successfully import the script:
```shell
$(lldb --print-script-interpreter-info | jq -r .executable) -m pip install lean_lldb
```
Usage
=====
Start a new LLDB session:
```shell
$ lldb /path/to/lean/program
```
or attach to an existing Lean process:
```shell
$ lldb /path/to/lean/program -p $PID
```
If you've followed the installation steps, the extension will now be automatically
loaded on start of a new LLDB session:
Pretty-printing
---------------
All known `lean_object`'s (i.e. runtime types) are automatically pretty-printed
when encountered, as if you tried to get a `repr()` of something in Python REPL,
e.g.:
```
(lldb) v -P2
(lean_object *) ctor = 0x0000000146458678 (Ctor#0.{1} objs=3, scalars=False) {
[0] = 0x0000000000000007 (Box 3)
[1] = 0x000000000000000d (Box 6)
[2] = 0x0000000000000013 (Box 9)
}
```
Potential issues and how to solve them
======================================
CPython 2.7.x
-------------
CPython 2.7.x is not supported. There are currently no plans to support it in the future.
Missing debugging symbols
-------------------------
Debugging symbols are required only for this extension to work. You can check if they are available as follows:
```shell
$ lldb /usr/bin/python
$ (lldb) type lookup lean_ctor_object
```
If debugging symbols are not available, you'll see something like:
```shell
no type was found matching 'lean_ctor_object'
```
Development
===========
Running tests
-------------
Tests currently require `make` and `docker` to be installed.
To run the tests against the *latest* released Lean version, do:
```
$ make test
```
To run the tests against a specific Lean (or LLDB) version, do:
```
$ LEAN_VERSION=X.Y LLDB_VERSION=Z make test
```
Supported CPython versions are:
* `4.10`
Supported LLDB versions:
* `16`
Contributions
=============
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.
Acknowledgements
================
I would like to thank [Roman Podoliaka](https://github.com/malor) for the [cpython-lldb project](https://github.com/malor/cpython-lldb). This project was a source of inspiration and a template for what you see here.
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)
Raw data
{
"_id": null,
"home_page": "https://github.com/ydewit/lean-lldb",
"name": "lean-lldb",
"maintainer": null,
"docs_url": null,
"requires_python": "<4.0,>=3.7",
"maintainer_email": null,
"keywords": "debugging, lldb, lean",
"author": "Yuri de Wit",
"author_email": "ydewit@gmail.com",
"download_url": "https://files.pythonhosted.org/packages/49/8a/e07d35279c9bfd2fe5df4a6b3597783eb3126475d5933c63303f56c767e1/lean_lldb-0.1.0.tar.gz",
"platform": null,
"description": "Overview\n========\n\n\n\n[](LICENSE)\n\n`lean_lldb` is an LLDB extension for debugging Lean programs.\n\nIt can be useful for debugging and troubleshooting stuck threads and crashes in Lean programs. Unlike most popular languages, Lean does not have *yet* (note that this is part of the roadmap) a debugger and without this extension we are stuck inspecting the lower-level Lean runtime in C.\n\nWhen analyzing the state of a Lean process, normally you would only have\naccess to Lean \"runtime-level\" information: most variables would be of type\n`lean_object*`, and stack traces would only contain Lean internal calls and\ncalls to library functions. Unless you are a Lean developer troubleshooting\nthe a Lean progream, that is typically not very useful. This extension,\nhowever, allows you to view a more compact and accessible representation of the same runtime information about the execution of\na program. At this point the only thing this extension provides is printing the values of variables, but it could also list the source code, display Lean\nstack traces, etc.\n\nWhile Lean already provides a similar extension for gdb [out of the box](\nhttps://github.com/leanprover/lean4/blob/38288ae07a24f469a85fd10e93cbbb130f0e9f6c/src/bin/lean-gdb.py),\nLLDB might be the debugger of choice on some operating systems, e.g.\non Mac OS.\n\nThis extension requires Lean programs to be built with debugging symbols enabled (see `buildType := .debug` in Lake). For now, a debugging build of the Lean runtime is not required, but that may change when we provide the ability to list Lean source code and Lean stack traces.\n\n\nFeatures\n========\n\n`lean_lldb` targets CPython 3.5+ and supports the following features:\n\n* pretty-priting of runtime values:\n * `lean_ctor_object`\n * `lean_closure_object`\n * `lean_array_object`\n * `lean_scalararray_object`\n * `lean_string_object`\n * `lean_mpz_object`\n * `lean_thunk_object`\n * `lean_task_object`\n * `lean_ref_object`\n * `lean_external_object`\n\n\nSome interesting ideas to consider:\n* printing of local variables\n* printing of Lean-level stack traces\n* listing the Lean source code\n* walking up and down the Lean call stack\n* \n\n**NOTE**: Although it may be interesting to push this project further and implement these additional features, a better use of time would be to look into generating DWARF symbols for a future, first-class debugger for Lean.\n\nInstallation\n============\n\nIf your version of LLDB is linked against system libpython, it's recommended\nthat you install the extension to the user site packages directory and allow\nit to be loaded automatically on start of a new LLDB session:\n\n```shell\n$ python -m pip install --user lean-lldb\n$ echo \"command script import lean_lldb\" >> ~/.lldbinit\n$ chmod +x ~/.lldbinit\n```\n\nAlternatively, you can install the extension to some other location and tell LLDB\nto load it from there, e.g. ~/.lldb:\n\n```shell\n$ mkdir -p ~/.lldb/lean_lldb\n$ python -m pip install --target ~/.lldb/lean_lldb lean-lldb\n$ echo \"command script import ~/.lldb/lean_lldb/lean_lldb.py\" >> ~/.lldbinit\n$ chmod +x ~/.lldbinit\n```\n\nMacOS\n-----\nLLDB bundled with MacOS is linked with the system version of CPython which may not even\nbe in your PATH. To locate the right version of the interpreter, use:\n```shell\n$ lldb --print-script-interpreter-info\n```\nThe output of the command above is a JSON with the following structure:\n```\n{\n \"executable\":\"/Library/.../Python3.framework/Versions/3.9/bin/python3\",\n \"language\":\"python\",\n \"lldb-pythonpath\":\"/Library/.../LLDB.framework/Resources/Python\",\n \"prefix\":\"/Library/.../Python3.framework/Versions/3.9\"\n}\n```\nWhere the value for \"executable\" is the CPython version that should be used to install\n`lean_lldb` for LLDB to be able to successfully import the script:\n```shell\n$(lldb --print-script-interpreter-info | jq -r .executable) -m pip install lean_lldb\n```\n\nUsage\n=====\n\nStart a new LLDB session:\n\n```shell\n$ lldb /path/to/lean/program\n```\n\nor attach to an existing Lean process:\n\n```shell\n$ lldb /path/to/lean/program -p $PID\n```\n\nIf you've followed the installation steps, the extension will now be automatically\nloaded on start of a new LLDB session:\n\nPretty-printing\n---------------\n\nAll known `lean_object`'s (i.e. runtime types) are automatically pretty-printed\nwhen encountered, as if you tried to get a `repr()` of something in Python REPL,\ne.g.:\n\n```\n(lldb) v -P2\n(lean_object *) ctor = 0x0000000146458678 (Ctor#0.{1} objs=3, scalars=False) {\n [0] = 0x0000000000000007 (Box 3)\n [1] = 0x000000000000000d (Box 6)\n [2] = 0x0000000000000013 (Box 9)\n}\n```\n\nPotential issues and how to solve them\n======================================\n\nCPython 2.7.x\n-------------\n\nCPython 2.7.x is not supported. There are currently no plans to support it in the future.\n\nMissing debugging symbols\n-------------------------\n\nDebugging symbols are required only for this extension to work. You can check if they are available as follows:\n\n```shell\n$ lldb /usr/bin/python\n$ (lldb) type lookup lean_ctor_object\n```\n\nIf debugging symbols are not available, you'll see something like:\n\n```shell\nno type was found matching 'lean_ctor_object'\n```\n\n\nDevelopment\n===========\n\nRunning tests\n-------------\n\nTests currently require `make` and `docker` to be installed.\n\nTo run the tests against the *latest* released Lean version, do:\n\n```\n$ make test\n```\n\nTo run the tests against a specific Lean (or LLDB) version, do:\n\n```\n$ LEAN_VERSION=X.Y LLDB_VERSION=Z make test\n```\n\nSupported CPython versions are:\n* `4.10`\n\nSupported LLDB versions:\n* `16`\n\nContributions\n=============\n\nContributions 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.\n\n\nAcknowledgements\n================\n\nI would like to thank [Roman Podoliaka](https://github.com/malor) for the [cpython-lldb project](https://github.com/malor/cpython-lldb). This project was a source of inspiration and a template for what you see here.\n\n\nReferences\n==========\n\n- [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/)\n- [Examples from the LLDB repo](https://github.com/llvm/llvm-project/tree/main/lldb/examples/synthetic)\n- [JUCE C++ LLDB formatters](https://melatonin.dev/blog/how-to-create-lldb-type-summaries-and-synthetic-children-for-your-custom-types/)\n- [Tips for writing LLDB pretty printers](https://offlinemark.com/tips-for-writing-lldb-pretty-printers/)\n- [Rust LLDB formatters](https://github.com/vadimcn/codelldb/blob/master/formatters/rust.py)\n- [LLDB - Variable Formatting](https://lldb.llvm.org/varformats.html)\n- [LLDB - Python Reference](https://lldb.llvm.org/use/python-reference.html)\n",
"bugtrack_url": null,
"license": "Apache-2.0",
"summary": "An LLDB extension for debugging Lean programs",
"version": "0.1.0",
"project_urls": {
"Homepage": "https://github.com/ydewit/lean-lldb",
"Repository": "https://github.com/ydewit/lean-lldb"
},
"split_keywords": [
"debugging",
" lldb",
" lean"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "c94d4819994b1eaefd3e38c3ce086135501eee3bfdee34f366d6ad043fa5d8c8",
"md5": "d93bc709a8b4cf63b0d7217d86146ed0",
"sha256": "ae8234a4eb690f0207fb3eb1045c759e197b889ddee85132586a048f09ee7124"
},
"downloads": -1,
"filename": "lean_lldb-0.1.0-py3-none-any.whl",
"has_sig": false,
"md5_digest": "d93bc709a8b4cf63b0d7217d86146ed0",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": "<4.0,>=3.7",
"size": 13504,
"upload_time": "2024-08-17T22:37:21",
"upload_time_iso_8601": "2024-08-17T22:37:21.984532Z",
"url": "https://files.pythonhosted.org/packages/c9/4d/4819994b1eaefd3e38c3ce086135501eee3bfdee34f366d6ad043fa5d8c8/lean_lldb-0.1.0-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "498ae07d35279c9bfd2fe5df4a6b3597783eb3126475d5933c63303f56c767e1",
"md5": "511ee3803865fef425294d6f1116fdfd",
"sha256": "a3b77ad829b0e3c52c9654a36ee2811e9438623206d729f0da6daba34d1a91ef"
},
"downloads": -1,
"filename": "lean_lldb-0.1.0.tar.gz",
"has_sig": false,
"md5_digest": "511ee3803865fef425294d6f1116fdfd",
"packagetype": "sdist",
"python_version": "source",
"requires_python": "<4.0,>=3.7",
"size": 14207,
"upload_time": "2024-08-17T22:37:23",
"upload_time_iso_8601": "2024-08-17T22:37:23.756042Z",
"url": "https://files.pythonhosted.org/packages/49/8a/e07d35279c9bfd2fe5df4a6b3597783eb3126475d5933c63303f56c767e1/lean_lldb-0.1.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-08-17 22:37:23",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "ydewit",
"github_project": "lean-lldb",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"lcname": "lean-lldb"
}
JSON
