ocamlPackages.sail: 0.16 → 0.18

pkgs/applications/virtualization/sail-riscv/default.nix

@@ -1,77 +1,60 @@
 {
   stdenv,
   fetchFromGitHub,
-  fetchpatch,
   lib,
-  arch,
-  ocamlPackages,
-  ocaml,
+  cmake,
+  gmp,
+  pkg-config,
+  sail,
+  ninja,
   zlib,
   z3,
 }:
 
 stdenv.mkDerivation rec {
   pname = "sail-riscv";
-  version = "0.5";
+  version = "0.6";
 
   src = fetchFromGitHub {
     owner = "riscv";
     repo = pname;
     rev = version;
-    hash = "sha256-7PZNNUMaCZEBf0lOCqkquewRgZPooBOjIbGF7JlLnEo=";
+    hash = "sha256-cO0ZOr2frMMLE9NUGDxy9+KpuyBnixw6wcNzUArxDiE=";
   };
 
-  nativeBuildInputs = with ocamlPackages; [
-    ocamlbuild
-    findlib
-    ocaml
+  nativeBuildInputs = [
     z3
+    cmake
+    pkg-config
+    ninja
     sail
   ];
-  buildInputs = with ocamlPackages; [
+  buildInputs = [
     zlib
-    linksem
+    gmp
   ];
   strictDeps = true;
 
-  patches = [
-    (fetchpatch {
-      url = "https://github.com/riscv/sail-riscv/pull/250/commits/8bd37c484b83a8ce89c8bb7a001b8ae34dc4d77f.patch";
-      hash = "sha256-tDgkGhcbT6phoCAvilxMI56YUuUqQFgvh+2QduOjdMg=";
-    })
-  ];
+  postPatch = ''
+    rm -r prover_snapshots
+  '';
 
-  postPatch =
-    ''
-      rm -r prover_snapshots
-    ''
-    + lib.optionalString stdenv.hostPlatform.isDarwin ''
-      substituteInPlace Makefile --replace "-flto" ""
-    '';
-
-  makeFlags = [
-    "SAIL=sail"
-    "ARCH=${arch}"
-    "SAIL_DIR=${ocamlPackages.sail}/share/sail"
-    "LEM_DIR=${ocamlPackages.sail}/share/lem"
-  ];
-
-  installPhase = ''
-    runHook preInstall
-
-    mkdir -p $out/bin
-    cp c_emulator/riscv_sim_${arch} $out/bin
-    mkdir $out/share/
-    cp -r generated_definitions/{coq,hol4,isabelle} $out/share/
-
-    runHook postInstall
+  preBuild = ''
+    ninja \
+      riscv_sim_rv32d      \
+      riscv_sim_rv32d_rvfi \
+      riscv_sim_rv32f      \
+      riscv_sim_rv32f_rvfi \
+      riscv_sim_rv64d      \
+      riscv_sim_rv64d_rvfi \
+      riscv_sim_rv64f      \
+      riscv_sim_rv64f_rvfi
   '';
 
   meta = with lib; {
     homepage = "https://github.com/riscv/sail-riscv";
     description = "Formal specification of the RISC-V architecture, written in Sail";
     maintainers = with maintainers; [ genericnerdyusername ];
-    broken = stdenv.hostPlatform.isDarwin && stdenv.hostPlatform.isAarch64;
     license = licenses.bsd2;
   };
 }

pkgs/development/ocaml-modules/sail/default.nix

@@ -1,10 +1,13 @@
 {
   lib,
-  fetchFromGitHub,
+  stdenv,
+  darwin,
+  fetchurl,
   buildDunePackage,
   base64,
   omd,
   menhir,
+  menhirLib,
   ott,
   linenoise,
   dune-site,
@@ -13,33 +16,37 @@
   lem,
   linksem,
   yojson,
+  version ? "0.18",
 }:
 
-buildDunePackage rec {
+buildDunePackage {
   pname = "sail";
-  version = "0.16";
+  inherit version;
 
-  src = fetchFromGitHub {
-    owner = "rems-project";
-    repo = "sail";
-    rev = version;
-    hash = "sha256-HY/rgWi0S7ZiAWZF0fVIRK6fpoJ7Xp5EQcxoPRCPJ5Y=";
+  src = fetchurl {
+    url = "https://github.com/rems-project/sail/releases/download/${version}/sail-${version}.tbz";
+    hash = "sha256-/NvaFPHtWfow4j2jSr4CVHQW48KoP77uVgbhAKXtzzU=";
   };
 
   minimalOCamlVersion = "4.08";
 
-  nativeBuildInputs = [
-    makeWrapper
-    ott
-    menhir
-    lem
-  ];
+  nativeBuildInputs =
+    [
+      makeWrapper
+      ott
+      menhir
+      lem
+    ]
+    ++ lib.optionals (stdenv.hostPlatform.isDarwin && stdenv.hostPlatform.isAarch64) [
+      darwin.sigtool
+    ];
 
   propagatedBuildInputs = [
     base64
     omd
     dune-site
     linenoise
+    menhirLib
     pprint
     linksem
     yojson

pkgs/top-level/all-packages.nix

@@ -17766,12 +17766,8 @@ with pkgs;
 
   xdragon = lowPrio (callPackage ../tools/X11/xdragon { });
 
-  sail-riscv-rv32 = callPackage ../applications/virtualization/sail-riscv {
-    arch = "RV32";
-  };
-
-  sail-riscv-rv64 = callPackage ../applications/virtualization/sail-riscv {
-    arch = "RV64";
+  sail-riscv = callPackage ../applications/virtualization/sail-riscv {
+    inherit (ocamlPackages) sail;
   };
 
   timeloop = pkgs.darwin.apple_sdk_11_0.callPackage ../applications/science/computer-architecture/timeloop { };