diff --git a/.gitignore b/.gitignore
index 155a9b5e7..73745a48f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -82,3 +82,4 @@ GTAGS
*.dsc
*.gcov
spot.spec
+default.nix
diff --git a/Makefile.am b/Makefile.am
index e198a977c..a5d842b4c 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -65,7 +65,8 @@ EXTRA_DIST = HACKING ChangeLog.1 tools/gitlog-to-changelog \
tools/help2man tools/man2html.pl \
tools/test-driver-teamcity $(UTF8) $(DEBIAN) \
m4/gnulib-cache.m4 .dir-locals.el \
- spot.spec spot.spec.in README.ltsmin
+ spot.spec spot.spec.in README.ltsmin \
+ default.nix default.nix.in
dist-hook: gen-ChangeLog
@@ -111,3 +112,6 @@ deb: dist
spot.spec: configure.ac spot.spec.in
sed 's/[@]VERSION[@]/$(VERSION)/;s/[@]GITPATCH[@]/@@@$(GITPATCH)/;s/@@@\.//' spot.spec.in > $@.tmp && mv $@.tmp $@
+
+default.nix: configure.ac default.nix.in
+ sed 's/[@]VERSION[@]/$(VERSION)/' default.nix.in > $@.tmp && mv $@.tmp $@
diff --git a/default.nix.in b/default.nix.in
new file mode 100644
index 000000000..8101e4f74
--- /dev/null
+++ b/default.nix.in
@@ -0,0 +1,35 @@
+# -*- mode: nix; coding: utf-8 -*-
+# Copyright (C) 2022 Laboratoire de Recherche et Développement de l'Epita
+# (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program. If not, see .
+
+{ pkgs ? import {} }:
+let
+ version = "@VERSION@";
+in
+pkgs.stdenv.mkDerivation {
+ inherit version;
+ pname = "spot";
+
+ buildInputs = [
+ pkgs.python3
+ ];
+
+ src = ./.;
+
+ enableParallelBuilding = true;
+}
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 000000000..dd215f1c6
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,61 @@
+{
+ "nodes": {
+ "flake-utils": {
+ "inputs": {
+ "systems": "systems"
+ },
+ "locked": {
+ "lastModified": 1731533236,
+ "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+ "owner": "numtide",
+ "repo": "flake-utils",
+ "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+ "type": "github"
+ },
+ "original": {
+ "owner": "numtide",
+ "repo": "flake-utils",
+ "type": "github"
+ }
+ },
+ "nixpkgs": {
+ "locked": {
+ "lastModified": 1741196730,
+ "narHash": "sha256-0Sj6ZKjCpQMfWnN0NURqRCQn2ob7YtXTAOTwCuz7fkA=",
+ "owner": "NixOS",
+ "repo": "nixpkgs",
+ "rev": "48913d8f9127ea6530a2a2f1bd4daa1b8685d8a3",
+ "type": "github"
+ },
+ "original": {
+ "owner": "NixOS",
+ "ref": "nixos-24.11",
+ "repo": "nixpkgs",
+ "type": "github"
+ }
+ },
+ "root": {
+ "inputs": {
+ "flake-utils": "flake-utils",
+ "nixpkgs": "nixpkgs"
+ }
+ },
+ "systems": {
+ "locked": {
+ "lastModified": 1681028828,
+ "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+ "owner": "nix-systems",
+ "repo": "default",
+ "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+ "type": "github"
+ },
+ "original": {
+ "owner": "nix-systems",
+ "repo": "default",
+ "type": "github"
+ }
+ }
+ },
+ "root": "root",
+ "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 000000000..f0f3f95b5
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,214 @@
+{
+ inputs = {
+ nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.11";
+ flake-utils.url = "github:numtide/flake-utils";
+ };
+ outputs = { self, nixpkgs, flake-utils, ... }:
+ flake-utils.lib.eachSystem
+ [
+ "x86_64-linux"
+ ]
+
+ (system:
+ let
+ pkgs = import nixpkgs { inherit system; };
+ lib = pkgs.lib;
+
+ mkSpotApps = appNames:
+ pkgs.lib.genAttrs appNames
+ (name: flake-utils.lib.mkApp {
+ drv = self.packages.${system}.spot;
+ name = name;
+ });
+
+ spotPackage =
+ let
+ inherit (builtins)
+ filter
+ head
+ isString
+ match
+ readFile
+ split
+ ;
+
+ # NOTE: Maintaining the version separately would be a pain, and we
+ # can't have a flake.nix.in with a @VERSION@ because it would make
+ # the flake unusable without running autoconf first, defeating some
+ # of its purpose.
+ #
+ # So let's get it the hard way instead :)
+ extractVersionRegex = ''^AC_INIT\(\[spot], \[([^]]+)], \[spot@lrde\.epita\.fr]\)$'';
+ getLines = (fileContent:
+ filter isString (split "\n" fileContent)
+ );
+ findVersionLine = (lines:
+ lib.lists.findFirst
+ (l: lib.strings.hasPrefix "AC_INIT(" l)
+ null
+ lines
+ );
+ getVersion = (file:
+ let
+ lines = getLines (readFile file);
+ versionLine = findVersionLine lines;
+ version = head (match extractVersionRegex versionLine);
+ in
+ version
+ );
+ in
+ {
+ lib,
+ pkgs,
+ stdenv,
+ # FIXME: do we want this flag?
+ buildOrgDoc ? false,
+ # Whether to enable Spot's Python 3 bindings
+ enablePython ? false
+ }:
+ stdenv.mkDerivation {
+ pname = "spot";
+ version = getVersion ./configure.ac;
+
+ src = self;
+
+ enableParallelBuilding = true;
+
+ # NOTE: Nix enables a lot of hardening flags by default, some of
+ # these probably harm performance so I've disabled everything
+ # (haven't benchmarked with vs without these, though).
+ hardeningDisable = [ "all" ];
+
+ # NOTE: mktexpk fails without a HOME set
+ preBuild = ''
+ export HOME=$TMPDIR
+ patchShebangs tools
+ '' + (if buildOrgDoc then ''
+ ln -s ${pkgs.plantuml}/lib/plantuml.jar doc/org/plantuml.jar
+ '' else ''
+ touch doc/org-stamp
+ '');
+
+ configureFlags = [
+ "--disable-devel"
+ "--enable-optimizations"
+ ] ++ lib.optional (!enablePython) [
+ "--disable-python"
+ ];
+
+ nativeBuildInputs = with pkgs; [
+ autoreconfHook
+
+ autoconf
+ automake
+ bison
+ flex
+ libtool
+ perl
+ ] ++ lib.optional buildOrgDoc [
+ graphviz
+ groff
+ plantuml
+ pdf2svg
+ R
+ ] ++ lib.optional enablePython [
+ python3
+ swig4
+ ];
+
+ buildInputs = with pkgs; [
+ # should provide the minimum amount of packages necessary for
+ # building tl.pdf
+ (texlive.combine {
+ inherit (texlive)
+ scheme-basic
+ latexmk
+
+ booktabs
+ cm-super
+ doi
+ doublestroke
+ etoolbox
+ koma-script
+ mathabx-type1
+ mathpazo
+ metafont
+ microtype
+ nag
+ pgf
+ standalone
+ stmaryrd
+ tabulary
+ todonotes
+ wasy-type1
+ wasysym
+ ;
+ })
+ ];
+ };
+ in
+ {
+ defaultPackage = self.packages.${system}.spot;
+
+ packages = {
+ # binaries + library only
+ spot = pkgs.callPackage spotPackage {};
+
+ # NOTE: clang build is broken on Nix when linking to stdlib++, using
+ # libcxx instead. See:
+ # https://github.com/NixOS/nixpkgs/issues/91285
+ spotClang = pkgs.callPackage spotPackage {
+ stdenv = pkgs.llvmPackages.libcxxStdenv;
+ };
+
+ spotWithOrgDoc = pkgs.callPackage spotPackage {
+ buildOrgDoc = true;
+ };
+
+ spotWithPython = pkgs.python3Packages.toPythonModule (
+ pkgs.callPackage spotPackage {
+ enablePython = true;
+ }
+ );
+
+ spotFull = pkgs.python3Packages.toPythonModule (
+ pkgs.callPackage spotPackage {
+ buildOrgDoc = true; enablePython = true;
+ }
+ );
+ };
+
+ apps = mkSpotApps [
+ "autcross"
+ "autfilt"
+ "dstar2tgba"
+ "genaut"
+ "genltl"
+ "ltl2tgba"
+ "ltl2tgta"
+ "ltlcross"
+ "ltldo"
+ "ltlfilt"
+ "ltlgrind"
+ "ltlmix"
+ "ltlsynt"
+ "randaut"
+ "randltl"
+ ];
+
+ devShell = pkgs.mkShell {
+ name = "spot-dev";
+ inputsFrom = [ self.packages.${system}.spotFull ];
+ buildInputs = [
+ pkgs.gdb
+ pkgs.clang-tools # for clangd
+ pkgs.bear
+
+ (pkgs.python3.withPackages (p: [
+ p.jupyter
+ p.ipython # otherwise ipython module isn't found when running ipynb tests
+ ]))
+ ];
+ };
+ });
+}
diff --git a/spot/tl/expansions2.cc b/spot/tl/expansions2.cc
index d80e5ffa3..c40298d7f 100644
--- a/spot/tl/expansions2.cc
+++ b/spot/tl/expansions2.cc
@@ -540,7 +540,7 @@ namespace spot
return {{f_bdd, formula::eword()}};
}
- auto rec = [&d, owner, opts, seen](formula f){
+ auto rec = [&d, owner, seen](formula f){
return expansion2(f, d, owner, exp_opts::None, seen);
};
@@ -711,7 +711,10 @@ namespace spot
if ((li & kj) != bddfalse)
res.push_back({li & kj, fj});
}
- res.push_back({li, formula::Fusion({ei, F})});
+
+ formula ei_fusion_F = formula::Fusion({ei, F});
+ if (!ei_fusion_F.is(op::ff))
+ res.push_back({li, ei_fusion_F});
}
finalize(res, opts, d, seen);