dominique-unruh/qrhl-tool

Issues

• Reloading Isabelle theories in qrhl-tool doesn't work right in Windows

  #78 opened 2 years ago by dominique-unruh
  0

• `print goal` should check assumptions

  #77 opened 2 years ago by dominique-unruh
  0

• Update upstream ProofGeneral

  #74 opened 2 years ago by dominique-unruh
  2

• Update webpage

  #76 opened 2 years ago by dominique-unruh
  0

• Support Isabelle2022

  #62 opened 2 years ago by dominique-unruh
  1

• ProofGeneral and qrhl-tool detect end of command differently.

  #60 opened 2 years ago by dominique-unruh
  1

• Document sp-tactic

  #61 opened 2 years ago by dominique-unruh
  0

• Document `rewrite` tactic.

  #71 opened 2 years ago by dominique-unruh
  0

• Document denotational-equivalence support in byqrhl tactic

  #64 opened 2 years ago by dominique-unruh
  0

• Make swap-tactic syntax simpler

  #69 opened 2 years ago by dominique-unruh
  2

• Document `print goal` command

  #67 opened 2 years ago by dominique-unruh
  1

• Fix finding of roots in `hashedcomputation.RootsDirectory`

  #75 opened 2 years ago by dominique-unruh
  1

• Add `rewrite` tactic to ProofGeneral syntax highlighting

  #73 opened 2 years ago by dominique-unruh
  1

• Make `print xxx` work consistently.

  #72 opened 2 years ago by dominique-unruh
  1

• Rewrite tactic that allows to replace some line(s) by something denotationally equivalent

  #70 opened 2 years ago by dominique-unruh
  1

• Line numbers in goal display

  #68 opened 2 years ago by dominique-unruh
  1

• Document `-q` option for `proofgeneral.sh`

  #65 opened 2 years ago by dominique-unruh
  2

• Fix syntax of measure in/with

  #66 opened 2 years ago by dominique-unruh
  0

• Document extended swap-tactic

  #63 opened 2 years ago by dominique-unruh
  1

• Sbt test fails due to Bad Parent Session

  #59 opened 2 years ago by ianhhlee
  4

• Support inputting ⟶ (implication arrow)

  #55 opened 3 years ago by dominique-unruh
  0

• Proper indentation support in Proof General

  #56 opened 3 years ago by dominique-unruh
  1

• Syntax highlighting: also after focus commands and after previous command.

  #57 opened 3 years ago by dominique-unruh
  1

• Parser / Proof General: Make sure comments are treated in the same way

  #58 opened 3 years ago by dominique-unruh
  1

• When an error happens in replay, adjust error message to say so more clearly

  #51 opened 3 years ago by dominique-unruh
  1

• Rename `colocal` and friends to something more understandable (and no overloading)

  #54 opened 3 years ago by dominique-unruh
  1

• Theories should be loaded with quick_and_dirty mode

  #30 opened 3 years ago by dominique-unruh
  0

• Documentation updates

  #47 opened 3 years ago by dominique-unruh
  0

• Include git revision in qrhl-tool startup output (even without debug logging)

  #49 opened 3 years ago by dominique-unruh
  1

• Get rid of "head of empty list" exception

  #50 opened 3 years ago by dominique-unruh
  1

• Add ! to isa-tactic.

  #52 opened 3 years ago by dominique-unruh
  1

• Undo can fail if there is an error in changed dependencies

  #53 opened 3 years ago by dominique-unruh
  0

• Printing/parsing ambiguity

  #48 opened 3 years ago by dominique-unruh
  0

• Isabelle theories should be reloaded when they change

  #33 opened 3 years ago by dominique-unruh
  2

• Search for qrhl-tool.conf in the "intended" current dir

  #39 opened 3 years ago by dominique-unruh
  1

• In manual, check if the examples use old syntax

  #46 opened 3 years ago by dominique-unruh
  0

• Update terse teleportation proof in manual (does not use isa thy anymore)

  #45 opened 3 years ago by dominique-unruh
  0

• Recreate proofgeneral.bat or explain different approach to run PG on Windows

  #34 opened 3 years ago by dominique-unruh
  1

• Use only Isabelle-special subscript symbols in output (otherwise copy&paste to jEdit may not work)

  #44 opened 3 years ago by dominique-unruh
  1

• Update example files to various new constant syntaxes

  #43 opened 3 years ago by dominique-unruh
  1

• Fix syntactic sugar in goal-state-display

  #29 opened 3 years ago by dominique-unruh
  0

• Enable ket-syntax described in the manual

  #41 opened 3 years ago by dominique-unruh
  0

• In rule-tactic, don't dump large raw error on user

  #37 opened 3 years ago by dominique-unruh
  0

• Phase out overloaded syntaxes

  #40 opened 3 years ago by dominique-unruh
  2

• Change notation \otimes_s -> \otimes_l

  #42 opened 3 years ago by dominique-unruh
  1

• `bin/qrhl` should finish in success case with something nicer than `EOF`

  #38 opened 3 years ago by dominique-unruh
  0

• Support for subscript/superscript in Isabelle terms

  #28 opened 3 years ago by dominique-unruh
  3

• Allow loading of different session than QRHL.QRHL

  #31 opened 3 years ago by dominique-unruh
  0

• Have qrhl-tool.conf in a per-user dir, in /etc, in current dir

  #32 opened 3 years ago by dominique-unruh
  1

• Document focusing in manual

  #27 opened 3 years ago by dominique-unruh
  0