about summary refs log tree commit diff
path: root/nixpkgs/pkgs/applications/science/logic
diff options
context:
space:
mode:
Diffstat (limited to 'nixpkgs/pkgs/applications/science/logic')
-rw-r--r--nixpkgs/pkgs/applications/science/logic/abella/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/anders/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/bitwuzla/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/celf/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/coq/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/cubicle/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/cvc3/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/cvc4/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/cvc5/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/dafny/default.nix4
-rw-r--r--nixpkgs/pkgs/applications/science/logic/dafny/deps.nix41
-rw-r--r--nixpkgs/pkgs/applications/science/logic/easycrypt/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/easycrypt/runtest.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/egglog/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/elan/0001-dynamically-patchelf-binaries.patch10
-rw-r--r--nixpkgs/pkgs/applications/science/logic/elan/default.nix10
-rw-r--r--nixpkgs/pkgs/applications/science/logic/fast-downward/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/gappa/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/glucose/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/kissat/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/lci/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/lean4/default.nix5
-rw-r--r--nixpkgs/pkgs/applications/science/logic/leo2/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/leo3/binary.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/logisim-evolution/default.nix57
-rw-r--r--nixpkgs/pkgs/applications/science/logic/logisim/default.nix45
-rw-r--r--nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/metis-prover/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/monosat/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/msat/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/naproche/default.nix13
-rw-r--r--nixpkgs/pkgs/applications/science/logic/open-wbo/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/opensmt/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/ott/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/prooftree/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/redprl/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/satallax/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/vampire/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/workcraft/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/z3/default.nix1
-rw-r--r--nixpkgs/pkgs/applications/science/logic/zchaff/default.nix1
46 files changed, 138 insertions, 85 deletions
diff --git a/nixpkgs/pkgs/applications/science/logic/abella/default.nix b/nixpkgs/pkgs/applications/science/logic/abella/default.nix
index 4483b8ad4756..7878626d6e9a 100644
--- a/nixpkgs/pkgs/applications/science/logic/abella/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/abella/default.nix
@@ -27,6 +27,7 @@ stdenv.mkDerivation (finalAttrs: {
 
   meta = {
     description = "Interactive theorem prover";
+    mainProgram = "abella";
     longDescription = ''
       Abella is an interactive theorem prover based on lambda-tree syntax.
       This means that Abella is well-suited for reasoning about the meta-theory
diff --git a/nixpkgs/pkgs/applications/science/logic/anders/default.nix b/nixpkgs/pkgs/applications/science/logic/anders/default.nix
index eb2be71f1681..dff6c86703d4 100644
--- a/nixpkgs/pkgs/applications/science/logic/anders/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/anders/default.nix
@@ -20,6 +20,7 @@ ocamlPackages.buildDunePackage rec {
 
   meta = with lib; {
     description = "Modal Homotopy Type System";
+    mainProgram = "anders";
     homepage = "https://homotopy.dev/";
     license = licenses.isc;
     maintainers = [ maintainers.suhr ];
diff --git a/nixpkgs/pkgs/applications/science/logic/bitwuzla/default.nix b/nixpkgs/pkgs/applications/science/logic/bitwuzla/default.nix
index 4af4058339d9..bacf8620e5fd 100644
--- a/nixpkgs/pkgs/applications/science/logic/bitwuzla/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/bitwuzla/default.nix
@@ -61,6 +61,7 @@ stdenv.mkDerivation rec {
 
   meta = with lib; {
     description = "A SMT solver for fixed-size bit-vectors, floating-point arithmetic, arrays, and uninterpreted functions";
+    mainProgram = "bitwuzla";
     homepage = "https://bitwuzla.github.io";
     license = licenses.mit;
     platforms = platforms.unix;
diff --git a/nixpkgs/pkgs/applications/science/logic/celf/default.nix b/nixpkgs/pkgs/applications/science/logic/celf/default.nix
index 044a6f3ca1c4..e1f0c237f673 100644
--- a/nixpkgs/pkgs/applications/science/logic/celf/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/celf/default.nix
@@ -28,6 +28,7 @@ stdenv.mkDerivation rec {
 
   meta = with lib; {
     description = "Linear logic programming system";
+    mainProgram = "celf";
     homepage = "https://github.com/clf/celf";
     license = licenses.gpl3;
     maintainers = with maintainers; [ bcdarwin ];
diff --git a/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix b/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix
index 2a8c058a80bb..543c6cb4310b 100644
--- a/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix
+++ b/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix
@@ -19,6 +19,7 @@ stdenv.mkDerivation {
 
   meta = with lib; {
     description = "Resolution-based theorem prover for Coalition Logic implemented in C++";
+    mainProgram = "CLProver++";
     homepage = "https://cgi.csc.liv.ac.uk/~ullrich/CLProver++/";
     license = licenses.gpl3; # Note that while the website states that it is GPLv2 but the file in the zip as well as the comments in the source state it is GPLv3
     maintainers = with maintainers; [ mgttlinger ];
diff --git a/nixpkgs/pkgs/applications/science/logic/coq/default.nix b/nixpkgs/pkgs/applications/science/logic/coq/default.nix
index e52a51936180..37a8aba7d8c7 100644
--- a/nixpkgs/pkgs/applications/science/logic/coq/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/coq/default.nix
@@ -57,6 +57,7 @@ let
    "8.17.1".sha256   = "sha256-x+RwkbxMg9aR0L3WSCtpIz8jwA5cJA4tXAtHMZb20y4=";
    "8.18.0".sha256   = "sha256-WhiBs4nzPHQ0R24xAdM49kmxSCPOxiOVMA1iiMYunz4=";
    "8.19.0".sha256   = "sha256-ixsYCvCXpBHqJ71hLQklphlwoOO3i/6w2PJjllKqf9k=";
+   "8.19.1".sha256   = "sha256-kmZ8Uk8jpzjOd67aAPp3C+vU2oNaBw9pr7+Uixcgg94=";
   };
   releaseRev = v: "V${v}";
   fetched = import ../../../../build-support/coq/meta-fetch/default.nix
diff --git a/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix b/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix
index f2e3eaab91dc..4be57a194635 100644
--- a/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix
@@ -22,6 +22,7 @@ stdenv.mkDerivation rec {
 
   meta = with lib; {
     description = "An advanced SAT Solver";
+    mainProgram = "cryptominisat5";
     homepage = "https://github.com/msoos/cryptominisat";
     license = licenses.mit;
     maintainers = with maintainers; [ mic92 ];
diff --git a/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix b/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix
index 5c15b8a17241..4b74cdd518ca 100644
--- a/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix
@@ -42,6 +42,7 @@ stdenv.mkDerivation rec {
 
   meta = {
     description = "Cryptographic protocol verifier in the computational model";
+    mainProgram = "cryptoverif";
     homepage    = "https://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/";
     license     = lib.licenses.cecill-b;
     platforms   = lib.platforms.unix;
diff --git a/nixpkgs/pkgs/applications/science/logic/cubicle/default.nix b/nixpkgs/pkgs/applications/science/logic/cubicle/default.nix
index c9382c5d0f1a..03409e68ea33 100644
--- a/nixpkgs/pkgs/applications/science/logic/cubicle/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/cubicle/default.nix
@@ -37,6 +37,7 @@ stdenv.mkDerivation rec {
 
   meta = with lib; {
     description = "An open source model checker for verifying safety properties of array-based systems";
+    mainProgram = "cubicle";
     homepage = "https://cubicle.lri.fr/";
     license = licenses.asl20;
     platforms = platforms.unix;
diff --git a/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix b/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix
index 0385909610e6..bec5a89cc691 100644
--- a/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix
@@ -28,6 +28,7 @@ stdenv.mkDerivation rec {
 
   meta = with lib; {
     description = "A prover for satisfiability modulo theory (SMT)";
+    mainProgram = "cvc3";
     maintainers = with maintainers;
       [ raskin ];
     platforms = platforms.unix;
diff --git a/nixpkgs/pkgs/applications/science/logic/cvc4/default.nix b/nixpkgs/pkgs/applications/science/logic/cvc4/default.nix
index 1513c7477985..ac45db8cb312 100644
--- a/nixpkgs/pkgs/applications/science/logic/cvc4/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/cvc4/default.nix
@@ -40,6 +40,7 @@ stdenv.mkDerivation rec {
 
   meta = with lib; {
     description = "A high-performance theorem prover and SMT solver";
+    mainProgram = "cvc4";
     homepage    = "http://cvc4.cs.stanford.edu/web/";
     license     = licenses.gpl3;
     platforms   = platforms.unix;
diff --git a/nixpkgs/pkgs/applications/science/logic/cvc5/default.nix b/nixpkgs/pkgs/applications/science/logic/cvc5/default.nix
index 2dff344e4edb..d34b29337296 100644
--- a/nixpkgs/pkgs/applications/science/logic/cvc5/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/cvc5/default.nix
@@ -30,6 +30,7 @@ stdenv.mkDerivation rec {
 
   meta = with lib; {
     description = "A high-performance theorem prover and SMT solver";
+    mainProgram = "cvc5";
     homepage    = "https://cvc5.github.io";
     license     = licenses.gpl3Only;
     platforms   = platforms.unix;
diff --git a/nixpkgs/pkgs/applications/science/logic/dafny/default.nix b/nixpkgs/pkgs/applications/science/logic/dafny/default.nix
index 5f56d612ab24..83d472c1abb1 100644
--- a/nixpkgs/pkgs/applications/science/logic/dafny/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/dafny/default.nix
@@ -8,13 +8,13 @@
 
 buildDotnetModule rec {
   pname = "Dafny";
-  version = "4.4.0";
+  version = "4.5.0";
 
   src = fetchFromGitHub {
     owner = "dafny-lang";
     repo = "dafny";
     rev = "v${version}";
-    hash = "sha256-rnPZms60vRtefEV+3IeVXoZJU9WMjVxPVioRaEcyw/o=";
+    hash = "sha256-NsQhJY++IaLyFc5jqo7TyZBcz0P8VUizGLxdIe9KEO4=";
   };
 
   postPatch = ''
diff --git a/nixpkgs/pkgs/applications/science/logic/dafny/deps.nix b/nixpkgs/pkgs/applications/science/logic/dafny/deps.nix
index a786d8b3d6fd..91fe5624ac7f 100644
--- a/nixpkgs/pkgs/applications/science/logic/dafny/deps.nix
+++ b/nixpkgs/pkgs/applications/science/logic/dafny/deps.nix
@@ -2,19 +2,19 @@
 # Please dont edit it manually, your changes might get overwritten!
 
 { fetchNuGet }: [
-  (fetchNuGet { pname = "Boogie"; version = "3.0.9"; sha256 = "12700rvm3zj73pkkjaypfa72fvqz8bp78hi3jkh89dqavhg3l7p5"; })
-  (fetchNuGet { pname = "Boogie.AbstractInterpretation"; version = "3.0.9"; sha256 = "1612d1x7smhcczmk21z9kswjjvq3h0r5mlf1zb8mznyx0154pckg"; })
-  (fetchNuGet { pname = "Boogie.BaseTypes"; version = "3.0.9"; sha256 = "0v6x8k61rl6bvp1zbvbhnlpkakbw11c2mf8glafmf4znrakwil23"; })
-  (fetchNuGet { pname = "Boogie.CodeContractsExtender"; version = "3.0.9"; sha256 = "045z0j7bhsb8fypzkz8spixfqdchcpsq3bb9bfwb95if2mna4zx2"; })
-  (fetchNuGet { pname = "Boogie.Concurrency"; version = "3.0.9"; sha256 = "00k08qh614vciadzk7lr1dcwsvrcfpslvs342amq12c25rxh3125"; })
-  (fetchNuGet { pname = "Boogie.Core"; version = "3.0.9"; sha256 = "03fip919iw7y3vwk5nj53jj73ry43z9fpn752j5fbgygkl2zbx4q"; })
-  (fetchNuGet { pname = "Boogie.ExecutionEngine"; version = "3.0.9"; sha256 = "098l1qmya021raqgdapxvwq3pra4v7wpv7j3dmmhsnpg8zs30jgi"; })
-  (fetchNuGet { pname = "Boogie.Graph"; version = "3.0.9"; sha256 = "1y8aai7wmsyh2pn9bl1rp2nifs3k9b8kb2lqx5rgs1fdiyk2q24j"; })
-  (fetchNuGet { pname = "Boogie.Houdini"; version = "3.0.9"; sha256 = "1ssr82swqmjsap6v344v2kwkfsv70gx082dk54x7vpapr56f1fgp"; })
-  (fetchNuGet { pname = "Boogie.Model"; version = "3.0.9"; sha256 = "1cy04a7dr1z7dxfkx6l9kfm30rx5wsn7g50b0wyzp4ns6sbkh47f"; })
-  (fetchNuGet { pname = "Boogie.Provers.SMTLib"; version = "3.0.9"; sha256 = "1ijzn67wl82ycr1k7gbh8dhq99zxqqjdc48glf4ld832l7sp3vam"; })
-  (fetchNuGet { pname = "Boogie.VCExpr"; version = "3.0.9"; sha256 = "0hivg31c8v9ix5b8mici6mxz1yzydwiyvgb510bnghxciwbnd4gp"; })
-  (fetchNuGet { pname = "Boogie.VCGeneration"; version = "3.0.9"; sha256 = "1j9853vixzpgdfd60c3hr5padfdj3sbrbhmr6jg9a0cr3afk72sm"; })
+  (fetchNuGet { pname = "Boogie"; version = "3.1.3"; sha256 = "0xzc7s0rjb8dhdkdf71g6pdsnyhbl534xpwd8gbx6g16a87iqx6i"; })
+  (fetchNuGet { pname = "Boogie.AbstractInterpretation"; version = "3.1.3"; sha256 = "0a7v2jkkbh59pyc5nz4avszm3dbmp4amkmr6lvn0gyc3hxgn8d3k"; })
+  (fetchNuGet { pname = "Boogie.BaseTypes"; version = "3.1.3"; sha256 = "1h94yl4ymhd2g14i5w8lnnh2zw7gx65qydzvv8cm8d5yn64gch63"; })
+  (fetchNuGet { pname = "Boogie.CodeContractsExtender"; version = "3.1.3"; sha256 = "0b1h1lz997lgyq34bx3ngnhgcrw8j4qvsa6iygb6bydxz7rirrf4"; })
+  (fetchNuGet { pname = "Boogie.Concurrency"; version = "3.1.3"; sha256 = "1aq0gdz1xkmp82c67vrmyvkncfbbj5zxrsg78lsmmi22h9qbkzm3"; })
+  (fetchNuGet { pname = "Boogie.Core"; version = "3.1.3"; sha256 = "0yhl272lv9lncjval2z7zl9wavlxx8bivj467zl2zzbrxw2k5wz8"; })
+  (fetchNuGet { pname = "Boogie.ExecutionEngine"; version = "3.1.3"; sha256 = "0p0zp329h6mddbswm3pdcyvy03y69vyznv11ph6bkpya21lsxqy7"; })
+  (fetchNuGet { pname = "Boogie.Graph"; version = "3.1.3"; sha256 = "1p8vb4x4iy7f0ycwb8f71j9a2ci8irwg3rvad2hg3rgbihbwp1qj"; })
+  (fetchNuGet { pname = "Boogie.Houdini"; version = "3.1.3"; sha256 = "06qlgi9f70r2w7w6h9qw3lx9dd4pbddpdplqjxi090rpry6dhrbz"; })
+  (fetchNuGet { pname = "Boogie.Model"; version = "3.1.3"; sha256 = "0fbvnrghaq17fdpjx12axxrrjp1mh99skaznmvxd1ylsqqnn4cbk"; })
+  (fetchNuGet { pname = "Boogie.Provers.SMTLib"; version = "3.1.3"; sha256 = "0x7gpc7m04in2gzdn4jgjphd2xjqrdfmh84wzwnwpvi5wyn869jc"; })
+  (fetchNuGet { pname = "Boogie.VCExpr"; version = "3.1.3"; sha256 = "0dyndhqz1yf9qnq9mw73g53rnz0xfbdbi3yk6pg7fdm1m3363h5p"; })
+  (fetchNuGet { pname = "Boogie.VCGeneration"; version = "3.1.3"; sha256 = "1bl83727zc1rhskx548p5pa27804n3f5i9n233jvcz6n6bfjn74k"; })
   (fetchNuGet { pname = "CocoR"; version = "2014.12.24"; sha256 = "0ps8h7aawkcc1910qnh13llzb01pvgsjmg862pxp0p4wca2dn7a2"; })
   (fetchNuGet { pname = "JetBrains.Annotations"; version = "2021.1.0"; sha256 = "07pnhxxlgx8spmwmakz37nmbvgyb6yjrbrhad5rrn6y767z5r1gb"; })
   (fetchNuGet { pname = "MediatR"; version = "8.1.0"; sha256 = "0cqx7yfh998xhsfk5pr6229lcjcs1jxxyqz7dwskc9jddl6a2akp"; })
@@ -40,6 +40,7 @@
   (fetchNuGet { pname = "Microsoft.Extensions.FileProviders.Abstractions"; version = "5.0.0"; sha256 = "01ahgd0b2z2zycrr2lcsq2cl59fn04bh51hdwdp9dcsdkpvnasj1"; })
   (fetchNuGet { pname = "Microsoft.Extensions.FileProviders.Physical"; version = "5.0.0"; sha256 = "00vii8148a6pk12l9jl0rhjp7apil5q5qcy7v1smnv17lj4p8szd"; })
   (fetchNuGet { pname = "Microsoft.Extensions.FileSystemGlobbing"; version = "5.0.0"; sha256 = "0lm6n9vbyjh0l17qcc2y9qwn1cns3dyjmkvbxjp0g9sll32kjpmb"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Logging"; version = "2.0.0"; sha256 = "1jkwjcq1ld9znz1haazk8ili2g4pzfdp6i7r7rki4hg3jcadn386"; })
   (fetchNuGet { pname = "Microsoft.Extensions.Logging"; version = "5.0.0"; sha256 = "1qa1l18q2jh9azya8gv1p8anzcdirjzd9dxxisb4911i9m1648i3"; })
   (fetchNuGet { pname = "Microsoft.Extensions.Logging.Abstractions"; version = "5.0.0"; sha256 = "1yza38675dbv1qqnnhqm23alv2bbaqxp0pb7zinjmw8j2mr5r6wc"; })
   (fetchNuGet { pname = "Microsoft.Extensions.Options"; version = "2.0.0"; sha256 = "0g4zadlg73f507krilhaaa7h0jdga216syrzjlyf5fdk25gxmjqh"; })
@@ -53,10 +54,9 @@
   (fetchNuGet { pname = "Microsoft.NETCore.Platforms"; version = "3.0.0"; sha256 = "1bk8r4r3ihmi6322jmcag14jmw11mjqys202azqjzglcx59pxh51"; })
   (fetchNuGet { pname = "Microsoft.NETCore.Targets"; version = "1.0.1"; sha256 = "0ppdkwy6s9p7x9jix3v4402wb171cdiibq7js7i13nxpdky7074p"; })
   (fetchNuGet { pname = "Microsoft.NETCore.Targets"; version = "1.1.0"; sha256 = "193xwf33fbm0ni3idxzbr5fdq3i2dlfgihsac9jj7whj0gd902nh"; })
-  (fetchNuGet { pname = "Microsoft.TestPlatform.Extensions.TrxLogger"; version = "17.0.0"; sha256 = "067vpfk5690j0d01lfy8mry42pkzz79l873cp2dby0hi8skfklaq"; })
-  (fetchNuGet { pname = "Microsoft.TestPlatform.ObjectModel"; version = "16.11.0"; sha256 = "1fc0ghk1cny4i8w43b94pxhl0srxisv6kaflkkp30ncsa9szhkxh"; })
-  (fetchNuGet { pname = "Microsoft.TestPlatform.ObjectModel"; version = "17.0.0"; sha256 = "1bh5scbvl6ndldqv20sl34h4y257irm9ziv2wyfc3hka6912fhn7"; })
-  (fetchNuGet { pname = "Microsoft.TestPlatform.TestHost"; version = "16.11.0"; sha256 = "0hp1vndf2jhyg1f3miq4g2068z5kpfzy6nmswm25vymghxp1ws4k"; })
+  (fetchNuGet { pname = "Microsoft.TestPlatform.Extensions.TrxLogger"; version = "17.9.0"; sha256 = "0wn38vj9i4gjw5zsl4wcivpqrmp1h5n6m1zxcfwj7yjn9hf45rz9"; })
+  (fetchNuGet { pname = "Microsoft.TestPlatform.ObjectModel"; version = "17.9.0"; sha256 = "1kgsl9w9fganbm9wvlkqgk0ag9hfi58z88rkfybc6kvg78bx89ca"; })
+  (fetchNuGet { pname = "Microsoft.TestPlatform.TestHost"; version = "17.9.0"; sha256 = "19ffh31a1jxzn8j69m1vnk5hyfz3dbxmflq77b8x82zybiilh5nl"; })
   (fetchNuGet { pname = "Microsoft.VisualStudio.Threading"; version = "16.7.56"; sha256 = "13x0xrsjxd86clf9cjjwmpzlyp8pkrf13riya7igs8zy93zw2qap"; })
   (fetchNuGet { pname = "Microsoft.VisualStudio.Threading.Analyzers"; version = "16.7.56"; sha256 = "04v9df0k7bsc0rzgkw4mnvi43pdrh42vk6xdcwn9m6im33m0nnz2"; })
   (fetchNuGet { pname = "Microsoft.VisualStudio.Validation"; version = "15.5.31"; sha256 = "1ah99rn922qa0sd2k3h64m324f2r32pw8cn4cfihgvwx4qdrpmgw"; })
@@ -64,8 +64,8 @@
   (fetchNuGet { pname = "Microsoft.Win32.Registry"; version = "4.6.0"; sha256 = "0i4y782yrqqyx85pg597m20gm0v126w0j9ddk5z7xb3crx4z9f2s"; })
   (fetchNuGet { pname = "Microsoft.Win32.SystemEvents"; version = "6.0.0"; sha256 = "0c6pcj088g1yd1vs529q3ybgsd2vjlk5y1ic6dkmbhvrp5jibl9p"; })
   (fetchNuGet { pname = "Nerdbank.Streams"; version = "2.6.81"; sha256 = "06wihcaga8537ibh0mkj28m720m6vzkqk562zkynhca85nd236yi"; })
+  (fetchNuGet { pname = "Newtonsoft.Json"; version = "11.0.2"; sha256 = "1784xi44f4k8v1fr696hsccmwpy94bz7kixxqlri98zhcxn406b2"; })
   (fetchNuGet { pname = "Newtonsoft.Json"; version = "13.0.1"; sha256 = "0fijg0w6iwap8gvzyjnndds0q4b8anwxxvik7y8vgq97dram4srb"; })
-  (fetchNuGet { pname = "NuGet.Frameworks"; version = "5.0.0"; sha256 = "18ijvmj13cwjdrrm52c8fpq021531zaz4mj4b4zapxaqzzxf2qjr"; })
   (fetchNuGet { pname = "OmniSharp.Extensions.JsonRpc"; version = "0.19.5"; sha256 = "0ilcv3cxcvjkd8ngiydi69pzll07rhqdv5nq9yjnhyj142ynw2cb"; })
   (fetchNuGet { pname = "OmniSharp.Extensions.JsonRpc.Generators"; version = "0.19.5"; sha256 = "1mac4yx29ld8fyirg7n0vqn81hzdvcrl8w0l9w5xhnnm6bcd42v8"; })
   (fetchNuGet { pname = "OmniSharp.Extensions.LanguageProtocol"; version = "0.19.5"; sha256 = "1clgrbw6dlh46iiiqhavwh15xqar41az352mb5r4ln8ql3wnmk1i"; })
@@ -104,7 +104,7 @@
   (fetchNuGet { pname = "runtime.unix.System.IO.FileSystem"; version = "4.3.0"; sha256 = "14nbkhvs7sji5r1saj2x8daz82rnf9kx28d3v2qss34qbr32dzix"; })
   (fetchNuGet { pname = "runtime.unix.System.Private.Uri"; version = "4.3.0"; sha256 = "1jx02q6kiwlvfksq1q9qr17fj78y5v6mwsszav4qcz9z25d5g6vk"; })
   (fetchNuGet { pname = "runtime.unix.System.Runtime.Extensions"; version = "4.3.0"; sha256 = "0pnxxmm8whx38dp6yvwgmh22smknxmqs5n513fc7m4wxvs1bvi4p"; })
-  (fetchNuGet { pname = "Serilog"; version = "2.10.0"; sha256 = "08bih205i632ywryn3zxkhb15dwgyaxbhmm1z3b5nmby9fb25k7v"; })
+  (fetchNuGet { pname = "Serilog"; version = "2.12.0"; sha256 = "0lqxpc96qcjkv9pr1rln7mi4y7n7jdi4vb36c2fv3845w1vswgr4"; })
   (fetchNuGet { pname = "Serilog.Extensions.Logging"; version = "3.0.1"; sha256 = "069qy7dm5nxb372ij112ppa6m99b4iaimj3sji74m659fwrcrl9a"; })
   (fetchNuGet { pname = "Serilog.Settings.Configuration"; version = "3.1.0"; sha256 = "1cj5am4n073331gbfm2ylqb9cadl4q3ppzgwmm5c8m1drxpiwkb5"; })
   (fetchNuGet { pname = "Serilog.Sinks.Debug"; version = "2.0.0"; sha256 = "1i7j870l47gan3gpnnlzkccn5lbm7518cnkp25a3g5gp9l0dbwpw"; })
@@ -114,8 +114,6 @@
   (fetchNuGet { pname = "System.Collections"; version = "4.3.0"; sha256 = "19r4y64dqyrq6k4706dnyhhw7fs24kpp3awak7whzss39dakpxk9"; })
   (fetchNuGet { pname = "System.Collections.Immutable"; version = "1.7.0"; sha256 = "1gik4sn9jsi1wcy1pyyp0r4sn2g17cwrsh24b2d52vif8p2h24zx"; })
   (fetchNuGet { pname = "System.Collections.Immutable"; version = "1.7.1"; sha256 = "1nh4nlxfc7lbnbl86wwk1a3jwl6myz5j6hvgh5sp4krim9901hsq"; })
-  (fetchNuGet { pname = "System.Collections.NonGeneric"; version = "4.0.1"; sha256 = "19994r5y5bpdhj7di6w047apvil8lh06lh2c2yv9zc4fc5g9bl4d"; })
-  (fetchNuGet { pname = "System.Collections.Specialized"; version = "4.0.1"; sha256 = "1wbv7y686p5x169rnaim7sln67ivmv6r57falrnx8aap9y33mam9"; })
   (fetchNuGet { pname = "System.CommandLine"; version = "2.0.0-beta4.22272.1"; sha256 = "1iy5hwwgvx911g3yq65p4zsgpy08w4qz9j3h0igcf7yci44vw8yd"; })
   (fetchNuGet { pname = "System.Configuration.ConfigurationManager"; version = "6.0.0"; sha256 = "0sqapr697jbb4ljkq46msg0xx1qpmc31ivva6llyz2wzq3mpmxbw"; })
   (fetchNuGet { pname = "System.Diagnostics.Debug"; version = "4.3.0"; sha256 = "00yjlf19wjydyr6cfviaph3vsjzg3d5nvnya26i2fvfg53sknh3y"; })
@@ -124,7 +122,6 @@
   (fetchNuGet { pname = "System.Dynamic.Runtime"; version = "4.0.11"; sha256 = "1pla2dx8gkidf7xkciig6nifdsb494axjvzvann8g2lp3dbqasm9"; })
   (fetchNuGet { pname = "System.Globalization"; version = "4.0.11"; sha256 = "070c5jbas2v7smm660zaf1gh0489xanjqymkvafcs4f8cdrs1d5d"; })
   (fetchNuGet { pname = "System.Globalization"; version = "4.3.0"; sha256 = "1cp68vv683n6ic2zqh2s1fn4c2sd87g5hpp6l4d4nj4536jz98ki"; })
-  (fetchNuGet { pname = "System.Globalization.Extensions"; version = "4.0.1"; sha256 = "0hjhdb5ri8z9l93bw04s7ynwrjrhx2n0p34sf33a9hl9phz69fyc"; })
   (fetchNuGet { pname = "System.IO"; version = "4.1.0"; sha256 = "1g0yb8p11vfd0kbkyzlfsbsp5z44lwsvyc0h3dpw6vqnbi035ajp"; })
   (fetchNuGet { pname = "System.IO"; version = "4.3.0"; sha256 = "05l9qdrzhm4s5dixmx68kxwif4l99ll5gqmh7rqgw554fx0agv5f"; })
   (fetchNuGet { pname = "System.IO.FileSystem"; version = "4.0.1"; sha256 = "0kgfpw6w4djqra3w5crrg8xivbanh1w9dh3qapb28q060wb9flp1"; })
diff --git a/nixpkgs/pkgs/applications/science/logic/easycrypt/default.nix b/nixpkgs/pkgs/applications/science/logic/easycrypt/default.nix
index 2869bcd6e1e3..782d15d61559 100644
--- a/nixpkgs/pkgs/applications/science/logic/easycrypt/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/easycrypt/default.nix
@@ -51,5 +51,6 @@ stdenv.mkDerivation rec {
     platforms = lib.platforms.all;
     homepage = "https://easycrypt.info/";
     description = "Computer-Aided Cryptographic Proofs";
+    mainProgram = "easycrypt";
   };
 }
diff --git a/nixpkgs/pkgs/applications/science/logic/easycrypt/runtest.nix b/nixpkgs/pkgs/applications/science/logic/easycrypt/runtest.nix
index c0d72d96e1d1..b714dc14991b 100644
--- a/nixpkgs/pkgs/applications/science/logic/easycrypt/runtest.nix
+++ b/nixpkgs/pkgs/applications/science/logic/easycrypt/runtest.nix
@@ -21,5 +21,6 @@ python3Packages.buildPythonApplication rec {
 
   meta = easycrypt.meta // {
     description = "Testing program for EasyCrypt formalizations";
+    mainProgram = "ec-runtest";
   };
 }
diff --git a/nixpkgs/pkgs/applications/science/logic/egglog/default.nix b/nixpkgs/pkgs/applications/science/logic/egglog/default.nix
index ab5653b50912..8b94c449c6be 100644
--- a/nixpkgs/pkgs/applications/science/logic/egglog/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/egglog/default.nix
@@ -25,6 +25,7 @@ rustPlatform.buildRustPackage {
 
   meta = with lib; {
     description = "A fixpoint reasoning system that unifies Datalog and equality saturation";
+    mainProgram = "egglog";
     homepage = "https://github.com/egraphs-good/egglog";
     license = licenses.mit;
     maintainers = with maintainers; [ figsoda ];
diff --git a/nixpkgs/pkgs/applications/science/logic/elan/0001-dynamically-patchelf-binaries.patch b/nixpkgs/pkgs/applications/science/logic/elan/0001-dynamically-patchelf-binaries.patch
index 74da9d854f34..0b33d4242eb7 100644
--- a/nixpkgs/pkgs/applications/science/logic/elan/0001-dynamically-patchelf-binaries.patch
+++ b/nixpkgs/pkgs/applications/science/logic/elan/0001-dynamically-patchelf-binaries.patch
@@ -2,7 +2,7 @@ diff --git a/src/elan-dist/src/component/package.rs b/src/elan-dist/src/componen
 index c51e76d..ae8159e 100644
 --- a/src/elan-dist/src/component/package.rs
 +++ b/src/elan-dist/src/component/package.rs
-@@ -56,6 +56,35 @@ fn unpack_without_first_dir<R: Read>(archive: &mut tar::Archive<R>, path: &Path)
+@@ -56,6 +56,37 @@ fn unpack_without_first_dir<R: Read>(archive: &mut tar::Archive<R>, path: &Path)
          entry
              .unpack(&full_path)
              .chain_err(|| ErrorKind::ExtractingPackage)?;
@@ -26,9 +26,11 @@ index c51e76d..ae8159e 100644
 +        use std::os::unix::fs::PermissionsExt;
 +        let new_path = dest_path.with_extension("orig");
 +        ::std::fs::rename(dest_path, &new_path)?;
-+        ::std::fs::write(dest_path, format!(r#"#! @shell@
-+LEAN_CC="${{LEAN_CC:-@cc@}}" exec -a "$0" {} "$@" -L {}/lib  # use bundled libraries, but not bundled compiler that doesn't know about NIX_LDFLAGS
-+"#, new_path.to_str().unwrap(), dest_path.parent().unwrap().parent().unwrap().to_str().unwrap()))?;
++        ::std::fs::write(dest_path, r#"#! @shell@
++dir="$(dirname "${BASH_SOURCE[0]}")"
++# use bundled libraries, but not bundled compiler that doesn't know about NIX_LDFLAGS
++LEAN_CC="${LEAN_CC:-@cc@}" exec -a "$0" "$dir/leanc.orig" "$@" -L"$dir/../lib"
++"#)?;
 +        ::std::fs::set_permissions(dest_path, ::std::fs::Permissions::from_mode(0o755))?;
 +    }
 +
diff --git a/nixpkgs/pkgs/applications/science/logic/elan/default.nix b/nixpkgs/pkgs/applications/science/logic/elan/default.nix
index 129aacc07f62..245f8db13ce6 100644
--- a/nixpkgs/pkgs/applications/science/logic/elan/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/elan/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, lib, runCommand, patchelf, makeWrapper, pkg-config, curl, runtimeShell, fetchpatch
+{ stdenv, lib, runCommand, patchelf, makeWrapper, pkg-config, curl, runtimeShell
 , openssl, zlib, fetchFromGitHub, rustPlatform, libiconv }:
 
 rustPlatform.buildRustPackage rec {
@@ -23,14 +23,6 @@ rustPlatform.buildRustPackage rec {
   buildFeatures = [ "no-self-update" ];
 
   patches = lib.optionals stdenv.isLinux [
-    # revert temporary directory creation, because it break the wrapper
-    # https://github.com/NixOS/nixpkgs/pull/289941#issuecomment-1980778358
-    (fetchpatch {
-      url = "https://github.com/leanprover/elan/commit/bd54acaab75d08b3912ee1f051af8657f3a9cfdf.patch";
-      hash = "sha256-6If/wxWSea8Zjlp3fx9wh3D0TjmWZbvCuY9q5c2qJGA=";
-      revert = true;
-    })
-
     # Run patchelf on the downloaded binaries.
     # This is necessary because Lean 4 is now dynamically linked.
     (runCommand "0001-dynamically-patchelf-binaries.patch" {
diff --git a/nixpkgs/pkgs/applications/science/logic/fast-downward/default.nix b/nixpkgs/pkgs/applications/science/logic/fast-downward/default.nix
index a73d141f45b8..77b538d1cbd8 100644
--- a/nixpkgs/pkgs/applications/science/logic/fast-downward/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/fast-downward/default.nix
@@ -59,6 +59,7 @@ stdenv.mkDerivation rec {
 
   meta = with lib; {
     description = "A domain-independent planning system";
+    mainProgram = "fast-downward";
     homepage = "https://www.fast-downward.org/";
     license = licenses.gpl3Plus;
     platforms = platforms.unix;
diff --git a/nixpkgs/pkgs/applications/science/logic/gappa/default.nix b/nixpkgs/pkgs/applications/science/logic/gappa/default.nix
index af6673caa54f..2eb8567aaa4c 100644
--- a/nixpkgs/pkgs/applications/science/logic/gappa/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/gappa/default.nix
@@ -17,6 +17,7 @@ stdenv.mkDerivation rec {
   meta = {
     homepage = "http://gappa.gforge.inria.fr/";
     description = "Verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic";
+    mainProgram = "gappa";
     license = with lib.licenses; [ cecill20 gpl2 ];
     maintainers = with lib.maintainers; [ vbgl ];
     platforms = lib.platforms.all;
diff --git a/nixpkgs/pkgs/applications/science/logic/glucose/default.nix b/nixpkgs/pkgs/applications/science/logic/glucose/default.nix
index 512f0414f1c6..a2392ef39861 100644
--- a/nixpkgs/pkgs/applications/science/logic/glucose/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/glucose/default.nix
@@ -40,6 +40,7 @@ stdenv.mkDerivation rec {
 
   meta = with lib; {
     description = "Modern, parallel SAT solver (${if enableUnfree then "parallel" else "sequential"} version)";
+    mainProgram = "glucose";
     homepage = "https://www.labri.fr/perso/lsimon/research/glucose/";
     license = if enableUnfree then licenses.unfreeRedistributable else licenses.mit;
     platforms = platforms.unix;
diff --git a/nixpkgs/pkgs/applications/science/logic/kissat/default.nix b/nixpkgs/pkgs/applications/science/logic/kissat/default.nix
index d1703340527b..65bcebdc6b1a 100644
--- a/nixpkgs/pkgs/applications/science/logic/kissat/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/kissat/default.nix
@@ -40,6 +40,7 @@ stdenv.mkDerivation rec {
 
   meta = with lib; {
     description = "A 'keep it simple and clean bare metal SAT solver' written in C";
+    mainProgram = "kissat";
     longDescription = ''
       Kissat is a "keep it simple and clean bare metal SAT solver" written in C.
       It is a port of CaDiCaL back to C with improved data structures,
diff --git a/nixpkgs/pkgs/applications/science/logic/lci/default.nix b/nixpkgs/pkgs/applications/science/logic/lci/default.nix
index 593b2c54c5cf..659855c23fb2 100644
--- a/nixpkgs/pkgs/applications/science/logic/lci/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/lci/default.nix
@@ -9,6 +9,7 @@ stdenv.mkDerivation rec {
   buildInputs = [readline];
   meta = {
     description = "Lambda calculus interpreter";
+    mainProgram = "lci";
     maintainers = with lib.maintainers; [raskin];
     platforms = with lib.platforms; linux;
     license = lib.licenses.gpl3;
diff --git a/nixpkgs/pkgs/applications/science/logic/lean4/default.nix b/nixpkgs/pkgs/applications/science/logic/lean4/default.nix
index fbc41a67d73b..dca55d969db4 100644
--- a/nixpkgs/pkgs/applications/science/logic/lean4/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/lean4/default.nix
@@ -50,11 +50,6 @@ stdenv.mkDerivation (finalAttrs: {
     "-DINSTALL_LICENSE=OFF"
   ];
 
-  # Work around https://github.com/NixOS/nixpkgs/issues/166205.
-  env = lib.optionalAttrs stdenv.cc.isClang {
-    NIX_LDFLAGS = "-l${stdenv.cc.libcxx.cxxabi.libName}";
-  };
-
   passthru.tests = {
     version = testers.testVersion {
       package = finalAttrs.finalPackage;
diff --git a/nixpkgs/pkgs/applications/science/logic/leo2/default.nix b/nixpkgs/pkgs/applications/science/logic/leo2/default.nix
index a72444adbba0..dcf2d5b7c33c 100644
--- a/nixpkgs/pkgs/applications/science/logic/leo2/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/leo2/default.nix
@@ -45,6 +45,7 @@ stdenv.mkDerivation rec {
 
   meta = with lib; {
     description = "A high-performance typed higher order prover";
+    mainProgram = "leo";
     maintainers = [ maintainers.raskin ];
     platforms = platforms.unix;
     license = licenses.bsd3;
diff --git a/nixpkgs/pkgs/applications/science/logic/leo3/binary.nix b/nixpkgs/pkgs/applications/science/logic/leo3/binary.nix
index 332b28db5fb6..0cdf8a4dc210 100644
--- a/nixpkgs/pkgs/applications/science/logic/leo3/binary.nix
+++ b/nixpkgs/pkgs/applications/science/logic/leo3/binary.nix
@@ -20,6 +20,7 @@ stdenv.mkDerivation rec {
 
   meta = with lib; {
     description = "An automated theorem prover for classical higher-order logic with choice";
+    mainProgram = "leo3";
     sourceProvenance = with sourceTypes; [ binaryBytecode ];
     license = licenses.bsd3;
     maintainers = [maintainers.raskin];
diff --git a/nixpkgs/pkgs/applications/science/logic/logisim-evolution/default.nix b/nixpkgs/pkgs/applications/science/logic/logisim-evolution/default.nix
index affbfc170b90..3d86c8cafdbc 100644
--- a/nixpkgs/pkgs/applications/science/logic/logisim-evolution/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/logisim-evolution/default.nix
@@ -1,25 +1,45 @@
-{ lib, stdenv, fetchurl, jre, makeWrapper, copyDesktopItems, makeDesktopItem, unzip }:
+{ lib
+, stdenv
+, fetchurl
+, jre
+, makeBinaryWrapper
+, copyDesktopItems
+, makeDesktopItem
+, desktopToDarwinBundle
+, unzip
+}:
 
-stdenv.mkDerivation rec {
+let
+  icon = fetchurl {
+    url = "https://github.com/logisim-evolution/logisim-evolution/raw/9e0afa3cd6a8bfa75dab61830822cde83c70bb4b/artwork/logisim-evolution-icon.svg";
+    hash = "sha256-DNRimhNFt6jLdjqv7o2cNz38K6XnevxD0rGymym3xBs=";
+  };
+in
+stdenv.mkDerivation (finalAttrs: {
   pname = "logisim-evolution";
   version = "3.8.0";
 
   src = fetchurl {
-    url = "https://github.com/logisim-evolution/logisim-evolution/releases/download/v${version}/logisim-evolution-${version}-all.jar";
-    sha256 = "sha256-TFm+fa3CMp0OMhnKBc6cLIWGQbIG/OpOOCG7ea7wbCw=";
+    url = "https://github.com/logisim-evolution/logisim-evolution/releases/download/v${finalAttrs.version}/logisim-evolution-${finalAttrs.version}-all.jar";
+    hash = "sha256-TFm+fa3CMp0OMhnKBc6cLIWGQbIG/OpOOCG7ea7wbCw=";
   };
-
   dontUnpack = true;
 
-  nativeBuildInputs = [ makeWrapper copyDesktopItems unzip ];
+  nativeBuildInputs = [
+    makeBinaryWrapper
+    copyDesktopItems
+    unzip
+  ] ++ lib.optionals stdenv.isDarwin [
+    desktopToDarwinBundle
+  ];
 
   desktopItems = [
     (makeDesktopItem {
-      name = pname;
+      name = "logisim-evolution";
       desktopName = "Logisim-evolution";
       exec = "logisim-evolution";
       icon = "logisim-evolution";
-      comment = meta.description;
+      comment = finalAttrs.meta.description;
       categories = [ "Education" ];
     })
   ];
@@ -29,22 +49,19 @@ stdenv.mkDerivation rec {
 
     mkdir -p $out/bin
     makeWrapper ${jre}/bin/java $out/bin/logisim-evolution --add-flags "-jar $src"
-
-    # Create icons
-    unzip $src "resources/logisim/img/*"
-    for size in 16 32 48 128 256; do
-      install -D "./resources/logisim/img/logisim-icon-$size.png" "$out/share/icons/hicolor/''${size}x''${size}/apps/logisim-evolution.png"
-    done
+    install -Dm444 ${icon} $out/share/icons/hicolor/scalable/apps/logisim-evolution.svg
 
     runHook postInstall
   '';
 
-  meta = with lib; {
+  meta = {
+    changelog = "https://github.com/logisim-evolution/logisim-evolution/releases/tag/v${finalAttrs.version}";
     homepage = "https://github.com/logisim-evolution/logisim-evolution";
     description = "Digital logic designer and simulator";
-    maintainers = with maintainers; [ emilytrau ];
-    sourceProvenance = with sourceTypes; [ binaryBytecode ];
-    license = licenses.gpl2Plus;
-    platforms = platforms.unix;
+    mainProgram = "logisim-evolution";
+    maintainers = with lib.maintainers; [ emilytrau ];
+    sourceProvenance = with lib.sourceTypes; [ binaryBytecode ];
+    license = lib.licenses.gpl3Only;
+    platforms = lib.platforms.unix;
   };
-}
+})
diff --git a/nixpkgs/pkgs/applications/science/logic/logisim/default.nix b/nixpkgs/pkgs/applications/science/logic/logisim/default.nix
index ea8a1416a77a..d278f1e78468 100644
--- a/nixpkgs/pkgs/applications/science/logic/logisim/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/logisim/default.nix
@@ -1,25 +1,39 @@
-{ lib, stdenv, fetchurl, jre, makeWrapper, copyDesktopItems, makeDesktopItem, unzip }:
+{ lib
+, stdenv
+, fetchurl
+, jre
+, makeBinaryWrapper
+, copyDesktopItems
+, makeDesktopItem
+, desktopToDarwinBundle
+, unzip
+}:
 
-stdenv.mkDerivation rec {
+stdenv.mkDerivation (finalAttrs: {
   pname = "logisim";
   version = "2.7.1";
 
   src = fetchurl {
-    url = "mirror://sourceforge/project/circuit/${lib.versions.majorMinor version}.x/${version}/logisim-generic-${version}.jar";
-    sha256 = "1hkvc9zc7qmvjbl9579p84hw3n8wl3275246xlzj136i5b0phain";
+    url = "mirror://sourceforge/project/circuit/${lib.versions.majorMinor finalAttrs.version}.x/${finalAttrs.version}/logisim-generic-${finalAttrs.version}.jar";
+    hash = "sha256-Nip4wSrRjCA/7YaIcsSgHNnBIUE3nZLokrviw35ie8I=";
   };
-
   dontUnpack = true;
 
-  nativeBuildInputs = [ makeWrapper copyDesktopItems unzip ];
+  nativeBuildInputs = [
+    makeBinaryWrapper
+    copyDesktopItems
+    unzip
+  ] ++ lib.optionals stdenv.isDarwin [
+    desktopToDarwinBundle
+  ];
 
   desktopItems = [
     (makeDesktopItem {
-      name = pname;
+      name = "logisim";
       desktopName = "Logisim";
       exec = "logisim";
       icon = "logisim";
-      comment = meta.description;
+      comment = finalAttrs.meta.description;
       categories = [ "Education" ];
     })
   ];
@@ -34,18 +48,19 @@ stdenv.mkDerivation rec {
     unzip $src "resources/logisim/img/*"
     for size in 16 20 24 48 64 128
     do
-      install -D "./resources/logisim/img/logisim-icon-$size.png" "$out/share/icons/hicolor/''${size}x''${size}/apps/logisim.png"
+      install -Dm444 "./resources/logisim/img/logisim-icon-$size.png" "$out/share/icons/hicolor/''${size}x''${size}/apps/logisim.png"
     done
 
     runHook postInstall
   '';
 
-  meta = with lib; {
+  meta = {
     homepage = "http://www.cburch.com/logisim/";
     description = "Educational tool for designing and simulating digital logic circuits";
-    maintainers = with maintainers; [ emilytrau ];
-    sourceProvenance = with sourceTypes; [ binaryBytecode ];
-    license = licenses.gpl2Plus;
-    platforms = platforms.unix;
+    mainProgram = "logisim";
+    maintainers = with lib.maintainers; [ emilytrau ];
+    sourceProvenance = with lib.sourceTypes; [ binaryBytecode ];
+    license = lib.licenses.gpl2Only;
+    platforms = lib.platforms.unix;
   };
-}
+})
diff --git a/nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix b/nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix
index 30c13c6036f9..19ade58fbfaa 100644
--- a/nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix
@@ -23,6 +23,7 @@ stdenv.mkDerivation rec {
 
   meta = {
     description = "Fast translation from LTL formulae to Buchi automata";
+    mainProgram = "ltl2ba";
     homepage    = "http://www.lsv.ens-cachan.fr/~gastin/ltl2ba";
     license     = lib.licenses.gpl2Plus;
     platforms   = lib.platforms.darwin ++ lib.platforms.linux;
diff --git a/nixpkgs/pkgs/applications/science/logic/metis-prover/default.nix b/nixpkgs/pkgs/applications/science/logic/metis-prover/default.nix
index 5b17403dc7f4..bd6f71860bdb 100644
--- a/nixpkgs/pkgs/applications/science/logic/metis-prover/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/metis-prover/default.nix
@@ -24,6 +24,7 @@ stdenv.mkDerivation {
 
   meta = with lib; {
     description = "Automatic theorem prover for first-order logic with equality";
+    mainProgram = "metis";
     homepage = "https://www.gilith.com/research/metis/";
     license = licenses.mit;
     maintainers = with maintainers; [ gebner ];
diff --git a/nixpkgs/pkgs/applications/science/logic/monosat/default.nix b/nixpkgs/pkgs/applications/science/logic/monosat/default.nix
index 5b894d2c9376..067ba8ceb1b3 100644
--- a/nixpkgs/pkgs/applications/science/logic/monosat/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/monosat/default.nix
@@ -61,6 +61,7 @@ let
 
     meta = {
       description = "SMT solver for Monotonic Theories";
+      mainProgram = "monosat";
       platforms   = platforms.unix;
       license     = if includeGplCode then licenses.gpl2 else licenses.mit;
       homepage    = "https://github.com/sambayless/monosat";
diff --git a/nixpkgs/pkgs/applications/science/logic/msat/default.nix b/nixpkgs/pkgs/applications/science/logic/msat/default.nix
index dc2b1a221199..299fe95224eb 100644
--- a/nixpkgs/pkgs/applications/science/logic/msat/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/msat/default.nix
@@ -9,5 +9,6 @@ with ocamlPackages; buildDunePackage {
 
   meta = msat.meta // {
     description = "SAT solver binary based on the msat library";
+    mainProgram = "msat";
   };
 }
diff --git a/nixpkgs/pkgs/applications/science/logic/naproche/default.nix b/nixpkgs/pkgs/applications/science/logic/naproche/default.nix
index f6743745a7b6..d2070ba8240f 100644
--- a/nixpkgs/pkgs/applications/science/logic/naproche/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/naproche/default.nix
@@ -2,13 +2,13 @@
 
 with haskellPackages; mkDerivation {
   pname = "Naproche-SAD";
-  version = "unstable-2023-07-11";
+  version = "unstable-2024-01-18";
 
   src = fetchFromGitHub {
     owner = "naproche";
     repo = "naproche";
-    rev = "4c399d49a86987369bec6e1ac5ae3739cd6db0a8";
-    sha256 = "sha256-Ji6yxbDEcwuYAzIZwK5sHNltK1WBFBfpyoEtoID/U4k=";
+    rev = "bb3dbcbd2173e3334bc5bdcd04c07c6836a11387";
+    hash = "sha256-DWcowUjy8/VBuhqvDYlVINHssF4KhuzT0L+m1YwUxoE=";
   };
 
   isExecutable = true;
@@ -20,11 +20,7 @@ with haskellPackages; mkDerivation {
   ];
 
   prePatch = "hpack";
-
-  checkPhase = ''
-    export NAPROCHE_EPROVER=${eprover}/bin/eprover
-    dist/build/Naproche-SAD/Naproche-SAD examples/cantor.ftl.tex -t 60 --tex=on
-  '';
+  doCheck = false; # Tests are broken in upstream
 
   postInstall = ''
     wrapProgram $out/bin/Naproche-SAD \
@@ -35,4 +31,5 @@ with haskellPackages; mkDerivation {
   description = "Write formal proofs in natural language and LaTeX";
   maintainers = with lib.maintainers; [ jvanbruegge ];
   license = lib.licenses.gpl3Only;
+  mainProgram = "Naproche-SAD";
 }
diff --git a/nixpkgs/pkgs/applications/science/logic/open-wbo/default.nix b/nixpkgs/pkgs/applications/science/logic/open-wbo/default.nix
index 3677eb39de6a..2290ff29224b 100644
--- a/nixpkgs/pkgs/applications/science/logic/open-wbo/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/open-wbo/default.nix
@@ -21,6 +21,7 @@ stdenv.mkDerivation {
   meta = with lib; {
     broken = (stdenv.isLinux && stdenv.isAarch64);
     description = "State-of-the-art MaxSAT and Pseudo-Boolean solver";
+    mainProgram = "open-wbo";
     maintainers = with maintainers; [ gebner ];
     platforms = platforms.unix;
     license = licenses.mit;
diff --git a/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix b/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix
index 6d073400209d..4a5f453f3547 100644
--- a/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix
@@ -31,6 +31,7 @@ stdenv.mkDerivation rec {
   meta = with lib; {
     broken = (stdenv.isLinux && stdenv.isAarch64);
     description = "A satisfiability modulo theory (SMT) solver";
+    mainProgram = "opensmt";
     maintainers = [ maintainers.raskin ];
     platforms = platforms.linux;
     license = if enableReadline then licenses.gpl2Plus else licenses.mit;
diff --git a/nixpkgs/pkgs/applications/science/logic/ott/default.nix b/nixpkgs/pkgs/applications/science/logic/ott/default.nix
index a00c565fb4e0..b8197aaa4123 100644
--- a/nixpkgs/pkgs/applications/science/logic/ott/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/ott/default.nix
@@ -29,6 +29,7 @@ stdenv.mkDerivation rec {
 
   meta = {
     description = "A tool for the working semanticist";
+    mainProgram = "ott";
     longDescription = ''
       Ott is a tool for writing definitions of programming languages and
       calculi. It takes as input a definition of a language syntax and
diff --git a/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix b/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix
index 4966bf608bc9..957ebfd3ec43 100644
--- a/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix
+++ b/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix
@@ -32,6 +32,7 @@ stdenv.mkDerivation rec {
 
   meta = {
     description = "Extension of clingo to handle constraints over integers";
+    mainProgram = "clingcon";
     license = lib.licenses.mit;
     platforms = lib.platforms.unix;
     homepage = "https://potassco.org/";
diff --git a/nixpkgs/pkgs/applications/science/logic/prooftree/default.nix b/nixpkgs/pkgs/applications/science/logic/prooftree/default.nix
index 4e65c018d1a2..adb64f02c14f 100644
--- a/nixpkgs/pkgs/applications/science/logic/prooftree/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/prooftree/default.nix
@@ -19,6 +19,7 @@ stdenv.mkDerivation rec {
 
   meta = with lib; {
     description = "A program for proof-tree visualization";
+    mainProgram = "prooftree";
     longDescription = ''
       Prooftree is a program for proof-tree visualization during interactive
       proof development in a theorem prover. It is currently being developed
diff --git a/nixpkgs/pkgs/applications/science/logic/redprl/default.nix b/nixpkgs/pkgs/applications/science/logic/redprl/default.nix
index 656f3f1b653e..2749730f9d66 100644
--- a/nixpkgs/pkgs/applications/science/logic/redprl/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/redprl/default.nix
@@ -29,6 +29,7 @@ stdenv.mkDerivation {
 
   meta = with lib; {
     description = "A proof assistant for Nominal Computational Type Theory";
+    mainProgram = "redprl";
     homepage = "http://www.redprl.org/";
     license = licenses.mit;
     maintainers = with maintainers; [ acowley ];
diff --git a/nixpkgs/pkgs/applications/science/logic/satallax/default.nix b/nixpkgs/pkgs/applications/science/logic/satallax/default.nix
index af11cd0d6d8f..bd3e9d3e8351 100644
--- a/nixpkgs/pkgs/applications/science/logic/satallax/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/satallax/default.nix
@@ -80,6 +80,7 @@ stdenv.mkDerivation rec {
 
   meta = {
     description = "Automated theorem prover for higher-order logic";
+    mainProgram = "satallax";
     license = lib.licenses.mit;
     maintainers = [ lib.maintainers.raskin ];
     platforms = lib.platforms.unix;
diff --git a/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix b/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix
index 86c3db9942a1..288ddc06806a 100644
--- a/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix
+++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix
@@ -90,6 +90,7 @@ stdenv.mkDerivation rec {
   meta = {
     homepage = "http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html";
     description = "IDE for the TLA+ tools";
+    mainProgram = "tla-toolbox";
     longDescription = ''
       Integrated development environment for the TLA+ tools, based on Eclipse. You can use it
       to create and edit your specs, run the PlusCal translator, view the pretty-printed
diff --git a/nixpkgs/pkgs/applications/science/logic/vampire/default.nix b/nixpkgs/pkgs/applications/science/logic/vampire/default.nix
index a3c1aa3f131d..62427e2ee455 100644
--- a/nixpkgs/pkgs/applications/science/logic/vampire/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/vampire/default.nix
@@ -47,6 +47,7 @@ stdenv.mkDerivation rec {
   meta = with lib; {
     homepage = "https://vprover.github.io/";
     description = "The Vampire Theorem Prover";
+    mainProgram = "vampire";
     platforms = platforms.unix;
     license = licenses.bsd3;
     maintainers = with maintainers; [ gebner ];
diff --git a/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix b/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix
index 89f6e23c79d3..cc512acad793 100644
--- a/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix
@@ -25,6 +25,7 @@ stdenv.mkDerivation rec {
   meta = {
     homepage = "https://workcraft.org/";
     description = "Framework for interpreted graph modeling, verification and synthesis";
+    mainProgram = "workcraft";
     platforms = lib.platforms.linux;
     license = lib.licenses.mit;
     maintainers = with lib.maintainers; [ timor ];
diff --git a/nixpkgs/pkgs/applications/science/logic/z3/default.nix b/nixpkgs/pkgs/applications/science/logic/z3/default.nix
index b247599a0813..f35da4a732b0 100644
--- a/nixpkgs/pkgs/applications/science/logic/z3/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/z3/default.nix
@@ -79,6 +79,7 @@ let common = { version, sha256, patches ? [ ], tag ? "z3" }:
 
     meta = with lib; {
       description = "A high-performance theorem prover and SMT solver";
+      mainProgram = "z3";
       homepage = "https://github.com/Z3Prover/z3";
       changelog = "https://github.com/Z3Prover/z3/releases/tag/z3-${version}";
       license = licenses.mit;
diff --git a/nixpkgs/pkgs/applications/science/logic/zchaff/default.nix b/nixpkgs/pkgs/applications/science/logic/zchaff/default.nix
index 57f673042dc8..5e22ff448ed3 100644
--- a/nixpkgs/pkgs/applications/science/logic/zchaff/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/zchaff/default.nix
@@ -24,6 +24,7 @@ clangStdenv.mkDerivation rec {
   meta = with lib; {
     homepage = "https://www.princeton.edu/~chaff/zchaf";
     description = "Accelerated SAT Solver from Princeton";
+    mainProgram = "zchaff";
     license = licenses.mit;
     maintainers = with maintainers; [ siraben ];
     platforms = platforms.unix;