Stack Overflow
Stack Overflow

Questions tagged [proof-general]

Proof General is a generic front-end for proof assistants, based on Emacs.

Proof General is a generic front-end for proof assistants (like Coq or Isabelle), based on the customizable text editor Emacs.

See also http://proofgeneral.inf.ed.ac.uk/

39 questions
10
votes
2 answers

Agda-like programming in Coq/Proof General?

Unlike Agda, Coq tends to separate proofs from functions. The tactics Coq gives are great for writing proofs, but I'm wondering if there is a way to replicate some Agda-mode functionality. Specifically, I'd like: Some equivalent of Agda's ? or…
jmite
  • 8,171
  • 6
  • 40
  • 81
9
votes
1 answer

Unicode glyphs for keywords and operators in Coq/Proof General under Emacs

This question has to do with configuring the Coq mode within Proof General, in Emacs. I'm trying to have Emacs automatically replace keywords and notation in Coq with the corresponding Unicode glyphs. I managed to define fun to be the Greek…
Mayer Goldberg
  • 1,378
  • 11
  • 23
7
votes
2 answers

How do you look up where identifiers are defined in Coq efficiently?

In most IDEs or text editors, you can right-click a term and it takes you to the file where that term is defined. CoqIDE doesn't seem to have that, so I've been doing coqdoc myfile.v --html, then going to the generated HTML docs. But the only…
Lance
  • 75,200
  • 93
  • 289
  • 503
7
votes
1 answer

With Coq Proof General, Emacs executes on every period. How do I stop it?

I'm using Proof General in Emacs on Aquamacs and every time I write a period (".") everything is executed (up to that period). It seems like an electric behavior but it's not. All other keys behave normally. I know that this is some mode that…
Skuge
  • 1,010
  • 2
  • 11
  • 28
7
votes
2 answers

Unable to provide long (1024+ character) inputs to the OCaml toplevel and coqtop (and Proof General)

Edit 4: It turns out that this is actually just a limitation of TTY input in general; there's nothing specific about OCaml, Coq, or Emacs which is causing the problem. I'm working on a Coq program using Proof General in Emacs, and I've found a bug…
Antal Spector-Zabusky
  • 36,191
  • 7
  • 77
  • 140
6
votes
0 answers

How to resolve coq suffix import error (physical path bound to logical path)

Probably a coq newbie question, but I could not find a ready solution so I'll ask here for reference. The cocq version is 8.5pl2 I tried to build coqfj. The first make attempt has failed with some error in line 37 in src/FJ/ClassTable.v. This…
Lars Bohl
  • 1,001
  • 16
  • 20
6
votes
2 answers

Isabelle2016 and Proof General

I've been trying to learn to use Isabelle 2016. While in principle I like the idea of asynchronous proof checking, I don't like Isabelle/jEdit for a number of reasons, the most severe of which is that it uses too much memory (for me). It'd be great…
Pteromys
  • 1,441
  • 2
  • 12
  • 29
5
votes
4 answers

How to disable Verilog mode in emacs?

I'm trying to use coq with ProofGeneral, but the built-in Verilog mode shadows *.v filetype recognition. Can I somehow disable it and let ProofGeneral remap them to its coq mode?
Peteris
  • 3,548
  • 4
  • 28
  • 44
5
votes
2 answers

How do I display brackets around assumptions in Isabelle/jEdit?

When goals are displayed by Isabelle in ProofGeneral, assumptions are rendered as having brackets around them as so: In Isabelle/jEdit, however, this seems to have changed to meta-implication arrows: While I understand the former is somewhat…
davidg
  • 5,868
  • 2
  • 33
  • 51
4
votes
1 answer

How to change Coq Version in Proof General?

I have some code that only compiles coq code in Coq 8.09.0 . The version that I normally use is the most up-to-date version now which is Coq 8.11.0. I was able to create a new environment using opam switch and installed Coq 8.09.0 there. I…
Notemaster
  • 465
  • 1
  • 3
  • 15
4
votes
1 answer

Proof Process busy on combine_split

I'm doing the Software foundations exercises and doing the combine_split exercise I'm running into a wall when trying to prove an auxiliary lemma. When applying reflexivity within the assert the Proof Process just hangs there despite the equation…
Jose Javier Gonzalez Ortiz
  • 468
  • 1
  • 5
  • 16
3
votes
2 answers

How can I get C-c C-n to format the current line in proof-general coq-mode-map

I'm using proof-general to write Coq proofs. When I use C-c C-n in a proof, my cursor is moved to the next line, but the current line is not formatted. So for instance, if I type: intros n. my cursor moves to the next line, but intros n.…
azani
  • 486
  • 3
  • 14
2
votes
1 answer

"Symbol's value as variable is void" when adding a path to coqtop when opening emacs

I am trying to run emacs with proof generale to open Coq files. However, when I open emacs I get the following error message: Symbol's value as variable is void: “/Users/myusername/.opam/default/bin/coqtop” My emacs file is as follows: (setq…
user15598472
  • 23
  • 2
2
votes
1 answer

what is [...] in proof general and why can't I delete it

When I try and copy paste proof code, sometimes a [...] will show up (even though I did not copy anything of the kind) and I cannot delete it. I have to undo the copy in order to get rid of it. What does this mean? Thanks.
push33n
  • 398
  • 4
  • 12
2
votes
1 answer

Unicode symbols fail for Proof-general while writing Coq

I use Coq 8.11 in Ubuntu with Proof-general. I write: Ltac example1 := fail. and succeed. Say I want to use unicode symbols: Proof-General -> Display -> Quick Options -> Unicode Tokens then I write again: Ltac example2 ≔ fail. and fail…
user1868607
  • 2,558
  • 1
  • 17
  • 38
1
2 3