Js worker (#456)

* Add feature to parse a string as an input file

* Add a webworker for Alt-Ergo

* Add a small web example that uses the alt-ergo webworker

* Add documentation for the worker and its example

* Fix formatter

* Add the webworker build in javascript workflow in the ci

.github/workflows/build_js.yml

@@ -1,12 +1,8 @@
 name: Build Javascript
 
-# this worflow try to build and test the javascript version of Alt-Ergo
-# It only runs on `next` or `main` branch
-on:
-  push:
-    branches:
-      - next
-      - main
+# this worflow try to build and test the nodejs compatible version of Alt-Ergo
+# and try to build the webworker of Alt-Ergo
+on: [push,pull_request]
 
 env:
   OCAML_DEFAULT_VERSION: 4.10.0
@@ -21,7 +17,6 @@ env:
 jobs:
   compile_and_test_js:
     # check if the project build in js.
-    # If this test fails, no tests are done
     name: Compile AE with JsoO and test it with NodeJs
 
     runs-on: ubuntu-latest
@@ -63,7 +58,7 @@ jobs:
       - name: Install deps
         run: opam install ./*.opam --deps-only --with-test
 
-      # Add alt-ergo-js dependencies
+      # Add alt-ergo.js dependencies
       - name: Install Js_of_ocaml and zarith_stubs_js
         run: opam install js_of_ocaml zarith_stubs_js
 
@@ -73,7 +68,7 @@ jobs:
         run: opam install zarith.1.11
 
       # compile Alt-Ergo with Js_of_ocaml
-      - name: Make alt-ergo-js
+      - name: Make alt-ergo.js
         run: opam exec -- make js-node
 
       # Use Node Js actions
@@ -85,11 +80,30 @@ jobs:
       - name: Run simple example with node
         run: opam exec -- node alt-ergo.js non-regression/valid/everything/f1.ae
 
-      # Upload Alt-Ergo.js an artifact
+      # Upload Alt-Ergo.js as an artifact
       # the artifact name contains the system is builded on and the ocaml
       # compiler version used
       - name: Upload alt-ergo.js
         uses: actions/upload-artifact@v2
+        if: github.ref == 'refs/heads/main' || github.ref == 'refs/heads/next'
         with:
           name: alt-ergo-js-${{ runner.os }}-${{ env.OCAML_DEFAULT_VERSION }}
           path: "alt-ergo.js"
+
+      # Add alt-ergo-worker.js dependencies
+      - name: Install data-encoding js_of_ocaml-lwt
+        run: opam install data-encoding js_of_ocaml-lwt
+
+      # compile the Alt-Ergo web worker with Js_of_ocaml
+      - name: Make alt-ergo-worker.js
+        run: opam exec -- make js-worker
+
+      # Upload Alt-Ergo-worker.js as an artifact
+      # the artifact name contains the system is builded on and the ocaml
+      # compiler version used
+      - name: Upload alt-ergo-worker.js
+        uses: actions/upload-artifact@v2
+        if: github.ref == 'refs/heads/main' || github.ref == 'refs/heads/next'
+        with:
+          name: alt-ergo-worker-js-${{ runner.os }}-${{ env.OCAML_DEFAULT_VERSION }}
+          path: "alt-ergo-worker.js"

.github/workflows/build_make.yml

@@ -132,6 +132,10 @@ jobs:
       - name: Make ${{ matrix.package }}
         run: opam exec -- make ${{ matrix.package }}
 
+      # Clean repo
+      - name: Unpin the repo
+        run: opam pin remove .
+
   make_install:
     # Test every install/uninstall rules
     name: Make install

.gitignore

@@ -35,4 +35,9 @@ mlw
 tmp/
 *.tmp
 alt-ergo/tmp/
-_opam
+_opam
+
+# Generated javascript files
+alt-ergo.js
+alt-ergo-worker.js
+www/

Makefile

@@ -51,7 +51,7 @@ SPHINXBUILD = sphinx-build
 # - .ml files generated by menhir or ocamllex
 #   (since they reside in dune specific directory)
 GENERATED_USEFUL=$(UTIL_DIR)/config.ml $(BTEXT_DIR)/flags.dune
-GENERATED_LINKS=alt-ergo altgr-ergo alt-ergo.js AB-Why3-plugin.cma AB-Why3-plugin.cmxs fm-simplex-plugin.cma fm-simplex-plugin.cmxs
+GENERATED_LINKS=alt-ergo altgr-ergo alt-ergo.js alt-ergo-worker.js AB-Why3-plugin.cma AB-Why3-plugin.cmxs fm-simplex-plugin.cma fm-simplex-plugin.cmxs
 GENERATED=$(GENERATED_USEFUL) $(GENERATED_LINKS)
 
 
@@ -316,7 +316,24 @@ js-node: gen
 	$(DUNE) build $(DUNE_FLAGS) --profile=release $(BJS_DIR)/main_text_js.bc.js
 	ln -sf $(DEFAULT_DIR)/$(BJS_DIR)/main_text_js.bc.js alt-ergo.js
 
-.PHONY: js-node
+# Build a web worker for alt-ergo
+# zarith_stubs_js, data-encoding, js_of_ocaml and js_of_ocaml-lwt packages are needed for this rule
+js-worker: gen
+	$(DUNE) build $(DUNE_FLAGS) --profile=release $(BJS_DIR)/worker_js.bc.js
+	ln -sf $(DEFAULT_DIR)/$(BJS_DIR)/worker_js.bc.js alt-ergo-worker.js \
+
+# Build a small web example using the alt-ergo web worker
+# This example is available in the www/ directory
+# 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
+js-example: js-worker
+	$(DUNE) build $(DUNE_FLAGS) --profile=release $(BJS_DIR)/worker_example.bc.js
+	mkdir -p www
+	cp $(EXTRA_DIR)/worker_example.html www/index.html
+	cd www \
+	&& ln -sf ../$(DEFAULT_DIR)/$(BJS_DIR)/worker_js.bc.js alt-ergo-worker.js \
+	&& ln -sf ../$(DEFAULT_DIR)/$(BJS_DIR)/worker_example.bc.js alt-ergo-main.js
+
+.PHONY: js-node js-worker js-example
 
 # ================
 # Dependency graph
@@ -393,6 +410,10 @@ generated-clean:
 dune-clean:
 	$(DUNE) clean
 
+# Clean js example files
+js-clean:
+	rm -rf www
+
 # Clean ocamldot's build artifacts
 ocamldot-clean:
 	cd $(EXTRA_DIR)/ocamldot && $(MAKE) clean
@@ -405,7 +426,7 @@ makefile-distclean: generated-clean
 release-distclean:
 	rm -rf public-release
 
-.PHONY: generated-clean dune-clean makefile-distclean release-distclean
+.PHONY: generated-clean dune-clean js-clean makefile-distclean release-distclean
 
 emacs-edit:
 	emacs `find . -name '*'.ml* | grep -v _build | grep -v _opam` &

docs/sphinx_docs/Install/index.md

@@ -101,7 +101,7 @@ depending on whether ocamlopt is installed or only ocamlc is detected.
 
   2. Install with `make install-gui`
 
-#### Alt-Ergo in javascript
+#### Alt-Ergo with Nodejs
 
   1. Compile with `make js-node`
 
@@ -111,6 +111,34 @@ Js_of_ocaml-compiler
 zarith_stubs_js
 ```
 
+#### Alt-Ergo web worker
+
+  1. Compile with `make js-worker`
+
+For this build rule you will need the following aditional libraries :
+```
+js_of_ocaml
+js_of_ocaml-lwt
+zarith_stubs_js
+data-encoding
+```
+
+#### Alt-Ergo web worker small example
+
+  1. Compile with `make js-example`
+
+This command create a `www/` directory in which you can find a small js example running in the `index.html` file
+
+For this build rule you will need the following aditional libraries :
+```
+js_of_ocaml
+js_of_ocaml-lwt
+js_of_ocaml-ppx
+lwt_ppx
+zarith_stubs_js
+data-encoding
+```
+
 ### Plugins
 
 The steps below will build and install additional plugins (extension

docs/sphinx_docs/Usage/index.md

@@ -83,16 +83,66 @@ On windows, a binary at path `Z:\some\path\bin\alt-ergo` will look for preludes
 plugins in `Z:\some\path\share\alt-ergo\preludes` and
 `Z:\some\path\share\alt-ergo\plugins` respectively.
 
-### Javascript
+## Javascript
 
-Alt-Ergo can be compiled in Javascript see [INSTALL.md] for more informations.
+Alt-Ergo can be compiled in Javascript see the [install section] for more informations.
+
+### Js-node
 
 The Javascript version of Alt-Ergo compatible with node-js is executed with the following command:
 
         $ 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.
 
+### Js-worker
+
+A web worker of the alt-ergo solver is available with the command `make js-worker`. It uses Js_of_ocaml Worker's and Lwt. The `data-encoding` library is used to encode and decode messages to/from the worker. Since the messages are in JSon format, the Alt-Ergo worker can be used from any javascript code.
+
+#### Inputs
+
+This web worker takes a json file composed of a list of string representing each line of an input file. This json file can also be composed of an optional worker identifier (integer) and an optional name for the file to solve. The following code shows an example of a such json file :
+
+```
+{"filename": "testfile",
+ "worker_id": 42,
+ "content": [ "goal g : true" ] }
+```
+
+The worker also take a Json file that correspond to the options to set in Alt-Ergo, like the following example :
+
+```
+{"debug": true,
+ "sat_solver": "Tableaux",
+ "steps_bound": 1000 }
+```
+
+#### Outpus
+
+At the end of solving it returns a Json file corresponding to results, debug informations, etc:
+
+```
+{"worker_id": 42, "status": { "Unsat": 0 },
+"results": [ "Valid (0.1940) (0 steps) (goal g)", "" ],
+"debugs": [ "[Debug][Sat_solver]", "use Tableaux-like solver", "" ],
+"model": [ "[all-models] No SAT models found", "" ],
+"unsat_core": [ "unsat-core:", "", "", "" ],
+"errors": [ "" ],
+"warnings": [ "" ],
+"statistics": [ [], [] ] }
+```
+
+Options and results formats are available in `worker_interface` module. In this module you can also find functions to easily encode inputs and decode outputs.
+Look at the `worker_json_example.json` in the ressources `rsc` of the project to learn more.
+
+### Js-worker example
+
+A small example of how to use the Alt-Ergo web worker can be build with the command ```make js-example```. This command also makes the web worker if it has not already been built. It produces a `www` directory with an html page where you can write a small example, run the worker, and see the results. You can also look at the console of your browser to look at the json file sent
+
+
+[install section]: ../Install/index.md
+[Lwt]: https://ocsigen.org/lwt/
+[js_of_ocaml]: https://ocsigen.org/js_of_ocaml/
 [API documentation]: ../API/index.md
 [AB-Why3 README]: ../Plugins/ab_why3.md
 [Input section]: ../Input_file_formats/index

dune-project

@@ -1,4 +1,5 @@
 (lang dune 2.0)
+(allow_approximate_merlin)
 
 ; Since we want to generate opam files we need to provide informations ;
 (generate_opam_files true)

rsc/extra/subgraphs.dot

@@ -34,24 +34,42 @@ subgraph cluster_bin {
         label="BIN";
         style=filled;
         color=lightgray;
+        subgraph cluster_bin__common {
+                label="Common";
+                style=filled;
+                color=lightblue;
+                "Input_frontend";
+                "Parse_command";
+                "Signals_profiling";
+                "Solving_loop";
+        }
         subgraph cluster_bin__text {
                 label="Text";
                 style=filled;
                 color=lightblue;
-                "Main_input";
                 "Main_text";
-                "Main_gui";
         }
         subgraph cluster_bin__gui {
                 label="Gui";
                 style=filled;
                 color=lightblue;
+                "Main_gui"
                 "Gui_replay";
                 "Gui_session";
                 "Gui_config";
                 "Annoted_ast";
                 "Connected_ast";
         }
+        subgraph cluster_bin__js {
+                label="JS";
+                style=filled;
+                color=lightblue;
+                "Main_text_js";
+                "Options_interface";
+                "Worker_example";
+                "Worker_interface";
+                "Worker_js";
+        }
 }
 
 subgraph cluster_plugins {

rsc/extra/worker_example.html

@@ -0,0 +1,17 @@
+<!doctype html>
+
+<html>
+  <head>
+    <meta charset="utf-8">
+    <title>Alt-Ergo JS</title>
+    <meta name="description" content="Alt-Ergo Js">
+    <meta name="author" content="Alt-Ergo dev team">
+    <link rel="stylesheet" href="style.css">
+    <!-- ENTRY POINT -->
+    <script type="text/javascript" src="alt-ergo-main.js"></script>
+  </head>
+
+  <body>
+        <div id="main"></div>
+  </body>
+</html>

rsc/extra/worker_json_example.json

@@ -0,0 +1,55 @@
+// Example of json file that contains a filename and the content of the file
+{ "filename": "Try-alt-ergo",
+  "worker_id": 42,
+  "content":
+  "type 'a set\n\nlogic empty : 'a set\nlogic add : 'a , 'a set -> 'a set\n\\logic mem : 'a , 'a set -> prop\n\naxiom mem_empty:\n  forall x : 'a.\n  not mem(x, empty : 'a set)\n\naxiom mem_add:\n  forall x, y : 'a. forall s : 'a set.\n  mem(x, add(y, s)) <->\n  (x = y or mem(x, s))\n\nlogic is1, is2 : int set\nlogic iss : int set set\n\ngoal g_4:\n  is1 = is2 -> \n  (not mem(1, add(2+3, empty : int set))) and\n  mem (is1, add (is2, iss)) "
+}
+
+// Example of Json file that represent all options that can be set in the worker :
+{
+    "debug": false, "debug_ac": false, "debug_adt": false,
+    "debug_arith": false, "debug_arrays": false, "debug_bitv": false,
+    "debug_cc": false, "debug_combine": false, "debug_constr": false,
+    "debug_explanations": false, "debug_fm": false, "debug_fpa": 0,
+    "debug_gc": false, "debug_interpretation": false, "debug_ite": false,
+    "debug_matching": 0, "debug_sat": false, "debug_split": false,
+    "debug_sum": false, "debug_triggers": false, "debug_types": false,
+    "debug_typing": false, "debug_uf": false, "debug_unsat_core": false,
+    "debug_use": false, "debug_warnings": false, "rule": 0,
+    "case_split_policy": "AfterTheoryAssume", "enable_adts_cs": false,
+    "max_split": 0, "replay": false, "replay_all_used_context": false,
+    "save_used_context": false, "answers_with_loc": false,
+    "answers_with_loc": false, "frontend": "Legacy", "input_format": "Native",
+    "infer_input_format": false, "parse_only": false, "parsers": [],
+    "preludes": [], "type_only": false, "type_smt2": false,
+    "disable_weaks": false, "enable_assertions": false, "age_bound": 100,
+    "fm_cross_limit": 100, "steps_bound": 1000, "interpretation": 3,
+    "model": "MAll", "output_format": "Smtlib2", "infer_output_format": false,
+    "unsat_core": false, "verbose": false, "greedy": false,
+    "instanciate_after_backjump": false, "max_multi_triggers_size": 4,
+    "nb_triggers": 2, "no_ematching": false, "no_user_triggers": false,
+    "normalize_instances": false, "triggers_var": false,
+    "arith_matchin": false, "bottom_classes": false,
+    "cdcl_tableaux_inst": false, "cdcl_tableaux_th": false,
+    "disable_flat_formulas_simplifiaction": false, "enable_restarts": false,
+    "minimal_bj": false, "no_backjumping": false, "no_backward": false,
+    "no_decisions": false, "no_decisions_on": [], "no_sat_learning": false,
+    "sat_solver": "Tableaux", "tableaux_cdcl": false, "disable_ites": false,
+    "inline_lets": false, "rewriting": false, "term_like_pp": false,
+    "disable_adts": false, "no_ac": false, "no_contracongru": false,
+    "no_fm": false, "no_nla": false, "no_tcp": false, "no_theory": false,
+    "restricted": false, "tighten_vars": false, "use_fpa": false,
+    "timers": false, "file": "try-alt-ergo"
+}
+
+// Example of Json file that represent the results from a run of the Worker
+{
+    "worker_id": 42, "status": { "Unsat": 0 },
+    "results": [ "Valid (0.1940) (0 steps) (goal g)", "" ],
+    "debugs": [ "[Debug][Sat_solver]", "use Tableaux-like solver", "" ],
+    "model": [ "[all-models] No SAT models found", "" ],
+    "unsat_core": [ "unsat-core:", "", "", "" ]
+    "errors": [ "" ],
+    "warnings": [ "" ],
+    "statistics": [ [], [] ],
+}