hydra

package hydra

HyDRA Hybrid Distributed Reasoning Architecture server with a REST-API and database. HyDRA provides a simplified high-level programming interface to the KeYmaeara X prover. It provides components for proof tree simplification, tactic search, and custom tactic scheduling policies, as well as for storing and accessing proofs in files or databases. These components can be accessed remotely through a REST-API.

To do: Stub. Describe for real.

Linear Supertypes

AnyRef, Any

Ordering

Alphabetic
By Inheritance

Inherited

hydra
AnyRef
Any

Hide All
Show All

Visibility

Public
All

Type Members

class AcceptLicenseRequest extends Request with WriteRequest
class AddModelTacticRequest extends UserRequest with WriteRequest
case class AgendaAwesomeResponse(modelId: String, proofId: String, root: ProofTreeNode, leaves: List[ProofTreeNode], agenda: List[AgendaItem], closed: Boolean, marginLeft: Int, marginRight: Int) extends Response with Product with Serializable
case class AgendaItem(id: String, name: String, proofId: String, ancestors: List[String] = Nil) extends Product with Serializable
case class AgendaItemPOJO(itemId: Int, proofId: Int, initialProofNode: ProofTreeNodeId, displayName: String) extends Product with Serializable
class AngularTreeViewResponse extends Response
returns
JSON that is directly usable by angular.treeview
case class ApplicableAxiomsResponse(derivationInfos: List[(DerivationInfo, Option[DerivationInfo])], suggestedInput: Map[ArgInfo, Expression], topLevel: Boolean, suggestedPosition: Option[PositionLocator] = None) extends Response with Product with Serializable
case class ApplicableDefinitionsResponse(defs: List[(NamedSymbol, Expression, Option[Expression], Boolean)]) extends Response with Product with Serializable
case class BelleTermInput(value: String, spec: Option[ArgInfo]) extends Product with Serializable
class BellerophonTacticExecutor extends AnyRef
case class BooleanResponse(flag: Boolean, errorText: Option[String] = None) extends Response with Product with Serializable
class CancelToolRequest extends Request with ReadRequest
class CheckIsProvedRequest extends UserProofRequest with ReadRequest
class CheckTacticInputRequest extends UserProofRequest with ReadRequest
class CheckValidationRequest extends Request with ReadRequest
An idempotent request for the status of a validation request; i.e., validation requests aren't removed until the server is resst.
class ConfigurationPOJO extends AnyRef
class ConfigureMathematicaRequest extends LocalhostOnlyRequest with WriteRequest
class ConfigureMathematicaResponse extends Response
class ConfigureZ3Request extends LocalhostOnlyRequest with WriteRequest
class ConfigureZ3Response extends Response
class CounterExampleRequest extends UserProofRequest with ReadRequest
class CounterExampleResponse extends Response
class CreateControlledStabilityTemplateRequest extends UserRequest with ReadRequest
class CreateModelTacticProofRequest extends UserRequest with WriteRequest
class CreateProofRequest extends UserRequest with WriteRequest
class CreateUserRequest extends Request with WriteRequest
case class CreatedIdResponse(id: String) extends Response with Product with Serializable
trait DBAbstraction extends AnyRef
Proof database
class DashInfoResponse extends Response
case class DbLoadedProofTreeNode(db: DBAbstraction, id: ProofTreeNodeId, proof: ProofTree, children: List[ProofTreeNode], step: Option[ExecutionStep]) extends DbProofTreeNode with Product with Serializable
A loaded node (root if step=None, then also parent=None, maker=None, makerShortName=None).
case class DbPlainExecStepProofTreeNode(db: DBAbstraction, id: ProofTreeNodeId, proof: ProofTree, stepLoader: () ⇒ ExecutionStepPOJO) extends DbProofTreeNode with Logging with Product with Serializable
A proof tree node backed by a database of recorded execution steps.
A proof tree node backed by a database of recorded execution steps. An ID Some(step),None points to the source node where step was executed, an ID Some(step),Some(branch) represents a proxy for the branch subgoal created by step and searches the actual successor step on demand.
case class DbProofTree(db: DBAbstraction, proofId: String) extends ProofTreeBase with Product with Serializable
Builds proof trees from database-recorded step executions, starting at the specified root step (None: proof root).
abstract class DbProofTreeNode extends ProofTreeNode
A ProofTreeNode that happens to be stored in the database db.
case class DbRootProofTreeNode(db: DBAbstraction)(id: ProofTreeNodeId, proof: ProofTree) extends DbProofTreeNode with Product with Serializable
case class DbStepPathNodeId(step: Option[Int], branch: Option[Int]) extends ProofTreeNodeId with Product with Serializable
Identifies a proof tree node by the parent step + branch index.
case class DefaultLoginResponse(triggerRegistration: Boolean) extends Response with Product with Serializable
class DeleteAllModelsRequest extends UserRequest with WriteRequest
class DeleteModelProofStepsRequest extends UserModelRequest with WriteRequest
class DeleteModelRequest extends UserModelRequest with WriteRequest
class DeleteProofRequest extends UserProofRequest with WriteRequest
case class EmptyToken() extends SessionToken with Product with Serializable
class ErrorResponse extends Response
case class ExamplePOJO(id: Int, title: String, description: String, infoUrl: String, url: String, imageUrl: String, level: Int) extends Product with Serializable
A tutorial/case study example.
case class ExecutablePOJO(executableId: Int, belleExpr: String) extends Product with Serializable
case class ExecutionStep(stepId: Int, prevStepId: Option[Int], executionId: Int, localProvableLoader: () ⇒ ProvableSig, branch: Int, subgoalsCount: Int, openSubgoalsCount: Int, successorIds: List[Int], rule: String, executableId: Int, isUserExecuted: Boolean = true) extends Product with Serializable
A proof step in a proof execution trace, can be represented as a node in a proof tree.
case class ExecutionStepPOJO(stepId: Option[Int], executionId: Int, previousStep: Option[Int], branchOrder: Int, status: ExecutionStepStatus, executableId: Int, inputProvableId: Option[Int], resultProvableId: Option[Int], localProvableId: Option[Int], userExecuted: Boolean, ruleName: String, branchLabel: Option[String], numSubgoals: Int, numOpenSubgoals: Int) extends Product with Serializable
case class ExecutionTrace(proofId: String, executionId: String, steps: List[ExecutionStep]) extends Product with Serializable
case class ExpandTacticResponse(detailsProofId: Int, goalSequents: List[Sequent], backendGoals: List[Option[(String, String)]], tacticParent: String, stepsTactic: String, tree: List[ProofTreeNode], openGoals: List[AgendaItem], marginLeft: Int, marginRight: Int) extends Response with Product with Serializable
class ExportCurrentSubgoal extends UserProofRequest with ReadRequest
class ExtractDatabaseRequest extends LocalhostOnlyRequest with RegisteredOnlyRequest
class ExtractDatabaseResponse extends Response
class ExtractLemmaRequest extends UserProofRequest with ReadRequest
class ExtractModelSolutionsRequest extends UserRequest with ReadRequest
class ExtractProblemSolutionRequest extends UserProofRequest with ReadRequest
class ExtractProblemSolutionResponse extends Response
class ExtractTacticRequest extends UserProofRequest with WriteRequest
class FailedRequest extends UserRequest
class FullConfigurationResponse extends Response
class GenericOKResponse extends Response
class GetAgendaAwesomeRequest extends UserProofRequest with ReadRequest
Gets all tasks of the specified proof.
Gets all tasks of the specified proof. A task is some work the user has to do. It is not a KeYmaera task!
class GetAgendaItemResponse extends Response
class GetApplicableAxiomsRequest extends UserProofRequest with ReadRequest
class GetApplicableDefinitionsRequest extends UserProofRequest with ReadRequest
Gets the definitions that can be expanded at node nodeId.
class GetApplicableTwoPosTacticsRequest extends UserProofRequest with ReadRequest
case class GetBranchRootRequest(db: DBAbstraction, userId: String, proofId: String, nodeId: String) extends UserProofRequest with ReadRequest with Product with Serializable
class GetBranchRootResponse extends Response
class GetControlledStabilityTemplateResponse extends Response
class GetDerivationInfoRequest extends UserProofRequest with ReadRequest
class GetFormulaPrettyStringRequest extends UserProofRequest with ReadRequest
class GetFullConfigRequest extends LocalhostOnlyRequest with ReadRequest
class GetLemmasRequest extends UserProofRequest with ReadRequest
class GetMathematicaConfigSuggestionRequest extends LocalhostOnlyRequest with ReadRequest
class GetMathematicaConfigurationRequest extends LocalhostOnlyRequest with ReadRequest
class GetModelListRequest extends UserRequest with ReadRequest
class GetModelRequest extends UserRequest with ReadRequest
class GetModelResponse extends Response
class GetModelTacticRequest extends UserRequest with ReadRequest
class GetModelTacticResponse extends Response
case class GetPathAllRequest(db: DBAbstraction, userId: String, proofId: String, nodeId: String) extends UserProofRequest with ReadRequest with Product with Serializable
class GetPathAllResponse extends Response
class GetProblemResponse extends Response
class GetProofLemmasRequest extends UserProofRequest with ReadRequest
class GetProofNodeChildrenRequest extends UserProofRequest with ReadRequest
Gets the children of a proof node (browse a proof from root to leaves).
class GetProofProgressStatusRequest extends UserProofRequest with ReadRequest
class GetProofRootAgendaRequest extends UserProofRequest with ReadRequest
Gets the proof root as agenda item (browse a proof from root to leaves).
class GetSequentStepSuggestionRequest extends UserProofRequest with ReadRequest
class GetStepRequest extends UserProofRequest with ReadRequest
class GetTacticRequest extends UserProofRequest with ReadRequest
case class GetTacticResponse(tacticText: String, nodesByLoc: Map[Location, String]) extends Response with Product with Serializable
class GetTemplatesRequest extends UserRequest with ReadRequest
class GetTemplatesResponse extends Response
class GetToolRequest extends LocalhostOnlyRequest with ReadRequest
class GetUserThemeRequest extends UserRequest with ReadRequest
class GetWolframEngineConfigSuggestionRequest extends LocalhostOnlyRequest with ReadRequest
class GetWolframScriptConfigSuggestionRequest extends LocalhostOnlyRequest with ReadRequest
class GetZ3ConfigSuggestionRequest extends LocalhostOnlyRequest with ReadRequest
class GetZ3ConfigurationRequest extends LocalhostOnlyRequest with ReadRequest
trait HTMLPrinter extends AnyRef
Prints HTML tags and HTML operators.
class HotkeysRequest extends LocalhostOnlyRequest
case class HtmlResponse(html: Elem) extends Response with Product with Serializable
Responds with a dynamically generated (server-side) HTML page.
class InMemoryDB extends DBAbstraction
In-memory database, e.g., for stepping into tactics.
class InitializeProofFromTacticRequest extends UserProofRequest with ReadRequest
Create a proof if it does not exist yet.
Create a proof if it does not exist yet. Read request, so that guest users can check proofs.
case class InterpreterFuture[T](userId: String, interpreter: Interpreter, callable: Callable[T]) extends FutureTask[T] with Product with Serializable
class IsLicenseAcceptedRequest extends Request with ReadRequest
class IsLocalInstanceRequest extends Request with ReadRequest
case class JSResponse(code: String) extends Response with Product with Serializable
Responds with dynamically generated Javascript code.
class KeymaeraXVersionRequest extends Request with ReadRequest
class KeymaeraXVersionResponse extends Response
class KvpResponse extends Response
class KyxConfigRequest extends LocalhostOnlyRequest with ReadRequest
class KyxConfigResponse extends Response
class LabelledTraceToTacticConverter extends VerbatimTraceToTacticConverter
A verbatim trace to tactic converter whose tactics are as recorded in the database, but adds branch labels.
case class LemmasResponse(infos: List[ProvableInfo]) extends Response with Product with Serializable
class LicensesRequest extends Request with ReadRequest
class ListExamplesRequest extends UserRequest with ReadRequest
List of all predefined tutorials that can directly be imported from the KeYmaera X web UI, in order of display.
class ListExamplesResponse extends Response
class LocalLoginRequest extends LocalhostOnlyRequest with ReadRequest
abstract class LocalhostOnlyRequest extends Request
class LoginRequest extends Request with ReadRequest
class LoginResponse extends Response
class MathematicaConfigStatusRequest extends Request with ReadRequest
class MathematicaConfigSuggestionResponse extends Response
class MathematicaConfigurationResponse extends Response
class MockRequest extends Request
class MockResponse extends Response
class ModelListResponse extends Response
case class ModelPOJO(modelId: Int, userId: String, name: String, date: String, keyFile: String, description: String, pubLink: String, title: String, tactic: Option[String], numAllProofSteps: Int, temporary: Boolean) extends Product with Serializable
Data object for models.
Data object for models.
modelId
Identifies the model.
userId
Identifies the user.
name
The name of the model.
date
The creation date.
keyFile
The model file content.
description
The description of the model.
pubLink
Link to additional information (paper) on the model.
class ModelPlexArtifactResponse extends ModelPlexResponse
class ModelPlexCCodeResponse extends ModelPlexResponse
class ModelPlexMandatoryVarsResponse extends Response
class ModelPlexMonitorResponse extends ModelPlexArtifactResponse
class ModelPlexRequest extends UserRequest with RegisteredOnlyRequest
abstract class ModelPlexResponse extends Response
class ModelPlexSandboxResponse extends ModelPlexArtifactResponse
case class ModelUpdateResponse(modelId: String, name: String, content: String, title: Option[String], description: Option[String], errorText: Option[String]) extends Response with Product with Serializable
case class ModelUploadResponse(modelId: Option[String], errorText: Option[String]) extends Response with Product with Serializable
case class NewlyExpiredToken(token: String) extends SessionToken with Product with Serializable
case class NodeChildrenResponse(proofId: String, parent: ProofTreeNode, marginLeft: Int, marginRight: Int) extends Response with Product with Serializable
class NodeResponse extends Response
class ODEConditionsRequest extends UserProofRequest with ReadRequest
class ODEConditionsResponse extends Response
class OpenGuestArchiveRequest extends Request with ReadRequest
class OpenOrCreateLemmaProofRequest extends UserRequest with WriteRequest
class OpenProofRequest extends UserRequest with ReadRequest
case class OpenProofResponse(proof: ProofPOJO, loadStatus: String) extends Response with Product with Serializable
case class ParseErrorResponse(msg: String, expect: String, found: String, detailedMsg: String, loc: Location, exn: Throwable = null) extends ErrorResponse with Product with Serializable
class PegasusCandidatesRequest extends UserProofRequest with ReadRequest
class PegasusCandidatesResponse extends Response
class PlainResponse extends Response
class PossibleAttackResponse extends Response with Logging
class ProofAgendaResponse extends Response
class ProofIsLoadedResponse extends ProofStatusResponse
class ProofIsLoadingResponse extends ProofStatusResponse
case class ProofLemmasResponse(lemmas: List[(String, Int)]) extends Response with Product with Serializable
class ProofListResponse extends Response
class ProofNodeSequentRequest extends UserProofRequest with ReadRequest
case class ProofNodeSequentResponse(proofId: String, node: ProofTreeNode, marginLeft: Int, marginRight: Int) extends Response with Product with Serializable
class ProofNotLoadedResponse extends ProofStatusResponse
case class ProofPOJO(proofId: Int, modelId: Option[Int], name: String, description: String, date: String, stepCount: Int, closed: Boolean, provableId: Option[Int], temporary: Boolean = false, tactic: Option[String]) extends Product with Serializable
Data object for proofs.
Data object for proofs.
proofId
Identifies the proof.
modelId
Identifies the model; if defined, model formula must agree with provable's conclusion
name
The proof name.
description
A proof description.
date
The creation date.
stepCount
The number of proof steps in the proof.
closed
Indicates whether the proof is closed (finished proof) or not (partial proof).
provableId
Refers to a provable whose conclusion to prove.
temporary
Indicates whether or not the proof is temporary.
tactic
The tactic to recreate the proof.
class ProofProgressResponse extends ProofStatusResponse
case class ProofSession(proofId: String, invGenerator: Generator[GenProduct], invSupplier: Generator[GenProduct], defs: Declaration) extends Product with Serializable
A proof session storing information between requests.
case class ProofStateInfo(loc: Region, node: String) extends Product with Serializable
class ProofStatusResponse extends Response
class ProofTaskExpandRequest extends UserProofRequest with ReadRequest
class ProofTaskNodeRequest extends UserProofRequest with ReadRequest
class ProofTaskNodeResponse extends Response
class ProofTaskParentRequest extends UserProofRequest with ReadRequest
trait ProofTree extends AnyRef
The central proof tree data structure managing the proof search, consisting of a set of ProofTreeNode.
The central proof tree data structure managing the proof search, consisting of a set of ProofTreeNode. Unlike the stateless edu.cmu.cs.ls.keymaerax.core.Provable representation of the prover kernel, proof trees provide navigation and tactic scheduling infrastructure.

