katrinafyi · katrinafyi · Jul 28, 2025 · Jul 28, 2025 · Jul 28, 2025 · Jul 28, 2025
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -22,7 +22,7 @@ jobs:
     runs-on: ubuntu-24.04
     steps:
     - uses: actions/checkout@v4
-    - uses: cachix/install-nix-action@v25
+    - uses: cachix/install-nix-action@v31
     - run: nix build .#update
     - run: nix run .#update -- check
 
@@ -37,7 +37,7 @@ jobs:
           [aslp, bap-aslp, bap-primus, basil,
           retdec-uq-pac, asl-translator,
           gtirb-semantics, ddisasm,
-          retdec5, remill, alive2-aslp, alive2-regehr,
+          retdec5, remill, alive2-regehr,
           aslp_web, godbolt, aslp-server, aslp_offline,
           bnfc-treesitter,
         ]
@@ -47,7 +47,7 @@ jobs:
       run: { shell: "bash -ex -o pipefail {0}" }
     steps:
     - uses: actions/checkout@v4
-    - uses: cachix/install-nix-action@v25
+    - uses: cachix/install-nix-action@v31
     - uses: cachix/cachix-action@v14
       with:
         name: pac-nix

diff --git a/.github/workflows/monthly.yml b/.github/workflows/monthly.yml
@@ -18,7 +18,7 @@ jobs:
 
     steps:
     - uses: actions/checkout@v4
