anoma / vscode-juvix Goto Github PK

On my Mac system, for example, bash is in /bin.

I think it should - it's a run command, not a compile command. Then I'm left with binary files in the source directory which I need to delete manually.

That's a standard shortcut (see how it works in Haskell mode).

Use the subcommand read for each language, respectively.

When I click the "typecheck" button I get:

Invalid argument `/home/heliax/Documents/juvix/examples/milestone/Collatz/Collatz.juvix'

Usage: juvix ((-v|--version) | (-h|--help) | COMPILER_CMD | UTILITY_CMD) 
             [--no-colors] [--show-name-ids] [--internal-build-dir BUILD_DIR] 
             [--no-format] [--stdin] [--only-errors] [--no-termination] 
             [--no-positivity] [--no-stdlib]

  The Juvix compiler.

 *  The terminal process "/usr/bin/bash '-c', 'juvix --internal-build-dir .juvix-build  /home/heliax/Documents/juvix/examples/milestone/Collatz/Collatz.juvix'" failed to launch (exit code: 1). 

For some reason, this extension is creating random .juvix-build folders in the user's system while running. This behaviour is unexpected and can lead to clutter in the user's file system

When you start typing and you haven't yet finished writing correct code, all highlighting disappears, including of the already correct code typed earlier. This is very annoying.

• Add REPL
• Syntax highlighting (probably recommend some lisp extension)

Task provider with the following:

• type check
• compile
• HTML

When I click the "typecheck" button, the result of typechecking isn't displayed on success unless the result window is already open.

Resources:

• https://code.visualstudio.com/api/working-with-extensions/testing-extension
• https://code.visualstudio.com/api/extension-guides/testing
• https://github.com/redhat-developer/vscode-extension-tester/wiki

This happens each time a Juvix file is opened in VSCode. The folders are not deleted. They should be created in the temporary directory.

I constantly get a pop-up window saying "The task 'juvix: typecheck' is already active" and the error messages pop up constantly in the terminal window while typing. Maybe there should be some delay like a few seconds before you type check, or do type checking only after one stops typing, with a delay of a second or so?

Trying to save a *.geb file reverts to the previous content.

More precisely, I have a file with "6" in it on a single line, try to change it to "32", save, and it reverts back to "6".

When editing code, error underlines persist even after the problematic code has been fixed. The error underlines only disappear after the code is typechecked again.

Steps to reproduce:

1. Write code with an error that would cause an underline.
2. Fix the error in the code.
3. Notice that the error underline does not disappear immediately.

Expected behaviour:

After fixing the error, the underline should disappear automatically without needing to trigger a type check manually.

Actual behaviour:

The error underline persists until the code is type-checked again.

Possible solution:

Implement an automatic type check or error check when the code is updated (in the background), so the underline gets removed once the error is fixed.

See the attached image. The first three dashes (-) in the third comment line are black and non-italic.

That's a standard shortcut (see how it works in Haskell mode). Perhaps one needs a language server for this?

It's a no-op. It doesn't launch the REPL, even though there are no conflicting keybindings. I think there is some conflict with Alt+R which launches some VSCode popup about searching for regular expressions.

I propose we try changing this to Shift+Alt+E (for Evaluation).

The result is that if you have both extensions enabled, then Shift+Alt+L is bound either to starting Juvix REPL or a Bookmarks command.

I suggest using Shift+Alt+R instead.

The MBE is the Fibonacci example.

If you type in

module Bug;
end;

save, then change it to

module Bug;

f : Nat -> Nat;
f x := x;

end;

and save, then the module body disappears with no error message and you get

module Bug;
end;

back again.

This is the reason for

• #24.

It also makes errors spanning several lines highlight incorrectly.

Info to display: location of definition (file, line), type, associated judoc comment. This is standard behavior (see the Haskell mode). Perhaps one needs a language server for this, but since we can do jumping to definition, then we should at least be able to display the location of definition?

• For Modules
• For Data type declarations
• For Compile blocks
• For Axioms

Thanks to

• anoma/juvix#1737

one can run now juvix dev scope fileName.juvix --with-comments to get as standard output a nice Juvix program formatted.

Add the option to turn on/off the flag: --only-source for the HTML comand.

(originally by @batconjurer)

Syntax highlighting for partial expressions would be very helpful. Currently, only get it after a line is well formed.

See the following screenshot.

• Install package
• Compile and build a vscode package
• Run some linter.

After clicking run in a Juvix file I get:

The terminal process failed to launch: Starting directory (cwd) "/Users/heliax/Documents/juvix-2/.juvix-build" does not exist.

We want buttons same as we have for Juvix programs, namely:
Buttons for:

• load the REPL,
• compile, and
• run.

There exists a subcommand, juvix dev core read that may be used for formatting the code.

This issue occurs when working in VSCode without any workspace open.

Describe the bug
In the VS code support, ctrl+c does not copy text due to a clash in key bindings. This is very unexpected for users.

Expected behavior
Ctrl+C copies text to clipboard

The JuvixCore pretty printer is not suitable for formatting. For now, the output cannot even be parsed.

For instance, when putting the cursor inside to-str only to or str are highlighted, but not the whole identifier. Or in Stdlib.System.IO only Stdlib, System or IO are highlighted, but not the whole thing.

In general, highlighting always highlights any alphanumeric chunk of text even if it's not an identifier (keywords, text inside string literals). It should highlight only identifiers. See how it works with the Haskell extension.

Atm, we can only open a REPL if the active editor is a Juvix program.

TAB characters are not accepted by the Juvix compiler, so it should insert spaces instead.

The new command was added by:

• anoma/juvix#1886

Currently, instead of heading to the resource file like /some/path/Module.juvix it leads to /some/path/Module.juvix,11,3.
This means that the result of the highlight command is not properly parsed on the extension side.