diff --git a/guides/users/README.md b/guides/users/README.md index 3281b8dd5ceffaefe67c8d78770371f738beb3e5..acb86af0212aa55042ef82f3850cace30d02eb28 100644 --- a/guides/users/README.md +++ b/guides/users/README.md @@ -1,42 +1,42 @@ -- [TL;DR](#org4613395) -- [Topology](#org90ca725) -- [Algorithms](#org046b3be) -- [Examples](#org28013a7) -- [Batch mode](#org5e9fb35) - - [Running batch simulations](#org88f9350) - - [Running batch simulations with Built-in daemons](#org40c965c) - - [Running batch simulations with manual (a.k.a. custom) daemons](#orgdd8c074) - - [Running batch simulations with `lurette`](#orgf12417b) - - [Viewing Results](#org787fcde) - - [The `sasa` CLI](#orge7a4389) -- [Interactive mode](#orga4286ee) - - [Example: use `rdbg` from the `test/alea-coloring/` directory](#orgfd167f3) - - [The examples of test directory](#org54614c9) - - [Running interactive sessions with `rdbg`](#org8389710) - - [Getting `rdbg` on-line help](#org06a1ac5) - - [A `rdbg` `sasa` GUI](#orgdce894e) - - [Useful Modules](#orge82a14e) -- [Install](#org0021508) - - [TL;DR](#org377dcfe) - - [Not strictly mandatory, but useful, third-party software](#orgb7c9381) - - [Install `sasa` via opam (version >= 2.\*)](#orgb86401e) - - [Install `sasa` via `git`](#orgcbf1681) - - [Use `sasa` via docker](#orgc610ed3) - - [Use `sasa` via a Virtual Machine](#orgee4ae29) -- [Screencasts](#orgef0e2a0) -- [More](#org12cda47) -- [FAQ](#org3719ee5) - - [Is there a FAQ?](#org5f6beac) - - [I have a compilation error that I don't understand](#org9d35258) - - [I have the error `Invalid_argument("compare: functional value")`](#org63b0ec3) - - - -<a id="org4613395"></a> +- [TL;DR](#orgbd271a9) +- [Topology](#org7f566fb) +- [Algorithms](#org59c1a68) +- [Examples](#orgf365ef6) +- [Batch mode](#orgba350a9) + - [Running batch simulations](#org71360af) + - [Running batch simulations with Built-in daemons](#org71fc9c6) + - [Running batch simulations with manual (a.k.a. custom) daemons](#org32785d9) + - [Running batch simulations with `lurette`](#orge5f0aff) + - [Viewing Results](#orgf4a3e62) + - [The `sasa` CLI](#org37b1328) +- [Interactive mode](#org3ee1c63) + - [Example: use `rdbg` from the `test/alea-coloring/` directory](#org6223994) + - [The examples of test directory](#org7361545) + - [Running interactive sessions with `rdbg`](#org6e733a2) + - [Getting `rdbg` on-line help](#org4cd47c7) + - [A `rdbg` `sasa` GUI](#org6831b5f) + - [Useful Modules](#org9884b00) +- [Install](#org160a81b) + - [Install `sasa` via opam: TL;DR](#org7ffb4e0) + - [Install `sasa` via opam (long version)](#org868c435) + - [Not strictly mandatory, but useful, third-party software](#org321ff97) + - [Install `sasa` via `git`](#orgf73d6fa) + - [Use `sasa` via docker](#org398ecef) + - [Use `sasa` via a Virtual Machine](#org314e70c) +- [Screencasts](#orge319dc9) +- [More](#org34a195d) +- [FAQ](#orgab249a2) + - [Is there a FAQ?](#orgf9ef9e9) + - [I have a compilation error that I don't understand](#orge2003dc) + - [I have the error `Invalid_argument("compare: functional value")`](#orgccdb4e5) + + + +<a id="orgbd271a9"></a> # TL;DR -<a id="org061f39e"></a> SASA is a **Self-stabilizing Algorithms SimulAtor**, based on the so-called **Atomic State model** (ASM) introduced by <span class="underline">Dijkstra</span> in its seminal article on [Self-stabilizing distributed algorithms](http://www.cs.utexas.edu/~EWD/ewd04xx/EWD426.PDF). This model is also sometimes named "locally shared memory model with composite atomicity" +<a id="orgf830fc6"></a> SASA is a **Self-stabilizing Algorithms SimulAtor**, based on the so-called **Atomic State model** (ASM) introduced by <span class="underline">Dijkstra</span> in its seminal article on [Self-stabilizing distributed algorithms](http://www.cs.utexas.edu/~EWD/ewd04xx/EWD426.PDF). This model is also sometimes named "locally shared memory model with composite atomicity" Basically, one needs to provide: @@ -62,11 +62,11 @@ sasa ring.dot -l 4 # run a batch simulation for 4 steps [](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/poster.pdf) -<a id="org90ca725"></a> +<a id="org7f566fb"></a> # Topology -<a id="org3fa8e55"></a> <a id="orga56589a"></a> The topology is given via `.dot` files, that should +<a id="org8f2889a"></a> <a id="org193d09e"></a> The topology is given via `.dot` files, that should 1. follow the [graphviz/dot format](https://en.wikipedia.org/wiki/DOT_(graph_description_language)) 2. have nodes **labeled** by the `algo` field @@ -124,14 +124,14 @@ graph ring { Such parameters can be retrieved in algorithms using the `Algo.get_graph_attribute : string -> string` function. For example, if you know the graph diameter, you can define it as a graph attribute (a `Algo.diameter: unit -> int` function is provided, but it can be expensive to use for large graphs). -Some tools are provided in the `sasa` [distributions](#org49e7a9a) to generate such kinds of `dot` graphs: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-gg/> +Some tools are provided in the `sasa` [distributions](#org21de61c) to generate such kinds of `dot` graphs: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-gg/> -<a id="org046b3be"></a> +<a id="org59c1a68"></a> # Algorithms -<a id="org9930119"></a> +<a id="org779e381"></a> The following has been generated from [algo.mli](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/lib/algo/algo.mli) @@ -143,7 +143,7 @@ The following has been generated from [algo.mli](https://gricad-gitlab.univ-gren </iframe> -<a id="org28013a7"></a> +<a id="orgf365ef6"></a> # Examples @@ -183,14 +183,14 @@ The `test` directory also contains sub-directories which gathers programs shared - `test/*/my-rdbg-tuning.ml`: includes `test/my-rdbg-tuning.ml` and defines commands specific to the example of the directory. Indeed, `rdbg`, once launched, first tries to read the content of the file name `my-rdbg-tuning.ml` (if it exists). -<a id="org5e9fb35"></a> +<a id="orgba350a9"></a> # Batch mode  -<a id="org88f9350"></a> +<a id="org71360af"></a> ## Running batch simulations @@ -233,31 +233,37 @@ All the CLI commands above can be run automatically using a `make` rule containe make: 'ring.cmxs' is up to date. # Automatically generated by /home/jahier/.opam/4.14.0/bin/sasa version "v4.8.0" ("65d9837") - # on crevetete the 5/12/2022 at 22:34:53 + # on crevetete the 12/12/2022 at 10:53:48 #sasa ring.dot - #seed 27916546 + #seed 914504953 #inputs #outputs "p1_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "Enab_p1_conflict":bool "Enab_p2_conflict":bool "Enab_p3_conflict":bool "Enab_p4_conflict":bool "Enab_p5_conflict":bool "Enab_p6_conflict":bool "Enab_p7_conflict":bool "p1_conflict":bool "p2_conflict":bool "p3_conflict":bool "p4_conflict":bool "p5_conflict":bool "p6_conflict":bool "p7_conflict":bool "legitimate":bool potential:real round:bool round_nb:int #step 0 - #outs 0 1 0 0 1 1 0 t f t t t t t t f f t t f t f 6. f 0 + #outs 0 1 1 0 1 1 1 f t t f t t t f f f f f t f f 6. f 0 #step 1 - #outs 2 1 0 2 2 1 2 t f f t t f t f f f t f f t f 4. t 2 + #outs 0 1 1 0 1 0 1 f t t f f f f f t t f f f f f 2. f 1 #step 2 - #outs 2 1 0 1 2 1 0 f f f f f f f f f f f f f f t 0. t 2 + #outs 0 2 2 0 1 0 1 f t t f f f f f t t f f f f f 2. t 2 - This algo is silent after 6 moves, 2 steps, 2 rounds. + #step 3 + #outs 0 1 1 0 1 0 1 f t t f f f f f t f f f f f f 2. t 3 + + #step 4 + #outs 0 2 1 0 1 0 1 f f f f f f f f f f f f f f t 0. t 3 + + This algo is silent after 6 moves, 4 steps, 3 rounds. #quit nb: the simulation output (in the green frame) follows the [RIF](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-orga43b00b) conventions. -<a id="org40c965c"></a> +<a id="org71fc9c6"></a> ## Running batch simulations with Built-in daemons @@ -276,7 +282,7 @@ sasa -h | grep "\-daemon" --greedy-daemon, -gd -<a id="orgdd8c074"></a> +<a id="org32785d9"></a> ## Running batch simulations with manual (a.k.a. custom) daemons @@ -314,7 +320,7 @@ In order to enter such input more easily, one can use (requires [the lustre V4 t Daemons can also by simulated by [`lutin`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-4) programs via the use of [`lurette`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-9) (for batch executions) or [`rdbg`](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-10) (for interactive sessions). -<a id="orgf12417b"></a> +<a id="orge5f0aff"></a> ## Running batch simulations with `lurette` @@ -339,14 +345,14 @@ Note that for `lurette`, the role of the SUT (System Under Test) and the one of For more information on this topic: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-daemons/> -<a id="org787fcde"></a> +<a id="orgf4a3e62"></a> ## Viewing Results `sasa -rif` and `lurette` generates `.rif` files that can be viewed with `gnuplot-rif` or `sim2chro`; cf <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox/> -<a id="orge7a4389"></a> +<a id="org37b1328"></a> ## The `sasa` CLI @@ -433,11 +439,11 @@ More `sasa` options: Display the version ocaml version sasa was compiled with and exit. -<a id="orga4286ee"></a> +<a id="org3ee1c63"></a> # Interactive mode -<a id="org9e8abf6"></a> If you want to perform step-by-step simulations, you can use the `-custd` option. But if you want to perform step-by-step simulations without the burden of playing the role of the daemon, you can launch `sasa` under the control of [rdbg](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/). +<a id="orga5621e7"></a> If you want to perform step-by-step simulations, you can use the `-custd` option. But if you want to perform step-by-step simulations without the burden of playing the role of the daemon, you can launch `sasa` under the control of [rdbg](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/). Another advantage of [rdbg](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/) is its ability to display a graphical view of the current configuration during the simulation, to move step by step, or round by round, forward or backwards. @@ -446,7 +452,7 @@ cf <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbg-sasa/> Before reading this section, please read at least the [Basic usage Section if the rdbg documentation](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/README.html#outline-container-sec-3). -<a id="orgfd167f3"></a> +<a id="org6223994"></a> ## Example: use `rdbg` from the `test/alea-coloring/` directory @@ -489,7 +495,7 @@ rdbg [q] quit -<a id="org54614c9"></a> +<a id="org7361545"></a> ## The examples of test directory @@ -500,7 +506,7 @@ The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/t - `test/*/my-rdbg-tuning.ml`: includes `test/my-rdbg-tuning.ml` and defines commands specific to the example of the directory. Indeed, `rdbg`, once launched, first tries to read the content of the file name `my-rdbg-tuning.ml` (it it exists). -<a id="org8389710"></a> +<a id="org6e733a2"></a> ## Running interactive sessions with `rdbg` @@ -517,7 +523,7 @@ The [test](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/t All those commands are defined in (the common) [test/my-rdbg-tuning.ml](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test/my-rdbg-tuning.ml) that is included in (locals) `test/*/my-rdbg-tuning.ml` that are included in (generated) `test/*/rdbg-session.ml` files. `my-rdbg-tuning.ml` contains straigthforward `ocaml` code that defines various `rdbg` shortcuts to ease the simulation of `sasa` systems. Feel free to tailor those command to yours needs by modyfying the local `my-rdbg-tuning.ml`! -<a id="org06a1ac5"></a> +<a id="org4cd47c7"></a> ## Getting `rdbg` on-line help @@ -613,7 +619,7 @@ Here are 2 useful entry-points to rdbg on-line help: (rdbg) -<a id="orgdce894e"></a> +<a id="org6831b5f"></a> ## A `rdbg` `sasa` GUI @@ -627,7 +633,7 @@ opam install -y rdbgui4ocaml To use it: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbgui4sasa/> -<a id="orge82a14e"></a> +<a id="org9884b00"></a> ## Useful Modules @@ -662,51 +668,41 @@ Some modules, used by the sasa core engine, can be useful from `rdbg`. </iframe> -<a id="org0021508"></a> +<a id="org160a81b"></a> # Install -<a id="org49e7a9a"></a> <a id="orge58cf86"></a> +<a id="org21de61c"></a> <a id="org0706c07"></a> -<a id="org377dcfe"></a> +<a id="org7ffb4e0"></a> -## TL;DR +## Install `sasa` via opam: TL;DR -On debian-based distributions, open a terminal and copy/paste: - -```sh -sudo apt install -y zathura graphviz emacs opam -``` - -On other Linux (or mac) distributions, the packages names should be more or less the same. - -Then: +On **debian-based** distributions, open a terminal and copy/paste (on other Linux (or mac) distributions, the packages names should be more or less the same): ```sh +sudo apt install -y opam opam init -y eval $(opam env) echo "test -r ~/.opam/opam-init/init.sh && . ~/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true" >> ~/.bashrc -opam switch create 4.11.1 +opam switch create 4.14.1 eval $(opam env) opam install -y merlin tuareg opam user-setup install opam repo add -a verimag-sync-repo \ "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository" opam update -y -opam install -y sasa -``` - -And optionally (to define test oracles in Lustre or daemons in Lutin): +opam install -y sasa -```sh -opam depext -y rdbgui4sasa lutin -- useless with opam >= 2.1 +# optionally (to perform automated tests): +opam depext -y rdbgui4sasa lutin || echo "useless with opam >= 2.1" opam install -y rdbgui4sasa lutin lustre-v6 -``` -and optionally too (for `luciole`, a gtk-based UI useful to play daemon manually): +# optionally (Useful during interactive simulations) +opam install -y graphviz -```sh +# optionally (for =luciole=, a gtk-based UI useful to play daemon manually): mkdir ~/lv4 # for example cd ~/lv4 wget http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/linux64/lustre-v4-III-e-linux64.tgz @@ -716,83 +712,71 @@ echo "export PATH=$LUSTRE_INSTALL/bin:$PATH" >> ~/.bashrc sudo apt install -y wish ``` -and finally (for running examples in the `sasa/test/` directory): +For running examples in the `sasa/test/` directory to check it has worked: ```sh git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git ``` +Hopefully, everything went file. Otherwise, you can try one of methods below : -<a id="orgb7c9381"></a> -## Not strictly mandatory, but useful, third-party software +<a id="org868c435"></a> -In order to perform interactive simulations, you need to install the [graphviz](https://en.wikipedia.org/wiki/DOT_(graph_description_language)) tools suite and a pdf viewer that is able to auto-refresh (for instance `zathura`). E.g., on debian-based distribution: +## Install `sasa` via opam (long version) -```sh -sudo apt install zathura graphviz -``` +Follows more or less the same instructions as above, but described into more details in case you want to understand the rationale for each commands, and adapt it to your distribution. -Moreover, as you will write Ocaml programs, you definitely need to install the ocaml package manager [opam](http://opam.ocaml.org/doc/Install.html). `opam` works out of the box with most Linux distributions and OSX (mac). `opam` ought to work [on windows too](http://protz.github.io/ocaml-installer/). +As using `sasa` requires to write `Ocaml` programs, you definitely need to install the `Ocaml` package manager [opam](http://opam.ocaml.org/doc/Install.html). [opam](http://opam.ocaml.org/doc/Install.html) works out of the box with most Linux distributions and OSX (mac). `opam` ought to work [on windows too](http://protz.github.io/ocaml-installer/). ```sh -sudo apt install opam -opam init -opam switch create 4.11.1 +sudo apt install -y opam +opam init -y eval $(opam env) -echo "eval $(opam env)" >> ~/.bashrc ``` -You also need an editor. We advice `emacs` with `merlin` and `tuareg`. +The `opam init` ougth to have populated your shell resource file with the necessary configurations commands, but it case it didn't you can run something like: ```sh -sudo apt install emacs -opam install -y merlin tuareg -opam user-setup install -y +echo "eval $(opam env)" >> ~/.bashrc ``` -In order to be able to use `luciole` (a small GUI useful to interactively play the role of the daemon using gtk buttons) you can also install the Lustre V4 distribution. On linux: +Once opam is installed and configured, you may want to install (or not) the last version of the compiler. ```sh -mkdir ~/lv4 # for example -cd ~/lv4 -wget http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/linux64/lustre-v4-III-e-linux64.tgz -tar xvzf lustre-v4-III-e-linux64.tgz -echo "export LUSTRE_INSTALL=~/lv4/lustre-v4-III-e-linux64" >> ~/.bashrc # if you are using bash -echo "export PATH=$LUSTRE_INSTALL/bin:$PATH" >> ~/.bashrc -sudo apt install -y wish +opam switch create 4.14.1 +eval $(opam env) +echo "eval $(opam env)" >> ~/.bashrc ``` -Otherwise: <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html> - - -<a id="orgb86401e"></a> - -## Install `sasa` via opam (version >= 2.\*) - -Once opam (version >= 2.\*!) is installed and configured (see above), you can install `sasa` as follows: +Then, you need to add the `verimag-sync-repo` into your set of opam's repository: ```sh opam repo add -a verimag-sync-repo \ "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository" opam update -y +``` + +Now you should be able to install `sasa`: + +```sh opam install -y sasa ``` -If you want to use the `rdbgui4sasa` Graphical User Interface: +as well as the `rdbgui4sasa` Graphical User Interface: ```sh -opam depext -y rdbgui4sasa && opam install -y rdbgui4sasa +(opam depext -y rdbgui4sasa || echo "useless since opam 2.1") && opam install -y rdbgui4sasa ``` -If you want to be able to defined daemons in Lutin, or test oracles in Lustre, you can also install the corresponding packages packages. +If you want to be able to use the automated test framawork, you can also install the following packages: ```sh opam install -y lustre-v6 -opam depext -y lutin && opam install -y lutin +(opam depext -y lutin || echo "useless since opam 2.1") && opam install -y lutin ``` -Once this is done, upgrading to the last version of `sasa` is as simple as: +Then, if one day you want to upgrade your `sasa` version: ```sh opam update @@ -800,7 +784,40 @@ opam upgrade ``` -<a id="orgcbf1681"></a> +<a id="org321ff97"></a> + +### Not strictly mandatory, but useful, third-party software + +In order to perform interactive simulations, you need to install a pdf viewer that is able to auto-refresh (for instance `zathura`): + +```sh +sudo apt install zathura +``` + +You also need an editor, for instance `emacs` with `merlin` and `tuareg`. + +```sh +sudo apt install emacs +opam install -y merlin tuareg +opam user-setup install -y +``` + +In order to be able to use `luciole` (a small GUI useful to interactively play the role of the daemon using gtk buttons) you can also install the Lustre V4 distribution. On linux: + +```sh +mkdir ~/lv4 # for example +cd ~/lv4 +wget http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/linux64/lustre-v4-III-e-linux64.tgz +tar xvzf lustre-v4-III-e-linux64.tgz +echo "export LUSTRE_INSTALL=~/lv4/lustre-v4-III-e-linux64" >> ~/.bashrc # if you are using bash +echo "export PATH=$LUSTRE_INSTALL/bin:$PATH" >> ~/.bashrc +sudo apt install -y wish +``` + +For more information: <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html> + + +<a id="orgf73d6fa"></a> ## Install `sasa` via `git` @@ -844,14 +861,14 @@ make test One can also mimic the content of the `test` job in the project [.gitlab-ci.yml Gitlab CI script](https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/.gitlab-ci.yml). -<a id="orgc610ed3"></a> +<a id="org398ecef"></a> ## Use `sasa` via docker cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#docker). This docker image contains all the tools mentioned in this section (`sasa`, `lustre`, `opam`, `ocaml`, emacs, graphviz, etc.). -<a id="orgee4ae29"></a> +<a id="org314e70c"></a> ## Use `sasa` via a Virtual Machine @@ -861,7 +878,7 @@ cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-ve - passwd:sasa -<a id="orgef0e2a0"></a> +<a id="orge319dc9"></a> # Screencasts @@ -877,7 +894,7 @@ cf the Docker Install section of the [Synchrone Reactive Tool Box](http://www-ve cf <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/> -<a id="org12cda47"></a> +<a id="org34a195d"></a> # More @@ -886,12 +903,12 @@ cf <http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/> - Tutorials: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt//tags/sasa/> -<a id="org3719ee5"></a> +<a id="orgab249a2"></a> # FAQ -<a id="org5f6beac"></a> +<a id="orgf9ef9e9"></a> ## Is there a FAQ? @@ -900,7 +917,7 @@ Yes. Beside, some tutorials are also available here: <https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/> -<a id="org9d35258"></a> +<a id="orge2003dc"></a> ## I have a compilation error that I don't understand @@ -910,7 +927,7 @@ Beside, some tutorials are also available here: <https://verimag.gricad-pages.un - If the message is totally useless, please feel free to add an issue here <https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/issues> -<a id="org63b0ec3"></a> +<a id="orgccdb4e5"></a> ## I have the error `Invalid_argument("compare: functional value")` diff --git a/guides/users/README.org b/guides/users/README.org index d44f22e91cc28c00dcc2d607e6e7bb9cbf6a325d..2c08d9f21cf88fe261d2273bc3ee63fb77ac84ca 100644 --- a/guides/users/README.org +++ b/guides/users/README.org @@ -783,43 +783,35 @@ Some modules, used by the sasa core engine, can be useful from =rdbg=. <<distributions>> <<install>> -** TL;DR - -On debian-based distributions, open a terminal and copy/paste: -#+BEGIN_SRC sh :eval no -sudo apt install -y zathura graphviz emacs opam -#+END_SRC +** Install =sasa= via opam: TL;DR +On *debian-based* distributions, open a terminal and copy/paste (on +other Linux (or mac) distributions, the packages names should be more +or less the same): -On other Linux (or mac) distributions, the packages names should be more or less the -same. -Then: - -#+BEGIN_SRC sh :eval no +#+BEGIN_SRC sh :eval no +sudo apt install -y opam opam init -y eval $(opam env) echo "test -r ~/.opam/opam-init/init.sh && . ~/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true" >> ~/.bashrc -opam switch create 4.11.1 +opam switch create 4.14.1 eval $(opam env) opam install -y merlin tuareg opam user-setup install opam repo add -a verimag-sync-repo \ "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository" opam update -y -opam install -y sasa -#+END_SRC - -And optionally (to define test oracles in Lustre or daemons in Lutin): +opam install -y sasa -#+BEGIN_SRC sh :eval no -opam depext -y rdbgui4sasa lutin -- useless with opam >= 2.1 +# optionally (to perform automated tests): +opam depext -y rdbgui4sasa lutin || echo "useless with opam >= 2.1" opam install -y rdbgui4sasa lutin lustre-v6 -#+END_SRC +# optionally (Useful during interactive simulations) +opam install -y graphviz -and optionally too (for =luciole=, a gtk-based UI useful to play daemon manually): -#+BEGIN_SRC sh :eval no +# optionally (for =luciole=, a gtk-based UI useful to play daemon manually): mkdir ~/lv4 # for example cd ~/lv4 wget http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/linux64/lustre-v4-III-e-linux64.tgz @@ -829,90 +821,112 @@ echo "export PATH=$LUSTRE_INSTALL/bin:$PATH" >> ~/.bashrc sudo apt install -y wish #+END_SRC -and finally (for running examples in the =sasa/test/= directory): +For running examples in the =sasa/test/= directory to check it has worked: #+BEGIN_SRC sh :eval no git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git #+END_SRC -** Not strictly mandatory, but useful, third-party software +Hopefully, everything went file. Otherwise, you can try one of methods below : -In order to perform interactive simulations, you need to install the -[[https://en.wikipedia.org/wiki/DOT_(graph_description_language)][graphviz]] tools suite and a pdf viewer that is able to auto-refresh -(for instance =zathura=). E.g., on debian-based distribution: -#+BEGIN_SRC sh :eval no -sudo apt install zathura graphviz -#+END_SRC +** Install =sasa= via opam (long version) -Moreover, as you will write Ocaml programs, you definitely need to -install the ocaml package manager [[http://opam.ocaml.org/doc/Install.html][opam]]. =opam= works out of the box -with most Linux distributions and OSX (mac). =opam= ought to work [[http://protz.github.io/ocaml-installer/][on -windows too]]. +Follows more or less the same instructions as above, but described +into more details in case you want to understand the rationale for +each commands, and adapt it to your distribution. -#+BEGIN_SRC sh :eval no -sudo apt install opam -opam init -opam switch create 4.11.1 + +As using =sasa= requires to write =Ocaml= programs, you definitely +need to install the =Ocaml= package manager [[http://opam.ocaml.org/doc/Install.html][opam]]. [[http://opam.ocaml.org/doc/Install.html][opam]] works out +of the box with most Linux distributions and OSX (mac). =opam= ought +to work [[http://protz.github.io/ocaml-installer/][on windows too]]. + +#+BEGIN_SRC sh :eval no +sudo apt install -y opam +opam init -y eval $(opam env) -echo "eval $(opam env)" >> ~/.bashrc #+END_SRC -You also need an editor. We advice =emacs= with =merlin= and =tuareg=. -#+BEGIN_SRC sh :eval no -sudo apt install emacs -opam install -y merlin tuareg -opam user-setup install -y +The =opam init= ougth to have populated your shell resource file with +the necessary configurations commands, but it case it didn't you can +run something like: +#+BEGIN_SRC sh :eval no +echo "eval $(opam env)" >> ~/.bashrc #+END_SRC -In order to be able to use =luciole= (a small GUI useful to -interactively play the role of the daemon using gtk buttons) you can -also install the Lustre V4 distribution. On linux: +Once opam is installed and configured, you may want to install (or not) the last +version of the compiler. -#+BEGIN_SRC sh -mkdir ~/lv4 # for example -cd ~/lv4 -wget http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/linux64/lustre-v4-III-e-linux64.tgz -tar xvzf lustre-v4-III-e-linux64.tgz -echo "export LUSTRE_INSTALL=~/lv4/lustre-v4-III-e-linux64" >> ~/.bashrc # if you are using bash -echo "export PATH=$LUSTRE_INSTALL/bin:$PATH" >> ~/.bashrc -sudo apt install -y wish +#+BEGIN_SRC sh :eval no +opam switch create 4.14.1 +eval $(opam env) +echo "eval $(opam env)" >> ~/.bashrc #+END_SRC -Otherwise: -http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html - - -** Install =sasa= via opam (version >= 2.*) - -Once opam (version >= 2.*!) is installed and configured (see above), -you can install =sasa= as follows: +Then, you need to add the =verimag-sync-repo= into your set of opam's +repository: #+BEGIN_SRC sh :eval no :tangle sh/install-opam.sh :noweb yes :tangle-mode (identity #o444) opam repo add -a verimag-sync-repo \ "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository" opam update -y +#+END_SRC + +Now you should be able to install =sasa=: + +#+BEGIN_SRC sh :eval no :tangle sh/install-opam.sh :noweb yes :tangle-mode (identity #o444) opam install -y sasa #+END_SRC -If you want to use the =rdbgui4sasa= Graphical User Interface: +as well as the =rdbgui4sasa= Graphical User Interface: #+BEGIN_SRC sh :eval no :tangle sh/install-opam.sh :noweb yes :tangle-mode (identity #o444) -opam depext -y rdbgui4sasa && opam install -y rdbgui4sasa +(opam depext -y rdbgui4sasa || echo "useless since opam 2.1") && opam install -y rdbgui4sasa #+END_SRC -If you want to be able to defined daemons in Lutin, or test oracles in -Lustre, you can also install the corresponding packages packages. +If you want to be able to use the automated test framawork, you can also +install the following packages: #+BEGIN_SRC sh :eval no :tangle sh/install-opam.sh :noweb yes :tangle-mode (identity #o444) opam install -y lustre-v6 -opam depext -y lutin && opam install -y lutin +(opam depext -y lutin || echo "useless since opam 2.1") && opam install -y lutin #+END_SRC -Once this is done, upgrading to the last version of =sasa= is as -simple as: +Then, if one day you want to upgrade your =sasa= version: #+BEGIN_SRC sh :eval no opam update opam upgrade #+END_SRC +*** Not strictly mandatory, but useful, third-party software + +In order to perform interactive simulations, you need to install a +pdf viewer that is able to auto-refresh (for instance =zathura=): +#+BEGIN_SRC sh :eval no +sudo apt install zathura +#+END_SRC + +You also need an editor, for instance =emacs= with =merlin= and =tuareg=. +#+BEGIN_SRC sh :eval no +sudo apt install emacs +opam install -y merlin tuareg +opam user-setup install -y +#+END_SRC + +In order to be able to use =luciole= (a small GUI useful to +interactively play the role of the daemon using gtk buttons) you can +also install the Lustre V4 distribution. On linux: + +#+BEGIN_SRC sh +mkdir ~/lv4 # for example +cd ~/lv4 +wget http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/linux64/lustre-v4-III-e-linux64.tgz +tar xvzf lustre-v4-III-e-linux64.tgz +echo "export LUSTRE_INSTALL=~/lv4/lustre-v4-III-e-linux64" >> ~/.bashrc # if you are using bash +echo "export PATH=$LUSTRE_INSTALL/bin:$PATH" >> ~/.bashrc +sudo apt install -y wish +#+END_SRC + +For more information: +http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html ** Install =sasa= via =git=