Skip to content

Commit

Permalink
Merge branch 'main' into gabriela/fix-repl-instance-vars
Browse files Browse the repository at this point in the history
bugarela authored Sep 29, 2023

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
2 parents 661ab63 + 384c28e commit 5c0d034
Showing 10 changed files with 130 additions and 9 deletions.
7 changes: 6 additions & 1 deletion CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -8,12 +8,17 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
## UNRELEASED

### Added

- Added `--random-transitions` flag for `verify`, enabling symbolic simulation
through Apalache (#1188)

### Changed
### Deprecated
### Removed
### Fixed

- Fix a problem where state variables from instances didn't work properly in the REPL (#1190)
- Fixed a problem where state variables from instances didn't work properly in the REPL (#1190)
- Fixed a problem where referencing constants from an instance could cause a crash (#1191)

### Security

15 changes: 10 additions & 5 deletions README.md
Original file line number Diff line number Diff line change
@@ -102,12 +102,17 @@ editor (currently, VSCode, Emacs and Vim are supported).

- [REPL](./tutorials/repl/repl.md)

- VSCode plugin:
- Editor support:

We strongly encourage you to use the VSCode plugin for Quint. It provides
the quickest feedback loop for your specifications, reporting informative
errors as you type. Install the plugin from [Visual Studio Code
Marketplace][].
We strongly encourage you to configure your editor for Quint. Our language
server provides the quickest feedback loop for your specifications, reporting
informative errors as you type. These are instuctions for the currently
supported editors:

- VSCode: Install the plugin from [Visual Studio Code
Marketplace][].
- Emacs: Setup two custom packages from the [emacs folder](./editor-plugins/emacs).
- Vim/Neovim: Follow configuration instructions from the [vim folder](./editor-plugins/vim)

- VSCode plugin for [ITF traces][] by @hvanz:

2 changes: 2 additions & 0 deletions doc/quint.md
Original file line number Diff line number Diff line change
@@ -277,6 +277,8 @@ Options:
--invariant the invariants to check, separated by a comma [string]
--temporal the temporal properties to check, separated by a comma
[string]
--random-transitions choose transitions at random (= use symbolic simulation)
[boolean] [default: false]
--apalache-config Filename of the additional Apalache configuration (in the
HOCON format, a superset of JSON) [string]
--verbosity control how much output is produced (0 to 5)
90 changes: 90 additions & 0 deletions editor-plugins/vim/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,90 @@
# Vim support

This guide will help you set up Vim for Quint, including syntax highlighting and an integrated language server. Follow these easy steps for a smooth configuration.

## Syntax Highlighting

1. If you are using vim, copy the [quint.vim] file to `~/.vim/syntax/`.
1. If you are using neovim, copy the [quint.vim] file to `~/.config/nvim/syntax`.
2. Choose one of the following options to enable syntax highlighting for Quint:

- **Option A (Manual):** Open a Quint file in Vim and manually set the syntax with `:set syntax=quint`.

- **Option B (Automatic):** Add the following line to your `~/.vimrc` file:

```vim
au BufNewFile,BufReadPost *.qnt runtime syntax/quint.vim
```
- **Option C (Modelines):** Make sure you have modelines enabled and add the following line to the end of your Quint file:
```bluespec
// vim: syntax=quint
```
## Language Server
1. Install the [quint-language-server][] globally using npm:
```sh
npm i @informalsystems/quint-language-server -g
```

### Neovim

2. Enable language server integration by adding the following lines to your `~/.config/nvim/init.vim`:

```vim-script
autocmd FileType quint lua vim.lsp.start({name = 'quint', cmd = {'quint-language-server', '--stdio'}, root_dir = vim.fs.dirname()})
au BufRead,BufNewFile *.qnt setfiletype quint
```

### Vim

This requires vim built with Lua support (check with `vim --version`).

2. Install [`prabirshrestha/vim-lsp`](https://github.com/prabirshrestha/vim-lsp) (e.g., via vim-plug):

```vim-script
Plug 'prabirshrestha/vim-lsp'
```

3. Enable LSP for Quint

```vim-script
au BufRead,BufNewFile *.qnt setfiletype quint
if executable('quint-language-server')
au User lsp_setup call lsp#register_server({
\ 'name': 'quint',
\ 'cmd': {server_info->['quint-language-server', '--stdio']},
\ 'allowlist': ['quint'],
\ })
endif
function! s:on_lsp_buffer_enabled() abort
setlocal omnifunc=lsp#complete
setlocal signcolumn=yes
if exists('+tagfunc') | setlocal tagfunc=lsp#tagfunc | endif
nmap <buffer> gd <plug>(lsp-definition)
nmap <buffer> gs <plug>(lsp-document-symbol-search)
nmap <buffer> gS <plug>(lsp-workspace-symbol-search)
nmap <buffer> gr <plug>(lsp-references)
nmap <buffer> gi <plug>(lsp-implementation)
nmap <buffer> gt <plug>(lsp-type-definition)
nmap <buffer> <leader>rn <plug>(lsp-rename)
nmap <buffer> [g <plug>(lsp-previous-diagnostic)
nmap <buffer> ]g <plug>(lsp-next-diagnostic)
nmap <buffer> K <plug>(lsp-hover)
nnoremap <buffer> <expr><c-f> lsp#scroll(+4)
nnoremap <buffer> <expr><c-d> lsp#scroll(-4)
endfunction
augroup lsp_install
au!
autocmd User lsp_buffer_enabled call s:on_lsp_buffer_enabled()
augroup END
```

[quint.vim]: ./quint.vim
[quint-language-server]: https://www.npmjs.com/package/@informalsystems/quint-language-server
2 changes: 1 addition & 1 deletion editor-plugins/vim/quint.vim
Original file line number Diff line number Diff line change
@@ -4,7 +4,7 @@
" Latest Revision: 03 February 2023
"
" How to install:
" 1. Copy this file to ~/.vim/syntax/
" 1. Copy this file to ~/.vim/syntax/ (vim) or to ~/.config/nvim/syntax (neovim).
" 2a. Either manually set syntax with :set syntax=quint
" 2b. Or add the following in your ~/.vimrc
" au BufNewFile,BufReadPost *.qnt runtime syntax/quint.vim
5 changes: 5 additions & 0 deletions quint/src/cli.ts
Original file line number Diff line number Diff line change
@@ -240,6 +240,11 @@ const verifyCmd = {
type: 'string',
coerce: (s: string) => s.split(','),
})
.option('random-transitions', {
desc: 'choose transitions at random (= use symbolic simulation)',
type: 'boolean',
default: false,
})
.option('apalache-config', {
desc: 'Filename of the additional Apalache configuration (in the HOCON format, a superset of JSON)',
type: 'string',
3 changes: 3 additions & 0 deletions quint/src/cliCommands.ts
Original file line number Diff line number Diff line change
@@ -644,6 +644,9 @@ export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<V
next: 'q::step',
inv: args.invariant ? ['q::inv'] : undefined,
'temporal-props': args.temporal ? ['q::temporalProps'] : undefined,
tuning: {
'search.simulation': args.randomTransitions ? 'true' : 'false',
},
},
}

3 changes: 3 additions & 0 deletions quint/src/static/callgraph.ts
Original file line number Diff line number Diff line change
@@ -190,6 +190,9 @@ export class CallGraphVisitor implements IRVisitor {
const importedModule = this.context.modulesByName.get(decl.protoName)
if (importedModule) {
this.graphAddAll(decl.id, Set([importedModule.id]))
decl.overrides.forEach(([_param, expr]) => {
this.graphAddAll(expr.id, Set([decl.id]))
})
}
}

7 changes: 7 additions & 0 deletions quint/test/static/callgraph.test.ts
Original file line number Diff line number Diff line change
@@ -129,6 +129,7 @@ describe('compute call graph', () => {
| pure val myM = sqr(3)
| import B(M = myM) as B1
| pure val quadM = 2 * B1::doubleM
| pure val constRef = B1::M
| export B1.*
|}`
)
@@ -148,12 +149,18 @@ describe('compute call graph', () => {
const importB = findInstance(main, imp => imp.protoName === 'B')
const quadM = findDef(main, 'quadM')
const doubleM = findDef(B, 'doubleM')
const constRef = findDef(main, 'constRef')
const exportB1 = findExport(main, exp => exp.protoName === 'B1')

expect(graph.get(importA.id)?.toArray()).eql([A.id])
expect(graph.get(myM.id)?.toArray()).to.eql([sqr.id, importA.id])
expect(graph.get(importB.id)?.toArray()).to.eql([B.id, myM.id])
expect(graph.get(quadM.id)?.toArray()).to.eql([doubleM.id, importB.id])
expect(graph.get(exportB1.id)?.toArray()).to.eql([importB.id])

// Find the id for B1::M by checking the dependencies of constRef
// A regression for #1183, ensuring constants like B1::M depend on the instance statements
const B1Mid = graph.get(constRef.id)?.toArray()[0]!
expect(graph.get(B1Mid)?.toArray()).to.eql([importB.id])
})
})
5 changes: 3 additions & 2 deletions vscode/quint-vscode/server/README.md
Original file line number Diff line number Diff line change
@@ -14,9 +14,10 @@ npm i @informalsystems/quint-language-server -g

## Usage

There are currently two clients for this server:
There are currently three clients for this server:

1. The Quint [VSCode extension](https://marketplace.visualstudio.com/items?itemName=informal.quint-vscode)
2. The [Quint LSP client](https://github.com/informalsystems/quint/blob/main/editor-plugins/emacs/README.md) for Emacs
3. A [Neovim LSP client]((https://github.com/informalsystems/quint/blob/main/editor-plugins/vim/README.md)

They are capable of downloading and installing this server for you.
(1) and (2) are capable of downloading and installing this server for you. (3) requires manual installation (for now).

0 comments on commit 5c0d034

Please sign in to comment.