The Coq mailing list

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

Hi Fero,

Thank you! Now it's working.

Regards,

Mukesh Tiwari

On Fri, Aug 16, 2013 at 5:12 PM, Feró <ferenc.tamasi AT gmail.com> wrote:

I'd guess the path emacs uses does not contain coqtop.

If you start a shell and print $PATH from emacs, you should see it.

(M-x eshell, then echo $PATH, this works on linux)

On 8/16/13, mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:
> 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
>

--
Give me liberty or give me cash!