Skip to content

Commit 775891c

Browse files
HalbarothHalbaroth
committed
Update the installation documentation
- Explain how to install Alt-Ergo binary with `dune install`. - Simplify the Makefile targets for JavaScript artifacts. - Remove documentation about AB-Why3 plugin and mention it was deprecated and removed. - Reorganize a bit the documentation of the installation and move developer-specific details to the developer documentations. In particular. - Remove the documentation about `install` and `install-all` targets, as no one uses them and the user cannot specify a prefix directory with them. I kept them for the CI.
1 parent 2c6d421 commit 775891c

File tree

10 files changed

+67
-231
lines changed

10 files changed

+67
-231
lines changed

‎CONTRIBUTING.md‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,34 @@ Or directly from GitHub:
5050
$ nix run -f https://github.com/OCamlPro/alt-ergo/archive/master.tar.gz#alt-ergo alt-ergo
5151
```
5252

53+
## Develop with Opam
54+
55+
If you are using opam, you can set up a switch development for Alt-Ergo using:
56+
```shell
57+
$ make dev-switch
58+
```
59+
This command creates a local switch with all the dependencies required for
60+
building the Alt-Ergo binary and library.
61+
62+
To install dependencies for the JavaScript artifacts of Alt-Ergo in the
63+
current switch, run:
64+
```shell
65+
$ make js-deps
66+
```
67+
68+
## Build the project with Makefile
69+
70+
Once you have set up a development environment, you can use the following
71+
Makefile targets to compile different parts of the project:
72+
73+
| Target | Description |
74+
|-------------------|-----------------------------------------------|
75+
| `make bin` | Builds the Alt-Ergo binary and library. |
76+
| `make lib` | Builds only the Alt-Ergo library. |
77+
| `make js` | Builds the Alt-Ergo artifacts for JavaScript. |
78+
| `make plugins` | Builds the Alt-Ergo plugins. |
79+
| `make` | Builds everything. |
80+
5381
## Release Process
5482

5583
Alt-Ergo releases do not have a fixed schedule and are made based on features. We try to maintain the main branch (`next`) of the repository as stable as possible, and cut a release from there when an important feature is complete. We also make point release to fix important bugs.

‎Makefile‎

Lines changed: 3 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -173,32 +173,19 @@ html: doc
173173
# Javascript generation
174174
# ======================
175175

176-
# Build the text alt-ergo bin in Js with js_of_ocaml-compiler
177-
# zarith_stubs_js package is needed for this rule
178-
# note that --timeout option is ignored due to the lack of js primitives
179-
# and the use of input zip file is also unavailable
180-
js-node:
176+
js:
181177
$(DUNE) build $(DUNE_FLAGS) --profile=release $(BJS_DIR)/main_text_js.bc.js
182178
ln -sf $(DEFAULT_DIR)/$(BJS_DIR)/main_text_js.bc.js alt-ergo.js
183-
184-
# Build a web worker for alt-ergo
185-
# zarith_stubs_js, data-encoding, js_of_ocaml and js_of_ocaml-lwt packages are needed for this rule
186-
js-worker:
187179
$(DUNE) build $(DUNE_FLAGS) --profile=release $(BJS_DIR)/worker_js.bc.js
188-
ln -sf $(DEFAULT_DIR)/$(BJS_DIR)/worker_js.bc.js alt-ergo-worker.js \
189-
190-
# Build a small web example using the alt-ergo web worker
191-
# This example is available in the www/ directory
192-
# zarith_stubs_js, data-encoding, js_of_ocaml and js_of_ocaml-lwt js_of_ocaml-ppx lwt_ppx packages are needed for this rule
193-
js-example: js-worker
180+
ln -sf $(DEFAULT_DIR)/$(BJS_DIR)/worker_js.bc.js alt-ergo-worker.js
194181
$(DUNE) build $(DUNE_FLAGS) --profile=release $(BJS_DIR)/worker_example.bc.js
195182
mkdir -p www
196183
cp $(EXTRA_DIR)/worker_example.html www/index.html
197184
cd www \
198185
&& ln -sf ../$(DEFAULT_DIR)/$(BJS_DIR)/worker_js.bc.js alt-ergo-worker.js \
199186
&& ln -sf ../$(DEFAULT_DIR)/$(BJS_DIR)/worker_example.bc.js alt-ergo-main.js
200187

201-
.PHONY: js-node js-worker js-example
188+
.PHONY: js
202189

203190
# ================
204191
# Dependency graph

‎docs/sphinx_docs/Dev/index.rst‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Developer's documentation
55
.. toctree::
66
:maxdepth: 2
77
:caption: Contents
8-
8+
99
Project Architecture <architecture.md>
1010
Contributing guidelines <contributing.md>
1111

‎docs/sphinx_docs/Install/index.md‎

Lines changed: 32 additions & 133 deletions
Original file line numberDiff line numberDiff line change
@@ -1,146 +1,55 @@
11
# Installation
22

3-
## From a package manager
3+
This page explains how to install both the Alt-Ergo releases and the
4+
development versions. If you are interested in contributing to this project,
5+
please refer to the developer documentation.
46

5-
Alt-ergo is available on [opam], the ocaml package manager with the following command :
6-
```console
7-
opam install alt-ergo
8-
```
9-
10-
This command will install the Alt-ergo library `alt-ergo-lib`, as well as other librairies detailled in [dependencies](#dependencies).
7+
## Releases
118

12-
Since version 2.6.0, Alt-Ergo is compatible with opam 2.2 installations using both Cygwin and MSYS2 on Windows. To setup opam on Windows, please follow the instructions [here](https://ocamlpro.com/blog/2024_07_01_opam_2_2_0_releases/).
13-
14-
## From GitHub releases (Linux and macOS)
15-
16-
For convenience, binary releases for Linux and macOS (amd64 and arm64) of
17-
Alt-Ergo are provided on the GitHub release page. These binary releases are
18-
statically linked and very portable. They are distributed under the same
19-
licensing restrictions as the source code.
20-
21-
## From sources
22-
23-
### Dependencies
24-
25-
External dependencies graph generated with `dune-deps` (use `make archi` for source files dependencies):
26-
27-
![](deps.png)
28-
29-
To compile the sources of the library `alt-ergo-lib` and the binary `alt-ergo`, you will need the
30-
following libraries :
31-
```
32-
ocaml >= 4.08.1
33-
dune >= 3.0
34-
dune-build-info
35-
dune-site
36-
dolmen >= 0.10
37-
dolmen_type >= 0.10
38-
dolmen_loop >= 0.10
39-
ocplib-simplex >= 0.5.1
40-
zarith >= 1.11
41-
seq
42-
fmt >= 0.9.0
43-
ppx_blob >= 0.7.2
44-
camlzip >= 1.07
45-
menhir
46-
dune-site
47-
cmdliner >= 1.1.0
48-
psmt2-frontend >= 0.4
49-
stdlib-shims
50-
ppx_deriving
51-
```
52-
53-
You can install dependencies using:
9+
### Installing via opam
5410

11+
The recommended way to install Alt-Ergo releases is throught the OCaml package
12+
manager [opam]. Simply run:
5513
```console
56-
$ make deps
14+
opam install alt-ergo
5715
```
16+
to install the latest Alt-Ergo release in the current switch.
5817

59-
and create a development switch with:
60-
18+
A free version of Alt-Ergo is also available on opam. To install it, run:
6119
```console
62-
$ make dev-switch
63-
```
64-
65-
### Build and Install
66-
67-
The steps below will build and install native or bytecode binaries
68-
depending on whether ocamlopt is installed or only ocamlc is detected.
69-
70-
Note: these are somewhat obsolete; nowadays you can just use `dune`
71-
72-
#### Everything (binaries, plugins, library, ...)
73-
74-
1. Compile with `make`
75-
76-
2. Install with `make install-all`
77-
78-
3. Uninstall with `make uninstall-all`
79-
80-
#### Alt-Ergo library
81-
82-
1. Compile with `make alt-ergo-lib`
83-
84-
2. Install with `make install-lib`
85-
86-
#### Alt-Ergo binary
87-
88-
1. Compile with `make alt-ergo`
89-
90-
2. Install with `make install-bin`
91-
92-
#### Alt-Ergo with Nodejs
93-
94-
You can install dependencies using:
95-
96-
```
97-
$ make js-deps
20+
opam install alt-ergo-free
9821
```
9922

100-
1. Compile with `make js-node`
101-
102-
For this build rule you will need the following aditional libraries :
103-
```
104-
js_of_ocaml >= 5.4.0
105-
zarith_stubs_js >= v0.16.1
106-
```
23+
### Installing via GitHub releases (Linux and macOS)
10724

108-
#### Alt-Ergo web worker
25+
For convenience, binary releases for Linux and macOS (amd64 and arm64) of
26+
Alt-Ergo are provided on the [GitHub release page](https://github.com/OCamlPro/alt-ergo/releases).
27+
These binary releases are statically linked and very portable.
28+
They are distributed under the same licensing restrictions as the source code.
10929

110-
1. Compile with `make js-worker`
30+
## Development versions
11131

112-
For this build rule you will need the following aditional libraries :
32+
### Installing via opam
33+
To install the development version of Alt-Ergo from a cloned Git repository,
34+
run at the root of the repository:
11335
```
114-
js_of_ocaml >= 5.4.0
115-
js_of_ocaml-lwt
116-
zarith_stubs_js >= v0.16.1
117-
data-encoding
36+
opam install .
11837
```
38+
This installs `alt-ergo`, `alt-ergo-lib` and all their dependencies in the
39+
current switch.
11940

120-
#### Alt-Ergo web worker small example
121-
122-
1. Compile with `make js-example`
123-
124-
This command create a `www/` directory in which you can find a small js example running in the `index.html` file
125-
126-
For this build rule you will need the following aditional libraries :
41+
### Installing via Dune
42+
If you prefer install Alt-Ergo binary in a specific prefix directory [DIR], use
43+
the following commands:
12744
```
128-
js_of_ocaml >= 5.4.0
129-
js_of_ocaml-lwt
130-
js_of_ocaml-ppx
131-
lwt_ppx
132-
zarith_stubs_js >= v0.16.1
133-
data-encoding
45+
make deps
46+
make bin
47+
dune install -p alt-ergo --prefix DIR
13448
```
13549

13650
### Plugins
13751

138-
The steps below will build and install additional plugins (extension
139-
.cmxs if ocamlopt is installed or .cma if only ocamlc is detected).
140-
141-
#### The SatML Plugin
142-
143-
satML is now inlined and compiled directly with Alt-Ergo's source code
52+
The steps below will build and install additional plugins.
14453

14554
#### The Fm-Simplex Plugin
14655

@@ -151,18 +60,8 @@ The steps below will build and install additional plugins (extension
15160

15261
#### The AB-Why3 parser plugin
15362

154-
1. Compile with `make AB-Why3`
155-
156-
2. The AB-Why3 plugin is currently built and installed
157-
at the same time as the alt-ergo binary.
158-
159-
You can find more information in the [AB-Why3 README]
160-
161-
#### The profiler plugin
162-
163-
This plugin has been "inlined" in Alt-Ergo sources.
164-
63+
This plugin was deprecated in Alt-Ergo 2.6.0 and removed in Alt-Ergo
64+
2.7.0.
16565

166-
[AB-Why3 README]: ../Plugins/ab_why3.md
16766
[opam]: https://opam.ocaml.org/
16867
[here]: https://packages.debian.org/buster/alt-ergo

‎docs/sphinx_docs/Plugins/ab_why3.md‎

Lines changed: 0 additions & 73 deletions
This file was deleted.

‎docs/sphinx_docs/Plugins/index.md‎

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -23,9 +23,3 @@ be registered in the `(alt-ergo plugins)` site using
2323
[dune-site](https://dune.readthedocs.io/en/stable/reference/dune/plugin.html)
2424
to be available as an option to `--inequalities-plugin`.
2525
```
26-
27-
```{toctree}
28-
:maxdepth: 2
29-
30-
AB why3 <ab_why3>
31-
```

