isalink

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

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

 Go to latest Published: Oct 23, 2024 License: AGPL-3.0 Imports: 20 Imported by: 0

README

Gitlab Code Coverage Gitlab Pipeline Status GitLab License Golang Version

A golang library for an isabelle client and message parser (client & server). Built for GNU/Linux.

Mainly intended for ism and isa-bench, pre-alpha and breaking interface changes are expected.

TODO

  • Create conn and handshake
  • Create isabelle client replacement
  • wrappers for actions (help, create_session, ...)
  • Lifecycle management (open, close)
  • Vendor as part of prooveit.nix
  • Message parsing
  • Message parsing
  • Nix tests for e2e with proveit.nix
    • base is done
    • basic client tests (for some commands already there)
    • isa-replay for ISM testing

Bugs & Issues

Platform support

IsaLink only actively supports GNU/Linux (x86_64) and testing is done on a NixOS stable (x86_64) runner.

BSDs and darwin may also work and patches for them will be accepted. However, darwin is not actively tested due to a lack of darwin CI runners.

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.

This is an internal library and any support is provided on a best effort basis.

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".

With nix installed you can continue:

  • 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

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 (
	DefaultSessionOptions = []string{"headless_consolidate_delay=0.5", "headless_prune_delay=5", "show_states"}
	ConnectionNotReady    = errors.New("Connection is not ready for request")
	UnexpectedStateErr    = errors.New("Recived a non-ok message")
	SessionCreationFailed = errors.New("Failed to create new session")
)

helper data for IsaConnection

View Source 
var (
	TaskFailedErr      = errors.New("Async task resulted in an Error")
	TaskFailedInnerErr = errors.New("Async task finished with a non-ok FINISHED")
)
View Source 
var AssertionFailed = errors.New("Assertion was not satisfied")
View Source 
var BufferExhaustedError = errors.New("Fixed size internal buffer exhausted")
View Source 
var (
	ErrCorruptState = errors.New("Can't close an unopened or corrupt connection")
)
View Source 
var (

	// error returned when the parser encounteres an unexpected value
	ErrInvalidReplay = errors.New("Unexpected token encountered in replay file")
)
View Source 
var (
	InvalidAddr = errors.New("Can't connect to invalid Addr")
)
View Source 
var ListSessionsUnsupported = errors.New("The server appears to not support the list_sessions command")

error for ListSessions call when list_sessions command is not supported

View Source 
var MessageFormatInvalidErr = errors.New("Message format was invalid")

helper values for parseMessage

View Source 
var NotImplementErr = errors.New("Command wrapper not implemented yet")

error to mark function prototypes

View Source 
var PasswordHandshake = errors.New("Password handshake failed")
View Source 
var PasswordUnterminated = errors.New("Password was not \\n terminated, this is required for direct writing")
View Source 
var UnexpectedContentMap = errors.New("Encountered an unexpected response schema")

Functions

func IsAsync 

func IsAsync(state ClientMessageType) bool

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

Types

type Assertion 

type Assertion struct {
	// contains filtered or unexported fields
}

await an event and apply validation logic

func (*Assertion) Execute 

func (as *Assertion) Execute(
	ctx context.Context,
	logger log.Logger,
	client *IsaClient,
	captures map[string]string,
	_ bool,
) error

func (*Assertion) String 

func (as *Assertion) String() string

type ClientContent 

type ClientContent = map[string]interface{}

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 server 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 similiar applications

func NewEchoMessage 

func NewEchoMessage(content []byte) *ClientMessage

create new message for ECHO commands

func NewMessage 

func NewMessage(state ClientMessageType, content map[string]interface{}) *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 Instruction 

type Instruction struct {
	ClientMessage // the message content to send
}

a single instrution including response validation parameters

func (*Instruction) Execute 

func (ins *Instruction) Execute(
	ctx context.Context,
	logger log.Logger,
	client *IsaClient,
	capture map[string]string,
	pwdCapture bool,
) error

implement step, note: we always augment capture with pwd

NOTE: this is sensitive to the current working directory

func (*Instruction) String 

func (ins *Instruction) String() string

type IsaClient 

type IsaClient struct {
	State IsaClientState
	// contains filtered or unexported fields
}

Client for interacting with an Isabelle Server (not mt-safe) 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 string) 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, , NOTE: doesn't perform handshake

func (*IsaClient) CreateSession 

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

create a new session, returns the used ID

