<commit_before>package provingground.interface

import provingground._

import scala.concurrent.ExecutionContext.Implicits.global
import MantleService._
import io.undertow.websockets.WebSocketConnectionCallback
import io.undertow.websockets.core.{AbstractReceiveListener, BufferedTextMessage, WebSocketChannel, WebSockets}
import io.undertow.websockets.spi.WebSocketHttpExchange
import monix.execution.CancelableFuture

import scala.util.Try

object MantleRoutes extends cask.Routes {
  @cask.staticFiles("docs")
  def docsRoute() = "docs"

  @cask.staticResources("resources")
  def public() = "."

  @cask.get("/")
  def root() =
    Site.page(indexHTML, "resources/", "ProvingGround HoTT Server", false)

  @cask.get("/index.html")
  def index() =
    Site.page(indexHTML, "resources/", "ProvingGround HoTT Server", false)

  @cask.get("/prover.html")
  def prover() =
    Site.page(proverHTML, "resources/", "ProvingGround HoTT Server", false)

  @cask.get("/leanlib.html")
  def leanlib() =
    Site.page(leanlibHTML, "resources/", "ProvingGround Lean Export", false)

  @cask.get("/interactive-prover.html")
  def interactiveProver() : String =
    Site.page(interactiveProverHTML, "resources/", "ProvingGround: Interactive prover", false)

  @cask.post("/monoid-proof")
  def seek() = {
    pprint.log("seeking proof")
    val pfFut = MonoidServer.seekResultFut
    pfFut.foreach((pf) => pprint.log(pf))
    "seeking proof"
  }

  @cask.route("build", methods = Seq("get", "post"))
  def site(request: cask.Request) =
    trySite()

  @cask.get("/scripts/index.html")
  def fiddle() = AmmService.indexHTML

  @cask.post("/scripts/kernel")
  def repl(request: cask.Request) = {
    val d = new String(request.readAllBytes())
    println(s"post received:\n$d")

    val result =
      AmmService.replResult(d) match {
        case Right(z) => "--RESULT--\n" + z
        case Left(z)  => "--ERROR--\n" + z
      }

    result
  }

  def sendProof(channel: WebSocketChannel): Unit = {
    val pfFut = MonoidServer.seekResultFut
    pfFut.foreach((pf) => WebSockets.sendTextBlocking(pf.toString, channel))
  }

  @cask.websocket("/monoid-websock")
  def showUserProfile(): cask.WebsocketResult = {
    new WebSocketConnectionCallback() {
      override def onConnect(exchange: WebSocketHttpExchange,
                             channel: WebSocketChannel): Unit = {
        channel.getReceiveSetter.set(
          new AbstractReceiveListener() {
            override def onFullTextMessage(
                channel: WebSocketChannel,
                message: BufferedTextMessage): Unit = {
              message.getData match {
                case "" => channel.close()
                case data =>
                  pprint.log(s"received $data over websocket")
                  sendProof(channel)
                  WebSockets.sendTextBlocking(data, channel)
              }
            }
          }
        )
        channel.resumeReceives()
      }
    }
  }

  import learning._

  @cask.websocket("/prover-websock")
  def proverSocket() =
    new TaskSocket(TermGenJson.all)

  initialize()

}

object MantleCask extends cask.Main(MantleRoutes, LeanRoutes) {
  override def port = Try(sys.env("PROVINGGROUND_PORT").toInt).getOrElse(8080)
  override def host = Try(sys.env("PROVINGGROUND_HOST")).getOrElse("localhost")
}

import monix.eval._


class TaskSocket(task: String => Task[String])
    extends WebSocketConnectionCallback() {

  import monix.execution.Scheduler.Implicits.global

  def respond(t: Task[String], channel: WebSocketChannel): CancelableFuture[Unit] =
    t.foreach((output) => WebSockets.sendTextBlocking(output, channel))

  override def onConnect(exchange: WebSocketHttpExchange,
                         channel: WebSocketChannel): Unit = {
    channel.getReceiveSetter.set(
      new AbstractReceiveListener() {
        override def onFullTextMessage(channel: WebSocketChannel,
                                       message: BufferedTextMessage): Unit = {
          message.getData match {
            case ""   => channel.close()
            case data =>
              respond(task(data), channel)
          }
        }
      }
    )
    channel.resumeReceives()
  }
}
<commit_msg>using "IP" for host address<commit_after>package provingground.interface

import provingground._