‎docs/sphinx_docs/conf.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@
4242
# Add any Sphinx extension module names here, as strings. They can be
4343
# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
4444
# ones.
45-
extensions = ['myst_parser']
45+
extensions = ['myst_parser', 'sphinx_markdown_tables']
4646

4747
# Add any paths that contain templates here, relative to this directory.
4848
templates_path = ['_templates']

‎docs/sphinx_docs/index.md‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,6 @@ Alt-ergo supports different input languages:
1818
- Alt-ergo supports the SMT-LIB language v2.6. **This is Alt-Ergo's preferred
1919
and recommended input format.**
2020
- The original input language is its native language, based on the language of the Why3 platform. Since the version 2.6.0, this language is deprecated.
21-
- It also (partially) supports the input language of Why3 through the [AB-Why3 plugin](../Plugins/ab_why3).
2221

2322
```{toctree}
2423
:caption: Contents

‎docs/sphinx_docs/requirements.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,4 +5,5 @@
55
sphinx >= 4.4.0
66
myst-parser
77
sphinx_rtd_theme
8+
sphinx-markdown-tables
89
#

‎shell.nix‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ pkgs.mkShell {
1313
pkgs.sphinx
1414
python3Packages.myst-parser
1515
python3Packages.sphinx-rtd-theme
16+
python3Packages.sphinx-markdown-tables
1617
ocaml
1718
dune_3
1819
ocaml-lsp

0 commit comments

Comments
 (0)