Skip to content

[ ide-mode ] return formatted version string for :interpret ":version" command#3768

Open
keram wants to merge 1 commit intoidris-lang:mainfrom
keram:ide-mode-interpret-version
Open

[ ide-mode ] return formatted version string for :interpret ":version" command#3768
keram wants to merge 1 commit intoidris-lang:mainfrom
keram:ide-mode-interpret-version

Conversation

@keram
Copy link
Copy Markdown
Contributor

@keram keram commented Apr 23, 2026

Note:
I acknowledge the AI contributing policy and made the changes primarily on own but I did consulted AI and been guided by it to make this change correctly.


Previously, the IDE command :version (via interpret) reused ShowVersion and returned a structured S-expression containing semantic version components and commit hash.

As idris-mode expects for output of :interpret command to be always a string. This leads to bad user experience on commands that return S-expression. See: idris-hackers/idris-mode#661 and idris-hackers/idris-mode#662

This introduces a dedicated VersionSExp constructor in IDEResult and updates process Version to return the raw version value directly.
The IDE mode now distinguishes between:

  • REPL (VersionIs x) -> structured AVersion (unchanged)
  • VersionSExp x -> formatted string via showVersion

As a result, :version in IDE interpret mode now produces a human-readable string (e.g. "0.8.0-") instead of a structured tuple.

Before:

idris2 --ide-mode
000018(:protocol-version 2 1)
(:version 1)
00002a(:return (:ok ((0 8 0) ("19a3f4ec0"))) 1)
((:interpret ":version") 2)
00002a(:return (:ok ((0 8 0) ("19a3f4ec0"))) 2)

After:

$ idris2 --ide-mode
000018(:protocol-version 2 1)
(:version 1)
00002a(:return (:ok ((0 8 0) ("ed55358b6"))) 1)
((:interpret ":version") 2)
000024(:return (:ok "0.8.0-ed55358b6") 2)

Next steps:

Update :opts command in similar way.

((:interpret ":opts") 3)
00009b(:return (:ok ((:show-implicits :False) ...)) 3) ;; should be string
((:get-options) 3)
00009b(:return (:ok ((:show-implicits :False) .. (:editor "vim"))) 3) ;; stay same

Description

Self-check

  • This is my first time contributing, I've carefully read CONTRIBUTING.md
    and I've updated CONTRIBUTORS with my name.
  • If this is a fix, user-facing change, a compiler change, or a new paper
    implementation, I have updated CHANGELOG_NEXT.md
  • I confirm that this contribution did not involve GenerativeAI nor Large Language Models.

… command

Previously, the IDE command `:version` (via `interpret`) reused
`ShowVersion` and returned a structured S-expression containing
semantic version components and commit hash.

As `idris-mode` expects for output of `:interpret` command to be always a string.
This leads to bad user experience on commands that return S-expression.
See: idris-hackers/idris-mode#661
and idris-hackers/idris-mode#662

This introduces a dedicated `VersionSExp` constructor in
`IDEResult` and updates `process Version` to return the raw `version`
value directly.
The IDE mode now distinguishes between:

 - `REPL (VersionIs x)` -> structured `AVersion` (unchanged)
 - `VersionSExp x`      -> formatted string via `showVersion`

As a result, `:version` in IDE interpret mode now produces
a human-readable string (e.g. "0.8.0-<hash>") instead of a structured tuple.

 Before:

```
idris2 --ide-mode
000018(:protocol-version 2 1)
(:version 1)
00002a(:return (:ok ((0 8 0) ("19a3f4ec0"))) 1)
((:interpret ":version") 2)
00002a(:return (:ok ((0 8 0) ("19a3f4ec0"))) 2)
```

 After:

```
$ idris2 --ide-mode
000018(:protocol-version 2 1)
(:version 1)
00002a(:return (:ok ((0 8 0) ("ed55358b6"))) 1)
((:interpret ":version") 2)
000024(:return (:ok "0.8.0-ed55358b6") 2)
```

 Next steps:

Update `:opts` command in similar way.
```
((:interpret ":opts") 3)
00009b(:return (:ok ((:show-implicits :False) ...)) 3) ;; should be string
((:get-options) 3)
00009b(:return (:ok ((:show-implicits :False) .. (:editor "vim"))) 3) ;; stay same
```
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant