Compare revisions

loutr · loutr · loutr · loutr · loutr · loutr
--- a/README.md
+++ b/README.md
-# 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 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
-The documentation, generated with `rust-doc` may be found [here](doc/proost/).
+clicking on the corresponding badge below the project name.
-### Usage 
-Please see the specification for insights on how to use `proost` and `tilleul`.
-### Build and install
+## 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!
+To install proost with `nix` installed, simply type:
+```sh
-### Development environment
+nix profile install git+ssh://git@gitlab.crans.org/loutr/proost.git?ref=main
-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.
+```
+A toplevel instance can then be launched with `proost`. Alternatively, replace
-Please consider the syntax `nix develop --profile <a-file-of-your-choosing>`, which will prevent the garbage collection of the development dependencies.
+`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;

--- a/docs/manual.pdf
+++ b/docs/manual.pdf
--- a/docs/manual.tex
+++ b/docs/manual.tex
+\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}
--- a/docs/media/logo.png
+++ b/docs/media/logo.png
--- a/docs/proost.png
+++ b/docs/proost.png
--- a/docs/specs.pdf
+++ b/docs/specs.pdf
--- 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},
+		keywords=[2]{Prop, Type},
-    keywordstyle=\color{darkred},
+		keywordstyle=[2]\color{darkred},
-    keywords=[3]{def, check, eval, import},
+    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{\etun}{{\color{Green} ($\star$)} }
-\newcommand{\etde}{({\color{Orange} $\star\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
+  to change the purposes of the tool. An example of that is the syntax of the
-  the language, which is still largely unstable.
+  language, which is still largely unstable. }
-}
-\section{General purpose and functions}
+\section{General purpose and functions} This project aims at providing a small
-This project aims at providing a small tool for typechecking expressions written in
+tool for typechecking expressions written in the language of the Calculus of
-the language of the Calculus of Construction (CoC). This tool shall be
+Construction (CoC). This tool shall be both terminal and editor based through
-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 \texttt{proost} program that provides both compiler and toplevel-like
-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.
+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}
+\section{Project structure} Each category of the project is assigned some or all
-Each category of the project is assigned some or all members of the group,
+members of the group, meaning the designated members will \emph{mainly} make
-meaning the designated members will \emph{mainly} make progress in the associated categories
+progress in the associated categories and review the corresponding advancements.
-and review the corresponding advancements. Any member may regardless contribute to any part
+Any member may regardless contribute to any part of the development of the tool.
-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)
+due in December) or extra requirements that will be considered only if there is
-or extra requirements that will be considered only if there is enough time.
+enough time.
-\subsection{Language design \members{all members}}
+\subsection{Language design \members{all members}} The \texttt{proost} tool is a
-The \texttt{proost} tool is a simple proof assistant and does not provide any
+simple proof assistant and does not provide any tactics. As new features arrive
-tactics. As new features arrive from extensions of the kernel type theory, the
+from extensions of the kernel type theory, the \emph{madelaine} language must
-\emph{madelaine} language must provide convenient shorthands and notations. The syntax of commands is the following:
+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 \etun ¤import relative_path_to_file¤ typechecks
-  \item ¤def a := t¤ defines an alias ¤a¤ that can be used in any following command;
+		and loads the file in the current environment;
-  \item ¤def a : ty := t¤ defines an alias ¤a¤ that is checked to be of type ¤ty¤;
+	\item \etde ¤search t¤ searches ¤t¤ in all known terms, where ¤t¤ may contain
-  \item ¤check u : t¤ verifies ¤u¤ has type ¤t¤;
+		¤_¤ 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 =>
+def z := fun N: Type =>
-  fun f:(N -> N), x:N => x
+  fun f: (N -> N), x:N => x
-check z : Nat
+check z: Nat
 def succ := fun n: Nat, N: Type =>
-  fun f: (N -> N), x: N => f (n N f x)
+  fun f: (N -> N), x: N =>
-check succ : Nat -> Nat
+    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}}
+\subsection{Toplevel  \members{AuA}} The \texttt{proost} command, when provided
-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
+with no argument, is expected to behave like a toplevel, akin to \texttt{ocaml}
-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.
+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
-  \begin{center}
+order, that is, reading them as successive inputs in the toplevel. Further
-    \fbox{\includegraphics{proost.png}}
+features for this \emph{might} include a more extended notion of ``modules''
-  \end{center}
+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
+Extra care must be put into
-the kernel, along with satisfactory typing and reduction algorithms.
+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)}.
+and storing results of the most expensive functions \emph{(memoizing)}. This
-This model also provides stronger isolation properties, preventing several
+model also provides stronger isolation properties, preventing several memory
-memory pools (\emph{arena} is the technical term used in the project) from
+pools (\emph{arena} is the technical term used in the project) from interacting
-interacting with one another.
+with one another.
-This can
+This can be further extended with other invariants like ensuring every term in
-be further extended with other invariants like ensuring every term in memory is
+memory is in weak head normal form.
-in weak head normal form.
-\subsection{\etde Unification}
+\subsection{\etde Unification}\label{sec:unification}
-Early versions of the tool may require the user to explicit every type at play.
+Early versions of the tool may require the user
-Successive versions may gradually include unification tools (meta-variables)
+to explicit every type at play. Successive versions may gradually include
-of better quality to assist the user and alleviate some of their typing-annotation
+unification tools (meta-variables) of better quality to assist the user and
-burden.
+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.
+Tests are mandatory in every
-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.
+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}
--- a/kernel/src/lib.rs
+++ b/kernel/src/lib.rs
+#![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

--- a/parser/src/lib.rs
+++ b/parser/src/lib.rs
+#![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.

--- a/proost/src/main.rs
+++ b/proost/src/main.rs
+#![doc(html_logo_url = "https://gitlab.crans.org/loutr/proost/-/raw/main/docs/media/logo.png")]
 #![feature(let_chains)]
 mod error;

--- 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
+/// - a standard hinter;
-/// - customs validator, completer and highlighter
+/// - 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:
+/// A variation of [MatchingBracketValidator](https://docs.rs/rustyline/latest/rustyline/validate/struct.MatchingBracketValidator.html).
-/// no validation occurs when entering the import command
+///
+/// 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:
+/// A variation of [MatchingBracketHighlighter](https://docs.rs/rustyline/latest/rustyline/highlight/struct.MatchingBracketHighlighter.html).
-/// no check occurs before cursor
+///
-/// see: https://docs.rs/rustyline/10.0.0/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 {
No results found