isalink

package module
v0.0.0-...-3a4e46e Latest Latest
Warning

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

 Go to latest Published: Apr 16, 2024 License: AGPL-3.0 Imports: 18 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 (x86_64) runner with a 6.x kernel.

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, I recommend the 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're ready to go:

  • 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

INFO: The CI also just runs 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 BufferExhaustedError = errors.New("Fixed size internal buffer exhausted")
View Source 
var (
	CorruptStateErr = errors.New("Can't close an unopened or corrupt connection")
)
View Source 
var ErrAddEntry = errors.New("Failed to add entry")
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 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

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
	// 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, 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, 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, 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, args *SessionStartArgs) (string, error)

create a new session, returns the used ID

func (*IsaClient) Echo 

func (c *IsaClient) Echo(ctx context.Context, 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, 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) (bool, error)

check if list_sessions extensions is supported

func (*IsaClient) ListSessions 

func (c *IsaClient) ListSessions(ctx context.Context) ([]string, error)

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

func (*IsaClient) PurgeTheories 

func (c *IsaClient) PurgeTheories(ctx context.Context, sessionID string, theories []string, masterDir string, all bool) ([]string, error)

issue purge theories command

func (*IsaClient) ReadLine 

func (c *IsaClient) ReadLine(ctx context.Context) ([]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) (*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, session string) error

issue stop_session command

func (*IsaClient) UseTheory 

func (c *IsaClient) UseTheory(ctx context.Context, 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, 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, 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, msg []byte) (int, error)

raw write to underlying connection

func (*IsaClient) WriteMessage 

func (c *IsaClient) WriteMessage(ctx context.Context, 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 IsabelleDatabase 

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

a small abstraction over the Isabelle Servers Database this database is used by both isabelle client and server to exchange port and password for all locally running services

func OpenDatabase 

func OpenDatabase(path string, extended bool, createMissing bool) (*IsabelleDatabase, error)

Open a new database connection to sqlite://{path}, may upsert an extended table if `extended` is set. If `createMissing` is set, the database file at {path} will be created, if missing and not `createMissing` returns `os.ErrNotExist`

func (*IsabelleDatabase) AddEntry 

func (c *IsabelleDatabase) AddEntry(entry *ServerEntry) error

add entry in database (uses ctx.Backgroud internally) NOTE: this will also add the entry to the extended table, if the database is marked as Extended and entry.Host != nil

func (*IsabelleDatabase) AddEntryCtx 

func (c *IsabelleDatabase) AddEntryCtx(ctx context.Context, entry *ServerEntry) error

add entry in database NOTE: this will also add the entry to the extended table, if the database is marked as Extended and entry.Host != nil

func (*IsabelleDatabase) Clear 

func (c *IsabelleDatabase) Clear() error

clear all entries (uses ctx.Background internally) NOTE: this will also clear the extended table, if the database is marked as extended

func (*IsabelleDatabase) ClearCtx 

func (c *IsabelleDatabase) ClearCtx(ctx context.Context) error

clear all entries NOTE: this will also clear the extended table, if the database is marked as extended

func (*IsabelleDatabase) Close 

func (db *IsabelleDatabase) Close() error

close internal db connection

func (*IsabelleDatabase) Extended 

func (c *IsabelleDatabase) Extended() bool

check if database is marked as extended

func (*IsabelleDatabase) ListEntries 

func (c *IsabelleDatabase) ListEntries(showExtended bool) (map[string]*ServerEntry, error)

retrieve all entries from database (uses context.Background internally)

func (*IsabelleDatabase) ListEntriesCtx 

func (c *IsabelleDatabase) ListEntriesCtx(ctx context.Context, showExtended bool) (map[string]*ServerEntry, error)

retrieve all entries from database with supplied context returns mappings of name:ServerEntry{name, password, port, host?} NOTE: when both the extended table has precedence over the normal table on name conflicts

func (*IsabelleDatabase) RefreshExtended 

func (db *IsabelleDatabase) RefreshExtended() error

check wether extended table exists uses ctx.Background internally

func (*IsabelleDatabase) RefreshExtendedCtx 

func (db *IsabelleDatabase) RefreshExtendedCtx(ctx context.Context) error

check wether extended table exists

func (*IsabelleDatabase) SetExtended 

func (db *IsabelleDatabase) SetExtended(extended bool) error

drop extended table (uses context.Background()) NOTE: this drops the underlying extended table and marks the database as non-extended

func (*IsabelleDatabase) SetExtendedCtx 

func (db *IsabelleDatabase) SetExtendedCtx(ctx context.Context, extended bool) error

drop extended table NOTE: this drops the underlying extended table and marks the database as non-extended

func (*IsabelleDatabase) UncheckedSetExtended 

func (c *IsabelleDatabase) UncheckedSetExtended(extended bool)

set database extended state manually WARNING: this is only recommended if you modified the database externally

func (*IsabelleDatabase) UpdateEntry 

func (*IsabelleDatabase) UpdateEntry(entry *ServerEntry) error

update entry in database (primary key = name) NOTE: this will also update the extended table, if the database is marked as extended and entry.Host != nil

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 ServerEntry 

type ServerEntry struct {
	Port     uint16
	Name     string
	Password string
	Host     *string
}

a simple

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

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.