Bump the version of Dolmen to 0.10 (#1149)

* Bump the version of Dolmen to 0.10 The new version of Dolmen has been released yesterday! This commit updates the lock file and remove the hotfix for the issue #747 as the appropriate fix is included in the last release of Dolmen. * Dolmen 0.10 @ nix --------- Co-authored-by: Basile Clément <[email protected]>
OCamlPro · Jul 9, 2024 · 01f280a · 01f280a
1 parent a7cf228
commit 01f280a
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 51 deletions.
diff --git a/alt-ergo-lib.opam.locked b/alt-ergo-lib.opam.locked
@@ -27,9 +27,9 @@ depends: [
   "conf-zlib" {= "1"}
   "cppo" {= "1.6.9"}
   "csexp" {= "1.5.2"}
-  "dolmen" {= "dev"}
-  "dolmen_loop" {= "dev"}
-  "dolmen_type" {= "dev"}
+  "dolmen" {= "0.10"}
+  "dolmen_loop" {= "0.10"}
+  "dolmen_type" {= "0.10"}
   "dune" {= "3.11.1"}
   "dune-build-info" {= "3.11.1"}
   "dune-configurator" {= "3.11.1"}
@@ -86,18 +86,6 @@ conflicts: [
   "result" {< "1.5"}
 ]
 pin-depends: [
-  [
-    "dolmen.dev"
-    "git+https://github.com/Gbury/dolmen.git#5e22e653ec376336bbbed50aca4946db8edbc90f"
-  ]
-  [
-    "dolmen_loop.dev"
-    "git+https://github.com/Gbury/dolmen.git#5e22e653ec376336bbbed50aca4946db8edbc90f"
-  ]
-  [
-    "dolmen_type.dev"
-    "git+https://github.com/Gbury/dolmen.git#5e22e653ec376336bbbed50aca4946db8edbc90f"
-  ]
   [
     "js_of_ocaml.5.4.0"
     "https://github.com/ocsigen/js_of_ocaml/releases/download/5.4.0/js_of_ocaml-5.4.0.tbz"

diff --git a/nix/sources.json b/nix/sources.json
@@ -1,14 +1,27 @@
 {
     "dolmen": {
-        "branch": "5e22e653ec376336bbbed50aca4946db8edbc90f",
+        "branch": "v0.10",
         "description": "Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction",
         "homepage": "",
         "owner": "Gbury",
         "repo": "dolmen",
-        "rev": "5e22e653ec376336bbbed50aca4946db8edbc90f",
-        "sha256": "1wmmq3x8zcp2zh3xpchjvhyj85qbydrpd2cf9awn4nxxaqi06yjn",
+        "rev": "c33632daab31fb3bb719031169baa6c984bb860f",
+        "sha256": "1vvlg72sbwmpnh0kvwkbvnxxgwrdqcy5adqp26n3hpq3mix4sp7d",
         "type": "tarball",
-        "url": "https://github.com/Gbury/dolmen/archive/5e22e653ec376336bbbed50aca4946db8edbc90f.tar.gz",
+        "url": "https://github.com/Gbury/dolmen/archive/c33632daab31fb3bb719031169baa6c984bb860f.tar.gz",
+        "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz",
+        "version": "0.10"
+    },
+    "landmarks": {
+        "branch": "b0c753cd2a4c4aa00dffdd3be187d8ed592fabf7",
+        "description": "A Simple Profiling Library for OCaml",
+        "homepage": "https://github.com/LexiFi/landmarks",
+        "owner": "LexiFi",
+        "repo": "landmarks",
+        "rev": "b0c753cd2a4c4aa00dffdd3be187d8ed592fabf7",
+        "sha256": "02lr5grxcczikkdvz75vhrpgpfnq7z9svzgxxvimll0ijplgp6js",
+        "type": "tarball",
+        "url": "https://github.com/LexiFi/landmarks/archive/b0c753cd2a4c4aa00dffdd3be187d8ed592fabf7.tar.gz",
         "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz",
         "version": "dev"
     },
@@ -49,18 +62,5 @@
         "url": "https://github.com/Armael/pp_loc/archive/d8162fd289849ea2f4125054ab88540416bdaa25.tar.gz",
         "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz",
         "version": "2.1.0"
-    },
-    "landmarks": {
-      "branch": "b0c753cd2a4c4aa00dffdd3be187d8ed592fabf7",
-      "description": "A Simple Profiling Library for OCaml",
-      "homepage": "https://github.com/LexiFi/landmarks",
-      "owner": "LexiFi",
-      "repo": "landmarks",
-      "rev": "b0c753cd2a4c4aa00dffdd3be187d8ed592fabf7",
-      "sha256": "02lr5grxcczikkdvz75vhrpgpfnq7z9svzgxxvimll0ijplgp6js",
-      "type": "tarball",
-      "url": "https://github.com/LexiFi/landmarks/archive/b0c753cd2a4c4aa00dffdd3be187d8ed592fabf7.tar.gz",
-      "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz",
-      "version": "dev"
     }
 }
diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
@@ -1081,25 +1081,7 @@ let rec mk_expr
             semantic_trigger ~loc ?var trigger
 
           (* Unary functions from FixedSizeBitVectors theory *)
-          | B.Bitv_extract { i; j; _ }, [ x ] ->
-            let t = mk x in
-            let _ =
-              (* This temporary fix throws aways ill-typed expression produced
-                 by Dolmen 0.9. See issue
-                 https://github.com/Gbury/dolmen/issues/174.
-                 This code will be removed as soon as the next version of
-                 Dolmen has been released. See issue
-                 https://github.com/OCamlPro/alt-ergo/issues/748. *)
-              match E.type_info t with
-              | Tbitv m ->
-                if m <= i then
-                  Fmt.failwith
-                    "%alength of bitvector extraction exceeds the length\
-                     of its argument."
-                    Loc.report loc
-              | _ -> assert false
-            in
-            E.BV.extract i j t
+          | B.Bitv_extract { i; j; _ }, [ x ] -> E.BV.extract i j (mk x)
           | B.Bitv_not _, [ x ] -> E.BV.bvnot (mk x)
           | B.Bitv_neg _, [ x ] -> E.BV.bvneg (mk x)