JakeHillion/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
72,797 Commits 2 Branches 0 Tags 12 GiB
c6932509b8
Commit Graph

247 Commits

Author SHA1 Message Date
Arseniy Seroka
c6932509b8 Merge pull request #11302 from fkz/sad 
add package: system for automated deduction
 2015-11-27 22:25:44 +03:00
Fabian Schmitthenner
dc164dc2ee system for automated deduction: init at 2.3-25 2015-11-27 15:12:09 +00:00
John Wiegley
2b8ef119c5 Revert "coq: 8.5b2 -> 8.5b3" 
This reverts commit c111b0cd4d.

@oconnorr I will restore this once there is more ecosystem to support it.
 2015-11-25 12:58:07 -08:00
Joachim Fasting
4229525eac spass: reimplement using mkDerivation 2015-11-24 14:45:15 +01:00
Joachim Fasting
0a4e12c0e2 opensmt: reimplement using mkDerivation 2015-11-24 14:45:15 +01:00
Joachim Fasting
c6d645803a iprover: reimplement using mkDerivation 2015-11-24 14:45:15 +01:00
Joachim Fasting
a228252b69 cvc3: reimplement using mkDerivation 2015-11-24 14:45:15 +01:00
Russell O'Connor
c111b0cd4d coq: 8.5b2 -> 8.5b3 2015-11-19 00:10:22 -05:00
Marco Maggesi
a487b3326b Update HOL Light to version 2015-11-02 2015-11-03 15:24:56 +01:00
Vincent Laporte
9a1245280d hol_light: add support for camlp5 > 6.12 2015-09-23 19:04:51 +02:00
Gabriel Ebner
5493dccfbb metis-prover: init at 2.3 2015-09-21 21:42:20 +02:00
William A. Kennington III
773b4deb7c Merge commit 'a6f6c0e' into master.upstream 
This is a partial merge of staging where we have up to date binaries for
all packages.
 2015-09-15 12:16:49 -07:00
Marco Maggesi
cb2a05b826 HOL Light: findlib is not necessary (nor actually used). Remove dependency. 2015-09-13 18:08:20 +02:00
Russell O'Connor
4cc5f5dbb6 coq: Add csdp dependency 
The csdp program is invoked for some uses of Micromega tactics.
 2015-09-10 11:50:38 -04:00
Austin Seipp
d8858e48e2 nixpkgs/jonprl: minor touchups 
Signed-off-by: Austin Seipp <aseipp@pobox.com>
 2015-09-09 07:48:55 -05:00
Brian McKenna
e9bdf0fc07 JonPRL: init at 0.1.0 2015-09-09 21:23:48 +10:00
Vladimír Čunát
8f33b8cc93 mass rewrite of find parameters to cross-platform style 
Fixes #9044, close #9667. Thanks to @taku0 for suggesting this solution.
Now we have no modes starting with `/` or `+`.

Rewrite the `-perm` parameters of find:
 - completely safe: rewrite `/0100` and `+100` to `-0100`,
 - slightly semantics-changing: rewrite `+111` to `-0100`.
I cross-verified the `find` manual pages for Linux, Darwin, FreeBSD.
 2015-09-06 10:26:30 +02:00
Marco Maggesi
97b27e69c0 Update HOL Light to svn r244. 2015-09-01 16:30:27 +02:00
Austin Seipp
16b47aff4b nixpkgs: saw-tools 0.1-20150609 -> 0.1.1-20150731 
Signed-off-by: Austin Seipp <aseipp@pobox.com>
 2015-08-30 02:58:47 -05:00
Gabriel Ebner
0349b05695 veriT: 201410 -> 201506 2015-08-26 09:31:39 +02:00
Austin Seipp
1239465314 nixpkgs: lean 20150328 -> 20150821 
Signed-off-by: Austin Seipp <aseipp@pobox.com>
 2015-08-21 13:57:16 -05:00
Michael Raskin
6863fde515 E prover: 1.8 -> 1.9 2015-08-08 21:01:31 +03:00
Michael Raskin
178014373e E prover: switch to the new location 2015-07-05 18:52:42 +03:00
vbgl
5c537f3bdd Merge pull request #8296 from vbgl/ocamlp4 
OCaml-4.02: fix ocamlbuild rules for camlp4
 2015-06-25 23:54:13 +02:00
Vincent Laporte
715f78be7e E prover: do not build the manual 2015-06-25 23:21:25 +02:00
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