Commit graph

218 commits

Author SHA1 Message Date
Vincent Laporte
c260abbff8 hol_light: update to r199
And adds compatibility with camlp5-6.12
2014-10-01 00:44:15 +01:00
John Wiegley
57b292fb1b isabelle: Another Linux hash change? 2014-09-30 16:44:15 -05:00
John Wiegley
5a7ce1185b isabelle: Remove Linux patches (is this correct?) 2014-09-30 16:41:47 -05:00
John Wiegley
8d9cd1557b isabelle: Correct the 2014 sha value for Linux 2014-09-30 16:15:34 -05:00
John Wiegley
db690f28a3 isabelle: 2013 -> 2014, plus add darwin support 2014-09-30 12:57:30 -05:00
Vincent Laporte
f3b8d82ce6 Removes duplicate ssreflect 2014-09-28 14:03:15 +01:00
Vincent Laporte
fde68228d9 coq: setup-hook for libraries
Adds a hook to automatically populate the $COQPATH variable.
Coq libraries are expected to be installed in

    lib/coq/${coq-version}/user-contrib/
2014-09-28 14:03:14 +01:00
John Wiegley
4eedbfd786 coq_HEAD: update to latest Git HEAD 2014-09-23 13:19:51 -05:00
William A. Kennington III
31220480d8 boost: Update depdendent packages 2014-09-21 17:20:59 -07:00
Peter Simons
2a54f52b22 coq_HEAD: Revert "update to latest Git version"
This reverts commit bf009f87a9. The update
breaks the build.
2014-09-19 12:29:07 +02:00
Marco Maggesi
6110679bee Update hol_light to r198. Add myself as a maintainer 2014-09-16 16:55:56 +02:00
John Wiegley
10afb382b7 ott: 0.25 new expression 2014-09-15 21:50:07 +01:00
John Wiegley
bf009f87a9 coq_HEAD: update to latest Git version
In particular, to get the fix for #3585 in the Coq bug tracker
2014-09-09 18:02:32 +01:00
Michael Raskin
979f0e1d67 Update TPTP 2014-08-31 19:25:32 +04:00
John Wiegley
686fa594ab coq_HEAD: update to latest Git HEAD 2014-08-26 16:36:50 -05:00
Bjørn Forsman
c9baba9212 Fix many package descriptions
(My OCD kicked in today...)

Remove repeated package names, capitalize first word, remove trailing
periods and move overlong descriptions to longDescription.

I also simplified some descriptions as well, when they were particularly
long or technical, often based on Arch Linux' package descriptions.

I've tried to stay away from generated expressions (and I think I
succeeded).

Some specifics worth mentioning:
 * cron, has "Vixie Cron" in its description. The "Vixie" part is not
   mentioned anywhere else. I kept it in a parenthesis at the end of the
   description.

 * ctags description started with "Exuberant Ctags ...", and the
   "exuberant" part is not mentioned elsewhere. Kept it in a parenthesis
   at the end of description.

 * nix has the description "The Nix Deployment System". Since that
   doesn't really say much what it is/does (especially after removing
   the package name!), I changed that to "Powerful package manager that
   makes package management reliable and reproducible" (borrowed from
   nixos.org).

 * Tons of "GNU Foo, Foo is a [the important bits]" descriptions
   is changed to just [the important bits]. If the package name doesn't
   contain GNU I don't think it's needed to say it in the description
   either.
2014-08-24 22:31:37 +02:00
Eelco Dolstra
ce6b86cc68 Fix various evaluation problems
http://hydra.nixos.org/build/13616685
2014-08-22 11:57:40 +02:00
John Wiegley
708e16e675 ssreflect: 1.4 -> 1.5 2014-08-19 16:03:33 -05:00
John Wiegley
cfc70c60ab coq_HEAD: 8.5pre-fff9e2f7 -> 8.5pre-8bc01590 2014-08-16 00:13:15 -05:00
Michael Raskin
f1f0f0cf19 Update and fix LEO2 prover 2014-08-12 03:57:52 +04:00
John Wiegley
83cf279452 Add an expression for building Coq HEAD 2014-08-08 18:11:00 -05:00
Vladimír Čunát
52d9c93abe Merge 'staging' into master 2014-08-08 20:13:23 +02:00
Eelco Dolstra
8a7f3c3618 Mark a bunch of packages as broken or not supported on Darwin 2014-08-08 17:59:02 +02:00
Peter Simons
2d326e5032 Merge remote-tracking branch 'origin/master' into staging.
Conflicts:
	pkgs/desktops/e18/enlightenment.nix
2014-08-04 16:51:47 +02:00
Peter Simons
d0ca8c237e Fix broken license references. 2014-07-28 11:43:20 +02:00
Mateusz Kowalczyk
7a45996233 Turn some license strings into lib.licenses values 2014-07-28 11:31:14 +02:00
Eelco Dolstra
4f7289eec9 Don't use ensureDir 2014-07-22 11:01:32 +02:00
Benno Fünfstück
e10001042d fetchbzr, fetchdarcs, fetchhg: use rev attr
This makes it match the behaviour of fetchgit and fetchsvn, so it's
easier to write scripts that support all of them.
2014-06-28 21:06:10 +02:00
John Wiegley
34de04149e twelf: Fix the source URL 2014-06-27 10:46:24 -07:00
John Wiegley
ad96cc8bf9 twelf: new expression; prover for PL theory and logic 2014-06-26 15:54:45 -07:00
Austin Seipp
fe9133d522 verifast: 14.5, x86_64 linux only
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-06-10 16:38:45 -05:00
John Wiegley
c6261157f8 prooftree: new expression 0.12 2014-06-08 05:35:49 +00:00
Austin Seipp
453f93cc92 Merge pull request #2514 from jwiegley/coq
Make Coq buildable on any Unix
2014-05-17 14:49:57 -05:00
Austin Seipp
552db25e7f nixpkgs: add abc version 040509
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-05-17 14:09:09 -05:00
Russell O'Connor
5bbcebf2db Bump coq version to 8.4pl4. 2014-05-12 22:17:00 -04:00
John Wiegley
0a6b317071 Make Coq buildable on any Unix 2014-05-05 00:58:23 -05:00
Michael Raskin
4c55ae8588 Update TPTP and make URL set robust to moving old versions to archive 2014-05-03 00:53:46 +04:00
Austin Seipp
7d58646b08 z3/verifast: update license
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-05-01 19:09:24 -05:00
Austin Seipp
6d52463bd3 nixpkgs: add alt-ergo 0.95.2
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-05-01 02:42:31 -05:00
Austin Seipp
4ee4f76176 nixpkgs: add why3 0.83
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-05-01 02:30:39 -05:00
Austin Seipp
d1a32414cd nixpkgs: add ltl2ba 1.1
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-05-01 02:30:34 -05:00
Austin Seipp
aaa0304a45 nixpkgs: verifast 13.11.14
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-04-28 13:46:27 -05:00
Austin Seipp
0f1f2115e9 hol_light: fix script, upgrade to r189
This also tweaks the version number to just use the SVN revision (rather
than date), since it's unambiguous and increasing anyway.

Signed-off-by: Austin Seipp <aseipp@pobox.com>
2014-04-27 13:31:36 -05:00
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