@GrahamcOfBorg build ls4

Please investigate the build failure on ls4 on aarch64-linux .

@mmahut I was overly ambitious packaging this for unix since it requires FPU flags that glibc only has for x86. I've changed the platform.

@mmahut Just wanted to ping again on this; I can't send instructions to the build bot unfortunately.

@GrahamcOfBorg build ls4

@mmahut Argh sorry it looks like on Mac gcc needs to be an explicit dependency whereas this is not the case on Linux. Can you run build ls4 one more time? I don't have a Mac handy to test it unfortunately.

@GrahamcOfBorg build ls4

@mmahut It looks like everything finally built!

@mmahut Just wanted to ping on this to see if this could be merged.

Fixed up indentation.

@mmahut Let me know if there's anything else you want me to fix up.

@mmahut or @Ekleog it'd be great if either of you could take another look at this

@mmahut Will let you review if you can, as you already looked at the code, but overall it LGTM, with the exception that I wasn't able to easily confirm ls4 actually in general knowledge refers to this github repo -- ls4 does appear to be mentioned from the TLA+ github repo (as identified by the already-in-nixpkgs url), but without any link to this repo.

Yeah it was a bit tricky to ascertain whether this is the "real" ls4. I see the following as evidence for its authenticity:

• The repo and username is mentioned in this email on the TLA+ mailing list: http://discuss.tlapl.us/msg01185.html (although everything before .com is filtered out as xs).
• The creator of ls4 seems to be Martin Suda, based on http://ktiml.ms.mff.cuni.cz/~suda/ and quickbeam123 is mapped to Martin Suda on GitHub.

Thank you for your contributions.
This has been automatically marked as stale because it has had no activity for 180 days.
If this is still important to you, we ask that you leave a comment below. Your comment can be as simple as "still important to me". This lets people see that at least one person still cares about this. Someone will have to do this at most twice a year if there is no other activity.
Here are suggestions that might help resolve this more quickly:

1. Search for maintainers and people that previously touched the
   related code and @ mention them in a comment.
2. Ask on the NixOS Discourse. 3. Ask on the #nixos channel on
   irc.freenode.net.

Hey @SuperSandro2000, I'd be happy to make those changes if those are what's blocking this PR. Do you think that's all it takes for this PR to get merged?

Hey @SuperSandro2000, I'd be happy to make those changes if those are what's blocking this PR. Do you think that's all it takes for this PR to get merged?

Yeah, basically.

This is a semi-automatic executed nixpkgs-review which is checked by a human on a best effort basis and does not build all packages (e.g. lumo, tensorflow or pytorch).
If you have any questions or problems please reach out to SuperSandro2000 on IRC.

Result of nixpkgs-review pr 65619 run on x86_64-darwin 1

This is a semi-automatic executed nixpkgs-review which is checked by a human on a best effort basis and does not build all packages (e.g. lumo, tensorflow or pytorch).
If you have any questions or problems please reach out to SuperSandro2000 on IRC.

Result of nixpkgs-review pr 65619 run on x86_64-linux 1

Fails to build with:

Compiling: /build/source/core/Aiger2Spec.o
In file included from ../core/Aiger2Spec.h:25,
                 from /build/source/core/Aiger2Spec.cc:42:
../core/SolverTypes.h:50:16: error: friend declaration of 'Minisat::Lit mkLit(Minisat::Var, bool)' specifies default arguments and isn't a definition [-fpermissive]
   50 |     friend Lit mkLit(Var var, bool sign = false);
      |                ^~~~~
../core/SolverTypes.h:58:14: error: friend declaration of 'Minisat::Lit Minisat::mkLit(Minisat::Var, bool)' specifies default arguments and isn't the only declaration [-fpermissive]
   58 | inline  Lit  mkLit     (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
      |              ^~~~~
../core/SolverTypes.h:50:16: note: previous declaration of 'Minisat::Lit Minisat::mkLit(Minisat::Var, bool)'
   50 |     friend Lit mkLit(Var var, bool sign = false);
      |                ^~~~~
/build/source/core/Aiger2Spec.cc: In function 'void aiger_LoadSpec(const char*, int, int, int, int, int, int, int&, Clauses&, Clauses&, Clauses&, Clauses&)':
/build/source/core/Aiger2Spec.cc:605:5: warning: this 'else' clause does not guard... [-Wmisleading-indentation]
  605 |     else ; // undefined = no constraint
      |     ^~~~
/build/source/core/Aiger2Spec.cc:608:4: note: ...this statement, but the latter is misleadingly indented as if it were guarded by the 'else'
  608 |    if (refs[lit])
      |    ^~
In file included from ../core/Aiger2Spec.h:24,
                 from /build/source/core/Aiger2Spec.cc:42:
../mtl/Vec.h: In instantiation of 'void Minisat::vec<T>::capacity(int) [with T = Minisat::vec<Minisat::Lit>]':
../mtl/Vec.h:128:13:   required from 'void Minisat::vec<T>::growTo(int) [with T = Minisat::vec<Minisat::Lit>]'
../mtl/Vec.h:86:48:   required from 'void Minisat::vec<T>::push(const T&) [with T = Minisat::vec<Minisat::Lit>]'
/build/source/core/Aiger2Spec.cc:135:32:   required from here
../mtl/Vec.h:112:54: warning: 'void* realloc(void*, size_t)' moving an object of non-trivially copyable type 'class Minisat::vec<Minisat::Lit>'; use 'new' and 'delete' instead [-Wclass-memaccess]
  112 |     if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
      |                                             ~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In file included from ../core/Aiger2Spec.h:24,
                 from /build/source/core/Aiger2Spec.cc:42:
../mtl/Vec.h:44:7: note: 'class Minisat::vec<Minisat::Lit>' declared here
   44 | class vec {
      |       ^~~
make: *** [../mtl/template.mk:72: /build/source/core/Aiger2Spec.o] Error 1

I marked this as stale due to inactivity. → More info