See also
edu.cmu.cs.ls.keymaerax.core.Provable
ProvableSig
abstract class ProofTreeBase extends ProofTree
trait ProofTreeNode extends AnyRef
A Proof Tree Node represents the central element of managing a (possibly large compound) inference during proof search in a ProofTree.
A Proof Tree Node represents the central element of managing a (possibly large compound) inference during proof search in a ProofTree. Unlike the stateless edu.cmu.cs.ls.keymaerax.core.Provable representation of the prover kernel, proof trees provide navigation and tactic scheduling infrastructure.
Beyond providing proof tree navigation information, this type manages the interface to the kernel's provable. Proof tree nodes consist of a local provable that created this proof node, and which can later be stitched together after completing the entire subproof. The provable function can later perform the computation required to staple the proof together as far as the children have completed it.
The proof treee node also provides infrastructure for letting tactics run to expand this proof tree node.

See also
edu.cmu.cs.ls.keymaerax.core.Provable
ProvableSig
trait ProofTreeNodeId extends AnyRef
class ProofTreeResponse extends Response
class ProofVerificationResponse extends Response
class ProofsForModelRequest extends UserRequest with ReadRequest
class ProofsForUserRequest extends UserRequest with ReadRequest
case class ProvablePOJO(provableId: Int, provable: ProvableSig) extends Product with Serializable
class PruneBelowRequest extends UserProofRequest with WriteRequest
Prunes a node and everything below
class PruneBelowResponse extends Response
trait ReadRequest extends AnyRef
case class ReadWriteToken(token: String, username: String) extends UserToken with Product with Serializable
case class ReadonlyToken(token: String, username: String) extends UserToken with Product with Serializable
trait RegisteredOnlyRequest extends AnyRef
sealed trait Request extends Logging
A Request should handle all expensive computation as well as all possible side-effects of a request (e.g.
A Request should handle all expensive computation as well as all possible side-effects of a request (e.g. updating the database), but should not modify the internal state of the HyDRA server (e.g. do not update the event queue).
Requests objects should do work after getResultingUpdates is called, not during object construction.
Request.getResultingUpdates might be run from a new thread.
sealed trait Response extends AnyRef
Responses are like views -- they shouldn't do anything except produce appropriately formatted JSON from their parameters.
Responses are like views -- they shouldn't do anything except produce appropriately formatted JSON from their parameters.
To create a new response:
- Create a new object extending Response (perhaps with constructor arguments)
- override the json value with the json to be generated.
- override the schema value with Some(File(...)) containing the schema.
See BooleanResponse for the simplest example.
class RestartToolRequest extends LocalhostOnlyRequest
class RunBelleTermRequest extends UserProofRequest with WriteRequest
case class RunBelleTermResponse(proofId: String, nodeId: String, taskId: String, info: String) extends Response with Product with Serializable
class SaveFullConfigRequest extends LocalhostOnlyRequest with ReadRequest
case class SequentFormulaPOJO(sequentFormulaId: Int, sequentId: Int, isAnte: Boolean, index: Int, formulaStr: String) extends Product with Serializable
case class SequentPOJO(sequentId: Int, provableId: Int) extends Product with Serializable
trait SessionToken extends AnyRef

Note
a custom Option so that Scala doesn't use None as an implicit parameter.
class SetDefaultUserRequest extends LocalhostOnlyRequest with WriteRequest
class SetDefinitionsRequest extends UserProofRequest with WriteRequest
class SetToolRequest extends LocalhostOnlyRequest with WriteRequest
class SetUserThemeRequest extends UserRequest with ReadRequest
Sets the UI theme.
Sets the UI theme. @note ReadRequest allows changing theme in guest mode for presentation purposes.
class SetupSimulationRequest extends UserProofRequest with RegisteredOnlyRequest
class SetupSimulationResponse extends Response
class ShutdownReqeuest extends LocalhostOnlyRequest with RegisteredOnlyRequest
class SimulationRequest extends UserProofRequest with RegisteredOnlyRequest
class SimulationResponse extends Response
class StepwiseTraceRequest extends UserProofRequest with ReadRequest
class StopTaskRequest extends UserProofRequest with WriteRequest
class SystemInfoRequest extends LocalhostOnlyRequest with ReadRequest
class SystemInfoResponse extends Response
trait Tables extends AnyRef
Slick data model trait for extension, choice of backend or usage in the cake pattern.
Slick data model trait for extension, choice of backend or usage in the cake pattern. (Make sure to initialize this late.)
class TacticDiffRequest extends Request with ReadRequest
class TacticDiffResponse extends Response
class TacticErrorResponse extends ErrorResponse
case class TacticExecutionPOJO(executionId: Int, proofId: Int) extends Product with Serializable
case class TacticInfo(tacticText: String, nodesByLocation: List[ProofStateInfo]) extends Product with Serializable
class TaskResultRequest extends UserProofRequest with ReadRequest
case class TaskResultResponse(proofId: String, parent: ProofTreeNode, marginLeft: Int, marginRight: Int, progress: Boolean = true) extends Response with Product with Serializable
class TaskStatusRequest extends UserProofRequest with ReadRequest
case class TaskStatusResponse(proofId: String, nodeId: String, taskId: String, status: String, progress: Option[(Option[(BelleExpr, Long)], Seq[(BelleExpr, Either[BelleValue, BelleThrowable])])]) extends Response with Product with Serializable
class TempDBTools extends AnyRef
Create models and record proofs in a temporary database.
case class TemplatePOJO(title: String, description: String, text: String, selectRange: Option[Region], imageUrl: Option[String]) extends Product with Serializable
A text template with optional region to select and set the cursor to on display.
class TestSynthesisRequest extends UserRequest with RegisteredOnlyRequest
class TestSynthesisResponse extends Response
class TestToolConnectionRequest extends LocalhostOnlyRequest
class ToolConfigErrorResponse extends ErrorResponse
class ToolConfigStatusResponse extends Response
class ToolStatusRequest extends Request with ReadRequest
class ToolStatusResponse extends Response
trait TraceToTacticConverter extends AnyRef
abstract class TraceToTacticConverterBase extends TraceToTacticConverter
class UIAbbreviatingKeYmaeraXPrettierPrinter extends KeYmaeraXPrettierPrinter
class UIAbbreviatingKeYmaeraXPrettyPrinter extends KeYmaeraXWeightedPrettyPrinter
class UIKeYmaeraXAxiomPrettyPrinter extends KeYmaeraXWeightedPrettyPrinter with HTMLPrinter
User-interface pretty printer for UI axiom entries.
class UIKeYmaeraXPrettyPrinter extends UIAbbreviatingKeYmaeraXPrettyPrinter
User-interface pretty printer for KeYmaera X syntax.
class UndoLastProofStepRequest extends UserProofRequest with WriteRequest
Undoes the last proof step.
class UnimplementedResponse extends ErrorResponse
class UpdateModelRequest extends UserRequest with WriteRequest
class UpdateProofNameRequest extends UserProofRequest with WriteRequest
class UpdateProofNameResponse extends Response
class UpdateResponse extends Response
class UploadArchiveRequest extends UserRequest with WriteRequest
class UserLemmasRequest extends UserRequest with ReadRequest
class UserLemmasResponse extends Response
abstract class UserModelRequest extends UserRequest
class UserPOJO extends AnyRef
Data object for users.
abstract class UserProofRequest extends UserRequest
abstract class UserRequest extends Request
A request that requires an authenticated user who also passes the dataPermission check.
abstract class UserToken extends SessionToken
class ValidateProofRequest extends Request with ReadRequest
Returns a UUID whose status can be queried at a later time ({complete: true/false[, proves: true/false]}.
Returns a UUID whose status can be queried at a later time ({complete: true/false[, proves: true/false]}.

See also
CheckValidationRequest - calling this with the returned UUID should give the status of proof checking.
class ValidateProofResponse extends Response
class VerbatimTraceToTacticConverter extends TraceToTacticConverterBase
A verbatim trace to tactic converter whose tactics are as recorded in the database.
class VerboseTraceToTacticConverter extends LabelledTraceToTacticConverter
class WolframEngineConfigStatusRequest extends Request with ReadRequest
class WolframScriptConfigStatusRequest extends Request with ReadRequest
trait WriteRequest extends RegisteredOnlyRequest
class Z3ConfigStatusRequest extends Request with ReadRequest
class Z3ConfigSuggestionResponse extends Response
class Z3ConfigurationResponse extends Response

Value Members

object AgendaItem extends Serializable
object ArchiveEntryPrinter
object BellerophonTacticExecutor
Scheduler for Bellerophon tactics
object DBAbstractionObj extends Logging
object DBTools
object DatabasePopulator extends Logging
Populates the database from a JSON collection of models and tactics.
object DbPlainExecStepProofTreeNode extends Logging with Serializable
object ExecutionStepStatus extends Enumeration
object Helpers
JSON conversions for frequently-used response formats
object HyDRAInitializer extends Logging
Initializes the HyDRA server.
object HyDRAServerConfig
Config vars needed for server setup.
object KyxSslConfiguration
Created by nfulton on 6/25/16.
Created by nfulton on 6/25/16. Copied from https://gist.github.com/pymeat/7426513
object NonSSLBoot extends App with Logging
Creates a HyDRA server listening on a host and port specified in the database's config file under the configurations serverconfig.host and serverconfig.port.
Creates a HyDRA server listening on a host and port specified in the database's config file under the configurations serverconfig.host and serverconfig.port. Uses localhost and 8090 by default.

Note
The HyDRA_SSL environmental variable needs to be set properly because it is used in application.conf. Main.startServer should so the correct thing based upon the current value of that flag. However, from within IntelliJ, you may want to modify application.conf directly and comment out the assertion at the top of this object.
See also
SSLBoot for SSL-enabled deployments.
object Password
Password generation and checking using PBKDF2.
Password generation and checking using PBKDF2. Based on security advice from OWASP web security project.

See also
www.owasp.org Created by bbohrer on 12/29/15.
object ProofValidationRunner extends Logging
Global server state for proof validation requests.
Global server state for proof validation requests. For now, scheduling immediately dispatches a new thread where the validation occurs. In the future, we may want to rate-limit validation requests. The easiest way to do that is to create a thread pool with a max size.
object RequestHelper
object RestApi extends Logging
RestApi is the API router.
RestApi is the API router. See README.md for a description of the API.
object SQLite
Database implementation based on SQLite and Slick.
Database implementation based on SQLite and Slick. Stores and queries: - Lemmas (used for storing proof steps) - UI configuration - Users - Models - Proofs and proof steps - Proof agendas - Proof trees
Created by nfulton on 4/10/15.
object SSLBoot extends App with Logging
Boots a server with SSL enabled.
Boots a server with SSL enabled.
Booting from SSL requires a KeyStore.jks file in the keymaerax-webui/src/main/resources directory. The password for this key strong should be stored in the config table of the production database under the configuration key serverconfig.jks.

Note
The HyDRA_SSL environmental variable needs to be set properly because it is used in application.conf. Main.startServer should so the correct thing based upon the current value of that flag. However, from within IntelliJ, you may want to modify application.conf directly and comment out the assertion at the top of this object.
See also
NonSSLBoot is better if you are binding to localhost or only exposing your server to trusted clients (i.e., not on the internet or a semi-public intranet.)
object SessionManager

To do
replace this with an existing library that does The Right Things
do we want to enforce timeouts as well?
object SqliteTableGenerator
object Tables extends Tables
Stand-alone Slick data model for immediate use
object TacticExtractionErrors
object TacticInfoJsonProtocol extends DefaultJsonProtocol
object UIKeYmaeraXAxiomPrettyPrinter
object UIKeYmaeraXPrettyPrinter extends HTMLPrinter

Packages

KeYmaera X: An aXiomatic Tactical Theorem Prover

Package Structure

Entry Points

References

Proof Styles

Explicit Proof Certificates

Explicit Proofs

Proof by Search

Proof by Pointing

Proof by Congruence

Proof by Chase

Additional Mechanisms

KeYmaera X Kernel

Usage Overview

Constructing Proofs

Combining Proofs

Differential Dynamic Logic

Syntax

Static Semantics

Theorem Prover

Axioms

Uniform Substitutions

Sequent Proof Rules

Additional Capabilities

Stored Provable Mechanism

Error Reporting

Set Lattice

Overall Code Complexity

Lemma Mechanism

Usage Overview

Printing Differential Dynamic Logic

Printing Fully Parenthesized Forms

Parsing Differential Dynamic Logic

Parsing Only Formulas of Differential Dynamic Logic

Parsing Pretty-Printed Strings

Pretty-Printing Parsed Strings

Pretty-Printing Sequents

hydra 

package hydra

Type Members

Value Members

Inherited from AnyRef

Inherited from Any

Ungrouped

hydra