import scala.concurrent.ExecutionContext.Implicits.global
import MantleService._
import io.undertow.websockets.WebSocketConnectionCallback
import io.undertow.websockets.core.{AbstractReceiveListener, BufferedTextMessage, WebSocketChannel, WebSockets}
import io.undertow.websockets.spi.WebSocketHttpExchange
import monix.execution.CancelableFuture

import scala.util.Try

object MantleRoutes extends cask.Routes {
  @cask.staticFiles("docs")
  def docsRoute() = "docs"

  @cask.staticResources("resources")
  def public() = "."

  @cask.get("/")
  def root() =
    Site.page(indexHTML, "resources/", "ProvingGround HoTT Server", false)

  @cask.get("/index.html")
  def index() =
    Site.page(indexHTML, "resources/", "ProvingGround HoTT Server", false)

  @cask.get("/prover.html")
  def prover() =
    Site.page(proverHTML, "resources/", "ProvingGround HoTT Server", false)

  @cask.get("/leanlib.html")
  def leanlib() =
    Site.page(leanlibHTML, "resources/", "ProvingGround Lean Export", false)

  @cask.get("/interactive-prover.html")
  def interactiveProver() : String =
    Site.page(interactiveProverHTML, "resources/", "ProvingGround: Interactive prover", false)

  @cask.post("/monoid-proof")
  def seek() = {
    pprint.log("seeking proof")
    val pfFut = MonoidServer.seekResultFut
    pfFut.foreach((pf) => pprint.log(pf))
    "seeking proof"
  }

  @cask.route("build", methods = Seq("get", "post"))
  def site(request: cask.Request) =
    trySite()

  @cask.get("/scripts/index.html")
  def fiddle() = AmmService.indexHTML

  @cask.post("/scripts/kernel")
  def repl(request: cask.Request) = {
    val d = new String(request.readAllBytes())
    println(s"post received:\n$d")

    val result =
      AmmService.replResult(d) match {
        case Right(z) => "--RESULT--\n" + z
        case Left(z)  => "--ERROR--\n" + z
      }

    result
  }

  def sendProof(channel: WebSocketChannel): Unit = {
    val pfFut = MonoidServer.seekResultFut
    pfFut.foreach((pf) => WebSockets.sendTextBlocking(pf.toString, channel))
  }

  @cask.websocket("/monoid-websock")
  def showUserProfile(): cask.WebsocketResult = {
    new WebSocketConnectionCallback() {
      override def onConnect(exchange: WebSocketHttpExchange,
                             channel: WebSocketChannel): Unit = {
        channel.getReceiveSetter.set(
          new AbstractReceiveListener() {
            override def onFullTextMessage(
                channel: WebSocketChannel,
                message: BufferedTextMessage): Unit = {
              message.getData match {
                case "" => channel.close()
                case data =>
                  pprint.log(s"received $data over websocket")
                  sendProof(channel)
                  WebSockets.sendTextBlocking(data, channel)
              }
            }
          }
        )
        channel.resumeReceives()
      }
    }
  }

  import learning._

  @cask.websocket("/prover-websock")
  def proverSocket() =
    new TaskSocket(TermGenJson.all)

  initialize()

}

object MantleCask extends cask.Main(MantleRoutes, LeanRoutes) {
  override def port = Try(sys.env("PROVINGGROUND_PORT").toInt).getOrElse(8080)
  override def host = Try(sys.env("IP")).getOrElse("localhost")
}

import monix.eval._


class TaskSocket(task: String => Task[String])
    extends WebSocketConnectionCallback() {

  import monix.execution.Scheduler.Implicits.global

  def respond(t: Task[String], channel: WebSocketChannel): CancelableFuture[Unit] =
    t.foreach((output) => WebSockets.sendTextBlocking(output, channel))

  override def onConnect(exchange: WebSocketHttpExchange,
                         channel: WebSocketChannel): Unit = {
    channel.getReceiveSetter.set(
      new AbstractReceiveListener() {
        override def onFullTextMessage(channel: WebSocketChannel,
                                       message: BufferedTextMessage): Unit = {
          message.getData match {
            case ""   => channel.close()
            case data =>
              respond(task(data), channel)
          }
        }
      }
    )
    channel.resumeReceives()
  }
}

{'fraction_non_alphanumeric': 0.12336892052194544, 'fraction_numerical': 0.0009489916963226571, 'mean_word_length': 2.905048633626679, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 23, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1081338', 'n_tokens_mistral': 2677, 'n_tokens_neox': 2545, 'n_words': 482}