From 42221100dda39ccd032161637b75c6e4aae5436e Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Wed, 20 Oct 2021 11:54:16 +0200 Subject: [PATCH 1/3] nix: setup Nix Flake file * flake.nix, flake.lock: here --- flake.lock | 61 +++++++++++++++ flake.nix | 214 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 275 insertions(+) create mode 100644 flake.lock create mode 100644 flake.nix 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 + ])) + ]; + }; + }); +} From 059c5072df4be153449a2f34477c4221720da41a Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Thu, 3 Mar 2022 11:31:03 +0100 Subject: [PATCH 2/3] nix: provide package in release tarballs --- .gitignore | 1 + Makefile.am | 6 +++++- default.nix.in | 35 +++++++++++++++++++++++++++++++++++ 3 files changed, 41 insertions(+), 1 deletion(-) create mode 100644 default.nix.in 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; +} From c63412ab947ce0e16d2ec637da128048c25f37b4 Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Fri, 17 Oct 2025 17:36:40 +0200 Subject: [PATCH 3/3] translate_aa: fix sere copy When adapting the code to handle transition-based acceptance, a bug was introduced so that only accepting edges were copied to the result automaton. The self-loop labeled as false edge-case is here as prevention, I am not sure it happens in practice. * spot/twaalgos/translate_aa.cc: Here. --- spot/twaalgos/translate_aa.cc | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/spot/twaalgos/translate_aa.cc b/spot/twaalgos/translate_aa.cc index 6be7c4f85..50096a2c3 100644 --- a/spot/twaalgos/translate_aa.cc +++ b/spot/twaalgos/translate_aa.cc @@ -124,19 +124,16 @@ namespace spot bool edge_is_acc = ((trans_based && e.acc) || (!trans_based && sere_aut->state_is_accepting(e.dst))); - if (edge_is_acc) - { - // point to accepting sink instead of original dst if asked - if (use_accepting_sink) - aut_->new_edge(new_st, accepting_sink_, e.cond); - else - { - unsigned new_e = aut_->new_edge(new_st, register_state(e.dst), e.cond); - // remember if old edges were accepting - if (acc_edges != nullptr) - acc_edges->push_back(new_e); - } - } + unsigned new_edge; + // point to accepting sink instead of original dst if asked + if(use_accepting_sink && edge_is_acc) + new_edge = aut_->new_edge(new_st, accepting_sink_, e.cond); + else + new_edge = aut_->new_edge(new_st, register_state(e.dst), e.cond); + + // remember if old edges were accepting + if (acc_edges != nullptr && edge_is_acc) + acc_edges->push_back(new_edge); } } @@ -340,6 +337,9 @@ namespace spot for (unsigned i : acc_edges) { auto& e1 = aut_->edge_storage(i); + // self loop used to mark accepting state, skip it! + if (e1.cond == bddfalse) + continue; for (const auto& e2 : aut_->out(rhs_init)) aut_->new_edge(e1.src, e2.dst, e1.cond & e2.cond); }