Juvix Plugin for VSCode
This VS Code extension provides support for Juvix Lang.
Find "Juvix" in the VSCode marketplace and install it. Otherwise, launch VS Code
Quick Open (CtrlP), and paste the following command
followed by pressing enter.
ext install heliax.juvix-mode
If you, for some reason, want to install the extension manually,
you can do it by running the following commands.
git clone https://github.com/anoma/vscode-juvix
npx vsce package
code --install-extension juvix-X.X.X.vsix
If you don't have
npx installed, you can install it by running the following:
npm install -g vsce
npm install -g npx
To be able to use the extension, you need to have the latest binary of Juvix
installed. You can find detailed installation instructions
here. If you are using MacOS, you can
install Juvix using Homebrew.
brew tap anoma/juvix
brew install juvix
Once you have Juvix installed, you can check the version by running the
The extension provides semantic syntax highlighting for Juvix files. It also
provides a command palette with the following commands. You must edit Juvix
files within a workspace folder. Otherwise, the extension will not work
However, we recommend using the Command Palette (CtrlP) to
see which other commands are available by typing
Juvix and selecting the command you want to run.
This extension provides configurations using the VSCode's configuration UI
If you are debugging Juvix programs, you might want to use the extension in
development mode. To do so, enable in your configuration the
juvix-mode.enableDevTasks option. This will enable the extension to open a
panel and run the tasks specified in the active file. However, you can use
this feature even if it's not a Juvix file.
The extension will look for lines in the active file that contain the pattern
DEBUG: nameTASK where
nameTask is an entry in the
configuration option. Check the extension configuration to see some examples you
can use or add to your setup. Some strings are expanded in runtime. For
$filename will be replaced by the name of the active file. The
extension provides auto-completion for the default tasks. To trigger this feature,
debug somewhere in the file.
For example, if you have the following line in your configuration file:
"juvix-mode.enableDevTasks" : true,
"CatFile": "cat $filename"
Then, you can use the task
Parsed in your file by adding the following line:
-- DEBUG: Parsed
axiom A : Type;
The extension will run the command for the
Parsed task in a new tab and update
that view when the file changes. If the active file contains multiple
annotations, the extension will run all the commands in separate tabs. For
example, if you have the following lines in your file, the extension will open
two tabs, one for the
InternalArity task and another for the
open import B;
axiom a : A;
axiom b : A;
-- DEBUG: InternalArity
-- DEBUG: CoreLifting
To keep your debug annotations but not run the tasks on save, you can add the
NO-DEBUG! annotation, somewhere in the file. To run all the available tasks,
-- DEBUG: All
axiom A : Type;
The aforementioned features are experimental and might change in the future.
- Command palette with type checking, compilation, and running Juvix files.
- Semantic syntax highlighting.
- Support for light and dark themes.
- Support for Unicode input (e.g. λ, Π, Σ, etc.) pressing e.g.
\ + "alpha" +
- Support for user configuration options.
- Support for Juvix's REPL.
- Support for Juvix's debugging.