-    - uses: cachix/install-nix-action@v25
+    - uses: cachix/install-nix-action@v31
     - uses: cachix/cachix-action@v14
       with: { name: pac-nix, authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' }
 

diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml
@@ -16,15 +16,15 @@ jobs:
       fail-fast: false
       matrix:
         pkg: [asli, bap-asli-plugin, bap-primus, basil, gtirb-semantics,
-              asl-translator, alive2-aslp, alive2-regehr, aslp_web, compiler-explorer,
+              asl-translator, alive2-regehr, aslp_web, compiler-explorer,
               aslp-cpp, aslp-server, aslp_client_server_ocaml, bnfc-treesitter
         ]
 
     runs-on: ubuntu-24.04
 
     steps:
     - uses: actions/checkout@v4
-    - uses: cachix/install-nix-action@v25
+    - uses: cachix/install-nix-action@v31
     - uses: cachix/cachix-action@v14
       with: { name: pac-nix, authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' }
 

diff --git a/README.md b/README.md
@@ -27,8 +27,8 @@ For users of tools, the main packages are:
 - **[aslp][]**: the ASLp partial evaluator with ARM's MRA (provides `aslp` and `aslp-server`),
 - **[basil][]**: the Basil tool for analysis and transpilation to Boogie code (provides `basil`),
 - **[gtirb-semantics][]**: inserts instruction semantics from ASLp into the GTIRB from ddisasm (provides `gtirb-semantics`, `debug-gts.py`, and `proto-json.py`), and
-- **[bap-aslp][]**[^1]: a version of official BAP with a bundled ASLp plugin (this is the preferred BAP and provides the `bap` executable),
-- **[alive2-aslp][]**: a fork of [regehr/alive2][alive2-regehr], using Aslp to provide semantics for translation validation of the LLVM Aarch64 backend (provides `backend-tv`, others), and
+- **[bap-aslp][]**[^1]: a version of official BAP with a bundled ASLp plugin (this is the preferred BAP and provides the `bap` executable), and
+<!-- - **[alive2-aslp][]**: a fork of [regehr/alive2][alive2-regehr], using Aslp to provide semantics for translation validation of the LLVM Aarch64 backend (provides `backend-tv`, others), and -->
 - **[aslp-web][]**: a website for using the ASLp partial evaluator within the browser.
 
 These packages are each defined in a .nix file of the same name,
@@ -37,7 +37,7 @@ built into a package set in pkgs.nix.
 
 We also package some related third-party tools (without endorsement from their authors):
 - **[ddisasm][]**: GrammaTech's datalog disassembler (provides `ddisasm`),
-- **[alive2-regehr][]**: a fork of [AliveToolkit/alive2][alive2], performs translation validation of LLVM's Aarch64 backend by lifting MCInst back to LLVM IR (provides `backend-tv`, others).
+- **[alive2-regehr][]**: a fork of [AliveToolkit/alive2][alive2], performs translation validation of LLVM's backends by lifting MCInst back to LLVM IR (provides `backend-tv`, others).
 
 
 [aslp]: https://github.com/UQ-PAC/aslp

diff --git a/aslp/aslp-cpp.nix b/aslp/aslp-cpp.nix
@@ -4,9 +4,7 @@
 , cmake
 }:
 
-let
-  stdenv' = if stdenv.isDarwin then clang17Stdenv else stdenv;
-in stdenv'.mkDerivation {
+stdenv.mkDerivation {
   pname = "aslp-cpp";
   version = "0.1.5-unstable-2026-05-29";
 

diff --git a/aslp/overlay.nix b/aslp/overlay.nix
@@ -4,12 +4,12 @@ final: prev:
   aslp-cpp = prev.callPackage ./aslp-cpp.nix { };
 
   inherit (final.ocamlPackages_pac) aslp asli;
-  inherit (final.ocamlPackages_pac_5) aslp_web;
-  inherit (final.ocamlPackages_pac_5) aslp-server;
-  inherit (final.ocamlPackages_pac_5) aslp_client_server_ocaml;
-  inherit (final.ocamlPackages_pac_5) aslp_offline;
-  inherit (final.ocamlPackages_pac_5) aslp_offline_js;
-  inherit (final.ocamlPackages_pac_5) aslp_lifter_ocaml;
+  inherit (final.ocamlPackages_pac) aslp_web;
+  inherit (final.ocamlPackages_pac) aslp-server;
+  inherit (final.ocamlPackages_pac) aslp_client_server_ocaml;
+  inherit (final.ocamlPackages_pac) aslp_offline;
+  inherit (final.ocamlPackages_pac) aslp_offline_js;
+  inherit (final.ocamlPackages_pac) aslp_lifter_ocaml;
 
   overlay_ocamlPackages = ofinal: oprev: {
     asli = ofinal.callPackage ./asli.nix { inherit (final) z3; ocaml_z3 = ofinal.z3; };
@@ -27,48 +27,33 @@ final: prev:
     aslp_client_server_ocaml = ofinal.callPackage ./aslp_client_server_ocaml.nix { };
 
     mlbdd = ofinal.callPackage ./mlbdd.nix { };
-    cohttp = oprev.cohttp.overrideAttrs (p: rec {
-      version = "6.0.0";
-      src = final.fetchurl {
-        url = "https://github.com/mirage/ocaml-cohttp/releases/download/v${version}/cohttp-${version}.tbz";
-        hash = "sha256-VMw0rxKLNC9K5gimaWUNZmYf/dUDJQ5N6ToaXvHvIqk=";
-      };
-      propagatedBuildInputs = p.propagatedBuildInputs ++ [ ofinal.cohttp-http ofinal.logs ];
-      doCheck = false;
-    });
+    # cohttp = oprev.cohttp.overrideAttrs (p: rec {
+    #   version = "6.0.0";
+    #   src = final.fetchurl {
+    #     url = "https://github.com/mirage/ocaml-cohttp/releases/download/v${version}/cohttp-${version}.tbz";
+    #     hash = "sha256-VMw0rxKLNC9K5gimaWUNZmYf/dUDJQ5N6ToaXvHvIqk=";
+    #   };
+    #   propagatedBuildInputs = p.propagatedBuildInputs ++ [ ofinal.cohttp-http ofinal.logs ];
+    #   doCheck = false;
+    # });
     cohttp-eio = ofinal.callPackage ./cohttp-eio.nix {};
     cohttp-http = ofinal.callPackage ./cohttp-http.nix {};
 
-    buildDunePackage = final.makeOverridable ({ pname, version, ... }@args:
-      let
-        args' = builtins.removeAttrs args [ "minimalOCamlVersion" ];
-        ocaml = ofinal.ocaml;
-        minOCaml = args.minimalOCamlVersion or args.minimumOCamlVersion or "0";
-        guard = x:
-          if ! final.lib.versionAtLeast ocaml.version minOCaml
-          then throw "${pname}-${version} is not available for OCaml ${ocaml.version} (requires at least ${minOCaml})"
-          else x;
-        result = oprev.buildDunePackage args';
-      in
-      result.overrideAttrs { name = guard result.name; }
-    );
-
-    overrideDunePackage = f: drv:
-      drv.override (args: {
-        buildDunePackage = drv_: (args.buildDunePackage drv_).override f;
-      });
-
-    ocaml_pcre = ofinal.overrideDunePackage
-      rec {
-        version = "7.4.6";
-        minimalOCamlVersion = "4.08";
-        src = prev.fetchurl {
-          url = "https://github.com/mmottl/pcre-ocaml/releases/download/${version}/pcre-${version}.tbz";
-          sha256 = "17ajl0ra5xkxn5pf0m0zalylp44wsfy6mvcq213djh2pwznh4gya";
-        };
-      }
-      oprev.ocaml_pcre;
-
+    # buildDunePackage = final.makeOverridable oprev.buildDunePackage;
+    #
+    # overrideDunePackage = f: drv:
+    #   drv.override (args: {
+    #     buildDunePackage = drv_: (args.buildDunePackage drv_).override f;
+    #   });
+    #
+    # ocaml_pcre = ofinal.overrideDunePackage rec {
+    #   version = "7.4.6";
+    #   minimalOCamlVersion = "4.08";
+    #   src = prev.fetchurl {
+    #     url = "https://github.com/mmottl/pcre-ocaml/releases/download/${version}/pcre-${version}.tbz";
+    #     sha256 = "17ajl0ra5xkxn5pf0m0zalylp44wsfy6mvcq213djh2pwznh4gya";
+    #   };
+    # } oprev.ocaml_pcre;
 
     mirage-crypto-rng = oprev.mirage-crypto-rng.overrideAttrs { doCheck = false; };
   };

diff --git a/bap/overlay.nix b/bap/overlay.nix
@@ -25,5 +25,5 @@ final: prev:
     bap-build = ofinal.callPackage ./bap-build.nix { };
   };
 
-  inherit (final.ocamlPackages_pac) bap-aslp bap-asli-plugin bap-primus;
+  inherit (final.ocamlPackages_pac_4) bap-aslp bap-asli-plugin bap-primus;
 }
