mbid · HackerTrans

mbid

584 karmajoined 9 yıl önce

Submissions

Stop using REST for state synchronization (2024)

mbid.me

2 pointsby mbid2 yıl önce1 comments

comments

11 gün öncediscuss

That's pretty much the flow I formalized here: https://github.com/nvidia/rumpelpod

Instead of generating patches, this exposes the agent's checkout as a git remote though.

Most similar tools (and I believe your tooling as well?) bind-mount the repository checkout from the host into the container. This was always a source of user and permission errors for me, since you have to align the user ids inside and outside the container. Also, some build tools don't like it when the repo is on a different filesystem (bind mount vs container root) than the rest of the system. So I made rumpelpod just bake the repo checkout into the base image that the container is launched from, and since then I haven't had any issues like this.

For giving the agent access to a docker daemon I found sysbox to work very well. Usually the advice for nested containers is to pass in the host's docker socket into the container. But that would break the outer container isolation completely, since access to the docker daemon is equivalent to root access on the host. With sysbox it's trivial to run a nested docker instance inside the outer container. I haven't tried it with podman yet though. In theory sysbox is just another OCI runtime, but there's probably some tinkering required to get it to work.

26 gün öncediscuss

Yeah I should add a video to the README.

Have you tried running `rumpel codex foo123` in one of your repositories, asking it to commit something, then `rumpel merge foo123` to get the changes back to your local checkout? Use a different terminal for the merge command, or detach from the codex session with `ctrl-a d`. You can also look at the commit first with `rumpel review foo123`, or get a shell inside the agent environment via `rumpel enter foo123`.

26 gün öncediscuss

I recently got the tool I use to orchestrate agents in (remote/secure) devcontainers open-sourced at work to solve this properly: https://github.com/nvidia/rumpelpod

As others here have pointed out, it's exceedingly unlikely that a blocklist like proposed in the issue would ever be complete. You shouldn't allow agents direct yolo-access to your machine if it has sensitive data.

Codex works particularly well as a remote agent harness because of its client-server architecture: The server component runs in the container, which might be remote, while the client runs locally. So, in contrast to e.g. the claude cli where the frontend also runs remotely, there's no lag when you write/edit prompts.

2 ay öncediscuss

What's the point?

Sweden has lots of potential for long-term energy storage as hydro power, which makes wind power viable. Northern Germany is mostly flat and there's not even close to enough storage capacity (on the order of ~weeks) to make a wind powered grid economically competitive.

2 ay öncediscuss

How many solar panels does the UK produce?

2 ay öncediscuss

> similar as in Sweden

Sweden's electricity is ~40% hydro, ~27% nuclear and ~23% wind. How is this in any way comparable to Northern Germany?

2 ay öncediscuss

Not sure if you're serious, but this was not viable in the 2010s, or even today in Germany at all because of Germany's high latitude: No matter how efficient solar panels become, they will always be more economical to operate closer to the equator. Anyway, the Chinese factories for the most energy intensive parts of solar panel production mostly run on coal power.

2 ay öncediscuss

Solar panel production is extremely energy intensive. Germany has one of the highest energy costs in the world. So there was no way for Germany to maintain a competitive solar panel industry.

3 ay öncediscuss

Relevant prior work: https://github.com/jimblandy/context-switch

3 ay öncediscuss

This is outside of my expertise, but wouldn't multiple threads each submitting a single operation in parallel have the same effect?

3 ay öncediscuss

Right, I think the argument should be that transitioning from a synchronous to asynchronous programming model can improve the performance of a previously CPU/Memory-bound system so that it saturates the IO interface.

3 ay öncediscuss

I read this argument ("async is for I/O-bound applications") often, but it makes no sense to me. If your app is I/O bound, how does reducing the work the (already idling!) CPU has to spend on context switching improve the performance of the system?

3 ay öncediscuss

