Documentation ¶
Index ¶
- Variables
- func IsAsync(state ClientMessageType) bool
- type ClientContent
- type ClientMessage
- type ClientMessageType
- type IsaClient
- func (c *IsaClient) Cleanup(ctx context.Context, session string) error
- func (c *IsaClient) Close() error
- func (c *IsaClient) ConnectPooledClient(ctx context.Context, server netip.AddrPort) (*IsaClient, error)
- func (c *IsaClient) CreateSession(ctx context.Context, args *SessionStartArgs) (string, error)
- func (c *IsaClient) Echo(ctx context.Context, content []byte) (*ServerMessage, error)
- func (c *IsaClient) Handshake(ctx context.Context, password []byte, validateResponse bool) (*ServerMessage, error)
- func (c *IsaClient) HasLS(ctx context.Context) (bool, error)
- func (c *IsaClient) ListSessions(ctx context.Context) ([]string, error)
- func (c *IsaClient) PurgeTheories(ctx context.Context, sessionID string, theories []string, masterDir string, ...) ([]string, error)
- func (c *IsaClient) ReadLine(ctx context.Context) ([]byte, error)
- func (c *IsaClient) ReadMessage(ctx context.Context) (*ServerMessage, error)
- func (c *IsaClient) SetDeadline(t time.Time) error
- func (c *IsaClient) SetReadDeadline(t time.Time) error
- func (c *IsaClient) StopSession(ctx context.Context, session string) error
- func (c *IsaClient) UseTheory(ctx context.Context, session, theory, path string) error
- func (c *IsaClient) WaitState(ctx context.Context, skip []ServerMessageState, target ServerMessageState) (*ServerMessage, error)
- func (c *IsaClient) WaitTask(ctx context.Context, taskID string, unrelatedMsgChan chan<- *ServerMessage) (*ServerMessage, error)
- func (c *IsaClient) Write(ctx context.Context, msg []byte) (int, error)
- func (c *IsaClient) WriteMessage(ctx context.Context, msg ClientMessage) (int, error)
- type IsaClientState
- type IsabelleDatabase
- func (c *IsabelleDatabase) AddEntry(entry *ServerEntry) error
- func (c *IsabelleDatabase) AddEntryCtx(ctx context.Context, entry *ServerEntry) error
- func (c *IsabelleDatabase) Clear() error
- func (c *IsabelleDatabase) ClearCtx(ctx context.Context) error
- func (db *IsabelleDatabase) Close() error
- func (c *IsabelleDatabase) Extended() bool
- func (c *IsabelleDatabase) ListEntries(showExtended bool) (map[string]*ServerEntry, error)
- func (c *IsabelleDatabase) ListEntriesCtx(ctx context.Context, showExtended bool) (map[string]*ServerEntry, error)
- func (db *IsabelleDatabase) RefreshExtended() error
- func (db *IsabelleDatabase) RefreshExtendedCtx(ctx context.Context) error
- func (db *IsabelleDatabase) SetExtended(extended bool) error
- func (db *IsabelleDatabase) SetExtendedCtx(ctx context.Context, extended bool) error
- func (c *IsabelleDatabase) UncheckedSetExtended(extended bool)
- func (*IsabelleDatabase) UpdateEntry(entry *ServerEntry) error
- type SIMDClientMessage
- type SIMDServerMessage
- func (msg *SIMDServerMessage) Get(key string, iter *simdjson.Iter, elem *simdjson.Element) (string, error)
- func (msg *SIMDServerMessage) Ok() (bool, error)
- func (msg *SIMDServerMessage) Serialize() ([]byte, error)
- func (msg *SIMDServerMessage) TaskID(iter *simdjson.Iter, elem *simdjson.Element) (string, error)
- type ServerEntry
- type ServerMessage
- type ServerMessageState
- type SessionStartArgs
Constants ¶
This section is empty.
Variables ¶
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
var ( TaskFailedErr = errors.New("Async task resulted in an Error") TaskFailedInnerErr = errors.New("Async task finished with a non-ok FINISHED") )
var BufferExhaustedError = errors.New("Fixed size internal buffer exhausted")
var (
CorruptStateErr = errors.New("Can't close an unopened or corrupt connection")
)
var ErrAddEntry = errors.New("Failed to add entry")
var (
InvalidAddr = errors.New("Can't connect to invalid Addr")
)
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
var MessageFormatInvalidErr = errors.New("Message format was invalid")
helper values for parseMessage
var NotImplementErr = errors.New("Command wrapper not implemented yet")
error to mark function prototypes
var PasswordHandshake = errors.New("Password handshake failed")
var PasswordUnterminated = errors.New("Password was not \\n terminated, this is required for direct writing")
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) 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 ¶
connect a new client to a server instance, NOTE: doesn't perform handshake
func (*IsaClient) Cleanup ¶
purge theories and close session, basically just c.PurgeTheories + c.StopSession
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 ¶
create a new session, returns the used ID
func (*IsaClient) Echo ¶
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) ListSessions ¶
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 ¶
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 ¶
SetDeadline for the underlying TCP connection
func (*IsaClient) SetReadDeadline ¶
SetReadDeadline for the underlying TCP connection NOTE: assumes client != nil && client.conn != nil
func (*IsaClient) StopSession ¶
issue stop_session command
func (*IsaClient) UseTheory ¶
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) WriteMessage ¶
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 ¶
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) 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.