This project introduces lsp-eiffel, a server-side implementation of the language server protocol.

Configure your favorite editor with LSP support to use the language server. (Make a pull request with the specific instruction for your code editor e.g. IntelliJ, VSCode, Emacs, Neovim, Zed)

The configuration for helix has been merged upstream. Just install the language server and make sure it is visible in your $PATH.

The commands llm-correct-classes and llm-correct-features require specific inputs. First, you need to provide the path to the Eiffel project configuration file (ecf) after the --config option. Additionally, after the --classes option, you must specify the path to a file that contains a list of class names, with one name per line, that you wish to correct.

You need a Constructor tech API token to use the LLMs. You need access to AutoProof binaries to use the verifier.

This project needs the following environmental variables correctly set. The variable CONSTRUCTOR_APP_API_TOKEN must point to a constructor knowledge access token. The variable AP_COMMAND must point to the AutoProof executable.

This project is built using cargo. If you are new to cargo and rust, start from the official guide.

The command cargo test tests the current crate. The command cargo test --workspace runs all the tests in the workspace.

The command cargo build --release --workspace builds the language server and the standalone commands. The command cargo build --release -p eiffel-tools builds only the language server. The command cargo build --workspace builds the language server and the standalone commands in the workspace with debugging information e.g. bounds checks.

This project was born as a research project, most of the functionalities that make a language server truly useful (i.e. advanced code navigation, obvious code completion and in-place documentation) have not been built because there was no incentive in doing so. However, the infrastructure allows all these functionalities to be added easily. Feel free to write a PR, fork the project or get in touch for continuing this work.

Do you want to help the visibility of the project? You might want to read the draft of the scientific paper describing this tool (in the ./draft-paper folder) and getting in touch to cooperate on its conclusion.