Skip to content

Running Dev Tools in Dune #10964

@rgrinberg

Description

@rgrinberg

We’ve done good work on the automatic building and installation of dev tools, but I’d like to see a better design for how editor integration is going to look like. The proposed approach of prefixing every dev tool with dune isn’t going to scale at all.

Editors, various scripts, and other dev tools all expect the dev tools to exist in PATH when they’re running. We don’t want to update every single one of them to have a mode when running under dune’s package management.

We should think about how to make it easier for various dev-tools to integrate with each other rather than creating new barriers. Eventually, the end goal should be that someone should be able to create a dev tool and have dune manage it without modifying dune at all. This is the way to go to encourage the creation of better tooling.

If you’re out of ideas on what to do concretely, I suggest you just follow along in esy steps and provide an explicit dev environment that editors are expected to inherit and dev tools need to run in.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions