Siddharth
Siddharth
Superseded by #71
Two reasons: 1. LLVM's CMake config assumes that the binary/library one is building is configured using CMake's targets. However, Lean's `CMakeLists.txt` does not seem to use targets to build things...
TL;DR: I knew I could make `llvm-config` work, and using LLVM's `CMake` config seemed to require invasive changes to Lean's `CMake` config, which I was reluctant to perform.
@Kha would you like me to run a full `update-stage0`, since I do change the `src/stage0/CMakeLists.txt`? Running `update-stage0` would make the diff much larger. Perhaps we should update stage0 as...
@Kha I think you're right, now that we do not forward `-DLLVM, -DLLVM_CONFIG` to `stage0`, we don't need a bumped up `stage0/src/CmakeLists.txt` I'm still unclear on the CMake option forwarding...
@Kha I confess, I don't know the FFI well. If I understand the suggestion correctly, since we use raw pointers, we ought to cast the pointers to `usize_t` when crossing...
what's the difference between savedata and savestate? (I've never heard that terminology before)
Are there guarantees the GC makes? (pause time, for example?) What are the invariants we need to support for the GC to work?
@Kha I've updated the API to use `(Ptr α)` as a synonym for `USize`, and kept the opaque types (`BasicBlock`, `Value`, etc) around to index the `α` .
@Kha , I've fixed the API, and the warts left over in `CMakeLists.txt`.