Yeah I dont understand why people are glad its down. I have an account specifically curated to my interests, where I unsubscribed from all the default subs and only subscribed to things I'm interested in. Theres a lot of great niche communities out there for my hobbies that I've found on reddit.
I worked at APL for 3 years (2015 - 2018) and loved my time there. Although, the work got repetitive over time and was no longer challenging, the thing I loved the most was the social environment. Theres a lot to be said for having a good team/group of people around you. I still keep in touch with some of them.
I tried a pyflow a couple years ago. It was very confusing and not intuitive at all, which is what I think one of the biggest advantages of these types of GUIs is supposed to be. Doing simple things like adding inputs and operations to the graph were very difficult.
I ended up developing my own tool based on the flowchart editor in pyqtgraph. The GUI for that was quite intuitive and the code to modify it was also far simpler. That said there are a few features from pyflow that I wish the pyqtgraph editor had, like subgraphs.
My question was specifically referring to these huge 500 proofs that only a handful of people have even attempted to understand. What is the upper limit of what our current state-of-the-art proof assistants can handle?
The problem is not the limit of what proof checkers can handle - that probably goes beyond all known math. The problem is that long standing theories that 500 page proof is based on are not yet transcribed into formal language, so you'd need to do them first.
Can you print variables in lldb with the debug information?
One compiler that I use which emits llvm ir added support for debug information recently and its now possible to set breakpoints in gdb but you can't print out any stack variables or anything so its not useful other than figuring out which code paths execute.
I'd like to learn more about this. Maybe contribute to the compiler and fix this issue.
> I'd like to learn more about this. Maybe contribute to the compiler and fix this issue.
You need to create a call to the `llvm.dbg.declare` intrinsic that connects the stack variable alloca to a DILocalVariable metadata node, and place the call after the stack variable alloca. The rest of LLVM will handle tracing the stack location through the compiler to the output, including the alloca being promoted.
