JakeHillion/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
70,441 Commits 2 Branches 0 Tags 12 GiB
9d106f72e2
Commit Graph

238 Commits

Author SHA1 Message Date
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
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