Switch to Furo theme

docs/sphinx_docs/Alt_ergo_native/02_types/02_01_builtin.md

@@ -5,14 +5,14 @@ Creation and manipulation of values having those types are covered in [built-in
 
 ## Boolean types
  * `bool`, the preferred type to represent propositional variables. Boolean constants are `true` and `false`.
- * `prop`, an historical type still supported in Alt-Ergo 2.3.0.  
-    The historical separation comes from Alt-Ergo origins in the Coq ecosystem: in Coq, `prop` is much richer than `bool`.  
-    In Alt-Ergo 2.3.0, `prop` and `bool` have been merged in order to simplify interactions with the [SMT-LIB ](http://smtlib.cs.uiowa.edu/) standard.  
+ * `prop`, an historical type still supported in Alt-Ergo 2.3.0.
+    The historical separation comes from Alt-Ergo origins in the Coq ecosystem: in Coq, `prop` is much richer than `bool`.
+    In Alt-Ergo 2.3.0, `prop` and `bool` have been merged in order to simplify interactions with the [SMT-LIB ](http://smtlib.cs.uiowa.edu/) standard.
     More information on the `bool`/`prop` conflict can be found in [this section](#the-bool-prop-conflict).
 
 ## Numeric types
  * `int` for (arbitrary large) integers.
- * `real` for reals. This type actually represents the smallest extension of the rationals which is algebraically closed and closed by exponentiation. Rationals with arbitrary precision are used under the hood. 
+ * `real` for reals. This type actually represents the smallest extension of the rationals which is algebraically closed and closed by exponentiation. Rationals with arbitrary precision are used under the hood.
 
 ## Unit type
  `unit` is Alt-Ergo native language's [unit type](https://en.wikipedia.org/wiki/Unit_type).
@@ -25,7 +25,7 @@ Creation and manipulation of values having those types are covered in [built-in
  Alt-Ergo's native language's type system supports prenex polymorphism. This allows efficient reasoning about generic data structure.
  Type variables can be created implicitly, and are implicitly universally quantified in all formulas. Any formula which requires a type can accept a type variable.
  Type variable may be used to parametrize datatypes, as we will see when we will create new types, or in the following example of `farray`.
- 
+
  Type variables are indicated by an apostrophe `'`. For example, `'a` is a type variable.
 
 ## Polymorphic functional arrays
@@ -34,7 +34,7 @@ Creation and manipulation of values having those types are covered in [built-in
  The `farray` is parametrized by two types: the type of their indexes (default is `int`) and the type of their values (no default).
  Array can be accessed using any index of valid type.
  Functional polymorphic arrays are persistent structures: they may be updated, but only for the scope of an expression.
- 
+
 
 # Built-in operators
 
@@ -57,7 +57,7 @@ For all those operators, `bool` and `prop` are fully interchangeable.
 Prior to Alt-Ergo 2.3.0, Alt-Ergo's native language handled differently boolean variables `bool` and propositional variables `prop`.
 The two keywords still exist in Alt-Ergo 2.3.0, but those two types have been made fully compatible: any function or operator taking a `bool` or a `prop` as an argument accepts both.
 
-The historical separation comes from Alt-Ergo origins in the Coq ecosystem: in Coq, `prop` is much richer than `bool`. 
+The historical separation comes from Alt-Ergo origins in the Coq ecosystem: in Coq, `prop` is much richer than `bool`.
 In Alt-Ergo 2.3.0, `prop` and `bool` have been merged in order to simplify interactions with the [SMT-LIB ](http://smtlib.cs.uiowa.edu/) standard.
 
 Note that `bool` can be used in more syntactic constructs than `prop`.
@@ -202,9 +202,9 @@ Note that bitvectors are indexed from right to left.
 
 | Operation                     | Notation                                                             | Type                          |
 |-------------------------------|----------------------------------------------------------------------|-------------------------------|
-| Explicit declaration          | `[|<x>|]` <br> where `<x>` is a string of `0` and `1` without spaces | `bitv[<len(x)>]`              |
+| Explicit declaration          | `[\|<x>\|]` where `<x>` is a string of `0` and `1` without spaces    | `bitv[<len(x)>]`              |
 | Concatenation                 | `x @ y`                                                              | bitv[n], bitv[m] -> bitv[n+m] |
-| Extraction of contiguous bits | `x^{p,q}` <br> where 0<=p<=q<len(x)                                  | `bitv[q-p+1]`                 |
+| Extraction of contiguous bits | `x^{p,q}` where `0<=p<=q<len(x)`                                     | `bitv[q-p+1]`                 |
 
 
 ### Examples
@@ -216,14 +216,14 @@ logic register: bitv[8]
 (** Explicit declaration *)
 axiom a: register = [|00101010|]
 
-(** Concatenation 
+(** Concatenation
         Both goals are valid *)
 goal g1:
     forall x,y:bitv[16]. x@y=y@x -> x = y
 
 goal g2:
     forall x,y:bitv[3]. x@[|101|] = [|000101|] -> x=[|000|]
-    
+
 (** Extraction of contiguous bits *
         All goals are valid)
 goal g3:
@@ -235,10 +235,10 @@ goal g4:
     x^{2,3}=[|11|] ->
     x=[|1110|]
 
-goal g5 : 
-    forall x:bitv[32]. forall y:bitv[32]. forall s:bitv[32]. 
+goal g5 :
+    forall x:bitv[32]. forall y:bitv[32]. forall s:bitv[32].
     s = y^{0,15} @ x^{16,31} ->
-    (s^{16,31} = y^{0,15} and s^{0,15} = x^{16,31}) 
+    (s^{16,31} = y^{0,15} and s^{0,15} = x^{16,31})
 ```
 
 ## Type variables
@@ -252,15 +252,15 @@ logic g: 'b->'b
 axiom a1: forall x:'a.  g(f(x))=f(x)
 axiom a2: forall x:int. f(x)=0
 
-goal g1: 
+goal g1:
    (* Valid *)
    g(f(0.01)) = f(0.01)
 
-goal g2: 
+goal g2:
    (* Valid *)
    g(f(1)) = g(0)
 
-goal g3: 
+goal g3:
    (* I don't know *)
    g(f(0.01)) = g(0)
 ```

docs/sphinx_docs/Alt_ergo_native/04_setting_goals.md

@@ -65,9 +65,11 @@ logic x, y : int
 check_sat g: x = y
 ```
 
-```
+```sh
 $ alt-ergo test.ae --model
+```
 
+```
 unknown
 
 (model

docs/sphinx_docs/Dev/index.rst

@@ -4,8 +4,7 @@ Developer's documentation
 
 .. toctree::
    :maxdepth: 2
-   :caption: Contents
-
+
    Project Architecture          <architecture.md>
    Contributing guidelines       <contributing.md>
 

docs/sphinx_docs/Install/index.md

@@ -49,13 +49,13 @@ following libraries :
 
 You can install dependencies using:
 
-```
+```sh
 $ make deps
 ```
 
 and create a development switch with:
 
-```
+```sh
 $ make dev-switch
 ```
 
@@ -96,7 +96,7 @@ Note: these are somewhat obsolete; nowadays you can just use `dune`
 
 You can install dependencies using:
 
-```
+```sh
 $ make js-deps
 ```
 

docs/sphinx_docs/Plugins/ab_why3.md

@@ -57,8 +57,8 @@ Valid (0.0525) (215 steps) (goal g_5)
 If you have already installed this version of Alt-Ergo and this plugin, you should be able to simply use the command:
 
 
-```
- alt-ergo b-why3-POs.why --add-parser ABWhy3Plugin.cmxs --prelude b-set-theory-prelude-2020-02-28.ae
+```sh
+$ alt-ergo b-why3-POs.why --add-parser ABWhy3Plugin.cmxs --prelude b-set-theory-prelude-2020-02-28.ae
 ```
 
 

docs/sphinx_docs/Plugins/index.md

@@ -13,7 +13,9 @@ The `fm-simplex` inequality plugin comes built-in with Alt-Ergo and no further
 installation is required. It is distributed under the same licensing conditions
 as Alt-Ergo. It can be used as follows:
 
-    $ alt-ergo --inequalities-plugin fm-simplex [other-options] file.<ext>
+```sh
+$ alt-ergo --inequalities-plugin fm-simplex [other-options] file.<ext>
+```
 
 ```{note}
 If you are a developer of an external inequality plugin, your plugin needs to

docs/sphinx_docs/Usage/index.md

@@ -4,12 +4,17 @@
 
 Alt-Ergo is executed with the following command:
 
-        $ alt-ergo   [options] file.<ext>
+```sh
+$ alt-ergo [options] file.<ext>
+```
 
 The CDCL solver is now the default SAT engine. The command below
 allows to enable the old Tableaux-like SAT-solver:
 
-        $ alt-ergo   [options] --sat-solver Tableaux file.<ext>
+```sh
+$ alt-ergo [options] --sat-solver Tableaux file.<ext>
+
+```
 
 ### Files extensions
 Alt-Ergo supports file extensions:
@@ -41,7 +46,9 @@ SMT-LIB features will not work with the `legacy` frontend. Use the (default)
 
 Preludes can be passed to Alt-Ergo as follows:
 
-        $ alt-ergo --prelude p.ae --prelude some-path/q.ae [other-options] file.ae
+```sh
+$ alt-ergo --prelude p.ae --prelude some-path/q.ae [other-options] file.ae
+```
 
    Alt-Ergo will try to load a local prelude called "p.ae". If this
    fails, Alt-Ergo tries to load it from the default preludes
@@ -57,7 +64,9 @@ Alt-Ergo can be compiled in Javascript see the [install section] for more inform
 
 The Javascript version of Alt-Ergo compatible with node-js is executed with the following command:
 
-        $ node alt-ergo.js  [options] file.<ext>
+```sh
+$ node alt-ergo.js [options] file.<ext>
+```
 
 Note that timeout options and zip files are not supported with this version because of the lack of js primitives.
 

docs/sphinx_docs/alt_ergo_lexer.py

@@ -1,5 +1,6 @@
 from pygments.lexer import RegexLexer, include
-from pygments.token import *
+from pygments.token import String, Text, Name, Comment,\
+    Keyword, Operator, Number
 
 __globals__ = [ 'AltErgoLexer' ]
 
@@ -24,7 +25,7 @@ class AltErgoLexer(RegexLexer):
     keyopts = (
         r',', r';', r'\(', r'\)', r':', r'->', r'<-', r'<->', r'=', r'<', r'<=',
         r'>', r'>=', r'<>', r'\+', r'-', r'\*', r'\*\*', r'\*\*\.', r'/', r'%',
-        r'@', r'\.', r'#', r'\[', r'\]', r'\{', r'\}', 'r\|', r'\^', r'\|->',
+        r'@', r'\.', r'#', r'\[', r'\]', r'\{', r'\}', r'\|', r'\^', r'\|->',
     )
 
     word_operators = ('and', 'in', 'or', 'xor')

docs/sphinx_docs/conf.py

@@ -17,7 +17,7 @@
 
 # -- Project information -----------------------------------------------------
 
-project = 'Alt-Ergo Documentation'
+project = 'Alt-Ergo'
 copyright = '2020 - 2023, Alt-Ergo developers'
 author = 'Alt-Ergo developers'
 
@@ -42,7 +42,7 @@
 # Add any Sphinx extension module names here, as strings. They can be
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
 # ones.
-extensions = ['myst_parser', 'sphinx_markdown_tables']
+extensions = ['myst_parser']
 
 # Add any paths that contain templates here, relative to this directory.
 templates_path = ['_templates']
@@ -57,10 +57,7 @@
 # The theme to use for HTML and HTML Help pages.  See the documentation for
 # a list of builtin themes.
 #
-html_theme = 'sphinx_rtd_theme'
-html_theme_options = {
-    'navigation_depth': 5,
-}
+html_theme = 'furo'
 
 # -- Options for MyST markdown parser ----------------------------------------
 

docs/sphinx_docs/index.md

@@ -16,12 +16,12 @@ If you are using Alt-Ergo as a library, see the [API documentation](API/index) (
 Alt-ergo supports different input languages:
 
 - Alt-ergo supports the SMT-LIB language v2.6. **This is Alt-Ergo's preferred
-  and recommended input format.** 
+  and recommended input format.**
 - The original input language is its native language, based on the language of the Why3 platform.
 - It also (partially) supports the input language of Why3 through the [AB-Why3 plugin](../Plugins/ab_why3).
 
+## Contents
 ```{toctree}
-:caption: Contents
 :maxdepth: 2
 
 Install                    <Install/index>

docs/sphinx_docs/requirements.txt

@@ -4,6 +4,5 @@
 ###### Requirements for sphinx doc ######
 sphinx >= 4.4.0
 myst-parser
-sphinx_rtd_theme
-sphinx-markdown-tables
+furo
 #

nix/default.nix

@@ -12,6 +12,7 @@ import sources.nixpkgs {
         dolmen_loop = pkgs.callPackage ./dolmen_loop.nix { };
         landmarks = pkgs.callPackage ./landmarks.nix { };
         landmarks-ppx = pkgs.callPackage ./landmarks-ppx.nix { };
+        furo = pkgs.callPackage ./furo.nix { };
       });
     })
   ];

shell.nix

@@ -12,8 +12,7 @@ pkgs.mkShell {
     pkgs.ocamlformat
     pkgs.sphinx
     python3Packages.myst-parser
-    python3Packages.sphinx-markdown-tables
-    python3Packages.sphinx-rtd-theme
+    python3Packages.furo
     ocaml
     dune_3
     ocaml-lsp