A few issues from a newbie

[zmitchell]

These are just a few issues I've run into while getting started.

Type aliases

When you define a type alias, it's not clear from the docs whether literals need to be wrapped in the alias or not. For instance:

type Path = str

# This?
pure val home: Path = "/home/zmitchell"
# or this?
pure val home: Path = Path("/home/zmitchell")

(I've gathered that it's the former, e.g. the bare literal, but that's not spelled out in the docs as far as I can tell).

Imports

For some reason, my import doesn't work at all. I have the following two files in the same directory:

dir/
    resolver.qnt
    basicSpells.qnt

and my resolver.qnt file looks like this:

module resolver {
    import basicSpells.* from "./basicSpells.qnt"

    type Foo = {
        bar: Option[int]
    }
}

(where basicSpells.qnt is copied from main),
but when I run quint typecheck resolver.qnt from inside dir I get

/home/zmitchell/src/quint-models/package-resolution/resolver.qnt:3:3 - error: [QNT013] import ... from './basicSpells.qnt': could not load
3:   import basicSpells.* from "./basicSpells.qnt"

I've checked that the file permissions are as they should be (i.e. the same as resolver.qnt).

Program name in help

The program name is reported as cli.js instead of quint.

❯ quint --help
cli.js

run an interactive Read-Evaluate-Print-Loop

Commands:
  cli.js parse <input>      parse a Quint specification
  cli.js typecheck <input>  check types and effects of a Quint specification
  cli.js compile <input>    compile a Quint specification into the target, the
                            output is written to stdout
  cli.js repl               run an interactive Read-Evaluate-Print-Loop[default]
  cli.js run <input>        Simulate a Quint specification and (optionally)
                            check invariants
  cli.js test <input>       Run tests against a Quint specification
  cli.js verify <input>     Verify a Quint specification via Apalache
  cli.js docs <input>       produces documentation from docstrings in a Quint
                            specification

Options:
      --help       Show help                                           [boolean]
      --version    Show version number                                 [boolean]
  -r, --require    filename[::module]. Preload the file and, optionally, import
                   the module                                           [string]
  -q, --quiet      Disable banners and prompts, to simplify scripting (alias for
                   --verbosity=0)                     [boolean] [default: false]
      --verbosity  control how much output is produced (0 to 5)
                                                           [number] [default: 2]

This is 0.25.1 installed via Flox (which draws from nixpkgs).

Documentation gaps

I suspect for many people Quint is their first formal specification language, and therefore don't have much experience writing specifications. I also suspect most people don't have much experience developing distributed protocols, which makes the existing examples kind of hard to understand as a new user.

For instance, as a learning exercise I'm trying to write out the package resolution algorithm used by Flox to determine which packages to install for a user based on the requirements/constraints in their "environment"'s config file. I've pieced together some ideas for how to do that based on the lessons and the Secret Santa example, but having more "general purpose" examples to draw inspiration from would be helpful. Essentially I'm looking for "you understand the language and how to write 'hello world', now let's do something between 'hello world' and a blockchain protocol."

[bugarela]

Hi! Thank you for the feedback, specially on the docs!

For "Type aliases", good point, we should document that better.
For "Imports", you want to remove the .qnt from the file. The correct import is import basicSpells.* from "./basicSpells". I can see how that is confusing, we should probably just support both (as JS does iirc).
For "Program name in help", I see the same issue with nix-shell -p quint --run "quint --help". I was unaware of this, thanks for reporting.

As for more intermediate level examples, I'd look into Tic-Tac-Toe (it's not as simple as it may appear) and this Bank example which helps you find a vulnerability in the code with MBT. More on the distributed systems side, there's Two-Phase Commit. Unfortunately, we don't have blogposts/tutorials around these examples, so I see your point about we lacking intermediate-level material that it's not assuming you already now basics of distributed systems as well.

[zmitchell]

Thanks for the response and the additional examples. Another question I have is how to model certain data structures. Say I want to model something like a tagged-union (what Rust's enums are e.g. you have a finite set of options where each one can carry variant-specific data).

Say I want to model a collection of events, where each event kind can carry different data. I can think of a few different ways to model this, but I'm not sure which is idiomatic. These examples are for process lifecycle events because I'm working on a profiler that records these events and want to model the algorithm for ingesting, buffering, and post-processing the events.

This way I call the "generic event" approach. The downside is that you have to guard against the EventKind and extra being mismatched e.g. kind = Fork and extra = Some[ExecMeta].

type EventKind =
  Fork
  | Exec
  | Exit

type EventMeta = { ts: Int, pid: Int }

type ForkMeta = { childPid: Int }
type ExecMeta = { filename: str }
# No extra metadata for Exit

# `a` would be one of ForkMeta or ExecMeta
type Event[a] = { kind: EventKind, meta: EventMeta, extra: Option[a] }

The next approach is what I would typically reach for (because it looks like Rust), but I'm not sure if it's even possible in Quint:

type EventKind =
  Fork { meta: EventMeta, childPid: Int }
  | Exec { meta: EventMeta, filename: str }
  | Exit { meta: EventMeta }

In general I think you could do with a "records" tutorial so it's clear when and where you can use the record syntax.