Vincent Laporte
1d72ce49cf
coq-8.3: fix (needs make 3)
2015-06-25 08:55:31 +02:00
Vincent Laporte
f7dc2df7c0
acgtk: fix build with OCaml 4.02
2015-06-25 08:55:30 +02:00
laMudri
723cd518b9
hol: k.8 -> k.10, closes #8477
2015-06-24 10:04:54 +02:00
Vincent Laporte
542d20384f
Isabelle: fix download URL
2015-06-21 00:45:38 +02:00
Austin Seipp
a0301e9ce2
nixpkgs: saw-tools 0.1-20150609
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-06-18 11:37:51 -05:00
Austin Seipp
2dfb657b94
nixpkgs: picosat 936 -> 960, add myself as a maintainer
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-06-14 19:48:12 -05:00
Austin Seipp
44ef5a3ab0
cvc4: regenerate ./configure on rebuild
...
Otherwise some absurd error from ./configure crops up.
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-06-14 19:48:11 -05:00
Austin Seipp
da76434dbd
nixpkgs: yices 2.2.1 -> 2.3.1, now with source
...
It's still under a non-commercial license, but the source build is waay
better than the binary build. Can probably work on OS X too now.
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-06-14 19:48:11 -05:00
Austin Seipp
3d181a3175
nixpkgs: abc-verifier 20150406 -> 20150614
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-06-14 19:48:11 -05:00
Austin Seipp
6cfc2caaeb
nixpkgs/cvc4: touchups, add myself as maintainer
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-06-14 19:48:11 -05:00
Austin Seipp
da6eec001a
nixpkgs: z3 4.3.2 -> 4.4.0
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-06-11 22:10:56 -05:00
Marco
3af4c7065d
Update HOL Light to svn r232 (2015-05-31)
2015-06-03 11:17:39 +02:00
Vincent Laporte
28bfbb5562
why3: update from 0.85 to 0.86.1
2015-06-01 05:57:19 +02:00
Tobias Geerinckx-Rice
158e1cfdd0
Don't use "with licenses;" for single licences
...
And don't use square brackets on such lines.
2015-05-28 19:20:29 +02:00
Vincent Laporte
9f1eb28a20
Adds gappa 1.2.0
...
Gappa is a tool intended to help verifying and formally proving
properties on numerical programs dealing with floating-point or
fixed-point arithmetic.
Homepage: http://gappa.gforge.inria.fr/
2015-05-25 19:32:09 +02:00
Pascal Wittmann
c944422863
lean: fixed build
2015-05-16 12:12:58 +02:00
Aistis Raulinaitis
a5a740a17a
z3 opt
2015-05-08 23:45:07 -07:00
Joachim Fasting
bf7ad2d84f
meta.description fixups
...
Mostly scripted substitutions with a couple of subjective enhancements.
2015-04-30 18:17:42 +02:00
John Wiegley
9402a56620
coq_8_5: New expression
2015-04-26 22:29:15 -05:00
Vincent Laporte
4b9c90c64e
coq: update from 8.4pl5 to 8.4pl6
2015-04-15 07:18:08 +02:00
Austin Seipp
31f4c0c7d1
nixpkgs: abc-verifier 20140509 -> 20150406
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-04-06 07:57:27 -05:00
lethalman
b4824ffc5d
Merge pull request #7103 from gebner/verit
...
Add veriT, an SMT solver.
2015-03-31 12:31:26 +02:00
Gabriel Ebner
20428cd90f
Add veriT.
2015-03-31 09:14:38 +02:00
Ben Darwin
54dab782be
twelf: fix by actually including the Twelf SML heap image in the package and referencing the SML interpreter so the smlnj package won't be gc'd
2015-03-31 01:11:57 -04:00
Austin Seipp
a6813ca62d
nixpkgs: add lean-20150328, a theorem prover.
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-03-28 01:47:39 -05:00
Austin Seipp
75ab87edc8
nixpkgs: z3 is now MIT licensed.
...
It's also been moved to GitHub, meaning we can avoid some of the
hackiness in the original expression. This updates the Git revision, but
only so that it contains the proper license (it's otherwise equivalent
to Z3 v4.3.2)
Also, make sure the python API .py files exist besides the .pyc files.
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-03-28 01:04:06 -05:00
Eric Seidel
eff828a275
z3: copy all headers into nix store
2015-03-26 13:19:41 -07:00
Ben Darwin
172167c937
new package: abella 2.0.2
2015-03-24 00:54:03 -04:00
Marco
5f6e6b1661
Update HOL Light to r218
2015-02-17 10:23:51 +01:00
Vladimír Čunát
dbae4f109f
Merge branch 'master' into staging
...
Conflicts (relatively simple):
pkgs/applications/audio/spotify/default.nix
pkgs/build-support/cc-wrapper/default.nix
pkgs/development/compilers/cryptol/1.8.x.nix
2015-01-31 19:34:57 +01:00
Vincent Laporte
58297aa1e7
Why3: build also the Coq tactic.
2015-01-29 08:43:15 +01:00
Austin Seipp
d1b06927bc
nixpkgs: z3 4.3.1 -> 4.3.2
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-01-23 11:00:55 -06:00
Eric Seidel
f3c6827373
rename all occurrences of stdenv.cc.gcc to stdenv.cc.cc
2015-01-14 20:27:55 -08:00
Pavan Rikhi
56ea7c4128
matita_130312: mark as broken
2015-01-07 02:15:26 -05:00
John Wiegley
c4190b4894
abc: export buildFlags in the preBuild
2015-01-03 07:35:36 -05:00
Vincent Laporte
06fea66e7c
alt-ergo: update from 0.95.2 to 0.99.1
2014-12-31 15:48:39 +01:00
John Wiegley
28b6fb61e6
Change occurrences of gcc to the more general cc
...
This is done for the sake of Yosemite, which does not have gcc, and yet
this change is also compatible with Linux.
2014-12-26 11:06:21 -06:00
Pascal Wittmann
f94580da69
Fix license attribute of many bsd-like licensed packages
2014-12-21 00:00:35 +01:00
John Wiegley
d15cd4875f
coq_HEAD: update to latest Git version
2014-12-19 13:58:07 -06:00
John Wiegley
1825255272
coq_HEAD: update
2014-11-17 17:29:42 -06:00
Vincent Laporte
8227297567
hol_light: update from 199 to 205
2014-11-17 06:53:45 +00:00
Vincent Laporte
fbbd88017f
zarith: propagate build input gmp
2014-11-07 09:50:39 +00:00
Vincent Laporte
3d049938c8
Adds some “branch” meta-data
2014-11-06 19:40:50 +00:00
Mateusz Kowalczyk
007f80c1d0
Turn more licenses into lib.licenses style
...
Should eval cleanly, as far as -A tarball tells me.
Relevant: issue #2999 , issue #739
2014-11-06 00:48:16 +00:00
Peter Simons
b5fed52c43
Merge pull request #4238 from wkennington/master.boost
...
Make boost 156 the default
2014-11-03 23:03:01 +01:00
John Wiegley
d4c3e454a2
coq_HEAD: update to latest commit
2014-11-03 15:27:32 -06:00
John Wiegley
2b9e43b513
coq: 8.4pl4 -> 8.4pl5
2014-11-03 10:49:38 -06:00
William A. Kennington III
aa3e800be7
boost: Remove boost.lib
2014-11-02 17:22:27 -08:00
Jiri Marsik
ceba23605c
Added acgtk-1.1
2014-10-28 14:06:21 +01:00
Vincent Laporte
fe1d8d0015
cvc4: new derivation
...
CVC4 is an efficient open-source automatic theorem prover for
satisfiability modulo theories (SMT) problems.
Homepage: http://cvc4.cs.nyu.edu/web/
2014-10-12 16:21:02 +02:00