isalink

package module
v0.0.0-...-f98532e Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Jun 19, 2026 License: AGPL-3.0 Imports: 19 Imported by: 7

README

Gitlab Code Coverage Gitlab Pipeline Status GitLab License Golang Version

A Golang library for an isabelle client and message parser (client & server).

Mainly intended for ism. The Golang interfaces are intended for internal use only, no stable API is guaranteed.

Bugs & Issues

Platform support

IsaLink only actively supports Linux (x86_64) and testing is done on a NixOS stable (x86_64) runner. We should also support other systems, like aarch64 hosts, but they are not actively tested or validated.

BSDs and other Linux distributions may also work and patches for them will be accepted. Windows and other propietary systems are not tested and won't be actively supported.

Issues

All bug reports and feature requests go to the ISM issue tracker. Please prefix the issue title with isalink: <title> and add the isalink tag.

Building and Testing

The only supported way to build, develop and test isalink is with nix.

If you don't have nix installed, the recommend installer is The Determinate Nix Installer for darwin and GNU/Linux. You must have support for flakes and unified CLI enabled or make all nix calls with nix --experimental-features "flakes nix-command".

For stable CLIs
  • isa-client: A minimal reimplementation of the Isabelle server client. Intended for scenarios where startup time and memory usage are important.
    • nix build .#isalink-client
  • isabelle-client-shim: A small script that provides a shim over isabelle to use isa-client when requesting isabelle client.
    • nix build .#isabelle-client-shim

[^1]: A DSL to send client message and apply assertions against server responses.

Unstable CLIs

These CLIs are used in this repository for CI and packaging. We don't provide stability promises because we don't fully control the upstream repositories.

For development
  • Get a copy of the source code:
    • HTTPS: git clone https://git.tu-berlin.de/proveit/isalink
    • SSH: git clone git@git.tu-berlin.de:proveit/isalink.git
  • And you're ready to go:
    • Build the client binary: nix develop -c make build
    • Run tests: nix develop -c make test
    • Format code: nix fmt
      • Check formatting: nix fmt -- --check

Attributions

This software was created as part of the ProveIt project at TU Berlin by Joshua Kobschätzki j.k@cobalt.rocks. The copyright lies with the Project/ TU Berlin.

All source code, if not otherwise indicated, is licensed under the AGPL 3.0 license. Distributed binaries may follow the same license however no distribution of binaries is planned at the time of writing.

The GitLab repository icon is from the Carbon Icon Set by IBM under the Apache 2.0 license.

Documentation

Index

Constants

This section is empty.

Variables

View Source 
var (
	ErrConnectionNotReady = errors.New("connection is not ready for request")
	ErrUnexpectedState    = errors.New("received a non-ok message")
	ErrSessionCreation    = errors.New("failed to create new session")
	ErrUseTheories        = errors.New("failed to call use_theories")
	ErrSessionStop        = errors.New("failed to stop session")
	ErrPurgeTheories      = errors.New("failed to purge theories")
	ErrListSessions       = errors.New("failed to list sessions")
)

helper data for IsaClient

View Source 
var (
	ErrPasswordHandshake = errors.New("password handshake failed")
	ErrDeadlinePassed    = errors.New("deadline has passed before write")
)
View Source 
var (
	ErrTaskFailed      = errors.New("async task resulted in an Error")
	ErrTaskFailedInner = errors.New("async task finished with a non-ok FINISHED")
)
View Source 
var DefaultSessionOptions = []string{
	"headless_consolidate_delay=0.5",
	"headless_prune_delay=5",
	"show_states",
}
View Source 
var ErrBufferExhausted = errors.New("fixed size internal buffer exhausted")
View Source 
var ErrCorruptState = errors.New("can't close an unopened or corrupt connection")
View Source 
var ErrInvalidAddr = errors.New("can't connect to invalid Addr")
View Source 
var ErrListSessionsUnsupported = errors.New("server appears to not support the list_sessions command")

error for ListSessions call when list_sessions command is not supported

View Source 
var ErrMessageFormat = errors.New("message format was invalid")

helper values for parseMessage

View Source 
var ErrPasswordUnterminated = errors.New("password was not \\n terminated, this is required for direct writing")

