Emacs Stack Exchange
Emacs Stack Exchange

Questions tagged [proof-general]

Proof General is a generic front-end to several proof assistants such as Coq

The Proof General package provides a generic front-end to several proof assistants. It facilitates development by sending lines from a source file one by one to the proof assistant's read-eval-print loop and understands backtracking. It is actively maintained for Coq, and can also support Isabelle, HOL, ACL2, LEGO, Phox, as well as OCaml and Haskell to some extent.

External links

7 questions
4
votes
1 answer

How to add symbols to prettify and pretty modes?

I am trying to configure Emacs with ProofGeneral (the Coq IDE) to display mathematical symbols in place of the abbreviations ->, =>, forall and exists. My current .emacs script is as follows: ;; Open .v files with Proof General's Coq mode (load…
ryan221b
  • 151
  • 5
2
votes
1 answer

How to activate Coq for Org source blocks?

I have been writing some Coq code in Org, but when I try to run a source block, I get the following message: No org-babel-execute function for coq! I have tried to initialize the coq language in the org-babel-load-languages variable, but coq isn't…
James Leslie
  • 123
  • 5
2
votes
1 answer

proof-general no newline after C-c C-n

I am using proof-general mode for editing and executing Coq files in emacs. However, I am highly annoyed by the C-c C-n behavior of always going to the next line if the EoF is reached. As I tend to use it interactively, executing the proof as I go…
Sim
  • 123
  • 5
1
vote
0 answers

How to make the response-mode wrap text in proof general

I'm using proof general and I would like to have the response window wrap text. The default display is a three-window mode. The buffers are called proof-script-buffer proof-goals-buffer and proof-response-buffer (documentation). The first two wrap…
sdpoll
  • 111
  • 2
1
vote
0 answers

SSreflect not working with Emacs, Coq and ProofGeneral. How to install SSreflect in MacOS?

If I do something like - From mathcomp Require Import ssreflect. it gives me the following error. Error: Cannot load mathcomp.ssreflect.ssreflect: no physical path bound to mathcomp.ssreflect But if I do this instead - Require Import ssreflect. It…
Vedant Chavda
  • 11
  • 1
1
vote
1 answer

How does one save and close a file in Proof General without all of Evil shutting down?

I am using evil (emacs+vim). I am also using Proof General for the theorem prover Coq. I was trying to work with emacs but whenever I do: :x or :q in my coq .v file all of emacs closes as well (with all my buffers going down). I tried just…
Charlie Parker
  • 121
  • 6
0
votes
1 answer

Why does Evil autocomplete simpl. ESC to beta delta [] iota zeta.?

This might be a strange question but every time I type: simpl. Evil substitutes it with: simpl beta delta [] iota zeta. this is driving me nuts. Why is this happening and more importantely, how do I stop it? I want to be able to escape…
Charlie Parker
  • 121
  • 6