OKlibrary  0.2.1.6
Coq.hpp File Reference

Plans regarding installation of Coq. More...

Go to the source code of this file.


Detailed Description

Plans regarding installation of Coq.

Todo:
Improve Coq installation
  • Download documentation and make it available.
  • How to make the man-pages available?
  • What about LablGtk2 not found: CoqIde will not be available: This library comes normally with ocaml ?!
  • Tell the Coq-people about the incompatibility with Ocaml 3.10.0 (that is, the usage of the deprecated "pa_ifdef.cmo", removed in Ocaml 3.10.0).
  • The manual says
       If you wish to write tactics (and that really means that you belong
       to advanced users !) you *must* keep the Coq sources, without cleaning
       them.
        
    Now what does it mean to "keep the sources" --- they recommend not to use "make install", but then the manual etc. won't be installed? We ignore this first, since writing tactics will only come later, and we can reinstall Coq anytime.
Todo:
Improve ocaml installation
  • http://caml.inria.fr/
  • It should become an independent external source.
  • Where do we get lablgtk2 (the problems seems to be version 2) ?? (The Coq installation claims it's not there, but it should have been build by the Ocaml installation.)
  • Target "make cleanocaml" for removing the build-directory.
  • What about (after "configure")
    NDBM not found, the "dbm" library will not be supported.
       

Definition in file Coq.hpp.