Commit Graph

975 Commits

Author SHA1 Message Date
Austin Seipp
da0c8f33ef nixpkgs: yices 2.2.1
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-04-27 13:05:40 -05:00
Austin Seipp
5aa4495cb5 boolector: add version 1.5 and 1.6
There are two versions here because beginning with 1.6.0, Boolector has
a more restrictive, unfree license which disallows commercial use.

As a result, Boolector 1.5 is the default 'boolector' expression.

Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-04-07 09:17:05 -05:00
Shea Levy
a0a135d5ef Merge branch 'z3' of git://github.com/thoughtpolice/nixpkgs
z3: version 4.3.1
2014-03-28 23:54:43 -04:00
Austin Seipp
2646eac8b2 z3: version 4.3.1
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-03-21 02:50:54 -05:00
Shea Levy
389c3951a8 Merge branch 'coq' of git://github.com/thoughtpolice/nixpkgs
coq: 8.4pl2 -> 8.4pl3
2014-03-15 13:03:10 -04:00
Michael Raskin
8dc61a6519 Update EKRHyper 2014-03-08 21:12:59 +04:00
Austin Seipp
c0f779ceee coq: add myself to maintainer list.
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-03-07 20:52:33 -06:00
Austin Seipp
fa118fc677 coq: 8.4pl2 -> 8.4pl3
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-03-07 20:52:26 -06:00
Petr Rockai
ed5bd26574 STP: Simple Theorem Prover (a SMT solver for bitvectors & arrays). 2014-01-25 16:33:12 +01:00
Marco Maggesi
b504b1b4cb Update HOL Light to revision 179 2014-01-14 15:21:09 +01:00
Nixpkgs Monitor
191f349052 cvc3: update from 2.2 to 2.4.1 2013-12-18 18:18:23 +02:00
Michael Raskin
4140dc2628 Updating EKRHuper 2013-11-25 10:59:35 +04:00
Karn Kallio
6c32416a31 Fix HOL documentation build 2013-11-16 03:43:38 +02:00
Tom Ridge
f13bcf6463 HOL: update to k.8 2013-11-16 02:52:36 +02:00
Eelco Dolstra
c88055e1a2 Set meta.hydraPlatforms instead of meta.platforms for some packages 2013-11-05 00:06:10 +01:00
Michael Raskin
6944de0f94 Updating EProver to 1.8 2013-10-20 21:03:04 +04:00
Michael Raskin
70f609acbf Updating Ekrhyper 2013-10-20 21:02:37 +04:00
Peter Simons
7e06522645 hol: fix access to dot
Committing on behalf of Karn Kallio <tierpluspluslists@skami.org>.
2013-10-11 10:20:37 +02:00
Peter Simons
0ae1a8b847 hol: update to version k.8
Committing on behalf of Tom Ridge <tom.j.ridge@googlemail.com>.
2013-10-10 12:00:12 +02:00
Bjørn Forsman
083d0890f5 More description fixes
* Remove package name
* Start with upper case letter
* Remove trailing period

Also reword some descriptions and move some long descriptions to
longDescription.

I'm not touching generated packages.
2013-10-06 12:01:38 +02:00
Gergely Risko
b43347342b Add platforms to coq, so it's built on Hydra 2013-08-28 21:35:07 +02:00
Russell O'Connor
3538f7c549 Update download link for ssreflect. 2013-07-14 23:41:55 -04:00
Evgeny Egorochkin
0f99aace03 ssreflect: fix url 2013-07-14 02:08:54 +03:00
Russell O'Connor
c9f5959285 Update Coq to version 8.4pl2. 2013-06-14 12:16:52 -04:00
Evgeny Egorochkin
9c6f7cc9c1 Add package versions to some of the packages or fix existing ones to conform to nixpkgs conventions. 2013-06-07 03:15:45 +03:00
Michael Raskin
9d92fe013e Adding E-KRHyper theorem prover 2013-05-09 17:47:58 +04:00
Michael Raskin
646868b2e6 Adding Otter theorem prover. The development is frozen, but because of that Otter is considered a very reliable prover from soundness point of view. 2013-05-09 12:23:27 +04:00
Michael Raskin
e7b491a7e1 Update E prover 2013-04-21 16:30:40 +04:00
Marco Maggesi
fa2d85fded Update HOL Light to rev 157 2013-03-25 10:56:57 +01:00
Michael Raskin
d5288c7e3a TPTP had a bugfix without version change 2013-03-09 14:24:45 +04:00
Marco Maggesi
42a4178c2b Update HOL Light to revision 155 2013-02-08 15:26:35 +01:00
Marco Maggesi
34411286a6 Update HOL Light to revision 154 2013-02-08 15:20:06 +01:00
Eelco Dolstra
f286cc65b1 Fix bad URLs lacking a scheme 2013-01-14 18:26:46 +01:00
Michael Raskin
b31e6aa794 Merge pull request #231 from RSzibele/master
Added Logisim 2.7.1
2012-12-27 06:32:03 -08:00
RSzibele
fcdf685793 Added Logisim-2.7.1. 2012-12-27 16:25:39 +01:00
Marco Maggesi
49e4824b8a Update HOL Light (and fix installation) 2012-12-23 18:46:09 +01:00
Michael Raskin
1c3434cc16 Update E prover 2012-12-09 00:36:38 +04:00
Russell O'Connor
46d9146d64 Update SSReflect to version 1.4 2012-09-10 23:15:54 +02:00
Marco Maggesi
286d068b37 Upgrade Isabelle proof assistant to version 2012 2012-09-04 14:34:31 +02:00
Russell O'Connor
525b8015e7 Fixing configure patch for coq 8.3. 2012-08-19 01:11:11 -04:00
Russell O'Connor
eafd2008f1 Correcting filename. 2012-08-19 01:06:15 -04:00
Russell O'Connor
706cbc9318 Update coq to 8.4 2012-08-19 01:01:30 -04:00
Michael Raskin
2331ea4ec2 TPTP: update to 5.4.0 2012-07-07 20:32:48 +04:00
Marco Maggesi
5ca0b381e0 Update HOL Light to rev 141
svn path=/nixpkgs/trunk/; revision=34290
2012-05-30 20:53:13 +00:00
Russell O'Connor
dace27b4c4 Revert accidentaly patch of ssreflect.
svn path=/nixpkgs/trunk/; revision=34264
2012-05-28 20:57:54 +00:00
Russell O'Connor
417a07a0e9 Updatings ssreflect to depend on camlp5 version 6.
svn path=/nixpkgs/trunk/; revision=34263
2012-05-28 20:53:17 +00:00
Russell O'Connor
f02a71103a add support to make building coqide optional.
svn path=/nixpkgs/trunk/; revision=34262
2012-05-28 19:45:14 +00:00
Russell O'Connor
cfc8538326 Updating coq and ssreflect to patch level 4.
svn path=/nixpkgs/trunk/; revision=34146
2012-05-16 22:04:02 +00:00
Marco Maggesi
2cef87022c Update HOL Light to r134
svn path=/nixpkgs/trunk/; revision=33992
2012-05-05 16:46:53 +00:00
Michael Raskin
304facbf3b Adding LCI lambda calculus interpreter
svn path=/nixpkgs/trunk/; revision=33962
2012-05-01 05:07:39 +00:00
Michael Raskin
dd3ef46cac Update TPTP
svn path=/nixpkgs/trunk/; revision=33754
2012-04-12 07:23:52 +00:00
Russell O'Connor
bba264d897 Adding forgotten configure_130312 patch for matitia.
svn path=/nixpkgs/trunk/; revision=33433
2012-03-26 19:11:25 +00:00
Russell O'Connor
ec5dda12d2 Reparing stable build of Matita.
Also correcting the version and simplifying the prerelease package of Matita.


