diff --git a/docs/sphinx_docs/Alt_ergo_native/02_types/02_01_builtin.md b/docs/sphinx_docs/Alt_ergo_native/02_types/02_01_builtin.md index 811e78776..fe5ea7aee 100644 --- a/docs/sphinx_docs/Alt_ergo_native/02_types/02_01_builtin.md +++ b/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 | `[||]`
where `` is a string of `0` and `1` without spaces | `bitv[]` | +| Explicit declaration | `[\|\|]` where `` is a string of `0` and `1` without spaces | `bitv[]` | | Concatenation | `x @ y` | bitv[n], bitv[m] -> bitv[n+m] | -| Extraction of contiguous bits | `x^{p,q}`
where 0<=p<=q 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) ``` diff --git a/docs/sphinx_docs/Alt_ergo_native/04_setting_goals.md b/docs/sphinx_docs/Alt_ergo_native/04_setting_goals.md index bc178c3e0..9d62f5614 100644 --- a/docs/sphinx_docs/Alt_ergo_native/04_setting_goals.md +++ b/docs/sphinx_docs/Alt_ergo_native/04_setting_goals.md @@ -65,9 +65,11 @@ logic x, y : int check_sat g: x = y ``` -``` +```console $ alt-ergo test.ae --model +``` +``` unknown (model diff --git a/docs/sphinx_docs/Dev/architecture.md b/docs/sphinx_docs/Dev/architecture.md index bff8bc160..59de5fa26 100644 --- a/docs/sphinx_docs/Dev/architecture.md +++ b/docs/sphinx_docs/Dev/architecture.md @@ -3,7 +3,9 @@ If you're new to Alt-Ergo (or not), you may want to get the list of modules (files) with their dependencies with the following command: - make modules-dep-graph +```console +$ make modules-dep-graph +``` If everything goes well with the command above, a file modules-dep-graph.pdf will be generated. diff --git a/docs/sphinx_docs/Dev/index.rst b/docs/sphinx_docs/Dev/index.rst index 05b696e5d..92a4cb945 100644 --- a/docs/sphinx_docs/Dev/index.rst +++ b/docs/sphinx_docs/Dev/index.rst @@ -4,8 +4,7 @@ Developer's documentation .. toctree:: :maxdepth: 2 - :caption: Contents - + Project Architecture Contributing guidelines diff --git a/docs/sphinx_docs/Install/index.md b/docs/sphinx_docs/Install/index.md index 68d8b6259..f8c66d0c9 100644 --- a/docs/sphinx_docs/Install/index.md +++ b/docs/sphinx_docs/Install/index.md @@ -49,13 +49,13 @@ following libraries : You can install dependencies using: -``` +```console $ make deps ``` and create a development switch with: -``` +```console $ make dev-switch ``` @@ -96,7 +96,7 @@ Note: these are somewhat obsolete; nowadays you can just use `dune` You can install dependencies using: -``` +```console $ make js-deps ``` @@ -165,7 +165,6 @@ You can find more information in the [AB-Why3 README] This plugin has been "inlined" in Alt-Ergo sources. - -[AB-Why3 README]: ../Plugins/ab_why3.md -[opam]: https://opam.ocaml.org/ -[here]: https://packages.debian.org/buster/alt-ergo +## Links +- [AB-Why3 README](../Plugins/ab_why3.md) +- [opam](https://opam.ocaml.org/) diff --git a/docs/sphinx_docs/Model_generation.md b/docs/sphinx_docs/Model_generation.md index a7f2c8694..bdf3fbd22 100644 --- a/docs/sphinx_docs/Model_generation.md +++ b/docs/sphinx_docs/Model_generation.md @@ -176,7 +176,7 @@ Model generation is known to be sometimes incomplete in the presence of arrays. (get-model) ``` Execute the command - ```sh + ```console alt-ergo --produce-models INPUT.smt2 ``` We got the output diff --git a/docs/sphinx_docs/Plugins/ab_why3.md b/docs/sphinx_docs/Plugins/ab_why3.md index 64d75552e..dd5bfb175 100644 --- a/docs/sphinx_docs/Plugins/ab_why3.md +++ b/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 +```console +$ alt-ergo b-why3-POs.why --add-parser ABWhy3Plugin.cmxs --prelude b-set-theory-prelude-2020-02-28.ae ``` diff --git a/docs/sphinx_docs/Plugins/index.md b/docs/sphinx_docs/Plugins/index.md index 2b5e833fd..04c66dcab 100644 --- a/docs/sphinx_docs/Plugins/index.md +++ b/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. +```console +$ alt-ergo --inequalities-plugin fm-simplex [other-options] file. +``` ```{note} If you are a developer of an external inequality plugin, your plugin needs to diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md index 586b7a570..330f87475 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/docs/sphinx_docs/Usage/index.md @@ -4,12 +4,17 @@ Alt-Ergo is executed with the following command: - $ alt-ergo [options] file. +```console +$ alt-ergo [options] file. +``` 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. +```console +$ alt-ergo [options] --sat-solver Tableaux file. + +``` ### 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 +```console +$ 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. +```console +$ node alt-ergo.js [options] file. +``` Note that timeout options and zip files are not supported with this version because of the lack of js primitives. @@ -111,11 +120,12 @@ Since version 2.2.0, Alt-Ergo's library is also compiled and installed. See the [API documentation] (also available [on ocaml.org](https://ocaml.org/p/alt-ergo-lib/latest/doc/index.html)) for more information. -[install section]: ../Install/index.md -[Lwt]: https://ocsigen.org/lwt/ -[js_of_ocaml]: https://ocsigen.org/js_of_ocaml/ -[API documentation]: ../API/index -[AB-Why3 README]: ../Plugins/ab_why3.md -[Alt-ergo native language]: ../Alt_ergo_native/index -[SMT-LIB language]: ../SMT-LIB_language/index -[Dune-site plugins]: https://dune.readthedocs.io/en/stable/sites.html#plugins +## Links +- [install section](../Install/index.md) +- [Lwt](https://ocsigen.org/lwt/) +- [js_of_ocaml](https://ocsigen.org/js_of_ocaml/) +- [API documentation](../API/index) +- [AB-Why3 README](../Plugins/ab_why3.md) +- [Alt-ergo native language](../Alt_ergo_native/index) +- [SMT-LIB language](../SMT-LIB_language/index) +- [Dune-site plugins](https://dune.readthedocs.io/en/stable/sites.html#plugins) diff --git a/docs/sphinx_docs/alt_ergo_lexer.py b/docs/sphinx_docs/alt_ergo_lexer.py index 185883970..fce2bbb56 100644 --- a/docs/sphinx_docs/alt_ergo_lexer.py +++ b/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') diff --git a/docs/sphinx_docs/conf.py b/docs/sphinx_docs/conf.py index d7a305224..0cba6f563 100644 --- a/docs/sphinx_docs/conf.py +++ b/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 ---------------------------------------- diff --git a/docs/sphinx_docs/index.md b/docs/sphinx_docs/index.md index 52d7d6a47..4a889b80d 100644 --- a/docs/sphinx_docs/index.md +++ b/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 diff --git a/docs/sphinx_docs/requirements.txt b/docs/sphinx_docs/requirements.txt index 9d728ad7e..2e282846e 100644 --- a/docs/sphinx_docs/requirements.txt +++ b/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 # diff --git a/nix/default.nix b/nix/default.nix index 7742f9083..00ee3ecf9 100644 --- a/nix/default.nix +++ b/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 { }; }); }) ]; diff --git a/shell.nix b/shell.nix index e236f54d6..6813cfaaa 100644 --- a/shell.nix +++ b/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