diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c1c9ecbd83..2d264be5c8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -21,7 +21,7 @@ jobs: opam pin add -n easycrypt . opam install --deps-only easycrypt - name: Compile EasyCrypt - run: opam config exec -- make + run: opam exec -- make compile-nix: name: EasyCrypt compilation (nix) @@ -61,15 +61,15 @@ jobs: opam pin add -n easycrypt . opam install --deps-only easycrypt - name: Compile EasyCrypt - run: opam config exec -- make + run: opam exec -- make - name: Detect SMT provers run: | rm -f ~/.why3.conf - opam config exec -- ./ec.native why3config -why3 ~/.why3.conf + opam exec -- ./ec.native why3config -why3 ~/.why3.conf - name: Compile Library (${{ matrix.target }}) env: TARGET: ${{ matrix.target }} - run: opam config exec -- make $TARGET + run: opam exec -- make $TARGET - uses: actions/upload-artifact@v3 name: Upload report.log if: always() @@ -87,7 +87,7 @@ jobs: strategy: fail-fast: false matrix: - target: [ [ 'jasmin-eclib', 'jasmin-lang/jasmin', 'eclib', 'tests.config', 'jasmin' ] ] + target: [ [ 'jasmin-eclib', 'jasmin-lang/jasmin', 'eclib', 'tests.config', 'jasmin', 'Z3@4.8,Alt-Ergo@2.4' ] ] steps: - uses: actions/checkout@v3 with: @@ -102,14 +102,14 @@ jobs: opam pin add -n easycrypt easycrypt opam install --deps-only easycrypt - name: Compile & Install EasyCrypt - run: opam config exec -- make -C easycrypt build install + run: opam exec -- make -C easycrypt build install - name: Detect SMT provers run: | rm -f ~/.why3.conf ~/.config/easycrypt/why3.conf - opam config exec -- easycrypt why3config + opam exec -- easycrypt why3config - name: Compile project working-directory: project/${{ matrix.target[2] }} - run: opam config exec -- ec-runtest ${{ matrix.target[3] }} ${{ matrix.target[4] }} + run: opam exec -- ec-runtest --provers="{{ matrix.target[5] }}" ${{ matrix.target[3] }} ${{ matrix.target[4] }} - uses: actions/upload-artifact@v3 name: Upload report.log if: always() diff --git a/scripts/testing/runtest b/scripts/testing/runtest index ee77f5ff7d..fd7639f126 100755 --- a/scripts/testing/runtest +++ b/scripts/testing/runtest @@ -114,6 +114,13 @@ def _options(): default = False, help = 'add timing statistics') + parser.add_option( + '', '--provers', + action = 'store', + metavar = 'PROVERS', + default = None, + help = 'Select a set of provers') + parser.add_option( '', '--report', action = 'store', @@ -138,6 +145,7 @@ def _options(): options.timeout = cmdopt.timeout options.timing = cmdopt.timing options.jobs = cmdopt.jobs + options.provers = cpdopt.provers options.report = cmdopt.report defaults = dict( @@ -681,6 +689,9 @@ async def _run_all(options, allscripts, listener : Listener): command = [options.bin] + options.args + config.args if options.timeout: command.extend(['-timeout', str(options.timeout)]) + if options.provers: + for prover in options.provers.split(','): + command.extend(['-p', x]) if options.timing: tfilename = os.path.join( TIMING_DIR, os.path.splitext(config.filename)[0] + '.stats')