Bdep

config/tests.config

@@ -8,7 +8,7 @@ exclude = theories/prelude
 
 [test-examples]
 okdirs  = !examples
-exclude = examples/MEE-CBC examples/old examples/old/list-ddh !examples/incomplete examples/to-port
+exclude = examples/MEE-CBC examples/exclude examples/old examples/old/list-ddh !examples/incomplete examples/to-port
 
 [test-mee-cbc]
 okdirs = examples/MEE-CBC

dune

@@ -1,4 +1,9 @@
-(dirs src theories examples scripts)
+(env
+ (dev     (flags -rectypes -warn-error -a+31 -w +28+33-9-23-32-58-67-69))
+ (release (flags -rectypes -warn-error -a+31 -w +28+33-9-23-32-58-67-69)
+          (ocamlopt_flags -O3 -unbox-closures)))
+
+(dirs src libs theories examples scripts)
 
 (install
   (section (site (easycrypt commands)))

dune-project

@@ -1,5 +1,5 @@
-(lang dune 3.6)
-(using menhir 2.0)
+(lang dune 3.13)
+(using menhir 3.0)
 (using dune_site 0.1)
 
 (wrapped_executables false)
@@ -10,17 +10,24 @@
 
 (package
  (name easycrypt)
- (sites (lib theories) (libexec commands))
+ (sites (lib theories) (lib specs) (libexec commands))
  (depends
   (ocaml (>= 4.08.0))
   (batteries (>= 3))
+  bitwuzla
   (camlp-streams (>= 5))
   camlzip
-  (dune (>= 3.6))
+  cmdliner
+  dune
   dune-build-info
   dune-site
+  hex
+  iter
   (ocaml-inifiles (>= 1.2))
   (pcre (>= 7))
+  ppx_deriving
+  ppx_deriving_yojson
+  (progress (>= 0.2))
   (why3 (and (>= 1.7.0) (< 1.8)))
   yojson
   (zarith (>= 1.10))

easycrypt.opam

@@ -2,13 +2,20 @@
 depends: [
   "ocaml" {>= "4.08.0"}
   "batteries" {>= "3"}
+  "bitwuzla"
   "camlp-streams" {>= "5"}
   "camlzip"
-  "dune" {>= "3.6" & >= "3.6"}
+  "cmdliner"
+  "dune" {>= "3.13"}
   "dune-build-info"
   "dune-site"
+  "hex"
+  "iter"
   "ocaml-inifiles" {>= "1.2"}
   "pcre" {>= "7"}
+  "ppx_deriving"
+  "ppx_deriving_yojson"
+  "progress" {>= "0.2"}
   "why3" {>= "1.7.0" & < "1.8"}
   "yojson"
   "zarith" {>= "1.10"}

easycrypt.project

@@ -1,4 +1,6 @@
 [general]
 provers = Alt-Ergo@2.4
-provers = CVC5@1.0
-provers = Z3@4.12
+provers = CVC4@1.8
+provers = Z3@4.8
+
+rdirs = Jasmin:jasmin/eclib