So you are using VSCode
Go to GitHub Releases, click the latest successful run, scroll down to the bottom of the page, download the "aya-prover-vscode-extension", and unzip it. Then, follow VSCode docs to install the extension.
It remains to configure the Aya language server. There are two ways to use the server. First, open settings, search for "Aya path", you should see a text box. Then, you have a choice:
- Use a jar file. Put your
lsp-fatjar.jarfile path there. Make sure you have a
javaexecutable in the Path (recommended) or in
java.homekey in the settings json.
- Use the jlink version of Aya. Put the
aya-lsp.batif you are on Windows) file path there, which is under the
binfolder of the jlink distribution. In this case, you don't need to have a
javaexecutable in the Path.
Then, open a directory that is an Aya project (see project-tutorial). Open any
.aya file, you should see some basic highlight (keywords, comments, etc.). Wait for VSCode to activate the extension, and hit
Ctrl+L Ctrl+L to load the file. At this point, you should see advanced highlight (type names, constructors, etc.), with clickable definitions.
The rest of the features should be quite discoverable for regular programmers, such as hovering a red or a yellow wavy line to see the error message, etc. Please create issues and discuss ideas on how to improve the error reports.