additionally use broker service to know which tutors are available and to
subscribe to one or more of them.
- Usually, when the role of client is taken by an interactive proof assistant,
+ Usually, when the client role is taken by an interactive proof assistant,
new status are sent to the broker as soon as the proof change (e.g. when the
user applies a tactic or when a new proof is started) and hints are shown to
the user be the means of some effect in the user interface (e.g. popping a
dialog box or enlightening a tactic button).\ednote{CSC: questo \'e un
- possibile posto dove mettere una mini-sessione interattiva. L'appendice
- un altro.}
+ possibile posto dove mettere una reference a una mini-sessione interattiva.
+ \'E l'appendice un posto dove metterla?}
\myincludegraphics{interfaces}{t!}{10cm}{\hbugs{} \wss{} interfaces}
{\hbugs{} \wss{} interfaces}
providers and requesters for \emph{both} clients and tutors, see Fig.
\ref{interfaces}.
- With respect to client, a broker act as \ws{} provider, receiving the
+ With respect to the client, a broker acts as a \ws{} provider, receiving the
proof status and forwarding it to one or more tutors.
It also acts as a \ws{} requester sending
hints to the client as soon as they are available from the tutors.
- With respect to tutors, the \ws{} provider role is accomplished by receiving
- hints as soon as they are produced; as a requester, it is accomplished
- by asking for computations (\emph{musings} in \hbugs{} terminology) on
- status received by clients and by stopping already late but still
- ongoing \musings{}.
+ With respect to the tutors, the \ws{} provider role is accomplished by
+ receiving hints as soon as they are produced; as a requester, it is
+ accomplished by asking for computations (\emph{musings} in \hbugs{}
+ terminology) on status received by clients and by stopping already late but
+ still ongoing \musings{}.
Additionally brokers keep track of available tutors and clients
subscriptions.
which the client is subscribed), Execution Manager. The Service Manager
component is not required since the session handler, that identifies
a session between a service and a broker, is provided to the service by
- the broker instead of being received from the service when it is
+ the broker instead of being received from the service when the session is
initialized. In particular, a session is identified by an unique identifier
for the client (its URL) and an unique identifier for the broker (its
URL).
\paragraph{Tutors}
Tutors are software component able to consume proof status producing hints.
- \hbugs{} doesn't specify by which means hints should be produced: tutors can
- use any means necessary (heuristics, external theorem prover or CAS, ...).
- The only requirement is that there exists an agreement on the formats of
- proof status and hints.
+ \hbugs{} does not specify by which means hints should be produced: tutors
+ can use any means necessary (heuristics, external theorem prover or CAS,
+ etc.). The only requirement is that there exists an agreement on the
+ formats of proof status and hints.
Tutors act both as \ws{} providers and requesters for the broker. As
providers, they wait for commands requesting to start a new \musing{} on
\hbugs{} tutors act as MONET services.
+\section{An \hbugs{} Session Example}
+
\section{Implementation's Highlights}
\label{implementation}
In this section we present some of the most relevant implementation details of
unregister from brokers using \texttt{Unregister\_broker} method.
Each time the client status change, the status is sent to the
- broker using its \emph{Status} method. Using both clients registry (to
+ broker using its \texttt{Status} method. Using both clients registry (to
lookup client's subscription) and tutors registry (to check if some tutors
has unsubscribed), the broker is able to decide to which tutors the
new status must be forwarded.\ednote{CSC: qui o nei lavori futuri parlare
Consulting the \musings{} registry, the broker is able to know, at each
time, which \musings{} are in execution on which tutor. This peculiarity is
- exploited by the broker on invocation of Status method. Receiving a new
- status from the client implies indeed that the previous status no longer
- exists and all \musings{} working on it should be stopped: additionally to
- the already described behavior (i.e. starting new \musings{} on the
- received status), the broker takes also care of stopping ongoing
- computation invoking \texttt{Stop\_musing} tutors' method.
+ exploited by the broker on invocation of the \texttt{Status} method.
+ Receiving a new status from the client implies indeed that the previous
+ status no longer exists and all \musings{} working on it should be stopped:
+ additionally to the already described behavior (i.e. starting new
+ \musings{} on the received status), the broker takes also care of stopping
+ ongoing computation invoking the \texttt{Stop\_musing} method of the tutors.
\paragraph{\wss{}}
As already discussed, all \hbugs{} actors act as \wss{} offering one or more
services to neighbor actors. To grant as most accessibility as possible to
- our \wss{} we have chosen to bind them using the HTTP/POST bindings
- described in \cite{wsdlbindings}\footnote{Given that our proof assistant was
- entirely developed in the Objective Caml language, we have chosen to
- develop also \hbugs{} in that language in order to maximize code reuse. To
- develop \wss{} in Objective Caml we have developed an auxiliary generic
- library (\emph{O'HTTP}) that can be used to write HTTP 1.1 Web servers and
- abstract over GET/POST parsing. This library supports different kinds of Web
- servers architecture, including multi-process and multi-threaded ones.}.
+ our \wss{} we have chosen to bind them using the HTTP/POST\footnote{Given
+ that our proof assistant was entirely developed in the Objective Caml
+ language, we have chosen to develop also \hbugs{} in that language in order
+ to maximize code reuse. To develop \wss{} in Objective Caml we have
+ developed an auxiliary generic library (\emph{O'HTTP}) that can be used to
+ write HTTP 1.1 Web servers and abstract over GET/POST parsing. This library
+ supports different kinds of Web servers architecture, including
+ multi-process and multi-threaded ones.} bindings described in
+ \cite{wsdlbindings}.
\paragraph{Tutors}
Each tutor expose a \ws{} interface and should be able to work, not only for
incoming request following the classical one-thread-per-request approach in
web servers design.
If the received request is \texttt{Start\_musing}, a new thread is
- spawned to handle it and the thread in duty to handle the HTTP request
- returns an HTTP response containing an identifier of the just started
- musing. Otherwise, if the received request is \texttt{Stop\_musing},
- it carries a \texttt{musing} identifier used to identify the thread
- responsible for a \texttt{musing}; that thread gets killed and an HTTP
- response is returned.
-
+ spawned to handle it; the thread in duty to handle the HTTP request
+ returns an HTTP response containing the identifier of the just started
+ \texttt{musing}, and then dyes. If the received request is
+ \texttt{Stop\_musing}, instead, the spawned thread kills the thread
+ responsible for the \texttt{musing} whose identifier is the argument
+ of the \texttt{Stop\_musing} method.
+
This architecture turns out to be scalable and allows the running threads
to share the cache of loaded (and type-checked) theorems.
As we will explain in Sect. \ref{tutors}, this feature turns out to be
with the \helm{} Search-Engine and looks for lemmas that can be directly
applied.
- We have many plan for further developing both the \hbugs{} architecture and
+ We have many plans for further developing both the \hbugs{} architecture and
our prototype. Interesting results could be obtained
augmenting the informative content of each suggestion. We can for example
modify the broker so that also negative results are sent back to the client.
the client to trust other actors a bit more than in the current approach.
We plan also to add some rating mechanism to the architecture. A first
- improvement in this direction could be to distinguish between hints that, when
+ improvement in this direction could be distinguishing between hints that, when
applied, are able to completely close one or more goals and
tactics that progress in the proof by reducing one or more goals to new goals:
the new goals could be false and the proof can be closed only by backtracking.
privileging therefore non-overkilling solutions \cite{ring}.
We are also considering to follow the \OmegaAnts{} path more closely adding
- ``recursion'' to the system so that proof status resulting from the
+ ``recursion'' to the system so that the proof status resulting from the
application of old hints are cached somewhere and could be used as a starting
point for new hint searches. The approach is interesting, but it represents
a big shift towards automatic theorem proving: thus we must consider if it is
worth the effort given the increasing availability of automation in proof
- assistants' tactics and the ongoing development of \wss{} based on
+ assistants tactics and the ongoing development of \wss{} based on
already existent and well developed theorem provers.
Even if not strictly part of the \hbugs{} architecture, the graphical user
projects / helm.git / commitdiff