Commit Graph

166 Commits

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