merge

* flake.nix, flake.lock: here

.gitignore

@@ -82,3 +82,4 @@ GTAGS
 *.dsc
 *.gcov
 spot.spec
+default.nix

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 $@

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 <http://www.gnu.org/licenses/>.
+
+{ pkgs ? import <nixpkgs> {} }:
+let
+  version = "@VERSION@";
+in
+pkgs.stdenv.mkDerivation {
+  inherit version;
+  pname = "spot";
+
+  buildInputs = [
+    pkgs.python3
+  ];
+
+  src = ./.;
+
+  enableParallelBuilding = true;
+}

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
+}

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
+                ]))
+              ];
+            };
+          });
+}

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);