Functions

func IsAsync 

func IsAsync(state ClientMessageType) bool

is a client message async? refer to the system documentation for more information

Types

type ClientContent 

type ClientContent = map[string]any

alias for the content of a ClientMessage

type ClientMessage 

type ClientMessage struct {
	State   ClientMessageType // type of message, i.e., used command
	Content ClientContent
}

a decoded Isabelle client message (JSON format only)

func MustParseClientMessage 

func MustParseClientMessage(message []byte) *ClientMessage

parse a message from a string, panic on failure, only use on known-good messages NOTE: intended as a helper for unit tests and similar applications

func NewEchoMessage 

func NewEchoMessage(content string) *ClientMessage

create new message for ECHO commands

func NewMessage 

func NewMessage(state ClientMessageType, content map[string]any) *ClientMessage

create new empty message, mostly used for testing

func ParseClientMessage 

func ParseClientMessage(message []byte, msg *ClientMessage) (*ClientMessage, error)

parse a message from a string

func (*ClientMessage) Encode 

func (msg *ClientMessage) Encode() ([]byte, error)

encode a message TODO: optimize this to reduce allocs

func (*ClientMessage) Get 

func (msg *ClientMessage) Get(key string) (string, error)

gracefully try to extract a string value from content

func (*ClientMessage) IsAsync 

func (msg *ClientMessage) IsAsync() bool

is a client message async? refer to the system documentation for more information

func (*ClientMessage) String 

func (msg *ClientMessage) String() string

type ClientMessageType 

type ClientMessageType byte

state of an isabelle server message 

const (
	// zero value = invalid command
	ClientUnknown ClientMessageType = iota
	// echo
	ClientEcho
	// commands that don't have arguments
	ClientHelp
	ClientListSessions
	ClientShutdown
	// commands that require JSON arguments
	ClientPurgeTheories
	ClientSessionBuild
	ClientSessionStart
	ClientSessionStop
	ClientUseTheories
	ClientCancel
)

func (ClientMessageType) Bytes 

func (cmt ClientMessageType) Bytes() []byte

stringify to bytes

func (ClientMessageType) String 

func (cmt ClientMessageType) String() string

stringify ClientMessageState for debugging

type IsaClient 

type IsaClient struct {
	State IsaClientState // current client state, state machine for connection
	// contains filtered or unexported fields
}

Client for interacting with an Isabelle Server (not safe for concurrent use) Based on net.Conn with an internal buffer

Includes low level abstractions for reading individual lines and messages as well as direct wrappers for the client commands.

func ConnectClient 

func ConnectClient(
	ctx context.Context,
	logger log.Logger,
	server netip.AddrPort,
) (*IsaClient, error)

connect a new client to a server instance, NOTE: doesn't perform handshake

func (*IsaClient) Cleanup 

func (c *IsaClient) Cleanup(ctx context.Context, logger log.Logger, session uuid.UUID) error

purge theories and close session, basically just c.PurgeTheories + c.StopSession

func (*IsaClient) Close 

func (c *IsaClient) Close() error

Close underlying TCP connection

func (*IsaClient) ConnectPooledClient 

func (c *IsaClient) ConnectPooledClient(
	ctx context.Context,
	logger log.Logger,
	server netip.AddrPort,
) (*IsaClient, error)

connect a client to a server instance, may work on nil NOTE: doesn't perform handshake

func (*IsaClient) CreateSession 

func (c *IsaClient) CreateSession(
	ctx context.Context,
	logger log.Logger,
	args *SessionStartArgs,
) (uuid.UUID, error)

create a new session, returns the used ID

func (*IsaClient) Echo 

func (c *IsaClient) Echo(
	ctx context.Context,
	logger log.Logger,
	content string,
) (*ServerMessage, error)

echo command, NOTE: this doesn't require JSON contents for the request/ response. NOTE: requires '"' characters to escaped already with '\"', otherwise the server will reject the echo message

func (*IsaClient) Handshake 

func (c *IsaClient) Handshake(
	ctx context.Context,
	logger log.Logger,
	password []byte,
	validateResponse bool,
) (*ServerMessage, error)

