--- a/src/Doc/System/Presentation.thy Sun Feb 02 14:16:26 2025 +0100
+++ b/src/Doc/System/Presentation.thy Sun Feb 02 16:04:09 2025 +0100
@@ -208,14 +208,13 @@
text \<open>
The session information of a regular @{tool_ref build} can also be used to
generate a search index for full-text search over formal theory content. To
- that end, the \<^verbatim>\<open>Find_Facts\<close> module integrates Apache Solr\<^footnote>\<open>\<^url>\<open>https://solr.apache.org/\<close>\<close>,
+ that end, the \<^verbatim>\<open>Find_Facts\<close> module integrates Apache Solr\<^footnote>\<open>\<^url>\<open>https://solr.apache.org\<close>\<close>,
a full-text search engine, that can run embedded in a JVM process. Solr is
bundled as a separate Isabelle component, and its run-time dependencies
(as specified in @{setting SOLR_JARS}) need to be added separately to the
classpath of a regular Isabelle/Scala process.
\<^medskip>
-
A search index can be created using the @{tool_def find_facts_index} tool,
which has options similar to the regular @{tool_ref build}. User data such
as search indexes is stored in @{setting FIND_FACTS_HOME_USER}. The name of
@@ -242,19 +241,19 @@
\<close>}
This Isabelle/Scala HTTP server provides the both the front-end
- (implemented in the Elm\<^footnote>\<open>\<^url>\<open>https://elm-lang.org/\<close>\<close> language) and REST
+ (implemented in the Elm\<^footnote>\<open>\<^url>\<open>https://elm-lang.org\<close>\<close> language) and REST
endpoints for search queries with JSON data.
- Options \<^verbatim>\<open>-o\<close>, \<open>-v\<close> have the same meaning as usual.
+ Options \<^verbatim>\<open>-o\<close> and \<^verbatim>\<open>-v\<close> have the same meaning as in @{tool build}.
Option \<^verbatim>\<open>-d\<close> re-compiles the front-end in \<^path>\<open>$FIND_FACTS_HOME_USER/web\<close>
on page reload (when sources are changed).
- Option \<^verbatim>\<open>-p\<close> specifies an explicit TCP port for the server socket
- (assigned by the operating system per default). For public-facing servers,
- a common scheme is \<^verbatim>\<open>-p 8080\<close> that is access-restricted via firewall rules,
- with a reverse proxy in system space (that also handles SSL) on ports 80 and
- 443.
+ Option \<^verbatim>\<open>-p\<close> specifies an explicit TCP port for the server socket (assigned
+ by the operating system per default). For public-facing servers, a common
+ scheme is \<^verbatim>\<open>-p 8080\<close> that is access-restricted via firewall rules, with a
+ reverse proxy\<^footnote>\<open>E.g. via Caddy \<^url>\<open>https://caddyserver.com/docs\<close>\<close> in system
+ space (that also handles SSL) on ports 80 and 443.
\<close>
end
--- a/src/Doc/System/Sessions.thy Sun Feb 02 14:16:26 2025 +0100
+++ b/src/Doc/System/Sessions.thy Sun Feb 02 16:04:09 2025 +0100
@@ -203,7 +203,7 @@
although it uses relatively complex quasi-hierarchic naming conventions like
\<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to use unqualified
names that are relatively long and descriptive, as in the Archive of Formal
- Proofs (\<^url>\<open>https://isa-afp.org\<close>), for example.
+ Proofs (AFP, \<^url>\<open>https://isa-afp.org\<close>), for example.
\<close>
@@ -1104,6 +1104,7 @@
service. The system option @{system_option build_manager_ci_jobs} controls
which jobs are executed by the \<^verbatim>\<open>Build_Manager\<close>.
+ \<^medskip>
The command-line usage to start the server is:
@{verbatim [display]
\<open>Usage: isabelle build_manager [OPTIONS]
@@ -1119,9 +1120,11 @@
Run Isabelle build manager.
\<close>}
- \<^medskip> Options \<^verbatim>\<open>-o\<close> and \<^verbatim>\<open>-p\<close> are the same as in other server applications.
+ \<^medskip> Option \<^verbatim>\<open>-o\<close> has the same meaning as for @{tool build}.
- \<^medskip> Option \<^verbatim>\<open>-A\<close> refers to the AFP (must be a Mercurial clone)
+ \<^medskip> Option \<^verbatim>\<open>-p\<close> has the same meaning as for @{tool server}.
+
+ \<^medskip> Option \<^verbatim>\<open>-A\<close> refers to the AFP (must be a Mercurial clone).
\<^medskip> Option \<^verbatim>\<open>-D\<close> extra Isabelle components in a Mercurial repository clone to
be considered by the poller and CI jobs.
--- a/src/Doc/System/document/root.tex Sun Feb 02 14:16:26 2025 +0100
+++ b/src/Doc/System/document/root.tex Sun Feb 02 16:04:09 2025 +0100
@@ -19,7 +19,9 @@
\title{\includegraphics[scale=0.5]{isabelle_logo} \\[4ex] The Isabelle System Manual}
-\author{\emph{Makarius Wenzel}}
+\author{\emph{Makarius Wenzel} \\[3ex]
+ With Contributions by
+ Fabian Huch}
\makeindex