From f8849883bc2b97a6ead2176b380a49fed81bd4a7 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 3 Jun 2024 09:02:36 +0200 Subject: [PATCH] chore(update): tools, bump OCaml to 5.x --- README.md | 2 +- .../fstar/fstar-surface-ast/FStar_String.ml | 4 +- flake.lock | 87 +++++-------------- flake.nix | 2 +- frontend/exporter/src/types/copied.rs | 12 ++- 5 files changed, 34 insertions(+), 73 deletions(-) diff --git a/README.md b/README.md index 217c96bb4..b5bbfc400 100644 --- a/README.md +++ b/README.md @@ -49,7 +49,7 @@ Note: 1. Make sure to have the following installed on your system: -- [`opam`](https://opam.ocaml.org/) (`opam switch create 4.14.1`) +- [`opam`](https://opam.ocaml.org/) (`opam switch create 5.1.1`) - [`rustup`](https://rustup.rs/) - [`nodejs`](https://nodejs.org/) - [`jq`](https://jqlang.github.io/jq/) diff --git a/engine/backends/fstar/fstar-surface-ast/FStar_String.ml b/engine/backends/fstar/fstar-surface-ast/FStar_String.ml index 45c7ba415..9dcff4a94 100644 --- a/engine/backends/fstar/fstar-surface-ast/FStar_String.ml +++ b/engine/backends/fstar/fstar-surface-ast/FStar_String.ml @@ -29,8 +29,8 @@ let get s i = BatUChar.code (BatUTF8.get s (Z.to_int i)) let collect f s = let r = ref "" in BatUTF8.iter (fun c -> r := !r ^ f (BatUChar.code c)) s; !r -let lowercase = BatString.lowercase -let uppercase = BatString.uppercase +let lowercase = BatString.lowercase_ascii +let uppercase = BatString.uppercase_ascii let escaped = BatString.escaped let index = get exception Found of int diff --git a/flake.lock b/flake.lock index 836a2c82b..ad39d86a8 100644 --- a/flake.lock +++ b/flake.lock @@ -2,21 +2,16 @@ "nodes": { "crane": { "inputs": { - "flake-compat": "flake-compat", - "flake-utils": [ - "flake-utils" - ], "nixpkgs": [ "nixpkgs" - ], - "rust-overlay": "rust-overlay" + ] }, "locked": { - "lastModified": 1693787605, - "narHash": "sha256-rwq5U8dy+a9JFny/73L0SJu1GfWwATMPMTp7D+mjHy8=", + "lastModified": 1717386774, + "narHash": "sha256-YYMGHDo4f+tu7k2q6hWNiI5C8gAN5eksb3g3EbKFf4k=", "owner": "ipetkov", "repo": "crane", - "rev": "8b4f7a4dab2120cf41e7957a28a853f45016bd9d", + "rev": "ad21f86e47a2751faa99aecd0d494be70411d5e9", "type": "github" }, "original": { @@ -25,32 +20,16 @@ "type": "github" } }, - "flake-compat": { - "flake": false, - "locked": { - "lastModified": 1673956053, - "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=", - "owner": "edolstra", - "repo": "flake-compat", - "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9", - "type": "github" - }, - "original": { - "owner": "edolstra", - "repo": "flake-compat", - "type": "github" - } - }, "flake-utils": { "inputs": { "systems": "systems" }, "locked": { - "lastModified": 1692799911, - "narHash": "sha256-3eihraek4qL744EvQXsK1Ha6C3CR7nnT8X2qWap4RNk=", + "lastModified": 1710146030, + "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", "owner": "numtide", "repo": "flake-utils", - "rev": "f9e7cf818399d17d347f847525c5a5a8032e4e44", + "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", "type": "github" }, "original": { @@ -86,11 +65,11 @@ "hacl-star": { "flake": false, "locked": { - "lastModified": 1699634660, - "narHash": "sha256-/mAi8wdlO1HHYKVj8pN/y5FUM/AwVPNazYFSy9pDlpY=", + "lastModified": 1716379562, + "narHash": "sha256-42dF8kPEiveSPgHoicxZG/CCu3IhwJhtfvVNfrLczu8=", "owner": "hacl-star", "repo": "hacl-star", - "rev": "7f42aba60b37bc011d19472284bfcd3b95c1538e", + "rev": "9149b0c26b06a8e06a0920a07c33ddd18d94c519", "type": "github" }, "original": { @@ -101,16 +80,17 @@ }, "nixpkgs": { "locked": { - "lastModified": 1694343207, - "narHash": "sha256-jWi7OwFxU5Owi4k2JmiL1sa/OuBCQtpaAesuj5LXC8w=", - "owner": "NixOS", + "lastModified": 1717402443, + "narHash": "sha256-KlFiT8xFAVy29iYJU9nBwvkC7WTfUC/jak5jNFz5wHM=", + "owner": "nixos", "repo": "nixpkgs", - "rev": "78058d810644f5ed276804ce7ea9e82d92bee293", + "rev": "c149b8818b982d612f519c7e73449d355206a89a", "type": "github" }, "original": { - "id": "nixpkgs", - "type": "indirect" + "owner": "nixos", + "repo": "nixpkgs", + "type": "github" } }, "root": { @@ -120,35 +100,10 @@ "fstar": "fstar", "hacl-star": "hacl-star", "nixpkgs": "nixpkgs", - "rust-overlay": "rust-overlay_2" + "rust-overlay": "rust-overlay" } }, "rust-overlay": { - "inputs": { - "flake-utils": [ - "crane", - "flake-utils" - ], - "nixpkgs": [ - "crane", - "nixpkgs" - ] - }, - "locked": { - "lastModified": 1693707092, - "narHash": "sha256-HR1EnynBSPqbt+04/yxxqsG1E3n6uXrOl7SPco/UnYo=", - "owner": "oxalica", - "repo": "rust-overlay", - "rev": "98ccb73e6eefc481da6039ee57ad8818d1ca8d56", - "type": "github" - }, - "original": { - "owner": "oxalica", - "repo": "rust-overlay", - "type": "github" - } - }, - "rust-overlay_2": { "inputs": { "flake-utils": [ "flake-utils" @@ -158,11 +113,11 @@ ] }, "locked": { - "lastModified": 1716862669, - "narHash": "sha256-7oTPM9lcdwiI1cpRC313B+lHawocgpY5F07N+Rbm5Uk=", + "lastModified": 1717381101, + "narHash": "sha256-TcM4+oHTSLw8neTxk/Q0beODr8YiL+oI2j0ENYnNfk4=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "47b2d15658b37716393b2463a019000dbd6ce4bc", + "rev": "07098b424d114cd2dddec40be8d5586da339fddc", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 522c67996..ed325521d 100644 --- a/flake.nix +++ b/flake.nix @@ -1,11 +1,11 @@ { inputs = { + nixpkgs.url = "github:nixos/nixpkgs"; flake-utils.url = "github:numtide/flake-utils"; crane = { url = "github:ipetkov/crane"; inputs = { nixpkgs.follows = "nixpkgs"; - flake-utils.follows = "flake-utils"; }; }; rust-overlay = { diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index 7b61f17bb..40ebbdf5d 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -1205,11 +1205,17 @@ impl<'tcx, S: ExprState<'tcx>> SInto for rustc_middle::thir::Expr<'tcx> Some(contents) => contents, None => match kind { // Introduce intermediate `Cast` from `T` to `U` when casting from a `#[repr(T)]` enum to `U` - rustc_middle::thir::ExprKind::Cast { source } if let rustc_middle::ty::TyKind::Adt(def, _) = s.thir().exprs[source].ty.kind() => { + rustc_middle::thir::ExprKind::Cast { source } + if let rustc_middle::ty::TyKind::Adt(def, _) = + s.thir().exprs[source].ty.kind() => + { let tcx = s.base().tcx; let contents = kind.sinto(s); use crate::rustc_middle::ty::util::IntTypeExt; - let repr_type = tcx.repr_options_of_def(def.did()).discr_type().to_ty(s.base().tcx); + let repr_type = tcx + .repr_options_of_def(def.did()) + .discr_type() + .to_ty(s.base().tcx); if repr_type == ty { contents } else { @@ -1220,7 +1226,7 @@ impl<'tcx, S: ExprState<'tcx>> SInto for rustc_middle::thir::Expr<'tcx> contents: Box::new(contents), hir_id, attributes: vec![], - } + }, } } }