func (*IsaClient) Echo 

func (c *IsaClient) Echo(
	ctx context.Context,
	logger log.Logger,
	content []byte,
) (*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) ([]string, 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,
	sessionID string,
	theories []string,
	masterDir string,
	all bool,
) ([]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) 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 string) error

issue stop_session command

func (*IsaClient) UseTheory 

func (c *IsaClient) UseTheory(
	ctx context.Context,
	logger log.Logger,
	session, theory, path string,
) error

issue a use theory command WARNING: not actively tested NOTE: the current implementation will not behave well with multiple async tasks and/ or session per connection TODO: do this properly via JSON instead of using a template

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 but discards all other messages if unrelatedMsgChan == nil.

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 (
	IcsDisconnected IsaClientState = iota
	IcsIdle
	IcsCorrupt
	IcsConnecting
)

func (IsaClientState) DisplayState 

func (state IsaClientState) DisplayState() string

type Replay 

type Replay struct {
	// contains filtered or unexported fields
}

A list of steps to execute against a server instance for testing

func ParseReplay 

func ParseReplay(replay []byte, logger log.Logger) (*Replay, error)

Parse a replay from a script

func (*Replay) Execute 

func (replay *Replay) Execute(ctx context.Context, logger log.Logger, client *IsaClient) error

Execute a replay against a connected client, note: may be sensitive to current working directory if err == nil then replay was a success else replay failed assertion

func (*Replay) String 

func (replay *Replay) String() string

type SIMDClientMessage 

type SIMDClientMessage struct {
	State   ClientMessageType    // type of message, i.e., used command
	Content *simdjson.ParsedJson // message content

}

a decoded isabelle server message (JSON format only) intended for users that need that don't only need to parse & reencode messages

func ParseSIMDClientMessage 

func ParseSIMDClientMessage(message []byte, msg *SIMDClientMessage, opts ...simdjson.ParserOption) (*SIMDClientMessage, error)

parse a message from a string, gracefully handles messages terminated with (\r)?\n

func (*SIMDClientMessage) Get 

func (msg *SIMDClientMessage) Get(key string, iter *simdjson.Iter, elem *simdjson.Element) (string, error)

try to extract top-level field from content, allows reusable iter and elem otherwise root iter from msg is used and new elem is allocated

func (*SIMDClientMessage) IsAsync 

func (msg *SIMDClientMessage) IsAsync() bool

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

func (*SIMDClientMessage) Serialize 

func (msg *SIMDClientMessage) Serialize() ([]byte, error)

encode a message

type SIMDServerMessage 

type SIMDServerMessage struct {
	State   ServerMessageState
	Content *simdjson.ParsedJson
}

a decoded isabelle server message (JSON format only)

func ParseSIMDServerMessage 

func ParseSIMDServerMessage(message []byte, msg *SIMDServerMessage, opts ...simdjson.ParserOption) (*SIMDServerMessage, error)

parse a message from a string with reuse of msg buffer

func (*SIMDServerMessage) Get 

func (msg *SIMDServerMessage) Get(key string, iter *simdjson.Iter, elem *simdjson.Element) (string, error)

try to extract top-level field from content, allows reusable iter and elem otherwise root iter from msg is used and new elem is allocated

func (*SIMDServerMessage) Ok 

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

try to extract task field from content

func (*SIMDServerMessage) Serialize 

func (msg *SIMDServerMessage) Serialize() ([]byte, error)

encode a message

func (*SIMDServerMessage) TaskID 

func (msg *SIMDServerMessage) TaskID(iter *simdjson.Iter, elem *simdjson.Element) (string, error)

try to extract ok field from content , allows reusable iter and elem otherwise root iter from msg is used and new elem is allocated

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 similiar 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) 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 DEPRECATED: in favor of generic ServerMessage.Get

type ServerMessageState 

type ServerMessageState byte

state of an isabelle server message 

const (
	ServerUnknown ServerMessageState = iota
	ServerFinished
	ServerError
	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"`          // wether to give more NOTEs
	PrintMode      string   `json:"print_mode,omitempty"`       // wether to print more debug information
}

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

type Step 

type Step interface {
	fmt.Stringer

	// Realize encoded step instruction
	Execute(context.Context, log.Logger, *IsaClient, map[string]string, bool) error
}

abstract replay script step

Source Files

View all Source files

Directories

Path Synopsis
cmd
isa-client
isa-replay

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.