Shouldn't that have already been do-able? I know the The MOnSter 6502 is a thing. The 386 I have no idea about though, that's to far out of my wheel house.
I'm (hopefully) getting a G1X soon, so I think I'm going to put it to work printing this stuff out. I'm now excited for this as a use case and I kind of hope someone builds something to convert an existing factorio world into a 3d model, though it might be to big to actually print so maybe a way to take a section would be even better.
Yeah, that sounds like the system I rediscovered. The only other thing I'm adding to try and lean more into that system are assertions(?) that are in the middle of a function, that can basically break it up into blocks on their own where the first block proves it true and the second block assumes it's true. So effectively the same thing as breaking it into 2 smaller functions. My main thing right now is, I'm fairly certain there is something wrong with my compiler, I'm a basically a novice in contracts, I'm intermediate in compilers, I'm a novice on SMT proofs, and I wrote the whole thing at this point using AI just to test an idea. So I'm just trying to throw everything I can at it to try and break it. I need to start building it again from scratch (without AI) so I can truly understand where it might break and what doesn't work.
Ah damn, okay. Long functions with a lot of sub calls is a known problem. I've been able to work around some of the issues tried to them by making every function an independent "compile unit." and then solving them each individually in the SMT solver. My experience in contract based programming is still relatively light, I won't lie there. The most I've had to do with contracts was ada, and even then it wasn't much. Everything else has been self enforced in languages without explicit support (and hence no compile time checking.)
You sounds like you have more experience than me in this space (specifically contracts). I'm curious if you have any examples right off hand that would need whole program analysis. I need more examples to throw at my toy language that's not just another lock free work stealing queue.
Yeah, I heard spark was used on a small component in the nvidia gpu firmware so others seemingly agree. I'm mainly in the user mode driver space so my ideas have been around having a kernel mode driver that (assuming a correctly functioning pc) can't crash and user mode drivers that can't be exploited (at least in the rop chain sense). I'm kind of picking ideas from other languages that I like zig's error handling, ada's contracts, rust's lifetimes (hopefully soon to be replaced with more contracts instead), and things like how you can use "gas" in lean to prove a loops will terminate. I'm mainly building it up with AI right now for experimentation, but I also can't really trust it to be correct either because of using AI. Once I settle on the syntax more and pump out a lot more tests, I'm probably going to rewrite the compiler by hand (hopefully in the custom language itself.)
There is a small hint of it at the end, but I really hope compile time contract assertions become more common. I know some languages like spark, dafny and a few others do it and generate implicit contracts for things like divide by 0. I've been experimenting with my own custom language that do these things and going back to c++ every day at work is actually a slight let down because of it.
It's been a while since I've tried to run it, but it's a mix of Nvidia and AMD GPUs and only AMD CPUs (everything portable is all AMD though and that's where my gripes are.) I'm sure the opencl backend has gotten better over time, but it always seems to drag behind the cuda backend. At this point I wish we could just have a vulkan backend and be done with it.
Thanks for bringing that up though, after a quick search that I guess I haven't done in a long time, it appears that colmap does now have a hip backend. So I guess that's going to be my weekend now.
I'm sorry, but the article doesn't cover anything about the preprocessing steps that are required for 90% of gaussian splat implementations. That preprocessing step is almost always colmap which takes pictures or videos and uses SfM to figure out the camera parameters and their position in the 3d scene, it then does basic point reconstruction and dense point reconstruction. That info is what gaussian splats take in, it converts the points from a colmap project into gaussians and then optimizes them through differentiable rendering using backprop to optimize the gaussians to better match the images at the calculated positions of the camera from colmap. Looking over the project files also shows that they consume colmap projects, my question wasn't about the gaussian splat implementation, it was about the defacto standard colmap preprocessing step that is also required.
Thanks, I've been exploring a lot of the papers and seeing what I can get working. Some of it really has been interesting, but I just never seem to be able to get it to work well. I might just need to throw myself at it all a bit more. Thanks for the links though, I'll check them out.
I'm still very fascinated by gaussian splatting, but the issue I always run into is the need to use colmap to generate the camera positions and get the initial point cloud. Which colmap effectively still needs Nvidia for dense point clouds last I checked. I'm curious though does anyone have anything else they've tried that worked well? I've tried a few different things (most of the time getting stuck on just compiling the thing) so I'm curious if anyone has any suggestions that I should focus more heavily on getting working. I have some poor quality videos I'd like to try and use and I'm willing to put in some manual work, but it feels like it's all automatic or nothing. Thanks for any suggestions that any of you have.
I feel like it's good to note since I missed it. This post is from Feb 13, 2023. He has up to 8 posts on this at this point which don't appear to be linked to from this post. I think linking to all of them would be a bit much, but they're all currently listed on his main page [1].
Just in case anyone else decides to write along like the article suggests. I chose to use the live.lean-lang.org link, but it seems to default to a newer version of lean where the simp[xor] actually returns both sides still wrapped in the lambdas so the next simp[add_comm] will actually fail. The way to get around it is changing the version to v4.32.0 which the article doesn't seem to mention.
As someone who is in the rendering space for work. Having a higher framerate does help, but in a weird way. Basically the start of the frame rendering is what mostly dictates where objects are rendered. By getting a higher framerate the position of objects that you see in game are much closer to their "real" position. So it's less about seeing more frames at that point and more about seeing the most up to date information possible. Technically it could be possible to render the frame in sync with the framerate and just offset the rendering so it finishes right before it's pushed to the screen, but if you're slightly wrong you'll get really bad stuttering and the execution time of gpus and the cpu submitting the work isn't really deterministic.
Being fully stopped at a stop light isn't putting my or anyone else's life in danger. If I have a phone in my hand the car is not moving. I also finished the comment before the light turned green so the phone also was no longer in my hand when I needed to start moving.
Let me know if you want to hear anything specific about it. It kind of works, so it's not something I recommend doing if it can be avoided, but as Roxxik pointed out there is much room for improvement since this was just a naive just get it to run experiment.
On the technical details of mmap I agree (at least while single threaded which is how I believe I'm running it), but making it async does sound like an interesting method for speeding it up. My only goal with my testing was get as large of a model as possible running on a computer that "can't run it." I'm going to have to actually read through the code and figure out how it really works to really make any good optimizations, but as before this was just experiments with using and LLM (claude + codex) to just get it running. Since if they couldn't get it running I'm not sure if I would have wanted to spend time trying to get it working myself.
I also know I did some things that would actually make the perf worse to, like I believe I also had AI mmap the KV Cache to make sure to runs under any circumstance. For actual optimizations based on what I currently know, I'm probably going to try and get the llm running under my igpu on my laptop with persistent shader that has some kind of inbuilt request mechanism. That way the weights that are loaded can be used as fast as possible.
For the expert prediction, I assume I could use the medusa paper as kind of a kick off point for that since I'm already using it to try and predict the next 4 tokens. Doing verification on those 4 tokens is about as much as I can do though since it started to thrash on loading the experts. So some method of predicting even more tokens, but then batching together those with the same experts would probably yield slightly better results in this weird case.
Note: All of my tests have been around programming since that's the use case I'm interested in. I don't actually know if this would preform well in other cases (and anything more broad than that I assume would be slower.)
Yeah I'll see what I can transfer over from my llama.cpp work. As before I'm not too experienced with llm work, but I have a lot of experiments I'm trying out. So I'll make a PR if I get any interesting results.
I was actually just working on the same thing as this, but I went down the route of mmapping the entire model into memory to avoid the extra ram usage. I also had Claude implement Medusa[1] on the model to try and avoid loading an additional model into memory but still get the benefits of MTP. Currently at a stop light so I can't list everything and I didn't get to read your full post either yet.
To expand since I just got home, I'm making all of my modifications to llama.cpp, the goal was to eventually put this on a SBC of some kind with an nvme to handle the mmapped files. I think the theoretical limit of my current setup is about 1.8 tok/s based on prior testing but that is also with the additional medusa heads not fully trained (I honestly don't know if the counting it's generated tokens or not.)
In the end it seems like the idea we had is similar, I just don't know how to write an llm parser/runner from scratch yet and instead of specifying what needed to stay in memory I just let the linux kernel handle it.
Oh last note, I also capped llama.cpp usage to 16GB of my 32GB, so it might be possible to get it down even lower.
I think I can understand that reasoning. I do have a tendency to explore, especially at the start since it gives me a view of what the site can already do, cause I wouldn't want to run into issues with my own projects without knowing of the possible limitations ahead of time.
If anything since the keyboard shortcut already exists, you could always put it in little cursor menu at the bottom of the screen. But yeah up to you, I look forward to your progress.
Seems interesting an I'll take more of a peek after work, but one thing that stood out to me is the only way back to the home page after navigating to a repo is the back button. Going back to the home page via the back button also doesn't retain that "new" was selected. But I agree with others, I do like the simplicity of the site.
I can't say I know how they actually did it, but taking a look at the trailer I can point out that it looks like the spaces are confined and your character is on rails. I'm mainly going off of the instant direction changes that don't appear to be 45 degrees off from the camera direction. Once it's constrained down to a single line/path you could do some wild things like cube mapping a video, where the position in the video is tied to the characters position. I can't say I know how they would take that video though, my best guess there is the scenes are constructed in 3d software, just it was to expensive for real time rendering.
All good, and agreed the fork author is in the wrong here. I just like keeping the facts straight since that can inform better arguments and discussions.
An example give by donho is "SomeProject : a macOS port of Notepad++" so it seems like the name can be used which will make it appear in searches. It just has to be clearly something else.
The only place I see that is from a user "LiEnby" not "aletik", and none of aletik's existing messages are edited. All replies I see with the message are also to LiEnby. I don't agree with aletik's slow response in any way, but I don't think your claim is correct either. Do you have anything to prove that this was said by aletik?