Playground: give eq its own files and examples

.github/workflows/pages.yml

@@ -0,0 +1,82 @@
+# Deploys the site in site/ to GitHub Pages: the landing page plus the
+# playground, which runs AutoQ compiled to WebAssembly (wasm/build.sh).
+#
+# One-time setup before the first run: in the repository settings, open
+# Settings -> Pages -> Build and deployment and set Source to "GitHub Actions".
+# Without that, the Configure Pages step fails. (Passing `enablement: true` to
+# actions/configure-pages would enable Pages automatically, but it needs a
+# token with admin rights; the default GITHUB_TOKEN does not have them.)
+#
+# After the first deploy, compare the page_url printed by the deploy step with
+# the canonical and og: URLs in site/index.html (https://fmlab-iis.github.io/AutoQ/).
+#
+# The first run builds Z3 and the ANTLR runtime for WebAssembly, which takes
+# a while; later runs restore them from the cache.
+name: Deploy landing page
+
+on:
+  push:
+    branches: [main]
+    paths:
+      - "site/**"
+      - "wasm/**"
+      - "src/**"
+      - "include/**"
+      - "cli/**"
+      - "CMakeLists.txt"
+      - ".github/workflows/pages.yml"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+concurrency:
+  group: "pages"
+  cancel-in-progress: false
+
+env:
+  EMSDK_VERSION: "6.0.12"
+
+jobs:
+  deploy:
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0  # autoq -v reports the commit from git describe
+
+      - name: Install Boost headers
+        run: sudo apt-get update && sudo apt-get install -y libboost-dev
+
+      - name: Install Emscripten
+        run: |
+          git clone --depth 1 https://github.com/emscripten-core/emsdk.git "$RUNNER_TEMP/emsdk"
+          "$RUNNER_TEMP/emsdk/emsdk" install "$EMSDK_VERSION"
+          "$RUNNER_TEMP/emsdk/emsdk" activate "$EMSDK_VERSION"
+
+      - name: Cache Z3 and ANTLR for WebAssembly
+        uses: actions/cache@v4
+        with:
+          path: build-wasm/deps
+          key: wasm-deps-${{ env.EMSDK_VERSION }}-${{ hashFiles('wasm/build.sh') }}
+
+      - name: Build the playground (AutoQ to WebAssembly)
+        run: |
+          source "$RUNNER_TEMP/emsdk/emsdk_env.sh"
+          wasm/build.sh site/playground
+
+      - name: Configure Pages
+        uses: actions/configure-pages@v5
+      - name: Upload site
+        uses: actions/upload-pages-artifact@v3
+        with:
+          path: site
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v4

.gitignore

