max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: Nix: debugging tip

Browse source
This commit is contained in:
Sebastian Ullrich 2020-11-29 18:13:35 +01:00
parent 9527058df9
commit 967c9c7d00
1 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
doc/make/nix.md
View file

@ -104,3 +104,17 @@ nix run .\?rev=$(git rev-parse @^) scratch.lean
```
...more surely to come...
# Debugging
Since Nix copies all source files before compilation, you will need to map debug symbols back to the original path using `set substitute-path` in GDB.
For example, for a build on Linux with the Nix sandbox activated:
```bash
(gdb) f
#1 0x0000000000d23a4f in lean_inc (o=0x1) at /build/source/build/include/lean/lean.h:562
562 /build/source/build/include/lean/lean.h: No such file or directory.
(gdb) set substitute-path /build/source/build src
(gdb) f
#1 0x0000000000d23a4f in lean_inc (o=0x1) at /build/source/build/include/lean/lean.h:562
562 static inline void lean_inc(lean_object * o) { if (!lean_is_scalar(o)) lean_inc_ref(o); }
```