Ptival/PeaCoq

Issues

• Docker image: missing files

  #43 opened 7 years ago by VolkerStolz
  1

• Serialization of Coq's types.

  #44 opened 6 years ago by ejgallego
  5

• Building PeaCoq on NixOS

  #38 opened 8 years ago by Zimmi48
  12

• Online demo

  #39 opened 8 years ago by langston-barrett
  2

• Description and screenshots in README

  #40 opened 8 years ago by langston-barrett
  0

• Fail loudly when the wrong version of coqtop is found

  #37 opened 8 years ago by Ptival
  0

• Trouble on "Building OCaml plugin" setup.sh step

  #36 opened 8 years ago by darzu
  10

• Make proof search for contradictions more aggressive?

  #20 opened 9 years ago
  0

• Automatically inserting `Qed` and going out of proof mode is inconvenient

  #18 opened 8 years ago by gasche
  1

• Typescript fails to build on latest version of typescript compiler

  #35 opened 8 years ago by hugovincent
  7

• Does that support JAVA non-script?

  #27 opened 8 years ago by 13Kill
  1

• Unsupported unicode character:0x200b

  #29 opened 8 years ago by tbelaire
  1

• setup for Test.hs

  #32 opened 9 years ago by tbelaire
  7

• Could you port the PeaCoq to windows?

  #31 opened 9 years ago by Kuznetsov2100
  1

• Showing proof context

  #30 opened 9 years ago by tbelaire
  2

• PeaCoq does not support "Proof with (...)."

  #17 opened 9 years ago by Ptival
  0

• Editor should insert a space before a command if there is none

  #15 opened 9 years ago by Ptival
  0

• Search highlight interferes with documentation

  #12 opened 9 years ago by Ptival
  0

• Backtracking can cause infinite loop in proof tree mode

  #13 opened 9 years ago by Ptival
  0

• Mac: failed to run

  #28 opened 9 years ago by corwin-of-amber
  3

• Docker image fails to build

  #24 opened 9 years ago by emichael
  9

• firstorder causes proof tree to hang

  #26 opened 9 years ago by emichael
  4

• git is needed to run the server

  #22 opened 9 years ago by saludes
  5

• Error Installing in Debian Weezy

  #21 opened 9 years ago by wtonribeiro
  3

• Proof search should suggest "apply I" when the goal is "True".

  #19 opened 9 years ago
  0

• start server error

  #2 opened 10 years ago by stechu
  8

• Jitter bug

  #11 opened 9 years ago by Ptival
  1

• Failed cabal dependency resolution with base 4.8.0.0

  #16 opened 9 years ago by lukenels
  0

• Bug in parsing or printing precedence

  #14 opened 10 years ago by Ptival
  1

• Parenthesis matching would be wondrous!

  #5 opened 10 years ago by darzu
  1

• [low-pri] More eager syntax highlighting

  #6 opened 10 years ago by darzu
  5

• Being able to go back and forth between the text mode of a proof and the proof tree

  #8 opened 10 years ago by emackay
  2

• Allow saving with ctrl-s

  #9 opened 10 years ago by darzu
  4

• Wrong child displaying when focusing on n-th subgoal

  #10 opened 10 years ago by tune-george
  1

• Highlighting + typing doesn't replace the highlighted region

  #4 opened 10 years ago by darzu
  8

• Basic help: keyboard shortcuts

  #3 opened 10 years ago by darzu
  2

• Syntax Error: Lexer: Unsupported Unicode character (0x200b)

  #7 opened 10 years ago by emackay
  2

• Getting started on Mac

  #1 opened 10 years ago by darzu
  5