attempt handshake with server, can optionally check if server responded with OK NOTE: the server will normally close the conn, if the password is invalid, so manual checking of the response is not really necessary NOTE: may return the handshake OK, if err == nil, this can be used to simulate the real client

func (*IsaClient) HasLS 

func (c *IsaClient) HasLS(ctx context.Context, logger log.Logger) (bool, error)

check if list_sessions extensions is supported

func (*IsaClient) ListSessions 

func (c *IsaClient) ListSessions(
	ctx context.Context,
	logger log.Logger,
) ([]uuid.UUID, error)

list sessions on Isabelle server (done via custom extensions, not always available)

func (*IsaClient) PurgeTheories 

func (c *IsaClient) PurgeTheories(
	ctx context.Context,
	logger log.Logger,
	args *PurgeTheoriesArgs,
) ([]string, error)

issue purge theories command

func (*IsaClient) ReadLine 

func (c *IsaClient) ReadLine(ctx context.Context, logger log.Logger) ([]byte, error)

read a line from the conn buffer and/or the conn NOTE: the output is only valid until the next call to ReadLine or another method that writes/ reads returns: (line, error)

func (*IsaClient) ReadMessage 

func (c *IsaClient) ReadMessage(ctx context.Context, logger log.Logger) (*ServerMessage, error)

func (*IsaClient) Reconnect 

func (c *IsaClient) Reconnect(
	ctx context.Context,
	logger log.Logger,
	password []byte,
	validateResponse bool,
) error

reconnect underlying client

func (*IsaClient) SetDeadline 

func (c *IsaClient) SetDeadline(t time.Time) error

SetDeadline for the underlying TCP connection

func (*IsaClient) SetReadDeadline 

func (c *IsaClient) SetReadDeadline(t time.Time) error

SetReadDeadline for the underlying TCP connection NOTE: assumes client != nil && client.conn != nil

func (*IsaClient) StopSession 

func (c *IsaClient) StopSession(
	ctx context.Context,
	logger log.Logger,
	session uuid.UUID,
) error

issue stop_session command

func (*IsaClient) TestMode 

func (c *IsaClient) TestMode()

dedicated function to enable logging for testing

func (*IsaClient) WaitState 

func (c *IsaClient) WaitState(
	ctx context.Context,
	logger log.Logger,
	skip []ServerMessageState,
	target ServerMessageState,
) (*ServerMessage, error)

await server messages while skipping all messages with state \in skip

func (*IsaClient) WaitTask 

func (c *IsaClient) WaitTask(
	ctx context.Context,
	logger log.Logger,
	taskID string,
	unrelatedMsgChan chan<- *ServerMessage,
) (*ServerMessage, error)

await an async task. This function will redirect all other messages to unrelatedMsgChan if defined

func (*IsaClient) Write 

func (c *IsaClient) Write(
	ctx context.Context,
	logger log.Logger,
	msg []byte,
) (int, error)

raw write to underlying connection

func (*IsaClient) WriteMessage 

func (c *IsaClient) WriteMessage(
	ctx context.Context,
	logger log.Logger,
	msg *ClientMessage,
) (int, error)

Write a client message directly

type IsaClientState 

type IsaClientState byte

state of an IsaClient, starts with disconnected 

const (
	// client is disconnected -> unusable with no attached TCP connection
	IcsDisconnected IsaClientState = iota
	// client is connected and usable for r/w
	IcsIdle
	// client is in unknown and unrecoverable state
	IcsCorrupt
	// client is performing handshake and not yet ready for use
	IcsConnecting
)

func (IsaClientState) String 

func (state IsaClientState) String() string

type PurgeTheoriesArgs 

type PurgeTheoriesArgs struct {
	SessionID uuid.UUID // session to purge theories in
	Theories  []string  // theories to purge explicitly
	MasterDir string    // master_dir, as in use_theories, for relative theory names
	All       bool      // purge all theories
}

func (*PurgeTheoriesArgs) Map 

func (args *PurgeTheoriesArgs) Map() map[string]any

convert to generic map

type ServerMessage 

type ServerMessage struct {
	State   ServerMessageState // message type
	Content any                // content of message as parsed JSON
}

a decoded isabelle server message (JSON format only, except when State = Echo)

func MustParseServerMessage 