svn path=/nixpkgs/trunk/; revision=33420
2012-03-25 21:27:30 +00:00
Russell O'Connor
510308e039 Adding a package for a preview release of Matita.
svn path=/nixpkgs/trunk/; revision=33418
2012-03-25 20:43:00 +00:00
Russell O'Connor
f9a5fa373e Upgrading HOL4 to version k.7.
svn path=/nixpkgs/trunk/; revision=33306
2012-03-20 19:11:22 +00:00
Marco Maggesi
dba8b32385 Update HOL Light to rev 128
svn path=/nixpkgs/trunk/; revision=33196
2012-03-17 16:36:36 +00:00
Marco Maggesi
699de0f3f9 Fix building of Coq and update to version 8.3pl3. (Forgot to save files)
svn path=/nixpkgs/trunk/; revision=33195
2012-03-17 16:30:23 +00:00
Marco Maggesi
af37461b11 Fix building of Coq and update to version 8.3pl3.
svn path=/nixpkgs/trunk/; revision=33194
2012-03-17 16:26:20 +00:00
Yury G. Kudryashov
215a07c1a9 svn merge ^/nixpkgs/trunk
Merge conflicts:
* unzip (almost trivial)
* dvswitch (trivial)
* gmp (copied result of `git merge`)

The last item introduced gmp-5.0.3, thus full rebuild.
+ensureDir->mkdir -p in TeX packages was catched by git but not svn.

svn path=/nixpkgs/branches/stdenv-updates/; revision=32091
2012-02-06 23:03:12 +00:00
Marco Maggesi
7c90b6a9bc Update HOL Light to rev 122.
svn path=/nixpkgs/trunk/; revision=31956
2012-02-01 14:37:50 +00:00
Eelco Dolstra
c556a6ea46 * "ensureDir" -> "mkdir -p". "ensureDir" is a rather pointless
function, so obsolete it.

svn path=/nixpkgs/branches/stdenv-updates/; revision=31644
2012-01-18 20:16:00 +00:00
Yury G. Kudryashov
0c79434ccb svn merge ^/nixpkgs/trunk
svn path=/nixpkgs/branches/stdenv-updates/; revision=31567
2012-01-14 21:34:37 +00:00
Marco Maggesi
97d48a5426 Update HOL Light to rev 118
svn path=/nixpkgs/trunk/; revision=31468
2012-01-10 16:12:11 +00:00
Yury G. Kudryashov
394fd28e4e svn merge ^/nixpkgs/trunk
svn path=/nixpkgs/branches/stdenv-updates/; revision=31280
2012-01-04 15:22:16 +00:00
Michael Raskin
07de46c2fa Update E prover
svn path=/nixpkgs/trunk/; revision=31269
2012-01-04 10:31:49 +00:00
Yury G. Kudryashov
08761e83fc Merge trunk
svn path=/nixpkgs/branches/stdenv-updates/; revision=31207
2012-01-02 14:12:40 +00:00
Marco Maggesi
fd64bc5289 Oops!
svn path=/nixpkgs/trunk/; revision=31126
2011-12-28 12:49:29 +00:00
Marco Maggesi
ff3b0ed420 Update HOL Light to r116
svn path=/nixpkgs/trunk/; revision=31125
2011-12-28 12:45:59 +00:00
Yury G. Kudryashov
a670a7aca1 merge trunk
A few conflicts due to renames

svn path=/nixpkgs/branches/stdenv-updates/; revision=30947
2011-12-16 22:57:21 +00:00
Marco Maggesi
74c3fc3085 Update HOL Light to rev 114
svn path=/nixpkgs/trunk/; revision=30922
2011-12-16 07:44:29 +00:00
Eelco Dolstra
eda3fd1730 * Sync with the trunk.
svn path=/nixpkgs/branches/stdenv-updates/; revision=30852
2011-12-12 16:54:35 +00:00
Marco Maggesi
bf394d80ec Update url for Isabelle2011
svn path=/nixpkgs/trunk/; revision=30574
2011-11-26 18:45:15 +00:00
Russell O'Connor
845f2a8658 adding camlp5 as a propogated build input to ulex 0.8
matita and ulex must build against the same version of camlp5, so in an attempt to force them to always be the same I am adding a propgatedBuildInput to ulex.
Granted Matita still requires camlp5_traditional and this is less obvious in the matita file now, so I am not entirely sure this is the right design choice.

