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 05e2f48d4d..ade2f97306 100755 --- a/scripts/testing/runtest +++ b/scripts/testing/runtest @@ -121,6 +121,13 @@ def _options(): default = None, help = 'Why3 configuration file') + parser.add_option( + '', '--provers', + action = 'store', + metavar = 'PROVERS', + default = None, + help = 'Select a set of provers') + parser.add_option( '', '--report', action = 'store', @@ -146,6 +153,7 @@ def _options(): options.timing = cmdopt.timing options.why3 = cmdopt.why3 options.jobs = cmdopt.jobs + options.provers = cpdopt.provers options.report = cmdopt.report defaults = dict( @@ -691,6 +699,9 @@ async def _run_all(options, allscripts, listener : Listener): command.extend(['-timeout', str(options.timeout)]) if options.why3: command.extend(['-why3', options.why3]) + 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')