From 9faa7fc5dbb8c8e975e7651723adc6aa84685f94 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andreas=20Sch=C3=A4rtl?= <andreas@schaertl.me> Date: Wed, 11 Nov 2020 08:42:57 +0100 Subject: [PATCH] report: review --- doc/report/applications-screenshots.tex | 5 +++-- doc/report/implementation.tex | 8 ++------ doc/report/legal.tex | 2 +- 3 files changed, 6 insertions(+), 9 deletions(-) diff --git a/doc/report/applications-screenshots.tex b/doc/report/applications-screenshots.tex index cd4fffd..7ec633b 100644 --- a/doc/report/applications-screenshots.tex +++ b/doc/report/applications-screenshots.tex @@ -27,6 +27,7 @@ \shadowbox{\includegraphics[width=\textwidth]{figs/explore4.png}} \caption{The original source code for a given node in our data set.\\}\label{fig:isrc} \end{subfigure} - \caption{Exploring the Isabelle~export~\cite{uloisabelle} with a rudimentary - web interface.}\label{fig:appss} + \caption{Exploring the Isabelle~export~\cite{uloisabelle} with a + rudimentary web interface. A demo of this tool is available at + \url{https://ulordf4j.mathhub.info}.}\label{fig:appss} \end{figure*} diff --git a/doc/report/implementation.tex b/doc/report/implementation.tex index f2b3f09..f930ecc 100644 --- a/doc/report/implementation.tex +++ b/doc/report/implementation.tex @@ -325,12 +325,8 @@ of this is easy to deploy using a single Docker Compose file. Our concrete implementation is useful in so far as that we can use it to experiment with ULO data sets. But development also provided -insight about (1)~which components this class of systems requires and -(2)~which problems need to be solved. One topic we discussed at large +insight about (1)~which components this class of system requires and +(2)~which problems need to be solved. One topic we discussed at length is version management. It is easy to dismiss this in these early stages of development, but no question it is something to keep in mind. - -With our stack ready for use, we will now continue with a look at some -interesting applications and queries built on top of this -infrastructure. diff --git a/doc/report/legal.tex b/doc/report/legal.tex index 521d801..ad5680e 100644 --- a/doc/report/legal.tex +++ b/doc/report/legal.tex @@ -4,7 +4,7 @@ Quellen angefertigt habe und dass die Arbeit in gleicher oder ähnlicher Form noch keiner anderen Prüfungsbehörde vorgelegen hat und von dieser als Teil einer Prüfungsleistung angenommen - wurde.Alle Ausführungen, die wörtlich oder sinngemäß übernommen + wurde. Alle Ausführungen, die wörtlich oder sinngemäß übernommen wurden, sind als solche gekennzeichnet. \end{otherlanguage*} -- GitLab