svn path=/nixpkgs/trunk/; revision=30552
2011-11-24 19:43:03 +00:00
Marco Maggesi
fa47d66e22 Updated HOL Light to revision 112
svn path=/nixpkgs/trunk/; revision=30369
2011-11-10 15:35:53 +00:00
Peter Simons
7edf0e8eaf synchronize with trunk
svn path=/nixpkgs/branches/stdenv-updates/; revision=29870
2011-10-18 08:47:36 +00:00
Russell O'Connor
491c6e43b1 Package for picosat.
svn path=/nixpkgs/trunk/; revision=29869
2011-10-17 22:18:21 +00:00
Shea Levy
4d70ba6cc9 Merge from trunk up through r28790
svn path=/nixpkgs/branches/stdenv-updates/; revision=28792
2011-08-24 19:16:43 +00:00
Marco Maggesi
a9d2f34301 Update HOL Light to release 102
svn path=/nixpkgs/trunk/; revision=28718
2011-08-21 08:41:22 +00:00
Michael Raskin
946cd2431f Update LEO-II
svn path=/nixpkgs/trunk/; revision=28180
2011-08-05 18:22:40 +00:00
Michael Raskin
d03599f8ce Adding TPTP
svn path=/nixpkgs/trunk/; revision=27468
2011-06-15 10:35:18 +00:00
Marco Maggesi
5b035e093d Update HOL Light to rev 92
svn path=/nixpkgs/trunk/; revision=27459
2011-06-14 17:09:19 +00:00
Marco Maggesi
1298fd8aba Update hol_light and cleanup:
* Update hol_light to rev 90
* Remove dmtcp checkpoint (it doesn't work properly).
* General cleanup and simplification

svn path=/nixpkgs/trunk/; revision=27290
2011-05-21 11:18:35 +00:00
Marco Maggesi
8e5beab31f Fix building of Isabelle2011
svn path=/nixpkgs/trunk/; revision=27253
2011-05-14 21:09:57 +00:00
Marco Maggesi
a041cad70a Update HOL Light to r89
svn path=/nixpkgs/trunk/; revision=26916
2011-04-21 14:39:29 +00:00
Michael Raskin
b4faf64bae Update Isabelle to an existing tarball...
svn path=/nixpkgs/trunk/; revision=26903
2011-04-20 12:24:34 +00:00
Russell O'Connor
bec1a9c44f update coq to 8.3pl1
update ssreflect to 1.3pl1

svn path=/nixpkgs/trunk/; revision=26692
2011-04-05 11:59:25 +00:00
Marco Maggesi
436e1d72a7 * Coq: fix compilation of coqide (path to lablgkt)
svn path=/nixpkgs/trunk/; revision=25360
2011-01-03 13:49:15 +00:00
Michael Raskin
e55aa52856 Fix lablgtk reference
svn path=/nixpkgs/trunk/; revision=25341
2011-01-02 17:25:18 +00:00
Russell O'Connor
88ec92d14c Matita and its dependencies.
svn path=/nixpkgs/trunk/; revision=25328
2010-12-31 17:48:55 +00:00
Eelco Dolstra
aa6f43149a * Sync with the trunk.
svn path=/nixpkgs/branches/stdenv-updates/; revision=25308
2010-12-28 16:42:00 +00:00
Marco Maggesi
51d6c8df91 * Handle variable createFindlibDestdir correctly in ocaml-findlib
* Fix HOL Light derivation

svn path=/nixpkgs/trunk/; revision=25269
2010-12-23 19:28:06 +00:00
Eelco Dolstra
c14382cb45 * Sync with the trunk.
svn path=/nixpkgs/branches/stdenv-updates/; revision=25225
2010-12-21 15:14:33 +00:00
Marco Maggesi
e7accaf8d3 * Update camlp5
svn path=/nixpkgs/trunk/; revision=25206
2010-12-20 10:32:22 +00:00
Lluís Batlle i Rossell
ee04ffcb55 Updating from trunk. I resolved simple conflicts.
svn path=/nixpkgs/branches/stdenv-updates/; revision=25061
2010-12-11 12:47:00 +00:00
Michael Raskin
07dd3f074b Adding MiniSAT
svn path=/nixpkgs/trunk/; revision=24984
2010-12-05 19:54:27 +00:00
Michael Raskin
6b8abaa29e Adding OpenSMT
svn path=/nixpkgs/trunk/; revision=24978
2010-12-05 18:22:14 +00:00
Michael Raskin
a9f70d542d Adding CVC3 satisfiability modulo theory (SMT) solver
svn path=/nixpkgs/trunk/; revision=24975
2010-12-05 17:28:41 +00:00
Michael Raskin
44ac8c5ea1 Adding iProver
svn path=/nixpkgs/trunk/; revision=24969
2010-12-04 18:39:44 +00:00
Michael Raskin
86e44e72bf Adding SPASS
svn path=/nixpkgs/trunk/; revision=24967
2010-12-04 11:43:01 +00:00
Michael Raskin
64ed7e705d Adding Satallax prover
svn path=/nixpkgs/trunk/; revision=24963
2010-12-03 11:26:34 +00:00
Michael Raskin
c32bd62956 Adding LEO2 automated higher-order prover
svn path=/nixpkgs/trunk/; revision=24952
2010-12-01 21:29:42 +00:00
Michael Raskin
373fabf1c0 Fix settings patch for Isabelle
svn path=/nixpkgs/trunk/; revision=24951
2010-12-01 21:29:20 +00:00
Michael Raskin
b89881d098 Update Isabelle
svn path=/nixpkgs/trunk/; revision=24950
2010-12-01 21:25:21 +00:00
Michael Raskin
3c452363ce Use a patch to fix make 3.82 build of Coq
svn path=/nixpkgs/branches/stdenv-updates/; revision=24817
2010-11-23 05:54:58 +00:00
Marco Maggesi
0430167083 Update Coq
svn path=/nixpkgs/trunk/; revision=24597
2010-11-04 11:24:27 +00:00
Marco Maggesi
078587a846 Update HOL Light
svn path=/nixpkgs/trunk/; revision=24591
2010-11-03 22:20:05 +00:00
Marco Maggesi
4e5db40581 Update HOL Light to version 20100820 (rev57 on google code).
Also replace the monolitic derivation hol_light_binaries with smaller
derivations.  Now the installation works as follows:

# Install the base system and a script "start_hol_light"
$ nix-env -i hol_light_sources hol_light

# Install a checkpointed executable with the core library preloaded
$ nix-env -i hol_light_core_dmtcp

# Install HOL Light binaries preloaded with other specific libraries:
$ nix-env -i hol_light_multivariate_dmtcp
$ nix-env -i hol_light_complex_dmtcp
$ nix-env -i hol_light_sosa_dmtcp
$ nix-env -i hol_light_card_dmtcp


svn path=/nixpkgs/trunk/; revision=23815
2010-09-15 21:41:18 +00:00
Marco Maggesi
44f2d4439f Change the name of the coq derivation to coq-devel-8.3pre1
i.e., remove the version from the name.  Nix has its own mechanism to
prevent a packages to be upgraded.  Instead we distinguish development
version (coq-dev-VERSION) from stable versions (coq-VERSION).

Also remove derivation for coq-8.3-beta0-1 which is now superseded by
coq-devel-8.3pre1.


svn path=/nixpkgs/trunk/; revision=23813
2010-09-15 19:39:48 +00:00
Marco Maggesi
8ab6f9861c Add coq-8.3rc1
Note: In this version we introduce a new schema for the name of the coq
derivations where the coq version is included in the name (i.e.,
"coq8.3-8.3pre1" instead of "coq-8.3pre1").  The reason for this is that often
coq releases introduce several incompatibilities.  Thus I argue that, in
general, users do not want nix-env to upgrade automatically form one release to
another.  Also version string "8.3pre1" is used instead of "8.3-rc1" to trigger
the nix mechanism for versions comparison.


svn path=/nixpkgs/trunk/; revision=23803
2010-09-14 21:15:58 +00:00
Marco Maggesi
df21c86e08 Improve hol_light:
*   Upgrade hol_light to the latest svn version on google code (r57).

  *   Improve and semplify the mechanism for the generation of checkpointed binaries.

  *   Make hol to work with camlp5 and thus with recent version of ocaml (>=3.10, <=3.11).

  *   Remove ocaml_with_sources which is not needed anymore.

svn path=/nixpkgs/trunk/; revision=23685
2010-09-08 13:07:45 +00:00
Peter Simons
098b763939 pkgs/applications/science/logic/prover9: fixed trivial syntax error
svn path=/nixpkgs/trunk/; revision=23453
2010-08-26 12:06:05 +00:00
Peter Simons
403938b004 pkgs/applications/science/logic/prover9: updated homepage and license
svn path=/nixpkgs/trunk/; revision=23447
2010-08-26 11:42:41 +00:00
Peter Simons
340d4a6ddd pkgs/applications/science/logic/prover9: initial version
svn path=/nixpkgs/trunk/; revision=23446
2010-08-26 11:37:05 +00:00
Michael Raskin
4f6c18925d Fix installation for updated E prover release
svn path=/nixpkgs/trunk/; revision=23435
2010-08-26 04:34:20 +00:00
Michael Raskin
05c7e81eaa Move E prover to applications/science/logic
svn path=/nixpkgs/trunk/; revision=23434
2010-08-25 22:38:11 +00:00
Peter Simons
970b3402e9 pkgs/applications/science/logic/hol: initial version
svn path=/nixpkgs/trunk/; revision=23430
2010-08-25 19:50:24 +00:00
Marco Maggesi
c0f343b752 Update Coq to version 8.2pl2 (patch by roconnor)
svn path=/nixpkgs/trunk/; revision=22971
2010-08-05 18:44:42 +00:00
Eelco Dolstra
cc84ac9e84 svn path=/nixpkgs/trunk/; revision=22880 2010-08-02 16:01:55 +00:00
Peter Simons
1295493b18 pkgs/applications/science/logic/coq: install coqide libraries
Patch courtesy of Russell O'Connor.

svn path=/nixpkgs/trunk/; revision=21838
2010-05-18 13:40:19 +00:00
Marco Maggesi
afbb01c90d Add expression for Coq 8.3 beta
svn path=/nixpkgs/trunk/; revision=21734
2010-05-11 20:14:46 +00:00
Marco Maggesi
513d653d68 Add HOL Light and its dependencies.
Add pkgs/applications/science/logic/hol_light
and pkgs/applications/science/emacs-modes/hol_light

Some functionalities of HOL Light requires the compiled sources of
OCaml.  For now we provide a new package ocaml_with_sources.  After
this shuold be merged with the current version of OCaml already
present in nixpkgs.


svn path=/nixpkgs/trunk/; revision=20008
2010-02-15 11:00:02 +00:00
Marco Maggesi
98aaa4421c Add expression for Isabelle2009
svn path=/nixpkgs/trunk/; revision=18905
2009-12-11 17:00:52 +00:00
Marco Maggesi
c713b0ed67 Preliminary version of package ssreflect
Add expression for ssreflect, an extension to the Coq Proof Assistant.
Still has some clitches (see TODO in default.nix) but is usable anyway.


svn path=/nixpkgs/trunk/; revision=18145
2009-11-05 15:08:12 +00:00
Marco Maggesi
a0207b3dc7 Updated Coq to version 8.2pl1
svn path=/nixpkgs/trunk/; revision=18069
2009-11-02 11:44:27 +00:00
Andres Löh
12ca68d114 Added a preliminary expression for Coq (no IDE support yet).
svn path=/nixpkgs/trunk/; revision=11983
2008-06-04 15:10:05 +00:00