ci: test extraction to EasyCrypt

.gitlab-ci.yml

@@ -226,6 +226,31 @@ libjade-extract-to-ec:
     paths:
     - libjade-main/proof/check.tar.gz
 
+test-extract-to-ec:
+  stage: test
+  parallel:
+    matrix:
+      - EASYCRYPT_REF: [release, dev]
+  variables:
+    EXTRA_NIX_ARGUMENTS: --arg ocamlDeps true --arg testDeps true --argstr ecRef $EASYCRYPT_REF
+    WHY3_CONF: $CI_PROJECT_DIR/why3.conf
+    ECARGS: -why3 $WHY3_CONF -I Jasmin:$CI_PROJECT_DIR/eclib
+    JSJOBS: $(NIX_BUILD_CORES)
+  extends: .common
+  needs:
+  - coq
+  - ocaml
+  dependencies:
+  - coq
+  - ocaml
+  script:
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'easycrypt why3config -why3 $WHY3_CONF'
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -C compiler CHECKCATS=extraction check'
+  artifacts:
+    when: always
+    paths:
+    - compiler/report.log
+
 push-compiler-code:
   stage: deploy
   environment: deployment

CHANGELOG.md

@@ -107,6 +107,11 @@
 
 - Using option `-oec` without option `-ec` extracts all functions.
 
+- Extraction to EasyCrypt is now tested in continuous integration
+  ([PR #259](https://github.com/jasmin-lang/jasmin/pull/259);
+  fixes [#136](https://github.com/jasmin-lang/jasmin/issues/136),
+  fixes [#104](https://github.com/jasmin-lang/jasmin/issues/104)).
+
 # Jasmin 22.0
 
 This release is the result of more than two years of active development. It thus

compiler/scripts/extract-and-check

@@ -13,5 +13,5 @@ set -x
 $(dirname $0)/../jasminc.native -oecarray ${DIR} -oec ${EC} "$@"
 $(dirname $0)/../jasminc.native -oecarray ${DIR} -CT -oec ${CT} "$@"
 
-easycrypt ${EC}
-easycrypt ${CT}
+easycrypt ${ECARGS} ${EC}
+easycrypt ${ECARGS} ${CT}