On Tue, 31 Aug 2004, Basile Starynkevitch [local] wrote:

> On Mon, Aug 30, 2004 at 11:57:05AM -0700, Robert M. Solovay wrote:
> >
> > I am using the HOL-light proof verifier which is written in OCaml.
>
> If you are talking about http://www.cl.cam.ac.uk/users/jrh/hol-light/
> then it is written in CamlLight, not Ocaml. HOL-light does not seems
> to be actively developped (but I don't know really and may be wrong).
> CamlLight is somehow an ancestor of Ocaml, and it is not, as far as I
> know, actively worked upon. The Cristal team actively work on Ocaml
> and Caml Light is no more developped (but has gotten minor maintanance
> fixes sometimes)

	The version I have of HOL -light [obtained from Harrison in
private correspondence] is ported to OCaml.

	The interest of HOL-light [for me] is that it's what is currently
being used in the Flyspeck project of Tom Hales.

	--Bob Solovay
>
> Take everything above with a grain of salt. I don't know really
> HOL-light & Caml-light.
>
> --
> Basile STARYNKEVITCH -- basile dot starynkevitch at inria dot fr
> Project cristal.inria.fr - temporarily
> http://cristal.inria.fr/~starynke --- all opinions are only mine
>
> -------------------
> To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
> Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners