% vim:nojs: tw=76 sw=4 sts=4 fo=awn fdm=marker

%

% 20090406 T. Bourke

%	Original document.

%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\documentclass[a4paper,draft]{article} % XXX

%\documentclass[a4paper,final]{article}

% Preamble

\usepackage[T1]{fontenc}

\usepackage{textcomp}

\usepackage{ifdraft}

\bibliographystyle{abbrv} % alpha

\newcommand{\refsec}[1]{Section~\ref{sec:#1}}

\newcommand{\reffig}[1]{Figure~\ref{fig:#1}}

\newcommand{\reftab}[1]{Table~\ref{tab:#1}}

%

\usepackage{acronym}

\usepackage{pst-all}

\usepackage{url}

\title{Isabelle find\_theorems on the web}

\author{T. Bourke\thanks{NICTA}}

\special{!/pdfmark where

 {pop} {userdict /pdfmark /cleartomark load put} ifelse

 [ /Author   (T. Bourke, NICTA)

   /Title    (IsabelleWWW: find_theorems

	      ($Date: 2008-10-03 16:09:02 +1000 (Fri, 03 Oct 2008) $))

   /Subject  (Web interface to find_theorems)

   /Keywords (isabelle, sml, http, www)

   /DOCINFO pdfmark}

\begin{document}

% Title page and abstract

\maketitle

\begin{abstract}

The Isabelle find\_theorems command processes queries against a theory 

database and returns a list of matching theorems.

It is usually given from the Proof General or command-line interface.

This document describes a web server implementation.

Two design alternatives are presented and an overview of an implementation 

of one is described.

\end{abstract}

\section{Introduction}\label{sec:intro}

This document describes the design and implementation of a web interface for 

the Isabelle find\_theorems command.

The design requirements and their consequences are detailed in \refsec{req}.

Two architectures were considered: \begin{enumerate}

\item \emph{one process}: integrate a web server into Isabelle.

\item \emph{two processes}: run Isabelle as a web server module.

\end{enumerate}

A brief evaluation of the one process architecture is presented in 

\refsec{oneproc}.

An implementation of the two process is presented in \refsec{twoproc}.

\section{Design requirements}\label{sec:req}

The main requirements are:\begin{enumerate}

\item The system will allow users to search for theorems from a web browser.

\item It will allow queries across disparate Isabelle theories.

\item It will, at a minimum, handle theories from the L4.verified project.

\item It will run on a secure network.

\item There will be at most ten simultaneous users.

\end{enumerate}

\noindent

Several \emph{a priori} choices are fixed:\begin{enumerate}

\item The search will run against an Isabelle heap.

\item A single heap will be built from the theories to be searched.

\item The system must be persistent, for two reasons: \begin{enumerate}

    \item Isabelle is slow to start against large heaps.

    \item Later enhancements may require tracking states at the server.

\end{enumerate}

\end{enumerate}

\section{Evaluation: Isabelle web server}\label{sec:oneproc}

The advantage of integrating a web server into Isabelle is that the 

find\_theorems service could be provided by a single process, which, in 

principle, would simplify administration.

Implementing even a simple \ac{HTTP} service from scratch is an unacceptable 

cost and fraught with potential problems and limitations.

It is preferable to adapt an existing system.

As Isabelle is written in \ac{SML}, only \ac{HTTP} services also written in 

\ac{SML} can realistically be considered.

In principle Isabelle compiles on both Poly/ML and \ac{SML/NJ}, but in 

practice the former is faster, more widely used, and better supported.

In particular, the L4.verified project does not build effectively on 

\ac{SML/NJ}.

This further limits the potential to adapt an existing system.

There are three \ac{SML} web server projects:\\

\centerline{\begin{tabular}{ll}

SMLServer &

    \url{http://www.smlserver.org}\\

FoxNet web server &

    \url{http://www.cs.cmu.edu/~fox/}\\

Swerve web server &

    \url{http://mlton.org/Swerve}

\end{tabular}}

Unfortunately, none of these projects is suitable.

The SMLServer is an Apache web server plugin.

It runs \ac{SML} programs that generate dynamic web pages.

SMLServer is based on the MLKit compiler.

It is unlikely that Isabelle and the l4.verified heaps could be compiled in 

MLKit, at least not without significant effort.

The FoxNet web server was developed as part of the Fox project at \ac{CMU}.

The source is not readily available.

The Swerve web server is part of an unpublished book on systems programming 

in \ac{SML}.

The source code is available and it is readily patched to run under the 

latest version of SML/NJ (110.67).

Adapting it to Poly/ML would require non-trivial effort because it is based 

on \ac{CML}, whose implementation on SML/NJ makes use of continuations 

(SMLofNJ.cont).

\section{Implementation: Isabelle web module}\label{sec:twoproc}

The description of the two process solution is divided into two subsections.

The first contains an overview of the architecture and web server specifics.

The second contains a summary of an \ac{SML} implementation of the web 

module in Isabelle.

\subsection{Architecture and web server}\label{sec:oneproc:arch}

\newcommand{\component}[1]{%

    \rput(0,0){\psframe(-.8,-.6)(.8,.6)}%

    \rput(0,0){\parbox{4.3em}{\centering{#1}}}}

\begin{figure}

\centering%

\begin{pspicture}(-4.8,0)(3.3,4)%\psgrid

    \newpsstyle{conn}{arrows=->}%

    %

    \rput(-2.2,3.3){\component{web server}}%

    \rput( 2.2,3.3){\component{web module}}%

    \rput(-2.2,0.7){\component{web client}}%

    \rput(-4.2,3.4){%

	\psellipse(0,-.2)(.4,.2)%

	\psframe[linestyle=none,fillstyle=solid,fillcolor=white]%

		(-.4,-.2)(.4,.1)%

	\psellipse(0,.1)(.4,.2)%

	\psline(-.38,-.2)(-.38,.1)\psline(.38,-.2)(.38,.1)%

    }%

    \psline[style=conn,arrows=<->](-3.0,3.3)(-3.8,3.3)%

    %

    \rput[rB](3.3,2.15){server}%

    \psline[linestyle=dashed](-4.8,2)(3.3,2)%

    \rput[rt](3.3,1.90){network}%

    %

    \rput[B](0.0,3.55){\psframebox*{module protocol}}%

    \psline[style=conn](-1.4,3.4)(1.4,3.4)%

    \psline[style=conn](1.4,3.2)(-1.4,3.2)%

    %

    \rput[B]{90}(-2.4,2.0){\psframebox*{\ac{HTTP}}}%

    \psline[style=conn](-2.1,2.7)(-2.1,1.3)%

    \psline[style=conn](-2.3,1.3)(-2.3,2.7)%

\end{pspicture}

\caption{Overview of web module architecture\label{fig:modulearch}}

\end{figure}

An overview of a simple web server architecture is presented in 

\reffig{modulearch}.

A \emph{web client} requests a \ac{URL} from a \emph{web server} over 

\ac{HTTP}.

The web server processes the request by fetching static elements from its 

local file system and communicating with \emph{web modules} to dynamically 

generate other elements.

The elements are sent back across the network to the web client.

The web server communicates with web modules over a \emph{module protocol}, 

which dictates a means of passing requests and receiving responses.

There are several common module protocols.

In the \ac{CGI}, the web server executes processes to service dynamic 

\acp{URL}.

Request details are placed in environment variables and sent on the standard 

input channels of processes, responses are read from the standard output 

channels of processes and transmitted back to web clients.

The chief disadvantage of \ac{CGI} is that it creates a new process for 

every request.

Fast \ac{CGI} web modules, on the other hand, run persistently in a loop.

They receive and respond to web server requests over a duplex socket.

The Fast \ac{CGI} protocol is quite complicated.

There are, however, alternatives like \ac{SCGI} that are easier for web 

modules to support.

This is important when programming in \ac{SML} because both the number of 

developers and available libraries are small.

An \ac{SCGI} web module listens on a socket for requests from a web server.

Requests are sent as stream of bytes.

The first part of the request is a null-delimited sequence of name and value 

pairs.

The second part is unparsed text sent from the web client.

The web module responds by sending text, usually \ac{HTTP} headers followed 

by \ac{HTML} data, back over the socket.

The whole protocol can be described in two 

pages.\footnote{\url{http://python.ca/scgi/protocol.txt}}

Both the Apache and Lighttpd web servers support the \ac{SCGI} protocol.

Lighttpd was chosen because it seemed to be small, fast, and easy to 

configure.

Two settings are required to connect lighttpd to an \ac{SCGI} web module: 

\begin{verbatim}

server.modules = ( "mod_scgi" )

scgi.server = ("/isabelle" => ((

		  "host" => "127.0.0.1",

		  "port" => 64000,

		  "check-local" => "disable")))

\end{verbatim}

In this example, the \texttt{scgi.server} entry directs the web server to 

pass all \acp{URL} beginning with \texttt{/isabelle} to the web module 

listening on port \texttt{64000}.

\subsection{Implementation in \acs{SML}}\label{sec:oneproc:impl}

\begin{table}

\begin{tabular}{lp{.70\textwidth}}

\textbf{Module}	     &	\textbf{Description}\\\hline

Mime		     &	Rudimentary support for mime types.\\

HttpStatus	     &	\ac{HTTP} header status codes.\\

HttpUtil	     &	Produce \ac{HTTP} headers and parse query strings.\\

Xhtml		     &	Rudimentary support for generating \ac{HTML}.\\

SocketUtil	     &	Routines from The Standard ML Basis Library

			book.\footnote{Chapter 10, Gansner and Reppy, 

			Cambridge University Press.}\\

\textbf{ScgiReq}     &	Parse \ac{SCGI} requests.\\

\textbf{ScgiServer}  &	\ac{SCGI} server event loop and dispatch.\\

\textbf{FindTheorems}&	\ac{HTML} interface to find\_theorems.

\end{tabular}

\caption{Web module implementation\label{tab:moduleimpl}}

\end{table}

The find\_theorems web module is implemented in \ac{SML}.

It uses elements of the Pure library in Isabelle.

The program comprises the nine modules shown in \reftab{moduleimpl}.

The three most important ones are shown in bold: ScgiReq, ScgiServer, and 

FindTheorems.

ScgiReq implements the client-side of the \ac{SCGI} protocol.

It maps a binary input stream into a request data type.

ScgiServer is a generic, multi-threaded \ac{SCGI} request dispatcher.

It accepts \ac{SCGI} requests on a designated socket, selects an appropriate 

handler from an internal list, and calls the handler in a new thread.

FindTheorems registers a handler with ScgiServer.

It parses \ac{SCGI}/\ac{HTTP} requests, calls the Isabelle find\_theorems 

function, and returns the results as \ac{HTML}.

The \ac{HTML} generation of individual theorems is handled by the \ac{HTML} 

print mode of Isabelle, but the form fields and page structure were manually 

implemented.

The server is started by calling \texttt{ScgiServer.server}.

Scripts have been created to automate this process.

\subsection{Handling symbols}\label{sec:unicode}

Isabelle theorems are usually written in mathematical notation.

Internally, however, Isabelle only manipulates \acs{ASCII} strings.

Symbols are encoded by strings that begin with a backslash and contain a 

symbol name between angle braces, for example, the symbol~$\longrightarrow$ 

becomes~\verb+\<longrightarrow>+.

The existing Thy/Html module in the Isabelle Pure theory converts many of 

these symbols to \ac{HTML} entities.

Custom routines are required to convert the missing symbols to \ac{HTML} 

\emph{numeric character references}, which are the Unicode codepoints of 

symbols printed in decimal between \verb+&#+ and \verb+;+.

Further, other routines were required for converting \acs{UTF-8} encoded 

strings sent from web browsers into Isabelle's symbol encoding.

Isabelle is distributed with a text file that maps Isabelle symbols to 

Unicode codepoints.

A module was written to parse this file into symbol tables that map back and 

forth between Isabelle symbols and Unicode codepoints, and also between 

Isabelle \acs{ASCII} abbreviations (like \verb+-->+ for $\longrightarrow$) 

and Unicode codepoints.

The conversion from Isabelle symbols to \ac{HTML} numeric character 

references is handled by a new printing mode, which is based in large part 

on the existing \ac{HTML} printing mode.

The new mode is used in combination with the existing \texttt{xsymbol} mode, 

to ensure that Isabelle symbols are used instead of \acs{ASCII} 

abbreviations.

The conversion from \acs{UTF-8} is handled by a custom routine.

Additionally, there is a JavaScript routine that converts from Isabelle 

symbol encodings to \acs{UTF-8}, so that users can conveniently view 

manually-entered or pasted mathematical characters in the web browser 

interface.

\section{Abbreviations}\label{sec:abbr}

\begin{acronym}[SML/NJ] % longest acronym here

    \acro{ASCII}{American Standard Code for Information Interchange}

    \acro{CGI}{Common Gateway Interface}

    \acro{CML}{Concurrent ML}

    \acro{CMU}{Carnegie Mellon University}

    \acro{HTML}{Hyper Text Markup Language}

    \acro{HTTP}{Hyper Text Transfer Protocol}

    \acro{ML}{Meta Language}

    \acro{SCGI}{Simple CGI}

    \acro{SML}{Standard ML}

    \acro{SML/NJ}{Standard ML of New Jersey}

    \acro{URL}{Universal Resource Locator}

    \acro{UTF-8}{8-bit Unicode Transformation Format}

    \acro{WWW}{World Wide Web}

\end{acronym}

\end{document}