diff --git a/basil/basls.nix b/basil/basls.nix
@@ -0,0 +1,52 @@
+{ lib
+, buildDunePackage
+, fetchFromGitHub
+, testVersion
+, basil_ast
+, basls
+, menhir
+, linol
+, linol-lwt
+, lsp
+, containers
+, zarith
+, ocamlgraph
+, hashcons
+, ppx_deriving
+, ppxlib
+}:
+
+pname:
+
+buildDunePackage {
+  pname = pname;
+  version = "0.1.0-unstable-2025-07-11";
+
+  src = fetchFromGitHub {
+    owner = "ailrst";
+    repo = "basls";
+    rev = "04d27999b1beec5bce8ada08e12ffa1625ed176e";
+    hash = "sha256-TRWfjcPDAR9PQKFJQ+mqAszwuQ7YcVr2AVzaseMjatE=";
+  };
+
+  buildInputs =
+    [ linol linol-lwt lsp containers zarith hashcons ppx_deriving ppxlib ocamlgraph ]
+    ++ lib.optional (pname == "basil_lsp") basil_ast;
+  nativeBuildInputs = [ menhir ];
+
+  postPatch = ''
+    substituteInPlace lib/lsp/dune \
+      --replace-fail ' common' 'basil_ast.common'
+    substituteInPlace bin/lsp/dune \
+      --replace-fail ' basillang' 'basil_ast'
+  '';
+
+  outputs = [ "out" "dev" ];
+
+  meta = {
+    homepage = "https://github.com/ailrst/basls";
+    description = "A simple proof of concept language server for Basil IR supporting goto definition and the symbol list for
+block and procedure labels";
+    maintainers = with lib.maintainers; [ katrinafyi ];
+  };
+}
diff --git a/basil/compiler-explorer.nix b/basil/compiler-explorer.nix
@@ -29,7 +29,7 @@ buildNpmPackage {
   patches = [
     (fetchpatch {
       url = "https://gist.githubusercontent.com/katrinafyi/e5a6b6d8bed540af46bba8c3cc3d9d08/raw/0001-support-environment-variables-in-properties.patch";
-      hash = "sha256-Tpx272FGaSBcScI0ee/4cT3QGI56V1QixKYjL7m1/Q8=";
+      hash = "sha256-DVSMc4s6jyNdeGvQFRV6kqxUILDy/z7ztXFvrlxXQyk=";
     })
   ];
 

diff --git a/basil/overlay.nix b/basil/overlay.nix
@@ -30,6 +30,13 @@ let
 
     start-godbolt = final.callPackage ./start-godbolt.nix { };
 
+    basls = final.ocamlPackages_pac.basil_lsp;
+
+    overlay_ocamlPackages = ofinal: oprev: {
+      basil_ast = ofinal.callPackage ./basls.nix { } "basil_ast";
+      basil_lsp = ofinal.callPackage ./basls.nix { } "basil_lsp";
+    };
+
   };
 in
 final: prev:

diff --git a/flake.lock b/flake.lock
diff --git a/gtirb/0001-gtirb-link-absl.patch b/gtirb/0001-gtirb-link-absl.patch
@@ -1,31 +1,26 @@
 diff --git a/CMakeLists.txt b/CMakeLists.txt
-index e176b6a7..1c03fe8f 100644
+index aeab2d2..dd9073c 100644
 --- a/CMakeLists.txt
 +++ b/CMakeLists.txt
-@@ -427,11 +427,8 @@ endif()
- # ---------------------------------------------------------------------------
- # protobuf
- # ---------------------------------------------------------------------------
--if(CL_API)
--  find_package(Protobuf 3.7.0 REQUIRED)
--else()
--  find_package(Protobuf 3.0.0 REQUIRED)
--endif()
-+set(protobuf_MODULE_COMPATIBLE TRUE CACHE BOOL "")
-+find_package(Protobuf REQUIRED CONFIG)
-
+@@ -437,6 +437,7 @@ if(NOT Protobuf_PROTOC_EXECUTABLE)
+       "Protobuf compiler is installed."
+   )
+ endif()
++find_package( absl REQUIRED )
+
  if(Protobuf_VERSION VERSION_LESS 3.2)
    add_definitions(-DPROTOBUF_SET_BYTES_LIMIT)
