The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Dear All,

I am trying to learn Coq and I have installed the Coq[1] for OSX 10.8.4.

Mukeshs-MacBook-Pro:~ mukeshtiwari$ coq
coq-tex       coqc          coqchk.opt    coqdoc        coqtags       coqtop.byte   coqwc        
coq_makefile  coqchk        coqdep        coqmktop      coqtop        coqtop.opt   


Mukeshs-MacBook-Pro:~ mukeshtiwari$ coqtop
Welcome to Coq 8.4 (September 2012)

Coq <

I have installed the Proof-General[2] for Emacs and .emacs configuration is

Mukeshs-MacBook-Pro:~ mukeshtiwari$ cat .emacs

(setq make-backup-files nil)

(setq c-default-style "linux"
      c-basic-offset 4)



(require 'tramp)
(setq tramp-default-method "scp")

(setenv "PATH" (concat "/usr/local/smlnj-110.75/bin:" (getenv "PATH")))
(setq exec-path (cons "/usr/local/smlnj-110.75/bin" exec-path))

(setenv "PATH" (concat "/Users/mukeshtiwari/Programming/GHC/ghc-7.6.1/bin:" (getenv "PATH")))
(setq exec-path (cons "/Users/mukeshtiwari/Programming/GHC/ghc-7.6.1/bin" exec-path))

(setenv "PATH" (concat "/Users/mukeshtiwari/.cabal/bin:" (getenv "PATH")))
(setq exec-path (cons "/Users/mukeshtiwari/.cabal/bin" exec-path))

(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))

(put 'downcase-region 'disabled nil)
(custom-set-variables
 ;; custom-set-variables was added by Custom.
 ;; If you edit it by hand, you could mess it up, so be careful.
 ;; Your init file should contain only one such instance.
 ;; If there is more than one, they won't work right.
 '(agda2-include-dirs (quote ("." "/Users/mukeshtiwari/Programming/Agda/Library/lib-0.7/src"))))
(custom-set-faces
 ;; custom-set-faces was added by Custom.
 ;; If you edit it by hand, you could mess it up, so be careful.
 ;; Your init file should contain only one such instance.
 ;; If there is more than one, they won't work right.
 )

(load-file "/Users/mukeshtiwari/Programming/Coq/ProofGeneral-4.2/ProofGeneral/generic/proof-site.el")


(require 'package)
(add-to-list 'package-archives
                      '("melpa" . "http://melpa.milkbox.net/packages/") t)
(package-initialize)
(unless (package-installed-p 'scala-mode2)
    (package-refresh-contents) (package-install 'scala-mode2))
Mukeshs-MacBook-Pro:~ mukeshtiwari$

When I am opening a file with .v extension, it showing

 Welcome to
              Coq Proof General!

                 Version 4.2.

        (C) LFCS, University of Edinburgh 2012


               Read the Proof General documentation
           Please report problems at Proof General trac
             Visit the Proof General wiki
               or the homepage

Find out about Emacs on the Help menu -- start with the Emacs Tutorial

      See this screen again with Proof-General -> About


I took this simple code from internet

(*
    Example proof script for Coq Proof General.

    example.v,v 11.0 2010/10/10 22:56:58 da Exp
*)

Module Example.

Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
  intros A B.
  intros H.
  elim H.
  split.
  assumption.
  assumption.
Save and_comms.

End Example.

and when I am trying to do C-c C-n ( Ctrl-c , Ctrl - n ) , I am getting

Starting: coqtop -emacs-U
apply: Searching for program: No such file or directory, coqtop

I also downloaded  CoqIdE_8.4pl2 and copied it to Application. When I am launching it, I am not getting any graphical interface but I can see CoqIdE in dock. When I am running top, I can see the codide.opt is running but no graphical interface!

1001  coqide.opt   0.0  00:00.20 2    1    62   147    8620K  8128K  18M    49M    2459M  994  994  sleeping 501  8359     648     2014     123      2749     5032      1939

Kindly tell me how to solve this problem ( Pardon me if I sound stupid ).

Regards,
Mukesh Tiwari

[1] http://coq.inria.fr/download
[2] http://proofgeneral.inf.ed.ac.uk/download