diff options
Diffstat (limited to 'pkgs/applications/science/logic')
43 files changed, 130 insertions, 72 deletions
diff --git a/pkgs/applications/science/logic/abella/default.nix b/pkgs/applications/science/logic/abella/default.nix index 4483b8ad4756a..7878626d6e9a3 100644 --- a/pkgs/applications/science/logic/abella/default.nix +++ b/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/pkgs/applications/science/logic/anders/default.nix b/pkgs/applications/science/logic/anders/default.nix index eb2be71f16815..dff6c86703d41 100644 --- a/pkgs/applications/science/logic/anders/default.nix +++ b/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/pkgs/applications/science/logic/bitwuzla/default.nix b/pkgs/applications/science/logic/bitwuzla/default.nix index 4af4058339d93..bacf8620e5fdc 100644 --- a/pkgs/applications/science/logic/bitwuzla/default.nix +++ b/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/pkgs/applications/science/logic/celf/default.nix b/pkgs/applications/science/logic/celf/default.nix index 044a6f3ca1c47..e1f0c237f6732 100644 --- a/pkgs/applications/science/logic/celf/default.nix +++ b/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/pkgs/applications/science/logic/clprover/clprover.nix b/pkgs/applications/science/logic/clprover/clprover.nix index 2a8c058a80bbc..543c6cb4310bd 100644 --- a/pkgs/applications/science/logic/clprover/clprover.nix +++ b/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/pkgs/applications/science/logic/cryptominisat/default.nix b/pkgs/applications/science/logic/cryptominisat/default.nix index f2e3eaab91dc7..4be57a1946356 100644 --- a/pkgs/applications/science/logic/cryptominisat/default.nix +++ b/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/pkgs/applications/science/logic/cryptoverif/default.nix b/pkgs/applications/science/logic/cryptoverif/default.nix index 5c15b8a17241f..4b74cdd518ca2 100644 --- a/pkgs/applications/science/logic/cryptoverif/default.nix +++ b/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/pkgs/applications/science/logic/cubicle/default.nix b/pkgs/applications/science/logic/cubicle/default.nix index c9382c5d0f1a7..03409e68ea336 100644 --- a/pkgs/applications/science/logic/cubicle/default.nix +++ b/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/pkgs/applications/science/logic/cvc3/default.nix b/pkgs/applications/science/logic/cvc3/default.nix index 0385909610e61..bec5a89cc691b 100644 --- a/pkgs/applications/science/logic/cvc3/default.nix +++ b/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/pkgs/applications/science/logic/cvc4/default.nix b/pkgs/applications/science/logic/cvc4/default.nix index 1513c74779851..ac45db8cb3127 100644 --- a/pkgs/applications/science/logic/cvc4/default.nix +++ b/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/pkgs/applications/science/logic/cvc5/default.nix b/pkgs/applications/science/logic/cvc5/default.nix index 2dff344e4edb7..d34b293372968 100644 --- a/pkgs/applications/science/logic/cvc5/default.nix +++ b/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/pkgs/applications/science/logic/dafny/default.nix b/pkgs/applications/science/logic/dafny/default.nix index 5f56d612ab249..83d472c1abb18 100644 --- a/pkgs/applications/science/logic/dafny/default.nix +++ b/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/pkgs/applications/science/logic/dafny/deps.nix b/pkgs/applications/science/logic/dafny/deps.nix index a786d8b3d6fd4..91fe5624ac7f7 100644 --- a/pkgs/applications/science/logic/dafny/deps.nix +++ b/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/pkgs/applications/science/logic/easycrypt/default.nix b/pkgs/applications/science/logic/easycrypt/default.nix index 2869bcd6e1e3c..782d15d615599 100644 --- a/pkgs/applications/science/logic/easycrypt/default.nix +++ b/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/pkgs/applications/science/logic/easycrypt/runtest.nix b/pkgs/applications/science/logic/easycrypt/runtest.nix index c0d72d96e1d10..b714dc14991b7 100644 --- a/pkgs/applications/science/logic/easycrypt/runtest.nix +++ b/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/pkgs/applications/science/logic/egglog/default.nix b/pkgs/applications/science/logic/egglog/default.nix index ab5653b50912e..8b94c449c6be2 100644 --- a/pkgs/applications/science/logic/egglog/default.nix +++ b/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/pkgs/applications/science/logic/fast-downward/default.nix b/pkgs/applications/science/logic/fast-downward/default.nix index a73d141f45b8f..77b538d1cbd86 100644 --- a/pkgs/applications/science/logic/fast-downward/default.nix +++ b/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/pkgs/applications/science/logic/gappa/default.nix b/pkgs/applications/science/logic/gappa/default.nix index af6673caa54f3..2eb8567aaa4ce 100644 --- a/pkgs/applications/science/logic/gappa/default.nix +++ b/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/pkgs/applications/science/logic/glucose/default.nix b/pkgs/applications/science/logic/glucose/default.nix index 512f0414f1c69..a2392ef398610 100644 --- a/pkgs/applications/science/logic/glucose/default.nix +++ b/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/pkgs/applications/science/logic/kissat/default.nix b/pkgs/applications/science/logic/kissat/default.nix index d1703340527b5..65bcebdc6b1a1 100644 --- a/pkgs/applications/science/logic/kissat/default.nix +++ b/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/pkgs/applications/science/logic/lci/default.nix b/pkgs/applications/science/logic/lci/default.nix index 593b2c54c5cf0..659855c23fb2d 100644 --- a/pkgs/applications/science/logic/lci/default.nix +++ b/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/pkgs/applications/science/logic/lean4/default.nix b/pkgs/applications/science/logic/lean4/default.nix index fbc41a67d73ba..dca55d969db4d 100644 --- a/pkgs/applications/science/logic/lean4/default.nix +++ b/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/pkgs/applications/science/logic/leo2/default.nix b/pkgs/applications/science/logic/leo2/default.nix index a72444adbba02..dcf2d5b7c33c3 100644 --- a/pkgs/applications/science/logic/leo2/default.nix +++ b/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/pkgs/applications/science/logic/leo3/binary.nix b/pkgs/applications/science/logic/leo3/binary.nix index 332b28db5fb62..0cdf8a4dc2103 100644 --- a/pkgs/applications/science/logic/leo3/binary.nix +++ b/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/pkgs/applications/science/logic/logisim-evolution/default.nix b/pkgs/applications/science/logic/logisim-evolution/default.nix index affbfc170b901..3d86c8cafdbc2 100644 --- a/pkgs/applications/science/logic/logisim-evolution/default.nix +++ b/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/pkgs/applications/science/logic/logisim/default.nix b/pkgs/applications/science/logic/logisim/default.nix index ea8a1416a77a4..d278f1e784687 100644 --- a/pkgs/applications/science/logic/logisim/default.nix +++ b/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/pkgs/applications/science/logic/ltl2ba/default.nix b/pkgs/applications/science/logic/ltl2ba/default.nix index 30c13c6036f96..19ade58fbfaa1 100644 --- a/pkgs/applications/science/logic/ltl2ba/default.nix +++ b/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/pkgs/applications/science/logic/metis-prover/default.nix b/pkgs/applications/science/logic/metis-prover/default.nix index 5b17403dc7f4b..bd6f71860bdb9 100644 --- a/pkgs/applications/science/logic/metis-prover/default.nix +++ b/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/pkgs/applications/science/logic/monosat/default.nix b/pkgs/applications/science/logic/monosat/default.nix index 5b894d2c9376f..067ba8ceb1b33 100644 --- a/pkgs/applications/science/logic/monosat/default.nix +++ b/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/pkgs/applications/science/logic/msat/default.nix b/pkgs/applications/science/logic/msat/default.nix index dc2b1a2211993..299fe95224eba 100644 --- a/pkgs/applications/science/logic/msat/default.nix +++ b/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/pkgs/applications/science/logic/naproche/default.nix b/pkgs/applications/science/logic/naproche/default.nix index f6743745a7b64..d2070ba8240ff 100644 --- a/pkgs/applications/science/logic/naproche/default.nix +++ b/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/pkgs/applications/science/logic/open-wbo/default.nix b/pkgs/applications/science/logic/open-wbo/default.nix index 3677eb39de6aa..2290ff29224b4 100644 --- a/pkgs/applications/science/logic/open-wbo/default.nix +++ b/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/pkgs/applications/science/logic/opensmt/default.nix b/pkgs/applications/science/logic/opensmt/default.nix index 6d073400209de..4a5f453f35478 100644 --- a/pkgs/applications/science/logic/opensmt/default.nix +++ b/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/pkgs/applications/science/logic/ott/default.nix b/pkgs/applications/science/logic/ott/default.nix index a00c565fb4e06..b8197aaa41230 100644 --- a/pkgs/applications/science/logic/ott/default.nix +++ b/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/pkgs/applications/science/logic/potassco/clingcon.nix b/pkgs/applications/science/logic/potassco/clingcon.nix index 4966bf608bc98..957ebfd3ec43f 100644 --- a/pkgs/applications/science/logic/potassco/clingcon.nix +++ b/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/pkgs/applications/science/logic/prooftree/default.nix b/pkgs/applications/science/logic/prooftree/default.nix index 4e65c018d1a20..adb64f02c14f8 100644 --- a/pkgs/applications/science/logic/prooftree/default.nix +++ b/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/pkgs/applications/science/logic/redprl/default.nix b/pkgs/applications/science/logic/redprl/default.nix index 656f3f1b653e9..2749730f9d667 100644 --- a/pkgs/applications/science/logic/redprl/default.nix +++ b/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/pkgs/applications/science/logic/satallax/default.nix b/pkgs/applications/science/logic/satallax/default.nix index af11cd0d6d8f9..bd3e9d3e8351e 100644 --- a/pkgs/applications/science/logic/satallax/default.nix +++ b/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/pkgs/applications/science/logic/tlaplus/toolbox.nix b/pkgs/applications/science/logic/tlaplus/toolbox.nix index 86c3db9942a1e..288ddc06806a8 100644 --- a/pkgs/applications/science/logic/tlaplus/toolbox.nix +++ b/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/pkgs/applications/science/logic/vampire/default.nix b/pkgs/applications/science/logic/vampire/default.nix index a3c1aa3f131d9..62427e2ee4554 100644 --- a/pkgs/applications/science/logic/vampire/default.nix +++ b/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/pkgs/applications/science/logic/workcraft/default.nix b/pkgs/applications/science/logic/workcraft/default.nix index 89f6e23c79d32..cc512acad7937 100644 --- a/pkgs/applications/science/logic/workcraft/default.nix +++ b/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/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix index b247599a0813a..f35da4a732b09 100644 --- a/pkgs/applications/science/logic/z3/default.nix +++ b/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/pkgs/applications/science/logic/zchaff/default.nix b/pkgs/applications/science/logic/zchaff/default.nix index 57f673042dc8a..5e22ff448ed37 100644 --- a/pkgs/applications/science/logic/zchaff/default.nix +++ b/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; |