From 74a80de4566a868734a2d1471ac723e03844a969 Mon Sep 17 00:00:00 2001
From: loutr <loutr@crans.org>
Date: Sun, 4 Dec 2022 19:19:31 +0100
Subject: [PATCH] =?UTF-8?q?Resolve=20"Preparations=20for=20the=20first=20r?=
=?UTF-8?q?elease"=20=E2=9C=A8=EF=B8=8F=20Closes=20#48=20=F0=9F=90=94?=
=?UTF-8?q?=EF=B8=8F=F0=9F=91=8D=EF=B8=8F=20Approved-by:=20aalbert=20<augu?=
=?UTF-8?q?stin.albert@bleu-azure.fr>=20Approved-by:=20v-lafeychine=20<vin?=
=?UTF-8?q?cent.lafeychine@proton.me>?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
🦀ï¸ðŸ°ðŸ¦€ï¸ðŸ°ðŸ¦€ï¸ðŸ°
* chore: change branch name mentions to main
* feat(docs): add user manual
* fix(rustyline): autocompletion format: bold -> grey
* doc(all): add Proost logo
* doc(rustyline_helper): minor URL adjustments
* chore(README): update
* feat(README): add Proost logo
* feat(docs): add Proost logo in specification (LFS test in disguise)
---
README.md | 58 ++++--
docs/manual.pdf | 3 +
docs/manual.tex | 181 ++++++++++++++++++
docs/media/logo.png | 3 +
.../screenshot_toplevel.png} | 0
docs/specs.pdf | 4 +-
docs/specs.tex | 155 ++++++++-------
kernel/src/lib.rs | 2 +
parser/src/lib.rs | 2 +
proost/src/main.rs | 1 +
proost/src/rustyline_helper.rs | 19 +-
11 files changed, 336 insertions(+), 92 deletions(-)
create mode 100644 docs/manual.pdf
create mode 100644 docs/manual.tex
create mode 100644 docs/media/logo.png
rename docs/{proost.png => media/screenshot_toplevel.png} (100%)
diff --git a/README.md b/README.md
index 139aa4f9..34ce159e 100644
--- a/README.md
+++ b/README.md
@@ -1,27 +1,53 @@
-# Proost
+<p align="center">
+ <img src="https://gitlab.crans.org/loutr/proost/-/raw/main/docs/media/logo.png" width="25%"/>
+</p>
+# Proost
A simple proof assistant written in Rust.
-The specification of the project may be found [here](docs/specs.pdf).
-
-The documentation, generated with `rust-doc` may be found [here](doc/proost/).
-
-### Usage
-Please see the specification for insights on how to use `proost` and `tilleul`.
+The specification of the project may be found [here](docs/specs.pdf), and the
+user manual [here](docs/manual.pdf). The API documentation can be found by
+clicking on the corresponding badge below the project name.
-### Build and install
-With `nix` installed, simply type `nix run git+ssh://git@gitlab.crans.org/loutr/proost.git?ref=main` to launch `proost`. Alternatively, clone this git repository and type `nix build` to perform a build and have it in the nix store. One can also type `nix profile install` in the repo to install `proost` to one's profile and use it everywhere!
-
-### Development environment
-With `nix` installed, simply type `nix develop`. This provides an environment with all the necessary tools, including `clippy` and `rustfmt`. There, it is possible to run the usual `cargo build` and so on.
-
-Please consider the syntax `nix develop --profile <a-file-of-your-choosing>`, which will prevent the garbage collection of the development dependencies.
+## Build and install
+To install proost with `nix` installed, simply type:
+```sh
+nix profile install git+ssh://git@gitlab.crans.org/loutr/proost.git?ref=main
+```
+A toplevel instance can then be launched with `proost`. Alternatively, replace
+`profile install` with `run` to give the program a go without installing it.
+
+Without `nix` installed, `git clone` the project and, with Rust and
+[`cargo`](https://doc.rust-lang.org/stable/cargo/) properly setup to an
+appropriate version (either through your package manager or
+[`rustup`](https://rustup.rs/)), do `cargo run --release`.
+
+## Development environment (with `nix`)
+Type `nix develop`. This provides an environment with all the necessary tools,
+including `cargo` (with `clippy`, `rustfmt`) and `rust-analyzer`. Then, use your
+regular `cargo` commands.
+
+Please consider the syntax `nix develop --profile <a-file-of-your-choosing>`,
+which will prevent the garbage collection of the development dependencies as
+long as the given file lives.
+
+## Crates
+The project is organised as such:
+- the crate `kernel` provides an interface for building and manipulating terms,
+ as well as type inference and type checking functions;
+- the crate `parser` provides parsing functions which return `Builder` objects,
+ which can be seen as template that can be provided to the kernel to get a
+ real, well-formed term to perform computations upon;
+- the crate `proost` provides a toplevel interface for end-users that can be
+ used to manipulate terms and query the kernel. It provides partial
+ auto-completion, some color highlighting and other readline-like features;
+- the crate `tilleul`, which is still in preparation, which will implement the
+ Language Server Protocol.
-### Crates dependencies
```mermaid
graph TD;
kernel-->tilleul;
- kernel-->parser;
+ kernel-.->parser;
parser-->tilleul;
parser-->proost;
kernel-->proost;
diff --git a/docs/manual.pdf b/docs/manual.pdf
new file mode 100644
index 00000000..27740b96
--- /dev/null
+++ b/docs/manual.pdf
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:59b0c8b367d4f2b0fd154ab5d2dd8f94ac16a6e7e334f304e7006dbb0ed3de4d
+size 374850
diff --git a/docs/manual.tex b/docs/manual.tex
new file mode 100644
index 00000000..0ddaa135
--- /dev/null
+++ b/docs/manual.tex
@@ -0,0 +1,181 @@
+\documentclass[twocolumn]{article}
+\usepackage[british]{babel}
+\usepackage{textcase}% provides \MakeTextUppercase (does not impact math mode)
+\usepackage{amssymb, amsmath, amsthm, mathrsfs}
+\usepackage{fancyhdr}
+\usepackage{listings}
+\usepackage{bussproofs} % proof tree
+\usepackage[dvipsnames]{xcolor}
+\usepackage{graphicx}
+\RequirePackage[a4paper, left=2cm, right=2cm, bottom=3cm, top=2.3cm, headsep=100pt]{geometry}
+\RequirePackage[small]{titlesec} % Taille des sections réduite
+\RequirePackage[pdfborderstyle={/S/U/W 0}]{hyperref} % Le paramètre retire les bordures autour des hyperliens
+
+\author{
+ Arthur \textsc{Adjedj}\\
+ Vincent \textsc{Lafeychine} \and
+ Augustin \textsc{Albert} \\
+ Lucas \textsc{Tabary-Maujean}
+}
+
+\title{
+ \includegraphics[height=2.5cm]{media/logo}
+
+ \textbf{Proost 0.1.0} \\
+ User manual
+ \\[1\baselineskip]\normalsize ENS Paris-Saclay
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Listings %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\definecolor{gray}{rgb}{0.5,0.5,0.5}
+\definecolor{paleblue}{rgb}{0.7,0.7,1}
+\definecolor{darkgray}{rgb}{0.1,0.1,0.1}
+\definecolor{dark}{rgb}{0,0,0}
+\definecolor{forestgreen}{rgb}{0,0.3,0}
+\definecolor{darkred}{rgb}{0.5,0,0}
+
+\lstdefinestyle{default}{
+ frame=tb,
+ basicstyle=\ttfamily,
+ numbers=left,
+ numbersep=5pt,
+ xleftmargin=1.5em,
+ framexleftmargin=1em,
+ numberstyle=\footnotesize\ttfamily\color{paleblue},
+ keywordstyle={\bfseries\itshape\color{dark}},
+ commentstyle=\color{gray},
+ texcl, % Back to TeX styling within *inline* comments
+ escapechar=`, % escape character for block comments
+ %escapebegin=\lst@commentstyle,
+ breaklines=true,
+ breakatwhitespace=true
+}
+\lstdefinestyle{proost}{
+ alsoletter={//,.,:,=},
+ style=default,
+ numberstyle=\scriptsize\ttfamily\color{paleblue},
+ comment=[l]{//},
+ keywords={fun, if},
+ keywordstyle=\color{forestgreen},
+ keywords=[2]{Prop, Type},
+ keywordstyle=[2]\color{blue},
+ keywords=[3]{def, check, eval, search, import},
+ keywordstyle=[3]\color{darkred},
+}
+\lstnewenvironment{proost}[1][]{\lstset{style=proost, #1}}{}
+
+\lstset{style=proost}
+\lstMakeShortInline[columns=flexible]¤
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% headings %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\pagestyle{fancy}
+\renewcommand{\headrulewidth}{0pt}
+\renewcommand{\footrulewidth}{0pt}
+
+\fancyhead{}
+\fancyfoot[L]{\small{\reflectbox{\copyright} \the\year{}}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% bussproofs settings %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% documentation at https://mirror.ibcp.fr/pub/CTAN/macros/latex/contrib/bussproofs/BussGuide2.pdf
+\EnableBpAbbreviations
+% Overriding default label style
+\def\RL#1{\RightLabel{\footnotesize\bfseries{#1}}}
+\def\LL#1{\LeftLabel{\footnotesize\bfseries{#1}}}
+
+% boxed proofs, used to align multiple proofs on a single line
+\newenvironment{bprooftree}
+ {\leavevmode\hbox\bgroup}
+ {\DisplayProof\egroup}
+
+\newcommand{\textr}[1]{{\footnotesize\textbf{\MakeTextUppercase{#1}}}}
+% Fixes alignment issues but not without some consistency issues
+\def\RL#1{\RightLabel{\makebox[0pt][l]{\textr{#1}}}}
+\def\LL#1{\LeftLabel{\makebox[0pt][r]{\textr{#1}}}}
+% consistent label (with width)
+\def\cRL#1{\RightLabel{\textr{#1}}}
+\def\cLL#1{\LeftLabel{\textr{#1}}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Divers %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\setlength{\columnsep}{20pt} % 10 pt par défaut
+
+\newcommand{\members}[1]{\texorpdfstring{\hfill\scriptsize #1}{}}
+
+\newcommand{\etun}{{\color{Green} ($\star$)} }
+\newcommand{\etde}{{\color{Orange} ($\star\star$)} }
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+\begin{document}
+\maketitle
+\thispagestyle{fancy}
+
+\section{Introduction}
+This program provides the user a set of tools to work with \(\lambda\)-terms as
+described in the Calculus of Construction. Through the Curry-Howard
+correspondence; users may associate a property or theorem they are willing to
+prove to a type which can be expressed in CoC. Proving it then corresponds to
+constructing a term of that type.
+
+Release 0.1.0 of the project includes a toplevel interface also called
+\texttt{proost}, which is the main way users can interact with this piece of
+software. For a use directly through the crate APIs, please refer to their
+respective documentations.
+
+\section{Toplevel session}
+In the toplevel, users are greeted with a prompt. There, they may enter the
+following commands:
+\begin{itemize}
+ \item ¤import file1 file2¤ typechecks
+ and loads the file in the current environment;
+ \item ¤search v¤ looks for the definition of variable ¤v¤;
+ \item ¤def a := t¤
+ defines an alias ¤a¤ that can be used in any following command;
+ \item ¤def a: ty := t¤ defines an alias ¤a¤ that is checked to
+ be of type ¤ty¤;
+ \item ¤check u: t¤ verifies ¤u¤ has type ¤t¤;
+ \item ¤check u¤ provides the type of ¤u¤;
+ \item ¤eval u¤ provides the definition of ¤u¤.
+\end{itemize}
+
+If the command succeeds, the toplevel returns a green check mark, with an
+associated result if there is any. Otherwise, a red cross indicates an error
+occurred, next to some details about it. The command is discarded and the user
+may enter another command.
+
+The toplevel provides to a certain extent history browsing, either \emph{via}
+the up and down arrow keys or some autocompletion from previous commands.
+
+\section{Language}
+This release includes no standard library, which means users have to build their
+theories from scratch. Besides, this version includes no notion of axioms, which
+means terms have to be built from encodings within CoC.
+
+Language syntax is as such:
+\begin{itemize}
+ \item Functions (\(\lambda\)-abstractions) are defined with the keyword ¤fun¤:
+ ¤fun x: A => u¤, ¤fun x y: A => u¤ (both ¤x¤ and ¤y¤ are of type ¤A¤),
+ ¤fun x: A, y: B => u¤ (multiple arguments, where ¤B¤ may depend on ¤x¤);
+
+ \item Dependent function types (\(\Pi\)-types) are defined with a pair of parentheses
+ before an arrow, as in: ¤(x: A) -> B¤, ¤(x y: A) -> B¤ or
+ ¤(x: A, y: B) -> C¤ (where the distinctions are similar to the previous
+ item. Additionally, there is some usual syntactic sugar when the output
+ type does not mention the input argument, which corresponds to usual
+ function types: ¤A -> B¤, ¤A -> B -> C¤ (right-associativity);
+
+ \item Function application of two terms ¤u¤ and ¤v¤ is simply written ¤u v¤,
+ and is left-associative when there are multiple arguments;
+
+ \item Variables are regular strings, which may only correspond to bound
+ variables or previously defined terms;
+
+ \item The type of propositions and higher-order types are written ¤Prop¤ and
+ ¤Type i¤, as usual.
+\end{itemize}
+
+This release includes a single example file \texttt{contraposition.mdln} which
+defines elementary propositional calculus operators and their constructors.
+\end{document}
diff --git a/docs/media/logo.png b/docs/media/logo.png
new file mode 100644
index 00000000..54c5d58e
--- /dev/null
+++ b/docs/media/logo.png
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:56b74451f3784b20119cd8ac31e48b9e2945031889302550f5ff5d8c1619a5d7
+size 408895
diff --git a/docs/proost.png b/docs/media/screenshot_toplevel.png
similarity index 100%
rename from docs/proost.png
rename to docs/media/screenshot_toplevel.png
diff --git a/docs/specs.pdf b/docs/specs.pdf
index 61b0e6b0..d83aea95 100644
--- a/docs/specs.pdf
+++ b/docs/specs.pdf
@@ -1,3 +1,3 @@
version https://git-lfs.github.com/spec/v1
-oid sha256:692eb24c1c4273336e2f6bffbd4d237fcf53f61b2adc269284443ee882c9f85f
-size 79075
+oid sha256:44d870d545b591bbc953ca1376d14ef3f4ae7ed3fc76712d23052a9390bd7db8
+size 421480
diff --git a/docs/specs.tex b/docs/specs.tex
index 4de5f420..3fc3371a 100644
--- a/docs/specs.tex
+++ b/docs/specs.tex
@@ -7,7 +7,7 @@
\usepackage{bussproofs} % proof tree
\usepackage[dvipsnames]{xcolor}
\usepackage{graphicx}
-\RequirePackage[a4paper, left=2cm, right=2cm, bottom=3cm, headsep=100pt]{geometry}
+\RequirePackage[a4paper, left=2cm, right=2cm, bottom=3cm, top=2.3cm, headsep=100pt]{geometry}
\RequirePackage[small]{titlesec} % Taille des sections réduite
\RequirePackage[pdfborderstyle={/S/U/W 0}]{hyperref} % Le paramètre retire les bordures autour des hyperliens
@@ -18,7 +18,10 @@
Lucas \textsc{Tabary-Maujean}
}
-\title{\textbf{Proost: specifications}\\
+\title{
+ \includegraphics[height=2.5cm]{media/logo}
+
+ \textbf{Proost: specifications}\\
\large A small proof assistant written in Rust
\\[1\baselineskip]\normalsize ENS Paris-Saclay
}
@@ -54,9 +57,9 @@
comment=[l]{//},
keywords={fun, if},
keywordstyle=\color{forestgreen},
- keywords={Prop, Type},
- keywordstyle=\color{darkred},
- keywords=[3]{def, check, eval, import},
+ keywords=[2]{Prop, Type},
+ keywordstyle=[2]\color{darkred},
+ keywords=[3]{def, check, eval, search, import},
keywordstyle=[3]\color{darkred},
}
\lstnewenvironment{proost}[1][]{\lstset{style=proost, #1}}{}
@@ -100,8 +103,8 @@
\newcommand{\members}[1]{\texorpdfstring{\hfill\scriptsize #1}{}}
-\newcommand{\etun}{({\color{Green} $\star$}) }
-\newcommand{\etde}{({\color{Orange} $\star\star$}) }
+\newcommand{\etun}{{\color{Green} ($\star$)} }
+\newcommand{\etde}{{\color{Orange} ($\star\star$)} }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -112,42 +115,50 @@
\emph{
This project is under development, and its specifications themselves are
subject to changes, should time be an issue or a general consensus be reached
- to change the purposes of the tool. An example of that is the syntax of
- the language, which is still largely unstable.
-}
+ to change the purposes of the tool. An example of that is the syntax of the
+ language, which is still largely unstable. }
-\section{General purpose and functions}
-This project aims at providing a small tool for typechecking expressions written in
-the language of the Calculus of Construction (CoC). This tool shall be
-both terminal and editor based through the \texttt{proost} program that provides both compiler and toplevel-like capacities and options and a LSP called \texttt{tilleul}.
-The file extension used by both programs is \texttt{.mdln}, which is short for \emph{madelaine}, the name of the language manipulated by users in these files.
+\section{General purpose and functions} This project aims at providing a small
+tool for typechecking expressions written in the language of the Calculus of
+Construction (CoC). This tool shall be both terminal and editor based through
+the \texttt{proost} program that provides both compiler and toplevel-like
+capacities and options and a LSP called \texttt{tilleul}. The file extension
+used by both programs is \texttt{.mdln}, which is short for \emph{madelaine},
+the name of the language manipulated by users in these files.
-\section{Project structure}
-Each category of the project is assigned some or all members of the group,
-meaning the designated members will \emph{mainly} make progress in the associated categories
-and review the corresponding advancements. Any member may regardless contribute to any part
-of the development of the tool.
+\section{Project structure} Each category of the project is assigned some or all
+members of the group, meaning the designated members will \emph{mainly} make
+progress in the associated categories and review the corresponding advancements.
+Any member may regardless contribute to any part of the development of the tool.
Some specific categories and items will be added a star \etun or two \etde to
indicate whether they are respectively late requirements (for the last release
-due in December)
-or extra requirements that will be considered only if there is enough time.
-
-\subsection{Language design \members{all members}}
-The \texttt{proost} tool is a simple proof assistant and does not provide any
-tactics. As new features arrive from extensions of the kernel type theory, the
-\emph{madelaine} language must provide convenient shorthands and notations. The syntax of commands is the following:
+due in December) or extra requirements that will be considered only if there is
+enough time.
+
+\subsection{Language design \members{all members}} The \texttt{proost} tool is a
+simple proof assistant and does not provide any tactics. As new features arrive
+from extensions of the kernel type theory, the \emph{madelaine} language must
+provide convenient shorthands and notations. The syntax of commands is the
+following:
\begin{itemize}
- \item \etun¤import relative_path_to_file¤ typecheck and load the the file in the current environment;
- \item ¤def a := t¤ defines an alias ¤a¤ that can be used in any following command;
- \item ¤def a : ty := t¤ defines an alias ¤a¤ that is checked to be of type ¤ty¤;
- \item ¤check u : t¤ verifies ¤u¤ has type ¤t¤;
+ \item \etun ¤import relative_path_to_file¤ typechecks
+ and loads the file in the current environment;
+ \item \etde ¤search t¤ searches ¤t¤ in all known terms, where ¤t¤ may contain
+ ¤_¤ joker identifiers (see section \ref{sec:unification});
+ \item ¤def a := t¤
+ defines an alias ¤a¤ that can be used in any following command;
+ \item ¤def a: ty := t¤ defines an alias ¤a¤ that is checked to
+ be of type ¤ty¤;
+ \item ¤check u: t¤ verifies ¤u¤ has type ¤t¤;
\item ¤check u¤ provides the type of ¤u¤;
\item ¤eval u¤ provides the definition of ¤u¤.
\end{itemize}
-Below is an overview of the syntax of the terms, both present and future. The syntax is strongly inspired by that of OCaml. Comments are defined using the keyword \texttt{//}.
+Below is an overview of the syntax of the terms, including hypothetical
+developments. The syntax is strongly inspired by that of OCaml. Comments are
+defined using the keyword \texttt{//}.
\vspace{1.2mm}
elementary type theory:
@@ -156,13 +167,14 @@ elementary type theory:
def Nat :=
(N: Type) -> (N -> N) -> N -> N
-def z := fun N:Type =>
- fun f:(N -> N), x:N => x
-check z : Nat
+def z := fun N: Type =>
+ fun f: (N -> N), x:N => x
+check z: Nat
def succ := fun n: Nat, N: Type =>
- fun f: (N -> N), x: N => f (n N f x)
-check succ : Nat -> Nat
+ fun f: (N -> N), x: N =>
+ f (n N f x)
+check succ: Nat -> Nat
\end{proost}
\etun universe polymorphism:
@@ -173,7 +185,7 @@ def foo.{i,j} : Type (max i j) + 1
\etde unification:
\begin{proost}
-def comm := \/ x,y, x + y = y + x
+def comm := \/x y, x + y = y + x
\end{proost}
\etde existential types:
@@ -182,26 +194,36 @@ def t := E n, n * n - n + 4 = 0
\end{proost}
-\subsection{Toplevel \members{AuA}}
-The \texttt{proost} command, when provided with no argument, is expected to behave like a toplevel, akin to \texttt{ocaml} or \texttt{coqtop}. There, user is greeted with a prompt and may enter commands. When provided with existing file paths, ¤proost¤ intends to typecheck them in
-order, that is, reading them as successive inputs in the toplevel. Further features for this \emph{might} include a more extended notion of ``modules'' where files may provides scopes.
-{
- \begin{center}
- \fbox{\includegraphics{proost.png}}
- \end{center}
-}
+\subsection{Toplevel \members{AuA}} The \texttt{proost} command, when provided
+with no argument, is expected to behave like a toplevel, akin to \texttt{ocaml}
+or \texttt{coqtop}. There, user is greeted with a prompt and may enter commands.
+When provided with existing file paths, ¤proost¤ intends to typecheck them in
+order, that is, reading them as successive inputs in the toplevel. Further
+features for this \emph{might} include a more extended notion of ``modules''
+where files may provides scopes.
+\begin{center}
+ \fbox{\includegraphics{media/screenshot_toplevel}}
+\end{center}
\subsection{\etun LSP \members{VL}}
-\texttt{tilleul} shall provide an implementation of the Language Server Protocol in order to provide linting and feedback during an editing session.
+\texttt{tilleul} shall provide an
+implementation of the Language Server Protocol in order to provide linting and
+feedback during an editing session.
\subsection{Parsing \members{AuA}}
-The parsing approach is straightforward and relies on external libraries. The parser is expected to keep adapting to changes made in the term definitions and unification capability. The parser is thoroughly tested to guarantee full coverage.
+The parsing approach is straightforward and
+relies on external libraries. The parser is expected to keep adapting to changes
+made in the term definitions and unification capability. The parser is
+thoroughly tested to guarantee full coverage.
\subsection{Kernel \members{all members}}
-The kernel manipulates \(\lambda\)-terms in the Calculus of Construction and is expected to store and manage them with a relative level of efficiency. The type theory used to build the terms will be successively extended with:
+The kernel manipulates
+\(\lambda\)-terms in the Calculus of Construction and is expected to store and
+manage them with a relative level of efficiency. The type theory used to build
+the terms will be successively extended with:
\begin{itemize}
\item abstractions, \(\Pi\)-types, predicative universes with \(\mathsf{Prop}\);
\item \etun universe polymorphism;
@@ -212,8 +234,9 @@ The kernel manipulates \(\lambda\)-terms in the Calculus of Construction and is
\subsection{\etun Optimisation \members{ArA LTM}}
-Extra care must be put into designing an efficient memory management model for
-the kernel, along with satisfactory typing and reduction algorithms.
+Extra care must be put into
+designing an efficient memory management model for the kernel, along with
+satisfactory typing and reduction algorithms.
In particular, the first iteration of the program manipulates directly terms on
the heap, with no particular optimisation: every algorithm is applied soundly
@@ -221,24 +244,26 @@ but naively.
A first refactor of the memory model includes using a common memory location for
terms, ensuring invariant like unicity of a term in memory, providing laziness
-and storing results of the most expensive functions \emph{(memoizing)}.
-This model also provides stronger isolation properties, preventing several
-memory pools (\emph{arena} is the technical term used in the project) from
-interacting with one another.
+and storing results of the most expensive functions \emph{(memoizing)}. This
+model also provides stronger isolation properties, preventing several memory
+pools (\emph{arena} is the technical term used in the project) from interacting
+with one another.
-This can
-be further extended with other invariants like ensuring every term in memory is
-in weak head normal form.
+This can be further extended with other invariants like ensuring every term in
+memory is in weak head normal form.
-\subsection{\etde Unification}
-Early versions of the tool may require the user to explicit every type at play.
-Successive versions may gradually include unification tools (meta-variables)
-of better quality to assist the user and alleviate some of their typing-annotation
-burden.
+\subsection{\etde Unification}\label{sec:unification}
+Early versions of the tool may require the user
+to explicit every type at play. Successive versions may gradually include
+unification tools (meta-variables) of better quality to assist the user and
+alleviate some of their typing-annotation burden.
\subsection{Developpement tools \members{VL LTM}}
-Tests are mandatory in every part of the project. A tool originally developed by the Mozilla team was modified to allow for a more precise branch coverage of the project.
-The Nix framework is used to automatically build and package the application as well as generating a docker image and providing developers tools of the same version.
+Tests are mandatory in every
+part of the project. A tool originally developed by the Mozilla team was
+modified to allow for a more precise branch coverage of the project. The Nix
+framework is used to automatically build and package the application as well as
+generating a docker image and providing developers tools of the same version.
% TODO elaborate, maybe
\end{document}
diff --git a/kernel/src/lib.rs b/kernel/src/lib.rs
index 19c5a3ed..fae36aaa 100644
--- a/kernel/src/lib.rs
+++ b/kernel/src/lib.rs
@@ -1,3 +1,5 @@
+#![doc(html_logo_url = "https://gitlab.crans.org/loutr/proost/-/raw/main/docs/media/logo.png")]
+
//! A kernel for the calculus of constructions.
//!
//! Terms can be built with functions from the [`term`] module. This module also provides essential
diff --git a/parser/src/lib.rs b/parser/src/lib.rs
index cc0a8d19..95486f02 100644
--- a/parser/src/lib.rs
+++ b/parser/src/lib.rs
@@ -1,3 +1,5 @@
+#![doc(html_logo_url = "https://gitlab.crans.org/loutr/proost/-/raw/main/docs/media/logo.png")]
+
//! Fast parser for λ-terms and commands using pest.
//! Provides functions to parse files and single commands.
diff --git a/proost/src/main.rs b/proost/src/main.rs
index 8c45a2dd..08d25afb 100644
--- a/proost/src/main.rs
+++ b/proost/src/main.rs
@@ -1,3 +1,4 @@
+#![doc(html_logo_url = "https://gitlab.crans.org/loutr/proost/-/raw/main/docs/media/logo.png")]
#![feature(let_chains)]
mod error;
diff --git a/proost/src/rustyline_helper.rs b/proost/src/rustyline_helper.rs
index a4fc0c7b..637ac220 100644
--- a/proost/src/rustyline_helper.rs
+++ b/proost/src/rustyline_helper.rs
@@ -12,8 +12,8 @@ use rustyline_derive::{Helper, Hinter};
const KEYWORDS: [&str; 5] = ["check", "def", "eval", "import", "search"];
/// An Helper for a RustyLine Editor that implements:
-/// - a standard hinter
-/// - customs validator, completer and highlighter
+/// - a standard hinter;
+/// - custom validator, completer and highlighter.
#[derive(Helper, Hinter)]
pub struct RustyLineHelper {
color: bool,
@@ -43,7 +43,7 @@ impl ConditionalEventHandler for TabEventHandler {
}
}
-/// A variation of FilenameCompleter:
+/// A variation of [FilenameCompleter](https://docs.rs/rustyline/latest/rustyline/completion/struct.FilenameCompleter.html):
/// file completion is available only after having typed import
impl Completer for RustyLineHelper {
type Candidate = Pair;
@@ -53,8 +53,9 @@ impl Completer for RustyLineHelper {
}
}
-/// A variation of MatchingBracketValidator:
-/// no validation occurs when entering the import command
+/// A variation of [MatchingBracketValidator](https://docs.rs/rustyline/latest/rustyline/validate/struct.MatchingBracketValidator.html).
+///
+/// No validation occurs when entering the import command
impl Validator for RustyLineHelper {
fn validate(&self, ctx: &mut ValidationContext) -> Result<ValidationResult> {
if ctx.input().starts_with("import") {
@@ -97,15 +98,15 @@ fn validate_brackets(input: &str) -> Option<ValidationResult> {
if stack.is_empty() { None } else { Some(ValidationResult::Incomplete) }
}
-/// A variation of MatchingBrackerHighlighter:
-/// no check occurs before cursor
-/// see: https://docs.rs/rustyline/10.0.0/rustyline/highlight/struct.MatchingBracketHighlighter.html
+/// A variation of [MatchingBracketHighlighter](https://docs.rs/rustyline/latest/rustyline/highlight/struct.MatchingBracketHighlighter.html).
+///
+/// No check occurs before cursor
impl Highlighter for RustyLineHelper {
fn highlight_hint<'h>(&self, hint: &'h str) -> Cow<'h, str> {
if !self.color {
return Owned(hint.to_owned());
}
- Owned(format!("{}", hint.bold()))
+ Owned(format!("{}", hint.bright_black()))
}
fn highlight_char(&self, _line: &str, _pos: usize) -> bool {
--
GitLab