Comments (9)
nrfulton
commented on May 26, 2024
Strange.
For me at tag 4.3.5 it just proves. Can you give a screenshot or specify a version/commit?
from keymaerax-release.
nrfulton
commented on May 26, 2024
Oh! NVM, you said solve.
Here's the message:
[Bellerophon Runtime] Dependent position tactic DependentPositionTactic(solve) is not applicable at 1
[Bellerophon Runtime] Could not initialize class edu.cmu.cs.ls.keymaerax.btactics.SimplifierV3$
in >>_<<
at edu.cmu.cs.ls.keymaerax.bellerophon.DependentTactic.computeExpr(BellerophonSyntax.scala:424)
at edu.cmu.cs.ls.keymaerax.bellerophon.AppliedDependentPositionTactic$$anon$1.computeExpr(BellerophonSyntax.scala:518)
at edu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter.apply(SequentialInterpreter.scala:102)
at edu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter.apply(SequentialInterpreter.scala:103)
at edu.cmu.cs.ls.keymaerax.hydra.BellerophonTacticExecutor$$anon$1.call(BellerophonTacticExecutor.scala:129)
at edu.cmu.cs.ls.keymaerax.hydra.BellerophonTacticExecutor$$anon$1.call(BellerophonTacticExecutor.scala:126)
Caused by: java.lang.NoClassDefFoundError: Could not initialize class edu.cmu.cs.ls.keymaerax.btactics.SimplifierV3$
at edu.cmu.cs.ls.keymaerax.btactics.AxiomaticODESolver$.edu$cmu$cs$ls$keymaerax$btactics$AxiomaticODESolver$$simplifier$lzycompute(AxiomaticODESolver.scala:28)
at edu.cmu.cs.ls.keymaerax.btactics.AxiomaticODESolver$.edu$cmu$cs$ls$keymaerax$btactics$AxiomaticODESolver$$simplifier(AxiomaticODESolver.scala:28)
at edu.cmu.cs.ls.keymaerax.btactics.AxiomaticODESolver$$anonfun$axiomaticSolve$1.apply(AxiomaticODESolver.scala:56)
at edu.cmu.cs.ls.keymaerax.btactics.AxiomaticODESolver$$anonfun$axiomaticSolve$1.apply(AxiomaticODESolver.scala:40)
at edu.cmu.cs.ls.keymaerax.btactics.TacticFactory$TacticForNameFactory$$anon$10$$anon$12.computeExpr(MiscTactics.scala:327)
at edu.cmu.cs.ls.keymaerax.bellerophon.SingleGoalDependentTactic.computeExpr(BellerophonSyntax.scala:431)
at edu.cmu.cs.ls.keymaerax.bellerophon.DependentTactic.computeExpr(BellerophonSyntax.scala:419)
... 11 more
from keymaerax-release.
rbohrer
commented on May 26, 2024
BTW I meant to assign this to myself but am too dumb to find the relevant button on GitHub.
The actual case where this came up was more complicated, part of a student's model for Lab 3
from keymaerax-release.
nrfulton
commented on May 26, 2024
Added you. For future reference, ctrl-F for "assignees" on this page and then click the little gear thingie.
from keymaerax-release.
rbohrer
commented on May 26, 2024
I don't have a gear thingy. Permissions sadness maybe?
…On Wed, Mar 8, 2017 at 2:32 PM, Nathan Fulton ***@***.***> wrote:
Added you. ctrl-F for "assignees" on this page and then click the little
gear thingie.
—
You are receiving this because you were assigned.
Reply to this email directly, view it on GitHub
<#28 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AB3rYba5M3A48YEDzc-Y0HcJYU7sju6zks5rjwIzgaJpZM4MXMek>
.
from keymaerax-release.
nrfulton
commented on May 26, 2024
@bbohrer did you ever get around to fixing this problem? If so, can you close it? If not, I'll take care of it over the weekend.
from keymaerax-release.
rbohrer
commented on May 26, 2024
Totally can't remember, but I feel like I probably didn't fix it if I left
it open. Maybe git log has info. Would check except floc. Also don't know
if maybe ode stuff has all changed since then?
…On Fri, Jul 13, 2018, 5:39 PM Nathan Fulton ***@***.***> wrote:
@bbohrer <https://github.com/bbohrer> did you ever get around to fixing
this problem? If so, can you close it? If not, I'll take care of it over
the weekend.
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#28 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AB3rYYd_Vc6msL1ZQJtmqFCjWm9bgm_Wks5uGM1bgaJpZM4MXMek>
.
from keymaerax-release.
nrfulton
commented on May 26, 2024
OK, I'll investigate :-)
from keymaerax-release.
smitsch
commented on May 26, 2024
See 8617f07
from keymaerax-release.
Related Issues (20)
- [UI] [enhancement] Model pop-up dialog does not auto-close upon running incomplete tactic
- empty Tactic block => internal safety check violated
- [UI] only allow editing existing model while "edit" button is active
- opening deleted proof-> lots of error dialogs
- [parser/printer?] KeYmaera X allows uploading models with Unicode characters, then errs HOT 1
- mond context-menu UI bug
- dV on "equals": an implementation is missing HOT 2
- KeyMaeraX not Loading HOT 2
- Mathematica and Wolfram Engine Configuration HOT 1
- Input {48, MemoryConstrained[...]} cannot be evaluated, cause: {HoldForm[MessageName[ForAll, "msgs"]]} HOT 2
- Configuration.sanitizedPathSegments breaks execution on Windows HOT 4
- Error with derived axioms database in KeYmaera 5.0.2 HOT 2
- Unable to use built-in implicitly defined functions (e.g., sin(x))
- Cannot prove lemmas due to overlapping UI elements HOT 1
- Archive only uploads halfway when some entries contain non-fatal errors
- Some syntax errors only found upon starting proof HOT 1
- Late definition usubst clash checking leads to less direct error messages
- [UI] [enhancement] Change right-click menu closing logic
- [UI] [enhancement] Not obvious to user why diRule breaks tactic editor goal-switching HOT 6
- [UI] [enhancement] raw token names in alternative tactic editor display are surprising
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from keymaerax-release.