search

UniFormal / MMT

The MMT Language and System
https://uniformal.github.io/
Other
68 stars 23 forks source link

Odd crash of checking.Solver.check: no backend applicable to http://cds.omdoc.org/urtheories?PLF #393

Closed makarius closed 5 years ago

makarius commented 5 years ago

This is for MMT/01e0736c15fd and Isabelle/d75cd481f8d9 with experimental type-checking enabled as follows:

isabelle mmt_build
isabelle mmt_import -o mmt_type_checking ZF

It produces the following exception trace:

get error: no backend applicable to http://cds.omdoc.org/urtheories?PLF
info.kwarc.mmt.api.frontend.Controller.$anonfun$retrieve$2(Controller.scala:460)
scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)
info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)
info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)
info.kwarc.mmt.api.frontend.Controller.logGroup(Controller.scala:73)
info.kwarc.mmt.api.frontend.Controller.retrieve(Controller.scala:453)
info.kwarc.mmt.api.frontend.Controller.$anonfun$iterate$2(Controller.scala:443)
scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)
info.kwarc.mmt.api.frontend.Controller.iterate(Controller.scala:431)
info.kwarc.mmt.api.frontend.Controller.iterate(Controller.scala:443)
info.kwarc.mmt.api.frontend.Controller.iterate(Controller.scala:421)
info.kwarc.mmt.api.frontend.Controller$$anon$3.forDeclarationsInScope(Controller.scala:335)
info.kwarc.mmt.api.RuleSet$.$anonfun$collectAdditionalRules$2(Rule.scala:139)
info.kwarc.mmt.api.RuleSet$.$anonfun$collectAdditionalRules$2$adapted(Rule.scala:138)
scala.collection.immutable.List.foreach(List.scala:389)
info.kwarc.mmt.api.RuleSet$.collectAdditionalRules(Rule.scala:138)
info.kwarc.mmt.api.RuleSet$.collectRules(Rule.scala:127)
info.kwarc.mmt.api.checking.Solver$.check(Solver.scala:882)
info.kwarc.mmt.isabelle.Importer$.check_term(Importer.scala:67)
info.kwarc.mmt.isabelle.Importer$.$anonfun$importer$5(Importer.scala:345)
info.kwarc.mmt.isabelle.Importer$.$anonfun$importer$5$adapted(Importer.scala:345)
scala.collection.Iterator.foreach(Iterator.scala:944)
scala.collection.Iterator.foreach$(Iterator.scala:944)
scala.collection.Iterator$ConcatIterator.foreach(Iterator.scala:176)
info.kwarc.mmt.isabelle.Importer$.add_constant$1(Importer.scala:345)
info.kwarc.mmt.isabelle.Importer$.$anonfun$importer$10(Importer.scala:392)
info.kwarc.mmt.isabelle.Importer$.decl_error$1(Importer.scala:360)
info.kwarc.mmt.isabelle.Importer$.$anonfun$importer$9(Importer.scala:388)
info.kwarc.mmt.isabelle.Importer$.$anonfun$importer$9$adapted(Importer.scala:387)
scala.collection.immutable.List.foreach(List.scala:389)
info.kwarc.mmt.isabelle.Importer$.$anonfun$importer$6(Importer.scala:387)
info.kwarc.mmt.isabelle.Importer$.$anonfun$importer$6$adapted(Importer.scala:367)
scala.collection.immutable.List.foreach(List.scala:389)
info.kwarc.mmt.isabelle.Importer$.import_theory$1(Importer.scala:367)
info.kwarc.mmt.isabelle.Importer$.$anonfun$importer$26(Importer.scala:464)
info.kwarc.mmt.isabelle.Importer$.$anonfun$importer$26$adapted(Importer.scala:464)
info.kwarc.mmt.isabelle.Importer$Isabelle.import_session(Importer.scala:710)
info.kwarc.mmt.isabelle.Importer$.importer(Importer.scala:464)
info.kwarc.mmt.isabelle.Importer$.$anonfun$main$1(Importer.scala:567)
isabelle.Command_Line$.$anonfun$tool0$1(command_line.scala:38)
isabelle.Command_Line$.tool(command_line.scala:29)
isabelle.Command_Line$.tool0(command_line.scala:38)
info.kwarc.mmt.isabelle.Importer$.main(Importer.scala:475)
info.kwarc.mmt.isabelle.Importer.main(Importer.scala)
florian-rabe commented 5 years ago

This means the theory http://cds.omdoc.org/urtheories?PLF is not found in any of the archives that are added to the mathpath.

So most likely you have not opened the MMT/urtheories archive.

makarius commented 5 years ago

OK, works.