Errors when referencing a subtactic within another subtactic

[EphesosX]

Subtactics defined using the syntax "tactic tac1 as ( something );" can be referenced by other subtactics, e.g. "tactic tac2 as ( tac1; something else );", but when browsing proofs, entering subtactics in the web UI as custom proof steps, or sometimes even when reloading the webpage with the proof, they will fail to load with an error like "Identifier 'tac1' not recognized as a tactic identifier.". I suspect that this is because subtactics parsed by the parser are not being properly loaded into DerivationInfo to be used by other subtactics after being parsed.

Using the first proof of https://github.com/LS-Lab/KeYmaeraX-projects/blob/master/ijrr/robix.kyx as an example, I load the proof in the web UI, hit browse, expand more details twice, and get the error:

16:46:47.810 [hydraloader-akka.actor.default-dispatcher-15] ERROR edu.cmu.cs.ls.keymaerax.bellerophon.parser.BelleParser$ - Error parsing
tactic dib as (diall ; diffInvariant("v=old(v)-b()t", 1) ; diffInvariant("-t(v+b()/2t)<=x-old(x)&x-old(x)<=t(v+b()/2t)", 1) ; diffInvariant("-t(v+b()/2t)<=y-old(y)&y-old(y)<=t(v+b()/2*t)", 1))
edu.cmu.cs.ls.keymaerax.parser.ParseException: 1:16 Identifier 'diall' is not recognized as a tactic identifier. Encountered while parsing diall
Found: at 1:16 to 1:20
Expected:
at edu.cmu.cs.ls.keymaerax.parser.ParseException$.apply(ParserErrors.scala:78) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.bellerophon.parser.BelleParser$.constructTactic(BelleParser.scala:509) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.bellerophon.parser.BelleParser$.parseStep(BelleParser.scala:391) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.bellerophon.parser.BelleParser$.parseLoop(BelleParser.scala:122) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.bellerophon.parser.BelleParser$.parseTokenStream(BelleParser.scala:106) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.bellerophon.parser.BelleParser$.parseInnerExpr(BelleParser.scala:139) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.bellerophon.parser.BelleParser$.parseStep(BelleParser.scala:318) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.bellerophon.parser.BelleParser$.parseLoop(BelleParser.scala:122) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.bellerophon.parser.BelleParser$.parseTokenStream(BelleParser.scala:106) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.bellerophon.parser.BelleParser$.parseWithInvGen(BelleParser.scala:40) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.bellerophon.parser.BelleParser$.apply(BelleParser.scala:31) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.hydra.Helpers$.nodeJson(Response.scala:752) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.hydra.Helpers$.nodesJson(Response.scala:739) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.hydra.NodeChildrenResponse.getJson(Response.scala:479) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.hydra.NodeChildrenResponse.getJson(Response.scala:472) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.hydra.Response.print(Response.scala:61) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.hydra.Response.print$(Response.scala:61) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.hydra.NodeChildrenResponse.print(Response.scala:472) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.hydra.RestApi$.completeResponse(RestApi.scala:110) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.hydra.RestApi$.standardCompletion(RestApi.scala:97) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.hydra.RestApi$.$anonfun$completeRequest$2(RestApi.scala:89) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.directives.RouteDirectives.$anonfun$complete$1(RouteDirectives.scala:47) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.StandardRoute$$anon$1.apply(StandardRoute.scala:19) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.StandardRoute$$anon$1.apply(StandardRoute.scala:19) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.directives.BasicDirectives.$anonfun$mapRouteResult$2(BasicDirectives.scala:66) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.directives.BasicDirectives.$anonfun$textract$2(BasicDirectives.scala:159) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.directives.BasicDirectives.$anonfun$mapRequestContext$2(BasicDirectives.scala:43) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.directives.BasicDirectives.$anonfun$textract$2(BasicDirectives.scala:159) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.directives.BasicDirectives.$anonfun$mapRequestContext$2(BasicDirectives.scala:43) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.directives.BasicDirectives.$anonfun$textract$2(BasicDirectives.scala:159) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.directives.BasicDirectives.$anonfun$textract$2(BasicDirectives.scala:159) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.RouteConcatenation$RouteWithConcatenation.$anonfun$$tilde$2(RouteConcatenation.scala:47) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.util.FastFuture$.strictTransform$1(FastFuture.scala:41) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.util.FastFuture$.transformWith$extension1(FastFuture.scala:45) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.util.FastFuture$.flatMap$extension(FastFuture.scala:26) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.RouteConcatenation$RouteWithConcatenation.$anonfun$$tilde$1(RouteConcatenation.scala:44) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.RouteConcatenation$RouteWithConcatenation.$anonfun$$tilde$1(RouteConcatenation.scala:44) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.RouteConcatenation$RouteWithConcatenation.$anonfun$$tilde$1(RouteConcatenation.scala:44) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.RouteConcatenation$RouteWithConcatenation.$anonfun$$tilde$1(RouteConcatenation.scala:44) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.directives.ExecutionDirectives.$anonfun$handleExceptions$2(ExecutionDirectives.scala:32) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.directives.BasicDirectives.$anonfun$mapRouteResultWith$2(BasicDirectives.scala:72) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.directives.BasicDirectives.$anonfun$textract$2(BasicDirectives.scala:159) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.directives.ExecutionDirectives.$anonfun$handleExceptions$2(ExecutionDirectives.scala:32) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.directives.BasicDirectives.$anonfun$textract$2(BasicDirectives.scala:159) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.http.scaladsl.server.Route$.$anonfun$asyncHandler$1(Route.scala:86) ~[keymaerax-4.7.1.jar:4.7.1]
at akka.stream.impl.fusing.MapAsyncUnordered$$anon$31.onPush(Ops.scala:1375) [keymaerax-4.7.1.jar:4.7.1]
at akka.stream.impl.fusing.GraphInterpreter.processPush(GraphInterpreter.scala:523) [keymaerax-4.7.1.jar:4.7.1]
at akka.stream.impl.fusing.GraphInterpreter.execute(GraphInterpreter.scala:409) [keymaerax-4.7.1.jar:4.7.1]
at akka.stream.impl.fusing.GraphInterpreterShell.runBatch(ActorGraphInterpreter.scala:606) [keymaerax-4.7.1.jar:4.7.1]
at akka.stream.impl.fusing.GraphInterpreterShell$AsyncInput.execute(ActorGraphInterpreter.scala:485) [keymaerax-4.7.1.jar:4.7.1]
at akka.stream.impl.fusing.GraphInterpreterShell.processEvent(ActorGraphInterpreter.scala:581) [keymaerax-4.7.1.jar:4.7.1]
at akka.stream.impl.fusing.ActorGraphInterpreter.akka$stream$impl$fusing$ActorGraphInterpreter$$processEvent(ActorGraphInterpreter.scala:749) [keymaerax-4.7.1.jar:4.7.1]
at akka.stream.impl.fusing.ActorGraphInterpreter$$anonfun$receive$1.applyOrElse(ActorGraphInterpreter.scala:764) [keymaerax-4.7.1.jar:4.7.1]
at akka.actor.Actor.aroundReceive(Actor.scala:539) [keymaerax-4.7.1.jar:4.7.1]
at akka.actor.Actor.aroundReceive$(Actor.scala:537) [keymaerax-4.7.1.jar:4.7.1]
at akka.stream.impl.fusing.ActorGraphInterpreter.aroundReceive(ActorGraphInterpreter.scala:671) [keymaerax-4.7.1.jar:4.7.1]
at akka.actor.ActorCell.receiveMessage(ActorCell.scala:612) [keymaerax-4.7.1.jar:4.7.1]
at akka.actor.ActorCell.invoke(ActorCell.scala:581) [keymaerax-4.7.1.jar:4.7.1]
at akka.dispatch.Mailbox.processMailbox(Mailbox.scala:268) [keymaerax-4.7.1.jar:4.7.1]
at akka.dispatch.Mailbox.run(Mailbox.scala:229) [keymaerax-4.7.1.jar:4.7.1]
at akka.dispatch.Mailbox.exec(Mailbox.scala:241) [keymaerax-4.7.1.jar:4.7.1]
at akka.dispatch.forkjoin.ForkJoinTask.doExec(ForkJoinTask.java:260) [keymaerax-4.7.1.jar:4.7.1]
at akka.dispatch.forkjoin.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1339) [keymaerax-4.7.1.jar:4.7.1]
at akka.dispatch.forkjoin.ForkJoinPool.runWorker(ForkJoinPool.java:1979) [keymaerax-4.7.1.jar:4.7.1]
at akka.dispatch.forkjoin.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:107) [keymaerax-4.7.1.jar:4.7.1]
Caused by: edu.cmu.cs.ls.keymaerax.bellerophon.ReflectiveExpressionBuilderExn: Identifier 'diall' is not recognized as a tactic identifier.
at edu.cmu.cs.ls.keymaerax.bellerophon.ReflectiveExpressionBuilder$.apply(ReflectiveExpressionBuilder.scala:86) ~[keymaerax-4.7.1.jar:4.7.1]
at edu.cmu.cs.ls.keymaerax.bellerophon.parser.BelleParser$.constructTactic(BelleParser.scala:507) ~[keymaerax-4.7.1.jar:4.7.1]
... 63 more

[EphesosX]

but when browsing proofs, entering subtactics in the web UI as custom proof steps, or sometimes even when reloading the webpage with the proof, they will fail to load with an error like "Identifier 'tac1' not recognized as a tactic identifier.".

Upon closer inspection, it seems that all subtactics are not recognized in the web UI, even when outside of a subtactic definition. E.g. entering "tactic tac1 as (something)" will be accepted as a proof step, but attempting to use tac1, even by itself, will fail with the same identifier not recognized error.