How many systems are there that can't just spawn a thread for each task they have to work on concurrently? This has to be a system that is A) CPU or memory bound (since async doesn't make disk or network IO faster) and B) must work on ~tens of thousands of tasks concurrently, i.e. can't just queue up tasks and work on only a small number concurrently. The only meaningful example I can come up with are load balancers, embedded software and perhaps something like browsers. But e.g. an application server implementing a REST API that needs to talk to a database anyway to answer each request doesn't really qualify, since the database connection and the work the database itself does are likely much more resource intensive than the overhead of a thread.

3 ay öncediscuss

I believe these ideas are much more mature and better explored for code gen, but similar techniques are useful also in the frontend of compilers, in the type checker. There's a blog post [1] by Niko Matsakis where he writes about adding equalities to Datalog so that Rust's trait solver can be encoded in Datalog. Instead of desugaring equality into a special binary predicate to normal Datalog as Niko suggests, it can be also be implemented by keeping track of equality with union-find and then propagating equality through relations, eliminating now-duplicate rows recursively. The resulting system generalizes both Datalog and e-graphs, since the functionality axiom ("if f(x) = y and f(x) = z, then y = z") is a Datalog rule with equality if you phrase it in terms of the graph of functions.

Systems implementing this are egglog [2] (related to egg mentioned in the article) and (self-plug, I'm the author) eqlog [3]. I've written about implementing Hindley-Milner type systems here: [4]. But I suspect that Datalog-based static analysis tools like CodeQL would also benefit from equalities/e-graphs.

[1] https://smallcultfollowing.com/babysteps/blog/2017/01/26/low...

[2] https://github.com/egraphs-good/egglog

[3] https://github.com/eqlog/eqlog

[4] https://www.mbid.me/posts/type-checking-with-eqlog-polymorph...

2 yıl öncediscuss

If you're interested in the details, you might want to have a look at papers [1] or [2].

You can add existentials in this framework, which basically means that the lifting problems mentioned above don't need to have unique solutions. But as you say, then the "minimal" databases aren't determined uniquely up to isomorphism anymore. So the result of Datalog evaluation now depends on the order in which you apply rules.

If I recall correctly, then [3] discusses a logic corresponding to accessible categories (Datalog + equality corresponds to locally presentable categories) which includes the the theory of fields. The theory of fields involves the negation 0 != 1, so perhaps that might give you a nicer way to incorporate negations without stratification.

[1] https://www.mbid.me/eqlog-semantics/

[2] https://arxiv.org/abs/2205.02425

[3] Locally presentable and accessible categories, https://www.cambridge.org/core/books/locally-presentable-and...

2 yıl öncediscuss

I actually started working on Eqlog because I wanted to use it to implement a type checker. You might want to skim the posts in my series on implementing a Hindley-Milner type system using Eqlog, starting here [1]. The meat is in posts 3 - 5.

The type checker of Eqlog is mostly implement in Eqlog itself [2]. The general idea is that your parser populates a Database with syntax nodes, which are represented as `...Node` types in the Eqlog program at [2], and then you propagate type information with Datalog/Eqlog evaluation. Afterwards, you check whether the Database contains certain patterns that you want to rule out, e.g. a variable that doesn't have a type [3].

There are still some unsolved problems if you're interested in writing the whole type checker in Datalog. For example, variable lookup requires quadratic memory when implemented in Datalog. I mention this and a possible solution at [4]. However, Datalog as is can probably still be useful for some subtasks during type checking. For example, the Rust compiler uses Datalog in some parts of the type checker I believe. Reach out via e.g. github to mbid@ if you'd like to discuss in more detail.

Regarding optimization you probably want to talk with somebody working with egglog, they have a dedicated Zulip [5]. I'd imagine that for prql you want to encode the algebraic rules of pipeline transformations, e.g. associativity of filter over append. Given the query AST, eqlog or egglog would give you all equivalent ways to write the query according to your rules. You'd then select the representation you estimate to be the most performant based on a score you assign to (sub)expression.

[1] https://www.mbid.me/posts/type-checking-with-eqlog-parsing/

[2] https://github.com/eqlog/eqlog/blob/9efb4d3cb3d9b024d681401b...

[3] https://github.com/eqlog/eqlog/blob/9efb4d3cb3d9b024d681401b...

[4] https://www.mbid.me/posts/dependent-types-for-datalog/#morph...

[5] https://egraphs.zulipchat.com

2 yıl öncediscuss

The post mentions the idea that querying a database D can be understood algebraically as enumerating all morphisms Q -> D, where Q is the "classifying" database of the query, i.e. a minimal database instance that admits a single "generic" result of the query. You can use this to give a neat formulation of Datalog evaluation. A Datalog rule then corresponds a morphism P -> H, where P is the classifying database instance of the rule body and H is the classifying database instance for matches of both body and head. For example, for the the transitivity rule

  edge(x, z) :- edge(x, y), edge(y, z).

you'd take for P the database instance containing two rows (a_1, a_2) and (a_2, a_3), and the database instance H contains additionally (a_1, a_3). Now saying that a Database D satisfies this rule means that every morphism P -> D (i.e., every match of the premise of the rule) can be completed to a commuting diagram

  P --> D
  |    ^
  |   /
  ⌄  /
  Q

where the additional map is the arrow Q -> D, which corresponds to a match of both body and head.

This kind of phenomenon is known in category theory as a "lifting property", and there's rich theory around it. For example, you can show in great generality that there's always a "free" way to add data to a database D so that it satisfies the lifting property (the orthogonal reflection construction/the small object argument). Those are the theoretical underpinnings of the Datalog engine I'm sometimes working on [1], and there they allow you to prove that Datalog evaluation is also well-defined if you allow adjoining new elements during evaluation in a controlled way. I believe the author of this post is involved in the egglog project [2], which might have similar features as well.

[1] https://github.com/eqlog/eqlog [2] https://github.com/egraphs-good/egglog

2 yıl öncediscuss

For me, the main problem with most tools that render to HTML was that they don't support all math typesetting libraries that latex supports. I used to work with category theory, where it's common to use the tikz-cd library to typeset commutative diagrams. tikz-cd is based on tikz, which is usually not supported for HTML output.

But apart from math typesetting, my latex documents were usually very simple: They just used sections, paragraphs, some theorem environments and references to those, perhaps similar to what the stack project uses [3]. Simple latex such as this corresponds relatively directly to HTML (except for the math formulas of course). But many latex to html tools try to implement a full tex engine, which I believe means that they lower the high-level constructs to something more low level (or that's at least my understanding). This results in very complicated HTML documents from even simple latex input documents.

So what would've been needed for me was a tool that can (1) render all math that pdflatex can render, but that apart from math only needs to (2) support a very limited set of other latex features. In a hacky way, (1) can be accomplished by simply using pdflatex to render each formula of a latex document in isolation to a separate pdf, then converting this pdf to svg, and then incuding this svg in the output HTML in the appropriate position. And (2) is simply a matter of parsing this limited subset of latex. I've prototyped a tool like that here [1]. An example output can be found here [2].

Of course, SVGs are not exactly great for accessibility. But my understanding is that many blind mathematicians are very good at reading latex source code, so perhaps an SVG with alt text set to the latex source for that image is already pretty good.

[1] https://github.com/mbid/latex-to-html

[2] https://www.mbid.me/lcc-model/

[3] https://stacks.math.columbia.edu/

3 yıl öncediscuss

If you're going to send out math as SVGs anyway, you can also just use your normal latex to PDF renderer (e.g. pdflatex) on each formula, and then convert the output PDFs to SVGs. That way, you get the same output you'd get with latex, and you can also use latex packages that aren't supported by MathJax (e.g. tikz-cd). I've prototyped a latex to html converter [1] based on that approach, but it's probably not ready for serious use. Here's an example: https://www.mbid.me/lcc-model/

[1] https://github.com/mbid/latex-to-html

3 yıl öncediscuss

> using KaTeX [...] switched to server-side rendering with MathJax

I've been meaning to look into KaTex. Could you elaborate on why you switched away from it? KaTeX appears to support server-side rendering already, in the sense that it generates plain HTML.