-diff --git a/src/gtirb/proto/CMakeLists.txt b/src/gtirb/proto/CMakeLists.txt
-index 74cf20a9..d53a8bd0 100644
---- a/src/gtirb/proto/CMakeLists.txt
-+++ b/src/gtirb/proto/CMakeLists.txt
-@@ -45,7 +45,7 @@ endforeach(PROTO_H)
- # Add proto library target
- add_library(gtirb_proto STATIC ${PROTO_CPP_SOURCES} ${PROTO_COPIED_HEADERS})
-
--target_link_libraries(gtirb_proto ${Boost_LIBRARIES} ${Protobuf_LIBRARIES})
-+target_link_libraries(gtirb_proto ${Boost_LIBRARIES} protobuf::libprotobuf)
-
- target_compile_definitions(gtirb_proto PRIVATE GTIRB_${PROJECT_NAME}_EXPORTS)
-
+diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
+index b8a01be..b837100 100644
+--- a/src/CMakeLists.txt
++++ b/src/CMakeLists.txt
+@@ -141,6 +141,9 @@ target_link_libraries(
+          # Link in this static lib, but don't make it a transitive dependency of
+          # TestGTIRB, etc
+   PRIVATE gtirb_proto
++         absl::log_internal_message
++         absl::log_internal_check_op
++         absl::status
+ )
+ target_compile_definitions(
+   ${PROJECT_NAME} PRIVATE GTIRB_${PROJECT_NAME}_EXPORTS
diff --git a/gtirb/ddisasm.nix b/gtirb/ddisasm.nix
@@ -4,7 +4,7 @@
 , fetchFromGitHub
 , fetchzip
 , cmake
-, boost183
+, boost
 , lief
 , libehp
 , gtirb
@@ -24,23 +24,27 @@ let
   };
 in stdenv.mkDerivation {
   pname = "ddisasm";
-  version = "0-unstable-2024-10-31";
+  version = "1.8.0-unstable-2025-07-14";
 
   src = fetchFromGitHub {
     owner = "GrammaTech";
     repo = "ddisasm";
-    rev = "17396b59537aaff73e2c7657ccd3b3eb2c3b6a04";
-    hash = "sha256-yFZ0QR1upmTzEyATsTM5bGPr0EPWxkyXKbGa5nYSEIE=";
+    rev = "5a8779f427ddfecd085f5bfd86c3a2006251ef8d";
+    hash = "sha256-ZSmm+uwfXvTRRiLFLZVy2XOSI/rFd5piJ+8J+s2lJG8=";
   };
 
   patches = [
     (fetchurl {
       url = "https://github.com/rina-forks/ddisasm/compare/main..determinism.patch";
       hash = "sha256-xISyR7ptR2LfHZJAGUyXqANLIab9yZrQFh8wLbJLsx8=";
     })
+    (fetchurl {
+      url = "https://github.com/rina-forks/ddisasm/commit/469b049582b0892b6b841071352ba459a1d260b8.patch";
+      hash = "sha256-n9jAagjyEmm2YKS5JXt5HDsWXt64s8A6qrJAYJrlu0I=";
+    })
   ] ++ lib.optional stdenv.isDarwin ./0001-ddisasm-disable-concurrent-souffle.patch;
 
-  buildInputs = [ cmake boost183 lief gtirb gtirb-pprinter libehp ];
+  buildInputs = [ cmake boost lief gtirb gtirb-pprinter libehp ];
   nativeBuildInputs = [ capstone-grammatech souffle ];
 
   cmakeFlags = [ "-DDDISASM_ENABLE_TESTS=OFF" "-DDDISASM_GENERATE_MANY=ON" ];

diff --git a/gtirb/gtirb-pprinter.nix b/gtirb/gtirb-pprinter.nix
@@ -3,7 +3,7 @@
 , fetchFromGitHub
 , cmake
 , python3
-, boost183
+, boost
 , abseil-cpp
 , doxygen
 , gtirb
@@ -31,7 +31,7 @@ stdenv.mkDerivation {
     )
   '';
 
-  buildInputs = [ cmake python3 gtirb boost183 abseil-cpp gtest ];
+  buildInputs = [ cmake python3 gtirb boost abseil-cpp gtest ];
   nativeBuildInputs = [ capstone-grammatech ];
 
   cmakeFlags = [ "-DGTIRB_PPRINTER_ENABLE_TESTS=OFF" ];