@@ -28,4 +28,8 @@ POPL24/TABLES/Algorithms/*.pdf
 POPL24/TABLES/Algorithms/*.tex
 POPL24/TABLES/Algorithms/*.log
 POPL24/TABLES/Algorithms/*.aux
-benchmark*/_others/**
+benchmark*/_others/**
+# WebAssembly build (wasm/build.sh); the playground binaries are built in CI
+build-wasm/
+site/playground/autoq.js
+site/playground/autoq.wasm

CMakeLists.txt

@@ -158,17 +158,26 @@ include(CTest)
 #                                DEPENDENCIES
 ##############################################################################
 
-# Boost
-set(Boost_USE_MULTITHREADED OFF)
-find_package(Boost 1.71.0...1.89.0 CONFIG COMPONENTS # 1.89.0 is for macOS on GitHub CI
-  filesystem
-#   system
-  unit_test_framework
-  REQUIRED)
-# IMPORTANT CHANGE: https://github.com/facebook/folly/issues/2489
-# Boost.System has been header-only since 1.69.
-# If someone increases minimum Boost to 1.71 then can just remove the system component.
-include_directories(${Boost_INCLUDE_DIRS})
+if (EMSCRIPTEN)
+  # WebAssembly build (wasm/build.sh). Only header-only parts of Boost are
+  # used, and Z3 and the ANTLR runtime are prebuilt static libraries.
+  set(AUTOQ_WASM_BOOST_INCLUDE "" CACHE PATH "Directory containing the boost/ headers")
+  set(AUTOQ_WASM_Z3_LIB "" CACHE FILEPATH "Z3 static library built with Emscripten")
+  set(AUTOQ_WASM_ANTLR4_LIB "" CACHE FILEPATH "ANTLR4 C++ runtime static library built with Emscripten")
+  include_directories(${AUTOQ_WASM_BOOST_INCLUDE})
+else()
+  # Boost
+  set(Boost_USE_MULTITHREADED OFF)
+  find_package(Boost 1.71.0...1.89.0 CONFIG COMPONENTS # 1.89.0 is for macOS on GitHub CI
+    filesystem
+  #   system
+    unit_test_framework
+    REQUIRED)
+  # IMPORTANT CHANGE: https://github.com/facebook/folly/issues/2489
+  # Boost.System has been header-only since 1.69.
+  # If someone increases minimum Boost to 1.71 then can just remove the system component.
+  include_directories(${Boost_INCLUDE_DIRS})
+endif()
 include_directories(../include/z3)
 
 # Doxygen - voluntary
@@ -189,6 +198,8 @@ endif()
 # Process subdirectories
 add_subdirectory(src)
 add_subdirectory(cli)
-add_subdirectory(unit_tests)
+if (NOT EMSCRIPTEN)
+  add_subdirectory(unit_tests)
+endif()
 # add_subdirectory(parametric)
 # add_subdirectory(tests)

cli/CMakeLists.txt

@@ -34,3 +34,23 @@ endforeach()
 if (MAKE_STATIC_AUTOQ)
   SET(CMAKE_CXX_LINK_EXECUTABLE "${CMAKE_CXX_LINK_EXECUTABLE} -static")
 endif()
+
+if (EMSCRIPTEN)
+  # WebAssembly build (wasm/build.sh): an ES module exporting createAutoQ().
+  # The playground (site/playground) writes the input files into the
+  # in-memory filesystem and runs main() through callMain() on a fresh
+  # instance per run.
+  target_link_options(autoq PRIVATE
+    -fwasm-exceptions
+    -sMODULARIZE=1
+    -sEXPORT_ES6=1
+    -sEXPORT_NAME=createAutoQ
+    -sENVIRONMENT=web,worker,node
+    -sINVOKE_RUN=0
+    -sEXIT_RUNTIME=1
+    -sALLOW_MEMORY_GROWTH=1
+    -sMAXIMUM_MEMORY=4GB
+    -sSTACK_SIZE=8MB
+    -sFORCE_FILESYSTEM=1
+    -sEXPORTED_RUNTIME_METHODS=callMain,FS)
+endif()

cli/autoq.cc

@@ -234,7 +234,9 @@ static void run_verification(const std::string& pre, const std::string& post, co
 int main(int argc, char **argv) {
 try {
     // set_timeout(600);
+#ifndef __EMSCRIPTEN__  // WebAssembly has no floating-point exception traps
     feenableexcept(FE_ALL_EXCEPT & ~FE_INEXACT);
+#endif
 
     CLI::App app{"AutoQ 2.0: An automata-based C++ tool for quantum program verification."};
     std::string pre, circuit, post, circuit1, circuit2;

site/assets/fonts/OFL.txt

@@ -0,0 +1,98 @@
+The web fonts in this folder are subsets served by Google Fonts and are
+used under the SIL Open Font License, Version 1.1:
+
+Bodoni Moda: Copyright 2020 The Bodoni Moda Project Authors (https://github.com/indestructible-type/Bodoni)
+Instrument Sans: Copyright 2022 The Instrument Sans Project Authors (https://github.com/Instrument/instrument-sans)
+JetBrains Mono: Copyright 2020 The JetBrains Mono Project Authors (https://github.com/JetBrains/JetBrainsMono)
+Noto Sans Math: Copyright 2022 Google LLC. All Rights Reserved.
+Noto Sans Mono: Copyright 2022 The Noto Project Authors (https://github.com/notofonts/latin-greek-cyrillic)
+
+The license is copied below, and is also available with a FAQ at:
+https://openfontlicense.org
+
+-----------------------------------------------------------
+SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
+-----------------------------------------------------------
+
+PREAMBLE
+The goals of the Open Font License (OFL) are to stimulate worldwide
+development of collaborative font projects, to support the font creation
+efforts of academic and linguistic communities, and to provide a free and
+open framework in which fonts may be shared and improved in partnership
+with others.
+
+The OFL allows the licensed fonts to be used, studied, modified and
+redistributed freely as long as they are not sold by themselves. The
+fonts, including any derivative works, can be bundled, embedded, 
+redistributed and/or sold with any software provided that any reserved
+names are not used by derivative works. The fonts and derivatives,
+however, cannot be released under any other type of license. The
+requirement for fonts to remain under this license does not apply
+to any document created using the fonts or their derivatives.
+
+DEFINITIONS
+"Font Software" refers to the set of files released by the Copyright
+Holder(s) under this license and clearly marked as such. This may
+include source files, build scripts and documentation.
+
+"Reserved Font Name" refers to any names specified as such after the
+copyright statement(s).
+
+"Original Version" refers to the collection of Font Software components as
+distributed by the Copyright Holder(s).
+
+"Modified Version" refers to any derivative made by adding to, deleting,
+or substituting -- in part or in whole -- any of the components of the
+Original Version, by changing formats or by porting the Font Software to a
+new environment.
+
+"Author" refers to any designer, engineer, programmer, technical
+writer or other person who contributed to the Font Software.
+
+PERMISSION & CONDITIONS
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of the Font Software, to use, study, copy, merge, embed, modify,
+redistribute, and sell modified and unmodified copies of the Font
+Software, subject to the following conditions:
+
+1) Neither the Font Software nor any of its individual components,
+in Original or Modified Versions, may be sold by itself.
+
+2) Original or Modified Versions of the Font Software may be bundled,
+redistributed and/or sold with any software, provided that each copy
+contains the above copyright notice and this license. These can be
+included either as stand-alone text files, human-readable headers or
+in the appropriate machine-readable metadata fields within text or
+binary files as long as those fields can be easily viewed by the user.
+
+3) No Modified Version of the Font Software may use the Reserved Font
+Name(s) unless explicit written permission is granted by the corresponding
+Copyright Holder. This restriction only applies to the primary font name as
+presented to the users.
+
+4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
+Software shall not be used to promote, endorse or advertise any
+Modified Version, except to acknowledge the contribution(s) of the
+Copyright Holder(s) and the Author(s) or with their explicit written
+permission.
+
+5) The Font Software, modified or unmodified, in part or in whole,
+must be distributed entirely under this license, and must not be
+distributed under any other license. The requirement for fonts to
+remain under this license does not apply to any document created
+using the Font Software.
+
+TERMINATION
+This license becomes null and void if any of the above conditions are
+not met.
+
+DISCLAIMER
+THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
+OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
+COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
+DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
+OTHER DEALINGS IN THE FONT SOFTWARE.