LS-Lab/KeYmaeraX-release

Issues

• Scala 2.13/dotty compatibility

  #68 opened 4 years ago by zstone1
  5

• Unable to use built-in implicitly defined functions (e.g., sin(x))

  #113 opened 10 months ago by wdsmth
  1

• Configuration.sanitizedPathSegments breaks execution on Windows

  #110 opened 5 months ago by bk-jb
  5

• Error with derived axioms database in KeYmaera 5.0.2

  #112 opened a year ago by ytzemih
  2

• Input {48, MemoryConstrained[...]} cannot be evaluated, cause: {HoldForm[MessageName[ForAll, "msgs"]]}

  #109 opened a year ago by krooken
  2

• Mathematica and Wolfram Engine Configuration

  #108 opened 2 years ago by umerhuzaifa
  1

• [UI] [enhancement] Change right-click menu closing logic

  #97 opened 3 years ago by rbohrer
  0

• opening deleted proof-> lots of error dialogs

  #103 opened 3 years ago by rbohrer
  0

• mond context-menu UI bug

  #105 opened 3 years ago by rbohrer
  0

• [Usability enhancement] certain "permanent" hides fail while same formula is "temporarily hidden

  #81 opened 3 years ago by rbohrer
  1

• KeyMaeraX not Loading

  #107 opened 3 years ago by umerhuzaifa
  2

• dV on "equals": an implementation is missing

  #106 opened 3 years ago by rbohrer
  2

• [UI] [enhancement] Model pop-up dialog does not auto-close upon running incomplete tactic

  #100 opened 3 years ago by rbohrer
  0

• [UI] only allow editing existing model while "edit" button is active

  #102 opened 3 years ago by rbohrer
  0

• Cannot prove lemmas due to overlapping UI elements

  #93 opened 3 years ago by rbohrer
  1

• [UI] [enhancement] Not obvious to user why diRule breaks tactic editor goal-switching

  #98 opened 3 years ago by rbohrer
  6

• [Usability enhancement] Deleting text in tactic window leads to incorrect underlining

  #80 opened 3 years ago by rbohrer
  1

• Some syntax errors only found upon starting proof

  #95 opened 3 years ago by rbohrer
  1

• [parser/printer?] KeYmaera X allows uploading models with Unicode characters, then errs

  #104 opened 3 years ago by rbohrer
  1

• [UI] [enhancement] raw token names in alternative tactic editor display are surprising

  #99 opened 3 years ago by rbohrer
  0

• empty Tactic block => internal safety check violated

  #101 opened 3 years ago by rbohrer
  0

• JDK 12 Build Error Again

  #92 opened 3 years ago by rbohrer
  0

• Archive only uploads halfway when some entries contain non-fatal errors

  #94 opened 3 years ago by rbohrer
  0

• Late definition usubst clash checking leads to less direct error messages

  #96 opened 3 years ago by rbohrer
  0

• HOST accepts only 127.0.0.1

  #91 opened 3 years ago by d01010101
  1

• "New Model" + "Start Proof" = Spurious Syntax Error Reported

  #89 opened 3 years ago by rbohrer
  0

• I'm trapped in the model editor

  #90 opened 3 years ago by rbohrer
  0

• "internal safety check violated"

  #88 opened 3 years ago by myradotzel
  1

• [UI] [enhancement] Visibility of temporary hiding UI

  #87 opened 3 years ago by rbohrer
  0

• [UI] [bug] Error using "minmax" tactic through top menu bar

  #85 opened 3 years ago by rbohrer
  2

• [UI] [bug-hancement] Interaction between temporary hiding and counterxample search UIs

  #86 opened 3 years ago by rbohrer
  0

• Java Versions in Build Instructions

  #83 opened 3 years ago by nrfulton
  1

• Backend Tool Termination - undefined symbol: uuid_generate

  #72 opened 3 years ago by Bckempa
  7

• [Enhancement request] useLemma with USubst or unification from Web UI

  #82 opened 3 years ago by rbohrer
  0

• Tactic serialization of "pending" generates tactic that doesn't parse due to string escaping

  #79 opened 3 years ago by rbohrer
  0

• Is there any plan to make user-defined tactics usable on the UI?

  #75 opened 4 years ago by rbohrer
  0

• Vector and Matrix Support

  #69 opened 4 years ago by zstone1
  5

• Variables to function

  #71 opened 3 years ago by L-Viard
  7

• Cannot export SharedDefinition of hybrid program binding unshared ProgramVariable

  #78 opened 3 years ago by rbohrer
  1

• Problem with Mathematica/Wolfram engine versions

  #73 opened 3 years ago by JaimePSantos
  1

• "Checking proof" hangs after combination of "expand," "expandAllDefs," and "tactic ... as"

  #74 opened 3 years ago by rbohrer
  1

• Proof won't rerun lemmas unless lemmadb cleared and prover restarted by hand

  #77 opened 3 years ago by rbohrer
  0

• Cryptic error when using comma-separated declaration syntax in SharedDefinitions

  #76 opened 4 years ago by rbohrer
  0

• Differential Weaken for Diamond

  #70 opened 4 years ago by L-Viard
  4

• When "-tool mathematica" is used, the mathematica paths in ~/.keymaerax/keymaerax.conf are ignored?

  #66 opened 5 years ago by ANogin
  2

• Hosted KeYmaera X Does Not Work

  #65 opened 5 years ago by nrfulton
  0

• Is it possible to populate the lemma database from a shell script without UI?

  #67 opened 5 years ago by ANogin
  0

• ^@ semantics

  #64 opened 5 years ago by SweeWarman
  2

• KeYmaera X hangs after -prove calls on OpenJDK when using wolframscript

  #63 opened 5 years ago by nrfulton
  1

• Bug in initialization code for wolframengine tool

  #62 opened 5 years ago by nrfulton
  0