HN Explorer

4 comments

[ 2.4 ms ] story [ 23.4 ms ] thread
Syzygies
I need a version of this for Lean 4; perhaps I can adapt this code.

AI generally struggles with less popular languages, and particularly with Lean 4, which is an excellent general purpose programming language that happens to have a primary goal to be a proof assistant. This skew in the training corpus really confuses AI.

Claude Opus 4 does better. I've looked at ways to serve the Lean 4 documentation; this Zig project is a better model for me.

Nia (https://www.trynia.ai) should generalize these tools, but it appears to have a "code base" focus for now. The right approach, but too specific a "system prompt".

1899-12-30
Are there any MCP servers that enrich the context with data from a language server and fetches relevant documentation based on the types provided from that information?
iudqnolq
I have a gut feeling that writing this kind of MCP server can't be the future of software development. I'd expect a two year old AI model to need this kind of handholding, but I don't understand why it's still necessary.

Couldn't any modern AI model know that Zig docs are relevant to the question, figure out how to find the docs, write some code to parse it, and guess how frequently to update it's cache?

I expect there to be plenty of problems AI can't write for the foreseeable future but they have a very different vibe from this.

Edit: I just asked Claude Sonnet 4 to pretend it has a tool that makes docs available that has an update frequency parameter. It said the zig stdlib should be updated weekly but the Java stdlib would only need quarterly. Seems reasonable to me.

ivanjermakov
> outdated docs are a problem

What do you need (external) docs for? Stdlib source code is available right away.