Add Expr constructors for the Reals SMT-LIB theory
#1495
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Build Javascript | |
| # 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 | |
| # Add OPAMYES=true to the environment, this is usefull to replace `-y` option | |
| # in any opam call | |
| OPAMYES: true | |
| # Alt-Ergo's depext crashs with with-test flag to yes | |
| # # The with-test flag is set to true to force installation of deps and | |
| # # depext needed to run the alt-ergo tests | |
| # OPAMWITHTEST: true | |
| jobs: | |
| compile_and_test_js: | |
| # check if the project build in js. | |
| name: Compile AE with JsoO and test it with NodeJs | |
| runs-on: ubuntu-latest | |
| steps: | |
| # Checkout the code of the current branch | |
| - name: Checkout code | |
| uses: actions/checkout@v3 | |
| # Update apt-get database | |
| - name: Update apt-get database | |
| run: sudo apt-get update | |
| # Retrieve the opam cache with unique key | |
| # A new cache is created/used if the `.opam` files changes or | |
| # if we use another ocaml version | |
| # This action only retrieve de .opam/ directory | |
| - name: Retrieve opam cache | |
| uses: actions/cache@v3 | |
| id: cache-opam | |
| with: | |
| path: ~/.opam | |
| key: v1-${{ runner.os }}-alt-ergo-js-${{ env.OCAML_DEFAULT_VERSION }}-${{ hashFiles('*.opam') }} | |
| # Get an OCaml environment with opam installed and the proper ocaml version | |
| # opam will used opam cache environment if retrieved | |
| - name: Use OCaml ${{ env.OCAML_DEFAULT_VERSION }} | |
| uses: ocaml/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: ${{ env.OCAML_DEFAULT_VERSION }} | |
| # Install dependencies | |
| - name: Install deps | |
| run: opam exec -- make test-deps js-deps | |
| # compile Alt-Ergo with Js_of_ocaml | |
| - name: Make alt-ergo.js | |
| run: opam exec -- make js-node | |
| # Use Node Js actions | |
| - uses: actions/setup-node@v2 | |
| with: | |
| node-version: '14' | |
| # Run simple test with node | |
| # TODO: use gentest to run more tests there. | |
| - name: Run simple example with node | |
| run: opam exec -- node alt-ergo.js tests/everything/f1.ae | |
| # 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" | |
| # 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" |