m

.github/workflows/main.yml

@@ -0,0 +1,54 @@
+name: Main workflow
+
+on:
+  pull_request:
+  push:
+  schedule:
+    # Prime the caches every Monday
+    - cron: 0 1 * * MON
+
+permissions:
+  contents: write
+
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          # - macos-latest
+          - ubuntu-latest
+        ocaml-compiler:
+          - 5.0.0
+
+    runs-on: ${{ matrix.os }}
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v3
+
+      - name: Use OCaml ${{ matrix.ocaml-compiler }}
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-pin: false
+          opam-depext: false
+      # - run: opam install . --deps-only
+      # z3 takes a long time to build and isn't needed for the web build
+      # - run: opam install menhir ppx_expect z3 brr js_of_ocaml-compiler
+      - run: opam install dune menhir ppx_deriving ppx_expect brr js_of_ocaml-compiler
+
+      - uses: actions/setup-node@v3
+        with:
+          node-version: 19
+      - run: npm install -g browserify
+      - run: npm install z3-solver
+
+      - run: eval $(opam env); dune build @web --profile release
+
+      - name: Deploy
+        uses: peaceiris/actions-gh-pages@v3
+        if: github.ref == 'refs/heads/StagedSL'
+        with:
+          github_token: ${{ secrets.GITHUB_TOKEN }}
+          publish_dir: _build/default/deploy

.gitignore

@@ -3,3 +3,5 @@ _build/
 *.conflicts
 boot/menhir/*.ml*
 .DS_Store
+node_modules
+package*.json

README.md

@@ -52,6 +52,7 @@ has a bug
 
 
 
+<<<<<<< HEAD
 
 
 # What is inside the `root directory` ?
@@ -81,3 +82,22 @@ opam switch 4.14.0+flambda
 dune exec ./hip.exe ../src/programs.t/parse_test.ml
 
 
+=======
+TODO:
+design the experiments to show that:
+re-reasoning does not cause too much overhead. 
+we can reason about multi-shot efficiently. 
+
+# Build web version
+
+```sh
+npm install z3-solver
+npm install -g browserify
+dune build @web
+```
+
+```sh
+cd _build/default
+python -m http.server 8005
+```
+>>>>>>> f109ddd921f33788f54cb5cd9addd7342a165288

dune

@@ -0,0 +1,37 @@
+
+; build web version
+
+(rule
+ (action (copy parsing/hipjs.bc.js hipjs.bc.js)))
+(rule
+ (action (copy web/main.js main.js)))
+
+(rule
+ (target coi-serviceworker.min.js)
+ (action (run curl -sOL https://raw.githubusercontent.com/gzuidhof/coi-serviceworker/master/coi-serviceworker.min.js)))
+
+(rule
+ (alias web)
+ (deps coi-serviceworker.min.js hipjs.bc.js bundle.js z3-built.js z3-built.wasm z3-built.worker.js)
+ (action (copy web/index.html index.html)))
+
+(rule
+ (targets z3-built.js z3-built.wasm z3-built.worker.js)
+ (deps (source_tree node_modules))
+ (action (progn
+  (run cp node_modules/z3-solver/build/z3-built.wasm z3-built.wasm)
+  (run cp node_modules/z3-solver/build/z3-built.worker.js z3-built.worker.js)
+  (run cp node_modules/z3-solver/build/z3-built.js z3-built.js))))
+
+(rule
+ (targets bundle.js)
+ (deps main.js)
+ (action (run browserify main.js -o bundle.js --standalone z3)))
+
+(rule
+ (alias web)
+ (targets (dir deploy))
+ (deps coi-serviceworker.min.js hipjs.bc.js bundle.js index.html z3-built.js z3-built.wasm z3-built.worker.js)
+ (action (progn
+  (run mkdir deploy)
+  (run cp %{deps} %{targets}))))

dune-project

@@ -1,4 +1,5 @@
-(lang dune 2.7)
+(lang dune 3.7)
 (using experimental_building_ocaml_compiler_with_dune 0.1)
 (using coq 0.2)
-(cram enable)
+(cram enable)
+(using directory-targets 0.1)