isalink

Info

isalink is developed for GNU/Linux. Windows and/ or Darwin may also work but are not supported.

isalink is the backbone of our message parsing and encoding. It provides an abstraction over isabelle server messages and client commands. This includes the isalink.IsaClient which wraps most common client commands with convenient methods. isalink.IsaClient is also used as the server connection part of the message passing pair for the gateway.

Code structure

cmd/: CLI tools
- isa-replay/: isa-replay see below
- isa-client/: isa-replay see below
client-commands.go: Abstractions around client commands like start_session
client.go: isalink.IsaClient and related stuff
client-messages.go: Client command parser
client_test.go: Tests for parser and isalink.IsaClient
server-messages.go: Server message parser
server_test.go: Server message parser tests

CLI tools

isalink provides two CLI tools, isa-replay and isa-client.

`isa-client`

A drop-in replacement for isabelle client which supports reading credentials from servers.db. It also importantly supports specifying arbitrary hosts as a CLI flag.

help reference

Usage of isa-client:
  -add_dir_header
    	If true, adds the file directory to the header of the log messages
  -alsologtostderr
    	log to standard error as well as files (no effect when -logtostderr=true)
  -cpuprofile file
    	write cpu profile to file
  -host string
    	explicit server host or (%ISABELLE_SERVER_HOST)
  -log_backtrace_at value
    	when logging hits line file:N, emit a stack trace
  -log_dir string
    	If non-empty, write log files in this directory (no effect when -logtostderr=true)
  -log_file string
    	If non-empty, use this log file (no effect when -logtostderr=true)
  -log_file_max_size uint
    	Defines the maximum size a log file can grow to (no effect when -logtostderr=true). Unit is megabytes. If the value is 0,the maximum file size is unlimited. (default 1800)
  -logtostderr
    	log to standard error instead of files (default true)
  -name string
    	explicit server name
  -one_output
    	If true, only write logs to their native severity level (vs also writing to each lower severity level; no effect when -logtostderr=true)
  -password string
    	explicit server password (default "anything")
  -port uint
    	explicit server port (or $)
  -skip_headers
    	If true, avoid header prefixes in the log messages
  -skip_log_headers
    	If true, avoid headers when opening log files (no effect when -logtostderr=true)
  -stderrthreshold value
    	logs at or above this threshold go to stderr when writing to files and stderr (no effect when -logtostderr=true or -alsologtostderr=true) (default 2)
  -v value
    	number for the log level verbosity
  -vmodule value
    	comma-separated list of pattern=N settings for file-filtered logging

`isa-replay`

Warning

isa-replay is fresh and still undergoing design. The intended use-case is to e2e test ISM.

A small CLI to write unit tests in an easy DSL for testing servers compatible with the isabelle server protocol.

replay file format

Replay files are small scripts that describe a sequential message exchange between a client and server.

They consist of two main units:

instructions: A client message that is being send to the server. An instruction is described as '-> {Message}', where {Message} is client message, like 'help'. These messages are validated by the client parser during startup and invalid messages will be rejected. An instruction may use previously captured content, see below, with string templates to allow for dynamic requests
assertions: A JSON expression describing an expected server behavior, this consists of three steps: waiting for (with optional skipping) a message with a specific state, (optional) matching regexps against the response body or full response and (optional) capturing part of the output for the next instructions

Hint

You can find example replay scripts in isalink repository.

help reference

Usage of isa-replay:
  -add_dir_header
    	If true, adds the file directory to the header of the log messages
  -alsologtostderr
    	log to standard error as well as files (no effect when -logtostderr=true)
  -cpuprofile file
    	write cpu profile to file
  -host string
    	explicit server host or (%ISABELLE_SERVER_HOST)
  -log_backtrace_at value
    	when logging hits line file:N, emit a stack trace
  -log_dir string
    	If non-empty, write log files in this directory (no effect when -logtostderr=true)
  -log_file string
    	If non-empty, use this log file (no effect when -logtostderr=true)
  -log_file_max_size uint
    	Defines the maximum size a log file can grow to (no effect when -logtostderr=true). Unit is megabytes. If the value is 0,the maximum file size is unlimited. (default 1800)
  -logtostderr
    	log to standard error instead of files (default true)
  -one_output
    	If true, only write logs to their native severity level (vs also writing to each lower severity level; no effect when -logtostderr=true)
  -password string
    	explicit server password (default "anything\n")
  -port uint
    	explicit server port (or $)
  -replay string
    	path to replay script
  -skip_headers
    	If true, avoid header prefixes in the log messages
  -skip_log_headers
    	If true, avoid headers when opening log files (no effect when -logtostderr=true)
  -stderrthreshold value
    	logs at or above this threshold go to stderr when writing to files and stderr (no effect when -logtostderr=true or -alsologtostderr=true) (default 2)
  -v value
    	number for the log level verbosity
  -vmodule value
    	comma-separated list of pattern=N settings for file-filtered logging

Documentation

isalink has a well documented source code. Most methods for isalink.IsaClient map directly to their client command equivalents. Please refer to the README of the GitLab repository for more information about current development progress.

ISM Documentation