[Prev][Next][Index][Thread]

Coq Release Info

Date: Thu, 4 Jun 92 18:54:58 +0200
To: distribution:@inria.fr; (see end of body)

First of all, all my apologies if you receive multiple versions of this
message because you are in the intersection of several mailing lists.

This is an announcement for the release of an improved version of Coq, 
our Proof Assistant for the Calculus of Inductive Constructions.

Coq is freely available by ftp as follows:
ftp nuri.inria.fr 
or ftp 128.93.1.26
with Name anonymous and Password your email address.
Then do
binary
cd INRIA/coq
get README
get coq.tar.Z
quit

Now uncompress coq.tar.Z, untar coq, and follow the README instructions.

Coq runs in CAML V3.1, also available on the same machine in directory
INRIA/caml/V3.1. Versions are currently available for the following machines:
Sun3, Sun4, Decstation, SONY68k, SONYR3000, Apollo, and Macintosh/AUX.
Coq has also an experimental version on top of caml-light, a smaller and more 
portable implementation of ML. 

We shall appreciate all comments, suggestions, bug reports.
Send such mail to: coq@margaux.inria.fr

The Coq users community is growing, and many users have similar difficulties.
We are now collecting addresses of actual users, in order to circulate 
information of general interest, and prepare distribution of users libraries.
If you want to be put on this users e-mailing list, send me a reply to this
effect, with a short description of your area of interest.

Gerard Huet

%%% overflow headers %%%
To: Harald.Ganzinger@mpi-sb.mpg.de, Juergen.Stuber@mpi-sb.mpg.de,
        Michael.Rusinowitch@loria.fr, Yves.Bertot@sophia.inria.fr,
        alban@fwi.uva.nl, amadio@loria.crin.fr, araragi@cslab.kecl.ntt.jp,
        atoenne@cs.uni-sb.de, basin@mpi-sb.mpg.de,
        besancon@lix.polytechnique.fr, card@masi.ibp.fr, cardelli@src.dec.com,
        casteran@labri.greco-prog.fr, cubric@opus.cs.mcgill.ca, dam@ai.mit.edu,
        dduggan@waterloo.edu, debec@ensta.ensta.fr, dkm@dcs.glasgow.ac.uk,
        er@cl.cam.ac.uk, erik@win.tue.nl, etxdasy@brazil.ericsson.se,
        felty@research.att.com, fp@cs.cmu.edu, fujiken@dumbo.ai.kyutech.ac.jp,
        gramlich@uklirb.informatik.uni-kl.de, gstav@theseas.ntua.gr,
        hayashi@whale.ryukoku.ac.jp, hutter@cs.uni-sb.de,
        hzhang@herky.cs.uiowa.edu, james@cray.com.usa, janin@IRO.UMontreal.CA,
        jf@id.dth.dk, jfg@cwi.nl, jt@malabar.mitre.org, jve@lifia.imag.fr,
        karst@phil.ruu.nl, koletsos@theseas.ntua.gr, liang@saul.cis.upenn.edu,
        refelcs.inria.fr@inria.fr, madden@aisb.edinburgh.ac.uk,
        marchand@polytechnique.fr,
        martin@inferenzsysteme.informatik.th-darmstadt.de,
        matsuda@tansei.cc.u-tokyo.ac.jp, melennec@stna7.stna.dgac.fr,
        mf@lri.fr, michal@eik.ii.uib.no, michou@grtc.cnrs-mrs.fr,
        mizuhito@ntt-20.ntt.jp, monin@LANNION.CNET.fr, nachum@cs.uiuc.edu,
        nickau@hrz.uni-siegen.dbp.de, nqthm-users@cli.com,
        parigot@logique.jussieu.fr, pavlovic@triples.matn.mcgill.ca,
        proof-sci@cs.chalmers.se, rccarel@urc.tue.nl,
        rda730f@monu6.cc.monash.edu.au, rewriting-list@loria.crin.fr,
        ruess@informatik.uni-ulm.de, rwh@cs.cmu.edu, saintlou@otl.scu.edu,
        sin@kurims.kyoto-u.ac.jp, sterba@anl.anl.fr,
        theorem-provers@mc.lcs.mit.edu, thomas@lannion.cnet.fr,
        tsuiki@sfc.keio.ac.jp, types@theory.lcs.mit.edu,
        vandi@vortex.ufrgs.anrs.br, volle@nsl.fr, waldinger@ai.sri.com,
        walsh@aisb.edinburgh.ac.uk, wb1@cec1.wustl.edu,
        yozo@titisha.is.titech.ac.jp, zanon@menfin.cert.fr
%%% end overflow headers %%%