Add WebAssembly build job to CI workflow (cvc5#10278)

Co-authored-by: Daniel Larraz <[email protected]>

.github/actions/install-dependencies/action.yml

@@ -6,8 +6,12 @@ inputs:
   windows-build:
     default: false
     type: boolean
+  wasm-build:
+    default: false
+    type: boolean
   shell:
     default: bash
+
 runs:
   using: composite
   steps:
@@ -57,6 +61,21 @@ runs:
         sudo update-alternatives --set x86_64-w64-mingw32-g++ /usr/bin/x86_64-w64-mingw32-g++-posix
         echo "::endgroup::"
 
+    - name: Install software for WebAssembly compilation
+      # Boolean inputs are actually strings:
+      # https://github.com/actions/runner/issues/1483
+      if: inputs.wasm-build == 'true'
+      shell: bash
+      run: |
+        echo "::group::Install software for WebAssembly compilation"
+        sudo apt-get update
+        git clone https://github.com/emscripten-core/emsdk.git
+        cd emsdk/
+        ./emsdk install '3.1.18'
+        ./emsdk activate '3.1.18'
+        echo "$(pwd)" >> $GITHUB_PATH
+        echo "$(pwd)/upstream/emscripten" >> $GITHUB_PATH
+
     - name: Install Windows software
       if: runner.os == 'Windows' && inputs.windows-build == 'true'
       uses: msys2/setup-msys2@v2

.github/workflows/ci.yml

@@ -81,6 +81,14 @@ jobs:
             strip-bin: x86_64-w64-mingw32-strip
             windows-build: true
 
+          - name: wasm:production
+            os: ubuntu-20.04
+            config: production --static --static-binary --auto-download --wasm=JS --wasm-flags='-s MODULARIZE'
+            cache-key: productionwasm
+            wasm-build: true
+            build-shared: false
+            build-static: true
+
           - name: ubuntu:production-clang
             os: ubuntu-20.04
             env: CC=clang CXX=clang++
@@ -123,6 +131,7 @@ jobs:
       with:
         with-documentation: ${{ matrix.build-documentation }}
         windows-build: ${{ matrix.windows-build }}
+        wasm-build: ${{ matrix.wasm-build }}
         shell: ${{ matrix.shell }}
 
     - name: Setup caches

INSTALL.rst

@@ -95,7 +95,18 @@ code).
 which modifies how the wasm and glue code are built and how they behave. An ``-s``
 should precede each flag.
 
-For example, to generate modularized glue code, use:
+For example, to generate a HTML page, use:
+
+.. code:: bash
+
+  ./configure.sh --static --static-binary --auto-download --wasm=HTML --name=prod
+
+  cd prod
+  make            # use -jN for parallel build with N threads
+
+After that, you can run ``python -m http.server`` within ``prod/bin``, open http://0.0.0.0:8000/cvc5.html with Chrome to visualize the page generated by Emscripten, write down a valid SMTLIB input, and press ESC twice to obtain its output.
+
+On the other hand, to generate a modularized glue code to be imported by custom web pages, use:
 
 .. code:: bash
 

cmake/FindCaDiCaL.cmake

@@ -116,6 +116,11 @@ if(NOT CaDiCaL_FOUND_SYSTEM)
     set(make_cmd "make")
   endif()
 
+  set(USE_EMAR "")
+  if(NOT(WASM STREQUAL "OFF"))
+    set(USE_EMAR  "-e s,ar rc,emar rc,")
+  endif()
+
   ExternalProject_Add(
     CaDiCaL-EP
     ${COMMON_EP_CONFIG}
@@ -128,7 +133,7 @@ if(NOT CaDiCaL_FOUND_SYSTEM)
             <SOURCE_DIR>/build/makefile
     COMMAND
       sed -i.orig -e "s,@CXX@,${CMAKE_CXX_COMPILER}," -e
-      "s,@CXXFLAGS@,${CXXFLAGS}," -e "s,@MAKEFLAGS@,,"
+      "s,@CXXFLAGS@,${CXXFLAGS}," -e "s,@MAKEFLAGS@,," ${USE_EMAR}
       <SOURCE_DIR>/build/makefile
     BUILD_COMMAND ${make_cmd} -C <SOURCE_DIR>/build libcadical.a
     INSTALL_COMMAND ${CMAKE_COMMAND} -E copy <SOURCE_DIR>/build/libcadical.a