Commit graph

737 commits

Author SHA1 Message Date
Austin Seipp 5069fa0a30 nixpkgs: remove sapic-0.9
SAPIC is bundled with Tamarin and doesn't have separate releases
anymore; add an appropriate 'throw' clause to the alias so people know
where to find it.

Signed-off-by: Austin Seipp <aseipp@pobox.com>
2019-01-19 18:54:38 -06:00
Austin Seipp fc159594a7 tamarin-prover: 1.4.0 -> 1.4.1, bundled sapic
With this, we can drop the old 1.4.0 patches for 8.4 support, since
those are now upstream.

Furthermore, SAPIC Is now bundled inside Tamarin, so we can drop the
external dependency. (This includes a patch that compiles SAPIC to
native code, much like the original, to reduce closure size.)

Signed-off-by: Austin Seipp <aseipp@pobox.com>
2019-01-19 18:54:38 -06:00
rnhmjoj bcf54ce5bb
treewide: use ${stdenv.shell} instead of /bin/sh where possible 2019-01-16 20:37:15 +01:00
Gabriel Ebner 49db581e8c elan: 0.7.1 -> 0.7.2 2019-01-15 10:05:45 +01:00
Austin Seipp c10650760d yices: s/fetchurl/fetchFromGitHub/
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2019-01-08 19:15:24 -06:00
Austin Seipp 38aa0a3df4 z3: 4.8.3 -> 4.8.4
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2019-01-08 19:15:24 -06:00
Austin Seipp d77f381055 symbiyosys: 2018.09.12 -> 2018.12.09
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2019-01-08 19:15:24 -06:00
Simon Lackerbauer f7367cbf1c abella: 2.0.5 -> 2.0.6 2019-01-08 17:05:30 +00:00
Jörg Thalheim 37fe593d48
cryptominisat: switch to python3 2019-01-05 16:38:10 +01:00
Jörg Thalheim 4a4d1d6497
cryptominisat: 5.0.1 -> 5.6.6 2019-01-05 12:45:44 +01:00
Vincent Laporte ea92816c74 why3: 1.1.0 -> 1.1.1 (#52980) 2018-12-29 21:05:23 +01:00
Samuel Dionne-Riel 3c38cc8058
Merge pull request #51813 from samueldr/aarch64/disable-non-arm-builds-part-1
aarch64: ZHF for aarch64 (1/??)
2018-12-20 21:06:52 -05:00
R. RyanTM ae22d3dc85 cubicle: 1.1.1 -> 1.1.2
Semi-automatic update generated by
https://github.com/ryantm/nixpkgs-update tools. This update was made
based on information from
https://repology.org/metapackage/cubicle/versions
2018-12-16 17:24:47 +01:00
Samuel Dionne-Riel 5e1dfd3025 avy: Disable build on aarch64-linux 2018-12-10 14:55:20 -05:00
Samuel Dionne-Riel 7aabdea1ca aspino: Disable build on aarch64-linux
This is due to glucose not building.
2018-12-10 14:55:20 -05:00
Samuel Dionne-Riel 516f436614 glucose: Disable build on aarch64-linux 2018-12-10 14:55:20 -05:00
Will Dietz a034d90e3b z3: 4.8.1 -> 4.8.3
https://github.com/Z3Prover/z3/releases/tag/z3-4.8.3
2018-11-27 22:00:19 -06:00
Gabriel Ebner 4e1323a0cf vampire: fix nondeterministic hash
Probably related to #8567
2018-11-22 14:15:55 +01:00
Gabriel Ebner f505340252 iprover: 2.5 -> 2018_Jul_24_11h 2018-11-21 12:15:48 +01:00
R. RyanTM 5648699f6c ltl2ba: 1.2b1 -> 1.2
Semi-automatic update generated by
https://github.com/ryantm/nixpkgs-update tools. This update was made
based on information from
https://repology.org/metapackage/ltl2ba/versions
2018-11-19 02:28:38 -08:00
Jörg Thalheim 218f12db70
Merge pull request #50324 from asymmetric/solc
solc: 0.4.25 -> 0.5.0
2018-11-15 21:26:32 +00:00
Jörg Thalheim abb0c81190
z3: restrict to x86_64
it uses x86-only header:

include <immintrin.h>
          ^~~~~~~~~~~~~
compilation terminated.
src/sat/sat_probing.cpp
make: *** [Makefile:182: util/mpz.o] Error 1
make: *** Waiting for unfinished jobs....
src/sat/sat_parallel.cpp
builder for '/nix/store/vd2wkhic8g77izxv659ackh6hcaamic3-z3-4.8.1.drv' failed with exit code 2
cannot build derivation '/nix/store/h5imnjsf31c45l558gw66vyzb0ickc1m-solc-0.5.0.drv': 1 dependencies couldn't be built
error: build of '/nix/store/h5imnjsf31c45l558gw66vyzb0ickc1m-solc-0.5.0.drv' failed
2018-11-15 21:25:53 +00:00
Piotr Bogdan 5d0eeeee38 coq2html: switch to default make 2018-11-15 17:41:25 +00:00
Gabriel Ebner b1c149d47a tptp: use urls instead of url
nix-prefetch-url breaks if the url argument to fetchurl is a list.
2018-11-15 15:56:18 +01:00
Gabriel Ebner b3844d00f6 tptp: 7.1.0 -> 7.2.0 2018-11-15 15:50:48 +01:00
Gabriel Ebner 155595b0c7 eprover: 2.1 -> 2.2 2018-11-07 22:33:25 +01:00
Jörg Thalheim b3ed2b4c18
Merge pull request #49728 from vbgl/acgtk-1.5.0
acgtk: 1.3.1 -> 1.5.0
2018-11-04 17:09:34 +00:00
Théo Zimmermann dd21f83950 coq_8_9: init at 8.9+beta1 2018-11-04 07:26:29 +00:00
Vincent Laporte 08ac103970
acgtk: 1.3.1 -> 1.5.0 2018-11-04 06:29:27 +00:00
Kevin Quick 411c665f33
yices: 2.6.0 -> 2.6.1 2018-11-02 15:49:09 -07:00
Will Dietz c417342cd2
Merge pull request #48579 from dtzWill/update/z3-4.8.1
z3: 4.7.1 -> 4.8.1
2018-11-02 04:02:24 -05:00
Jörg Thalheim 8df0ca2bbc
coq_8_4: remove
verasco was its only user
2018-10-30 13:31:11 +00:00
Joachim F b6a5cd8970
Merge pull request #48812 from mpickering/cedille
cedille bug fixes
2018-10-24 15:29:47 +00:00
Matthew Pickering 08e5ef20d8 cedille: Make a seperate output for the base library
For now, for normal usage you need to add `${cedille.lib}` to
the `~/.cedille/options` file so that cedille will find the base
libraries. There is no option to pass options by the command line.
2018-10-22 08:43:07 +00:00
Matthew Pickering f7d4bc2c71 cedille: Apply patch which unbreaks the options file
See https://github.com/cedille/cedille/issues/29
2018-10-22 08:42:01 +00:00
Vincent Laporte c091e93b99
Merge pull request #48617 from Zimmi48/passthru-ocamlPackages-in-coq-package
coq: add ocamlPackages in passthru
2018-10-19 09:38:07 +00:00
Vincent Laporte bc8d25c1ef
why3: 1.0.0 -> 1.1.0 2018-10-18 05:43:36 +00:00
Théo Zimmermann fa12476755
coq: add ocamlPackages in passthru
We might need OCaml packages that are not the one Coq is depending on
but they still need to come from the same package set (same OCaml version).
2018-10-17 13:26:43 +02:00
Will Dietz 51e511130a z3: 4.7.1 -> 4.8.1 2018-10-16 12:28:06 -05:00
Matthew Pickering 43ae33728b cedille: init at 1.0.0 2018-10-14 19:17:23 +00:00
Moritz Kiefer 6738033727
alt-ergo: 1.30->2.2.0, ocplib-simplex: 0.3->0.4 2018-10-13 17:45:45 +00:00
Vincent Laporte 6113d95235
prooftree: cleaning 2018-10-11 05:59:21 +00:00
Théo Zimmermann 2fdd38ed2d
camlp5_transitional: remove in favor of camlp5 (strict) 2018-10-10 19:44:54 +02:00
Théo Zimmermann 7ac0a23194
prooftree: 0.12 -> 0.13 2018-10-10 19:42:50 +02:00
Théo Zimmermann c76ffb9253
matita: remove broken package
As requested by Vincent Laporte.
2018-10-09 09:47:31 +02:00
Théo Zimmermann 34394a38ef
ocamlPackages_3_11_2: remove
This requires removing also the Coq 8.3 and Matita 0.5.8 packages.

Coq 8.3 was released 8 years ago (2010) and there is no trace left
of users of this version (contrary to Coq 8.4, released 2012).
It is well over time to remove it.

Matita 0.5.8 was released in 2010 and because this version was still
used for teaching according to the official website, a legacy release
(0.5.9) was released in 5 years later to compile with more recent
OCaml libraries.
Updating to 0.5.9 (or a more recent version like 0.99.3) should allow
getting rid of the dependency on older OCaml but it is hard to test
given that the package is already broken before this update.
2018-10-08 21:10:05 +02:00
Marco Maggesi 9a5f7b1630 hol_light: 2017-07-06 -> 2018-09-30
Also handle compatibility with newer version of OCaml (depend on num
library as needed).
2018-10-06 15:49:09 +00:00
Gabriel Ebner 0a7e258012 elan: 0.5.0 -> 0.7.1 2018-10-04 16:33:36 +02:00
Austin Seipp 919a3b7f9c symbiyosys: 2018.07.26 -> 2018.09.12
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2018-10-01 22:32:54 -05:00
Will Dietz eb91037e7b tree-wide: patchelf used during build -> nativeBuildInputs
In a few cases it wasn't clear so I left them as-is.

While visiting these moved other things to nativeBuildInputs
when it was clear they were one of these cases:

* makeWrapper
* archive utilities (in order to unpack src)
  * a few of these might no longer be needed but leaving for another day
2018-09-28 11:43:16 -05:00
Vincent Laporte 23900febe7 coq: 8.8.1 -> 8.8.2 (#47388) 2018-09-26 22:26:39 +02:00
Frederik Rietdijk de419917a3 Merge master into staging-next 2018-09-18 18:44:48 +02:00
Maximilian Bosch 2cfc0bb7ee tamarin-prover: fix ghc 8.4 build (#46597)
See https://hydra.nixos.org/build/81125645

`tamarin-prover' upstream has a patch to fix GHC 8.4 compilation (and
uses stack lts-12.1 now), but it's not released yet:

a08f6e4007

The build is divided in several derivations, therefore the patch had to
be splitted and rebased for `lib/term', `lib/theory' and `lib/utils' to
ensure that the patch applies properly during the `patchPhase'.

Addresses #45960
2018-09-13 14:11:09 +02:00
Uli Baum 1df2560dde Merge branch 'master' into staging-next 2018-09-13 10:08:53 +02:00
Markus Kowalewski 258c202565
prooftree: add license 2018-09-08 14:44:43 +02:00
Frederik Rietdijk b910b697f6 Merge master into staging 2018-09-02 12:10:33 +02:00
Markus Kowalewski e5974ddaec
jonprl: update homepage 2018-09-02 00:36:01 +02:00
Vladimír Čunát 2d6179d1e8
Merge branch 'master' into staging
A few trivial conflicts due to *Platforms mass replace.
2018-09-01 17:38:18 +02:00
Gabriel Ebner da3326902a vampire: fix nondeterministic hash
Probably related to #8567
2018-09-01 15:03:31 +02:00
John Ericson 2c2f1e37d4 reewide: Purge all uses stdenv.system and top-level system
It is deprecated and will be removed after 18.09.
2018-08-30 17:20:32 -04:00
Vladimír Čunát 8fc6472ace
gnome-documents, tlaplus: fix glib references 2018-08-30 19:47:41 +02:00
Matthew Bauer f7bc33abf0 Revert "treewide: fixup breakage due to absolute compiler path"
This reverts commit d0888d1503.
2018-08-22 01:14:53 +02:00
Vladimír Čunát d0888d1503
treewide: fixup breakage due to absolute compiler path
Some packages just can't handle them #44767.  It was tempting to try
to abstract this in some way, but I didn't do that ATM.
2018-08-21 12:34:33 +02:00
Vladimír Čunát cbabebcc2e
Merge branch 'master' into staging-next
Hydra: ?compare=1473892
2018-08-17 13:45:21 +02:00
Austin Seipp d5e496a2bb boolector: 2.4.1 -> 3.0.0, relicensed to MIT
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2018-08-15 20:44:05 -05:00
Austin Seipp 9b64100add btor2tools: init at pre55_8c150b39
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2018-08-15 20:44:05 -05:00
Austin Seipp 68cc845295 lingeling: init at pre1_03b4860d
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2018-08-15 20:44:05 -05:00
Austin Seipp 6e910b2b3d aiger: clean up configurePhase, install multi-output objects/headers
The library and header files are useful for other tools, such as
the upcoming 'lingeling'.

Signed-off-by: Austin Seipp <aseipp@pobox.com>
2018-08-15 20:44:05 -05:00
Vladimír Čunát 00df25ee57
Merge branch 'master' into staging-next
Hydra: ?compare=1472947
2018-08-12 10:33:41 +02:00
Silvan Mosberger 68d3350433
Merge pull request #44837 from Infinisil/fix/sad
sad: fix build
2018-08-09 22:36:14 +02:00
Silvan Mosberger e710f80018
sad: fix build 2018-08-09 22:13:44 +02:00
Frederik Rietdijk d9fa74ba78 Merge master into staging 2018-08-09 18:28:15 +02:00
Austin Seipp 752284680b symbiyosys: 2018.05.03 -> 2018.07.26
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2018-08-08 19:49:42 -05:00
John Ericson db965063b3 treewide: Make configureFlags lists 2018-08-03 17:06:03 -04:00
Frederik Rietdijk f3088832df
Merge pull request #43899 from r-ryantm/auto-update/tla-toolbox
tlaplusToolbox: 1.5.6 -> 1.5.7
2018-07-22 08:44:58 +02:00
Ricardo M. Correia 0cf09556eb
why3: 0.88.3 -> 1.0.0 2018-07-21 22:53:44 +00:00
R. RyanTM 9882d5635c tlaplusToolbox: 1.5.6 -> 1.5.7
Semi-automatic update generated by https://github.com/ryantm/nixpkgs-update tools. This update was made based on information from https://repology.org/metapackage/tla-toolbox/versions.
2018-07-21 08:39:53 -07:00
Jörg Thalheim 218298b30f
Merge branch 'master' into unused5 2018-07-21 15:41:22 +01:00
volth 52f53c69ce pkgs/*: remove unreferenced function arguments 2018-07-21 02:48:04 +00:00
volth 6d2857a311 [bot] treewide: remove unused 'inherit' in let blocks 2018-07-20 19:38:19 +00:00
Gabriel Ebner 862e4e4fdb cvc4: fix homepage url 2018-07-16 15:58:22 +01:00
Mario Rodas 1c88d0c6bd z3: fix darwin build (#43526) 2018-07-14 21:49:47 +02:00
Will Dietz efdf4711d8
Merge pull request #43445 from dtzWill/fix/yices-symlink
yices: fix symlink created to match version
2018-07-13 10:11:49 -05:00
Will Dietz f731c99e7d abc-verifier: 20160818 -> 2018-07-08
Now hosted on github.
2018-07-12 21:44:56 -05:00
Will Dietz 946a65ca5c yices: use lib.splitString, not everyone has builtins.splitVersion 2018-07-12 19:11:06 -05:00
Will Dietz 237c8f4148 yices: simplify ln command 2018-07-12 18:52:10 -05:00
Will Dietz 6ff8685057 yices: fix symlink to match version of package
To help avoid this happening again, derive the string to use
from the version directly instead of embedding it in installPhase.
2018-07-12 18:46:28 -05:00
Will Dietz d3a595f190 libpoly: 0.1.5 -> 0.1.7 (noop), cleanup a bit to modern style 2018-07-12 17:06:57 -05:00
Austin Seipp 54e9f7dcbe z3: move to multiple output packages
The Z3 source code is effectively compiled into two completely separate
objects: the z3 binary file, and the libz3.so library -- but the binary is not
linked against the shared library, it simply incorporates all of the object
files. The Z3 code base results in an ~25MB object on x86_64-linux. As a
result, splitting bin/ and lib/ results in a 50% reduction in closure size.

(The include/ directory is also surprisingly large at .5MB...)

This also splits the python API into a completely separate .python attribute,
as well.

Signed-off-by: Austin Seipp <aseipp@pobox.com>
2018-07-12 15:48:48 -05:00
Frederik Rietdijk 04cae0e5fb
Merge pull request #43333 from r-ryantm/auto-update/libpoly
libpoly: 0.1.4 -> 0.1.5
2018-07-11 19:01:02 +02:00
R. RyanTM 40e648b7ab yices: 2.5.4 -> 2.6.0
Semi-automatic update generated by https://github.com/ryantm/nixpkgs-update tools. This update was made based on information from https://repology.org/metapackage/yices/versions.
2018-07-11 08:45:45 -05:00
R. RyanTM a89b538f0b libpoly: 0.1.4 -> 0.1.5
Semi-automatic update generated by https://github.com/ryantm/nixpkgs-update tools. This update was made based on information from https://repology.org/metapackage/libpoly/versions.
2018-07-11 02:29:13 -07:00
Dan Peebles 1dd7bc7dfc monosat: update build to use handy new environment variable 2018-07-08 22:04:05 -04:00
Dan Peebles 0372c87481 monosat: cbaf79cf -> 2deeadef
Upstream fixed a few things I needed to work around
2018-07-08 21:57:00 -04:00
Dan Peebles 631dd7a4e9 monosat: init at 1nx3wh34
Also includes the python and java bindings (although java is only
currently enabled on Linux)
2018-07-08 12:43:29 -04:00
Will Dietz 67986382e4
Merge pull request #43071 from dtzWill/fix/vampire-portability
vampire: portability fixes
2018-07-05 11:13:42 -05:00
Gabriel Ebner bec83a2b9e cvc4: 1.5 -> 1.6 2018-07-05 17:57:06 +02:00
Will Dietz 7353d8396d vampire: enable parallel building 2018-07-05 10:13:40 -05:00
Will Dietz 600abbedc9 vampire: portability fixes
These have been submitted upstream,
but seconds before writing this message
so naturally no upstream response "yet" :).

Regardless of response, fetch patches
from the corresponding PR's for context
and of course hopefully they'll
be included in next version.
2018-07-05 10:13:32 -05:00
Will Dietz 8e6db30bb7 vampire: use CC/CXX from env, instead of always g++ 2018-07-05 10:11:32 -05:00