func MustParseServerMessage(message []byte) *ServerMessage

parse a message from a string, panic on failure, only use on known-good messages NOTE: intended as a helper for unit tests and similar applications

func ParseServerMessage 

func ParseServerMessage(message []byte) (*ServerMessage, error)

parse a message from a string

func (*ServerMessage) Get 

func (msg *ServerMessage) Get(key string) (string, error)

gracefully try to extract a string value from content

func (*ServerMessage) Json 

func (msg *ServerMessage) Json() ([]byte, error)

encode a message into JSON

func (*ServerMessage) Keys 

func (msg *ServerMessage) Keys() []string

returns keys of content, if content ~ map[string]any, otherwise empty array intended for debugging

func (*ServerMessage) Ok 

func (msg *ServerMessage) Ok() (bool, error)

try to extract ok field from content

func (*ServerMessage) String 

func (msg *ServerMessage) String() string

func (*ServerMessage) TaskID 

func (msg *ServerMessage) TaskID() (string, error)

try to extract task id from content

type ServerMessageState 

type ServerMessageState byte

state of an isabelle server message 

const (
	ServerUnknown ServerMessageState = iota
	ServerFinished
	ServerError
	ServerPreconditionError // server error for out of spec messages
	ServerFailed
	ServerInfo
	ServerNote
	ServerOk
	ServerEcho
)

func ParseServerState 

func ParseServerState(state []byte) ServerMessageState

parse a stringified state as server message state

func (ServerMessageState) Bytes 

func (sms ServerMessageState) Bytes() []byte

stringify to bytes

func (ServerMessageState) String 

func (sms ServerMessageState) String() string

stringify MessageState for debugging

type SessionStartArgs 

type SessionStartArgs struct {
	Session        string   `json:"session,omitempty"`          // target session name
	Preferences    string   `json:"preferences,omitempty"`      // env of isabelle systems
	Options        []string `json:"options"`                    // options, like -o for isabelle build, as `key=value` strings, if nil, then DefaultSessionOptions will be used instead
	Directories    []string `json:"dirs,omitempty"`             // additional dirs for ROOT and ROOTS
	IncludeSession []string `json:"include_sessions,omitempty"` // sessions to include in ns for session-qualified theory names
	Verbose        bool     `json:"verbose,omitempty"`          // whether to give more NOTEs
	PrintMode      string   `json:"print_mode,omitempty"`       // whether to print more debug information
	MasterDir      string   `json:"master_dir,omitempty"`       // set master_dir
}

Arguments for building a new isabelle session, as defined in the isabelle system documentation Equivalent to the `session_build_args` type.

func (*SessionStartArgs) Map 

func (args *SessionStartArgs) Map() map[string]any

type UseTheoriesArguments 

type UseTheoriesArguments struct {
	SessionID        uuid.UUID // session_id, required
	Theories         []string  // theories, required
	MasterDir        string    // master_dir, optional, default session tmp_dir
	PrettyMargin     float64   // pretty_margin, optional, default 76
	UnicodeSymbols   bool      // unicode_symbols, optional
	ExportPattern    string    // export_pattern, optional
	CheckDelay       float64   // check_delay, optional, default: 0.5
	CheckLimit       int       // check_limit, optional
	WatchdogTimeout  float64   // watchdog_timeout, default: 600
	NodesStatusDelay float64   // nodes_status_delay, default: -1
}

translation of use_theories_arguments

func (*UseTheoriesArguments) Map 

func (args *UseTheoriesArguments) Map() map[string]any

Source Files

  • args.go
  • client-commands.go
  • client-messages.go
  • client.go
  • server-messages.go

Directories

Path Synopsis
cmd
isa-client command
Test utils for isalink, intended for internal use, no stable API guarantees This was extracted from the main isalink tests ot use in `sync`.
 Test utils for isalink, intended for internal use, no stable API guarantees This was extracted from the main isalink tests ot use in `sync`.
sync package implements an abstraction over `isalink.IsaClient` that is safe for concurrent use it is intended for use with multiple readers that await asynchronous commands
 sync package implements an abstraction over `isalink.IsaClient` that is safe for concurrent use it is intended for use with multiple readers that await asynchronous commands

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.