runtest: allows to specify provers from the CLI

EasyCrypt · Dec 1, 2023 · ce354bd · ce354bd
1 parent 42a7841
commit ce354bd
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 8 deletions.
diff --git 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', '[email protected],[email protected]' ] ]
     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
@@ -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')