move things out of the doc to make it a proposer User Manual

.github/workflows/deploy.yml

@@ -38,6 +38,7 @@ jobs:
 
           nix-shell --run "
             dune build @doc &&
+            rm -rf doc/api &&
             mv _build/default/_doc/_html doc/api &&
             BISECT_FILE=\$(pwd)/bisect dune runtest --force --instrument-with bisect_ppx &&
             bisect-ppx-report html -o doc/coverage &&

HACKING.md

@@ -0,0 +1,103 @@
+# Hacking on Owi
+
+## Development setup
+
+To get a proper development setup:
+
+```shell-session
+$ git clone git@github.com:OCamlPro/owi.git
+$ cd owi
+$ opam install . --deps-only --with-test --with-doc --with-dev-setup
+$ git submodule update --init --recursive
+$ dune build @all
+```
+
+## Coding Guidelines
+
+### The `prelude` library
+
+We use the [`prelude`](https://forge.kumikode.org/kumikode/prelude) library to **hide dangerous functions** from the standard library.
+It is automatically opened in the whole project.
+More than dangerous functions, this library also hide some modules for which better alternatives exists.
+For instance, all system interactions are done using [`Bos`](https://erratique.ch/software/bos/doc/) and all the formatting is done with [`Fmt`](https://erratique.ch/software/fmt/doc/).
+
+### Printing
+
+Read the [Logs basics](https://erratique.ch/software/logs/doc/Logs/index.html#basics) and in particular, the [usage conventions](https://erratique.ch/software/logs/doc/Logs/index.html#usage).
+
+## Documentation
+
+### API
+
+You can build the documentation with:
+
+```shell-session
+$ dune build @doc
+$ xdg-open _build/default/doc/index.html
+```
+
+### User Manual
+
+```shell-session
+$ cd ./doc
+$ mdbook serve
+```
+
+## Testing
+
+### Unit tests
+
+Tests are mostly written using [Cram Tests].
+The ones that are integrated into documentation are using [MDX].
+You can run them as follow:
+
+```shell-session
+$ dune runtest
+```
+
+If you made some changes and the output of some tests is changing, the diff will be displayed.
+If you want to automatically accept the diff as being the new expected output, you can run:
+
+```shell-session
+$ dune promote
+```
+
+### Code coverage
+
+You can generate the code coverage report with:
+
+```shell-session
+BISECT_FILE=$(pwd)/bisect dune runtest --force --instrument-with bisect_ppx
+bisect-ppx-report html -o _coverage
+xdg-open _coverage/index.html
+```
+
+### Fuzzing
+
+See [test/fuzz].
+
+[Cram Tests]: https://dune.readthedocs.io/en/latest/reference/cram.html
+[MDX]: https://github.com/realworldocaml/mdx
+[test/fuzz]: ./test/fuzz 
+
+## Diagnostic
+
+### Profiling
+
+#### Landmarks
+
+```shell-session
+OCAML_LANDMARKS=on dune exec --instrument-with landmarks --profile release -- owi run test/run/binary_loop.wasm
+```
+
+See the discussion in [#871] to understand landmarks limitations in Owi.
+
+### Benchmarking
+
+#### Test-comp
+
+See [Symbocalypse].
+
+[#871]: https://github.com/OCamlPro/owi/pull/871
+[Symbocalypse]: https://github.com/OCamlPro/symbocalypse
+

README.md

@@ -9,7 +9,7 @@
 <div align="center">
 <br />
 
-[![build-badge]][build status] [![coverage-badge]][code coverage] [📘 documentation] [💬 zulip]
+[![build-badge]][build status] [![coverage-badge]][code coverage]
 
 </div>
 
@@ -19,12 +19,98 @@
 
 ### Key resources
 
-<div>
-  📘 <kbd><a href="https://ocamlpro.github.io/owi">Documentation</a></kbd> → Read the documentation<br />
-  💬 <kbd><a href="https://owi.zulipchat.com">Zulip community</a></kbd> → Ask questions and collaborate<br />
-</div>
+- 📘 [User Manual](https://ocamlpro.github.io/owi)
+  - [Install Owi](https://ocamlpro.github.io/owi/installation.html)
+  - [Quickstart](https://ocamlpro.github.io/owi/symex/quickstart.html)
+- 💬 [Zulip community](https://owi.zulipchat.com)
+- [List of supported Wasm proposals](https://webassembly.org/features)
+- [Changelog](./CHANGES.md)
+- [Hacking on Owi](./HACKING.md)
+
+### Explanations
+
+<details>
+
+  <summary>List of talks</summary>
+
+- [september 2023]: [ICFP OCaml track] @ The Westin Seattle - Seattle
+- [october 2023]: Wasm Research Day organized by the [WebAssembly Research Center] @ Google - Munich
+- april 2024: [OUPS (OCaml UserS in Paris)] @ Sorbonne Université - Paris
+- [november 2024]: [LVP working group] day of the [GdR GPL] @ Université Paris-Cité - Paris
+- [december 2024]: Léo Andrès' PhD defense @ Université Paris-Saclay - Gif-sur-Yvette
+- january 2025: [JFLA 2025] @ Domaine de Roiffé - Roiffé
+- [february 2025]: [Wasm Research Day 2025] (remote) @ Fastly - San Francisco
+- february 2025: [PPS Seminar] @ Université Paris-Cité - Paris
+- may 2025: [15th MirageOS hack retreat] @ Priscilla Queen of the Medina - Marrakech
+- june 2025: [\<Programming\> 2025] @ Faculty of Mathematics and Physics, Charles University - Prague
+- june 2025: [Dagstuhl Seminar 25241 - Utilising and Scaling the WebAssembly Semantics] @ Leibniz-Zentrum für Informatik - Dagstuhl
+- october 2025: [Wasm Research Day October 2025] @ Google - Munich
+
+</details>
+
+<details>
+
+  <summary>List of publications</summary>
+
+- [Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly], 2024
+- [Exécution symbolique pour tous ou Compilation d'OCaml vers WebAssembly], 2024
+- [Cross-Language Symbolic Runtime Annotation Checking], 2025
+- [Exécution symbolique pour la génération de tests ciblant des labels], 2026
+
+[Cross-Language Symbolic Runtime Annotation Checking]: https://inria.hal.science/hal-04798756/file/cross_language_symbolic_runtime_annotation_checking.pdf
+[Exécution symbolique pour la génération de tests ciblant des labels]: https://hal.science/hal-05427949
+[Exécution symbolique pour tous ou Compilation d'OCaml vers WebAssembly]: https://fs.zapashcanon.fr/pdf/manuscrit_these_leo_andres.pdf
+[Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly]: https://hal.science/hal-04627413
+
+[september 2023]: https://youtu.be/IM76cMP3Eqo
+[october 2023]: https://youtu.be/os_pknmiqmU
+[november 2024]: https://groupes.renater.fr/wiki/lvp/public/journee_lvp_novembre2024
+[december 2024]: https://fs.zapashcanon.fr/mp4/phd_defense.mp4
+[february 2025]: https://youtu.be/x6V-NJ9agjg
+
+[15th MirageOS hack retreat]: https://retreat.mirage.io
+[Dagstuhl Seminar 25241 - Utilising and Scaling the WebAssembly Semantics]: https://www.dagstuhl.de/seminars/seminar-calendar/seminar-details/25241
+[JFLA 2025]: https://jfla.inria.fr/jfla2025.html
+[GdR GPL]: https://gdr-gpl.cnrs.fr/
+[ICFP OCaml track]: https://icfp23.sigplan.org/home/ocaml-2023
+[LVP working group]: https://gdrgpl.myxwiki.org/xwiki/bin/view/Main/GTs/GT%20Langages%20et%20v%C3%A9rification%20de%20programmes%20(LVP)
+[OUPS (OCaml UserS in Paris)]: https://oups.frama.io
+[PPS Seminar]: https://www.irif.fr/seminaires/pps/index
+[\<Programming\> 2025]: https://2025.programming-conference.org
+[WebAssembly Research Center]: https://www.cs.cmu.edu/wrc
+[Wasm Research Day 2025]: https://www.cs.cmu.edu/~wasm/wasm-research-day-2025.html
+[Wasm Research Day October 2025]: https://www.cs.cmu.edu/~wasm/wasm-research-day-2025b.html
+
+</details>
+
+### References
+
+- TODO: man pages (see [here](https://ocamlpro.github.io/owi/manpages/owi.html#owi) for now)
+- TODO: high-level API for each language
+- TODO: Wasm API
+
+### About
+
+#### Fundings & Sponsors
+
+This project was partly funded through the [NGI0 Core] Fund, a fund established by [NLnet] with financial support from the European Commission's [Next Generation Internet] program :
+
+1. [First grant].
+2. [Second grant].
+
+[Next Generation Internet]: https://ngi.eu
+[NGI0 Core]: https://nlnet.nl/core
+[NLnet]: https://nlnet.nl
+[First grant]: https://nlnet.nl/project/OWI
+[Second grant]: https://nlnet.nl/project/OWI-2/
+
+#### Spelling and pronunciation
+
+Although the name Owi comes from an acronym (OCaml WebAssembly Interpreter), it must be written as a proper noun and only the first letter must be capitalized. It is possible to write the name in full lowercase when referring to the opam package or to the name of the binary.
+
+The reason we chose this spelling rather than the fully capitalized version is that in French, Owi is pronounced [o’wi(ʃ)] which sounds like "Oh oui !" which means "Oh yes!". Thus it should be pronounced this way and not by spelling the three letters it is made of.
 
-### License
+#### License
 
     Owi
     Copyright (C) 2021-2024 OCamlPro
@@ -56,5 +142,3 @@ Some code has been taken from the E-ACSL plugin of Frama-C. It is licensed under
 [build status]: https://github.com/ocamlpro/owi/actions
 [coverage-badge]: https://raw.githubusercontent.com/ocamlpro/owi/gh-pages/coverage/badge.svg
 [code coverage]: https://ocamlpro.github.io/owi/coverage
-[📘 documentation]: https://ocamlpro.github.io/owi
-[💬 zulip]: https://owi.zulipchat.com

doc/src/SUMMARY.md

@@ -2,13 +2,8 @@
 
 [Home](index.md)
 [Installation](installation.md)
-[Supported Wasm proposals](proposals.md)
 [Comparison with other tools](comparison.md)
-
-# Symbolic Execution Engine
-
-- [Symbolic Execution 101](symex/symbolic-execution-101.md)
-- [Quickstart](symex/quickstart.md)
+[Quickstart](symex/quickstart.md)
 
 # Bug-Finding, Testing & Pen-testing
 
@@ -32,12 +27,6 @@
 - [How to Speed it Up](sap/optimizations.md)
 - [Comparison to Rosette, Prolog, etc.](sap/comparison.md)
 
-# Going Further
-
-- [Talks and Papers](further/talks-papers.md)
-- [Commands and Options](further/commands.md)
-- [API: Symbols and Helpers](further/api.md)
-
 # WebAssembly Toolkit
 - [Overview](wasm-toolkit/overview.md)
 - [Comparison with Other Tools](wasm-toolkit/comparison.md)
@@ -65,18 +54,3 @@
 - [Overview](ocaml-api/overview.md)
 - [How to Define Custom Functions](ocaml-api/custom-functions.md)
 - [Generated API Documentation](ocaml-api/odoc.md)
-
-# Hacking
-- [Development Setup](hacking/setup.md)
-- [Coding Guidelines](hacking/guidelines.md)
-- [Documentation](hacking/doc.md)
-- [Testing](hacking/testing.md)
-- [Benchmarking](hacking/benchmarking.md)
-
-# About
-- [History of Owi](about/history.md)
-- [Authors and Contributors](about/authors.md)
-- [License](about/license.md)
-- [Funding](about/fundings.md)
-- [Changelog](about/changelog.md)
-- [Projects and People Using Owi](about/users.md)