In [1]:
import $cp.bin.`provingground-core-jvm-ac7ee25c26.fat.jar`
import provingground._ , interface._, HoTT._, learning._
repl.pprinter() = {
val p = repl.pprinter()
p.copy(
additionalHandlers = p.additionalHandlers.orElse {
translation.FansiShow.fansiHandler
}
)
}
Out[1]:
In [2]:
Utils.logger = {
import scribe._, writer._, Utils._
logger.withHandler(writer = FileWriter().path(file.LogPath.simple("modus-ponens.log"))).replace()
}
First we set things up.
In [3]:
import provingground._ , learning._, interface._, translation._, HoTT._
import monix.execution.Scheduler.Implicits.global
val A = Type.sym
val B = Type.sym
val MP = A ~>: (B ~>: (A ->: (A ->: B) ->: B))
val ts = TermState(FiniteDistribution.unif(Type), FiniteDistribution.unif(Type))
val tg = TermGenParams.zero.copy(appW = 0.1, unAppW = 0.1)
val lp = LocalProver(ts, tg)
import HoTTMessages._
Out[3]:
Next we post stuff. Note that this is still manual bot mode, but a session will only have a couple of useless triggers.
In [4]:
val web = new HoTTPostWeb()
val ws = WebState[HoTTPostWeb, HoTTPostWeb.ID](web)
val ws1 = ws.post(lp, Set())
val ws2 = ws1.flatMap(w => w.postApex(SeekGoal(MP, Context.Empty)))
In [5]:
import HoTTBot._
val sessF = ws2.map(w => HoTTWebSession.launch(w, Vector(fullGoalInContext , goalToProver(0.3, 0.7), lpToFinalState, reportSuccesses)))
In [6]:
Utils.reportText
Out[6]: