uframeit / uframeit

The current Unity-based implementation of the FrameIT approach

UFrameIT

The FrameIT project builds a Framework for developing Serious Games by combining Virtual Worlds with Mathematical Knowledge Management. The UFrameIT framework uses the Unity game engine with the MMT system. This repository contains the Unity project, which currently includes the framework itself and a demo game. MMT itself is a large system with many different use cases beyond FrameIT. It operates with archives of formalized knowledge. For FrameIT, we added a new archive that, in turn, makes use of archives that existed before and contain knowledge about mathematics and logics. Unity and MMT communicate via the FrameIT-Server

For more information about the project, please visit https://uframeit.org

Installation (for end users)

Just download our latest release: https://github.com/UFrameIT/UFrameIT/releases/latest

Installation (for students at KWARC)

Active Development happens at https://gl.kwarc.info/FrameIT/UFrameIT Stable Versions will be released on GitHub.

Installation (for developers)

First, you have to set up a development environment:

1. Install Unity 2020.3.x (LTS) via the Unity Hub.

   We periodically update to the latest LTS version. Currently, any 2020.3 version should work; you can safely ignore any version warnings popping up.

   Make sure to activate your license.

2. Install Git LFS

3. Clone this repository: git clone --recurse-submodules https://github.com/UFrameIT/UFrameIT.git

4. Follow the UFrameIT server's guide on setting up a dev environment.

   Thereby, you will also install the necessary archives of formalization UFrameIT/archives.

Running

1. Open the Unity Hub and add the folder where you cloned this repository to. Then open the project in the hub.
2. Follow the UFrameIT server installation guide to run the server
3. In Unity, select the scene MainMenue.unity (You can find it in Assets\Scenes\Menues) and run the game (Play Button). From there you can try out "TechDemo A" in the "Demo Category"; click on it to expand a list of levels to choose from.

Building and starting the UFrameIT Server for standalone run.

1. Get JAR-file of the UFrameIT Server
   • Download a prebuild Version here: frameit-mmt.jar
   • Or build your own JAR as described in the following chapter "Build FrameIT Server to JAR" below.
2. Download Archives folder
   • archives
3. Start Server with Command:

   •    Java -jar YourUFrameITServer.jar -bind :PortOfNewServer -archive-root LinkToFolderArchives
        Example: Java -jar frameit-mmt.jar -bind :8085 -archive-root C:\Users\abc\xyz\archives
     

Build FrameIT Server to JAR

First time setting up

1. Open in Intellij the project with the UFrameIT Server.
2. Navigate in Intellij to: File -> Project Structure -> Artifacts
3. In the Artifacts Menue, press the icon "+" than choose JAR -> From modules with dependencies
4. In the new Menue "CreateJAR from Modules"
   • find "Module:" and select "frameit-mmt"
   • find "Main Class:" and search for the "Server" or set the path to the Server:
     Link: ... -> frameit-mmt -> src -> info.kwac.mmt.frameit -> communication -> server -> Server
   • Set "JAR files from libraries" to "extract to the target JAR".
   • Press "Ok"
5. "Press OK"
6. Follow steps from next chapter:

Build the JAR

1. Open in Intellij the project with the UFrameIT Server.
2. Navigate in Intellij to: Build -> Build Artifacts -> SelectYourArtifact -> Build

• General to_JAR-file Tutorial

Useful Links for new Developers

• Publications

UFrameIT Unity Plugin

• Installation Guide

FrameIT Server

• Installation Guide
• Documentation
• FrameIT Server Request Examples
• MMT API Documentation

Formalized Knowledge

• Installation guide
• How to write a Scroll
• MMT Language Documentation
• MMT Tutorials

uframeit's Issues

Scroll application view should be put into situation theory, not situation space

Not critical, will only eventually lead to typechecking reporting warnings. So lest I forget, I document this here.

Implement ability to show/log situation theory, view, pushout, ...

In-game the user should be able to show/log the situation theory, the built view, and the pushout to a console or to a file with MMT surface syntax.

Components:

• Extend UFrameIT/mmt-server with a REST interface for querying surface syntax. MMT already has the ability to stringify in-memory theories/views/... to MMT surface syntax using the MMTSyntaxPresenter. @ComFreek knows about this.

• Extend the Unity game with buttons/logging, where the surface syntax is queried from UFrameIT/mmt-server. Who does this?

Formalization of measured lengths vs. length being a constant value

Current style of formalization:

• To formalize that users have to measure an angle, we currently use: angle : Σ α: ℝ. ⊦ ( ∠ A,B,C ) ≐ α.
• To formalize that an angle is exactly something (e.g. 90.0°), we currently use: rightAngle: ⊦ ( ∠ A,B,C ) ≐ 90.0.

Problem: The Unity angle gadget currently only generates facts of the first type.

Questions:

• Is this the right approach for formalization? Also from a didactics POV?

• Which one should fact gadgets on the game engine side generate? Should they, upon some standard angle (say 30, 45, 90, 180), always generate both facts?

• How about emitting just the first one and MMT helping along?

  Example: consider a scroll with required fact rightAngle: ⊦ ( ∠ A,B,C ) ≐ 90.0, among others. Also consider a situation theory into which we already emitted angle : Σ α: ℝ. ⊦ ( ∠ A,B,C ) ≐ α | = <90.0, sketch "as measured">.
  Now MMT should be able to infer that the type of rightAngle simplifies to ⊦ 90.0 ≐ 90.0 in the context of the situation theory (i.e. the same context in which scroll assignments live). And for that, MMT can synthesize a proof term.

Create an internal glossary / use a consistent glossary to the outside

feel free to edit this post

---

• FrameIT Project (short: FrameIT): the research project lead by Michael Kohlhase (see team) with deliverables being the FrameIT paper and the UFrameIT Prototype. See homepage at the Michael Kohlhase's research group: https://kwarc.info/systems/frameit/.

• FrameIT's CICM 2020 paper (short: FrameIT paper): https://link.springer.com/chapter/10.1007/978-3-030-53518-6_11 (up-to-date preprint here). See https://kwarc.github.io/bibs/frameit/ for more academic theses and projects done on FrameIT.

• UFrameIT Prototype (short: UFrameIT): the prototypical system including the UFrameIT Unity Frontend and the UFrameIT MMT Server. Website at https://uframeit.github.io/, installation instructions at https://github.com/UFrameIT/UFrameIT.

• UFrameIT Unity Frontend (short: Unity frontend): the frontend to the UFrameIT Prototype, a Unity project whose code is located at https://github.com/UFrameIT/UFrameIT.

• UFrameIT MMT Server (short: MMT server or frameit-mmt): code located at https://github.com/UniFormal/MMT/tree/devel/src/frameit-mmt

• UFrameIT formalization archives (short: UFrameIT archives): the MMT archives of formalization located at https://github.com/UFrameIT/archives.

Do not autoselect a scroll upon game start

I think it just confuses beginners when a seemingly irrelevant scroll (like MidPoint) is autoselected upon game start.

Increase server's performance

Requests of some type (e.g. /scroll/list) take a really long time upon the first request. Sometimes up to 14 seconds.

• Profile the server and find the bottleneck. (possibly simplification with fullRecursion = true or type checking?)

Replace brittle pushout implementation by better one

Currently, the pushout implementation is ad-hoc and brittle. E.g. if a solution theory includes any theory unrelated to the problem theory, the pushout computation will fail with an exception. This case hasn't occurred yet, but might in the future.

We should best wait for the pushout diagram opreator to be implemented correctly in MMT.

Document list of all used MKM features (for demonstation purposes)

Might grow over time and be nice to have in the future.

Preliminary list:

• scroll applicability checking
• apply scrolls
• preview scroll application
• label + description interpolation/verbalization
• view completion
• scroll error message parsing?

prefab fixing

-resourcefolder ????
-uniform parents for scaling

Decouple FrameIT approach from specific game engines

We have been prototyping and maturing the FrameIT idea in recent months by interfacing the Unity game engine with the MMT system.
We are now at a point where it makes sense to review our implementations and decouple them as much as it makes sense.

In particular verify

• @ComFreek for the MMT server that
  • it has nowhere have a dependence on Unity
  • the code itself (e.g. in variable names) and all documentation material only refers to game engine and not Unity
• @ComFreek for the MMT formalizations that Unity is nowhere mentioned, and at best only game engine is mentioned
• @richardmarcus for the https://uframeit.github.io website that it stresses the independence of the MMT server from the specific choice of game engine

UI freezes when computing pushouts

When I press the magic button, the UI freezes until MMT responds (as visible in the MMT console window). Do we do the network requests synchronously in the main thread?

Unity: show and visualize scroll outputs

The server already communicates the acquiredFacts in the responses to /scroll/{list,listall,dynamic}.

The scroll window in Unity should display the to-be-acquired facts, too. Even better if we could highlight them, too, given the hint feature that has now landed.

New FrameWorld Video

using the FrameIT2.0 Features.

Think about "highlight fact and its dependencies/induced completions"

• MMT side

  • given a tentative scroll application with a list of assignments and one designated assignment, can we get a list of the completions it (co-)induced? ("co-" meaning: possibly some completions are induced by presence of multiple assignments together only)

  • is the set of dependencies a subset of completions?

• Game engine side

Angle-GO has correct direction, but sometimes the wrong orientation around this direction

Implement "view completion" API

The groundwork of algorithms has already been implemented by @Jazzpirate. This just needs to be lightly interfaced with.

Fact-Datastructures

List + Datatypes
Nullspace-management

Implement backwards view completion API

1. User selects scroll
2. They "mark" a fact (tree height) they cannot get but want and assign it to the acquired fact slot of the scroll
3. Run view completion

Describe where to place mmt.jar for archives

https://github.com/UFrameIT/archives/blob/master/archives.iml#L16

Rendered distances should use a point separator for decimal numbers

E.g. currently it says "11,38 m". If the rest of the UI is in English, we should render "11.38 m".

Document format of checking errors from /scroll/dynamic

• awaiting internal confirmation

UFrameIT Content 4.0: Overview Issue

Overall

• What kind of puzzles do we want to have? Geometry/Physics/...?
• What kind of gadgets do we need?

Graphics

• What world do we want to have to embody the puzzles?
• Create/copy that world, assets, ...
• Create gadgets

Logic

• rework content to integratem with MitM ontology.
• Create MMT formalizations for new puzzle types
• Meta theories
• Scrolls

Implement "active document" API for meta datums

• add untyped constant labelOf to theory FrameIT/frameworld@MetaAnnotations
• edit all metadatums in scrolls, e.g. meta ?scrollDescription ... ${labelOf ...?uriOfFactSlotInProblemTheory}
• implement API in the server component render(meta: MetaDatum, scrollApplication: PartialScrollApplication)

Equality Rules

We want to solve the problem that users need the correct ordering of angles and distances without a hack. Two considerations:

a) How to implement this?

b) How much does the player need to be involved (e.g. mark distance as bidirectional?)

Updated Unity -> Server Requests

We need to update the Unity communication to use the new format #21 and #24

Implement "dynamic scroll" API + UX in Unity

I haven't stabilized the communication API yet, but it looks along the lines of:

where the request body is the same as for /scroll/apply (but allowing partial views).

Use a different icon for measured right angles

E.g. in the screenshot below I measured several angles, some of which are right angles.

The UI should visually distinguish measured angle values from measured right angles.

UX for name clashes in dynamic scrolls

E.g. the OppositeLen scroll has the following description

s"Given a triangle ${lverb A B C} and two known angles, we can deduce the missing angle by the sum of interior angles in triangles always being 180°"

With the partial scroll application A := C, B := A (with RHSs stemming from the situation theory) communicated to the server, the dynamic description reads:

Given a triangle CAC right angled at C, the distance CA can be computed from the angle at A and the distance AC

Here, the original C remaining C and looking like the assigned C is confusing. What can we do here?

• simple solution: use 𝔸, 𝔹, and ℂ for point labels in scrolls as to not clash with point labels for points marked by the player.
• complicated and robust solution: communicate some more formatting to the game engine (e.g. italics) and use that

Better UX for filling scrolls

Current situation: drag facts from the right side of the screen to the left into the scroll.

Problem: slow UX, drag over large part of the screen

Potential solutions:

Multipe possibilities:

• interactive filling mode such that one has just to repeatedly click on facts and they get automatically filled into the steadily increasing index position in the scroll.
• reorganize UI such that scrolls are near the fact list
• click on required fact in scroll to get a scroll list of potential facts to be filled in by the user

Play fireworks sound effect upon fireworks effect

We also play sound for rain, so why not for fireworks, too? 😄

View Completion in Unity

Need to implement user dialogue and visual effects for temporary facts to support this feature

Implement "dynamic scroll" API on server

Implement the dynamic scroll API that

• provides typechecking of (partial) scroll applications: already implemented
• provides "active documents"-like labels and descriptions of the scroll and required facts: #26, #30
• provides view completion support (expected type, inferred type): #31 (server component), #22 (game engine)

Merge Scenes

Even loading both seperate scenes has some issues so we will need combine them into a single one

Disambiguate labels between dynamic scroll info and marked points

E.g. the OppositeLen scroll has the following description

s"Given a triangle ${lverb A B C} and two known angles, we can deduce the missing angle by the sum of interior angles in triangles always being 180°"

With the partial scroll application A := C, B := A (with RHSs stemming from the situation theory) communicated to the server, the dynamic description reads:

Given a triangle CAC right angled at C, the distance CA can be computed from the angle at A and the distance AC

Here, the original C remaining C and looking like the assigned C is confusing. What can we do here?

• simple solution: use 𝔸, 𝔹, and ℂ for point labels in scrolls as to not clash with point labels for points marked by the player. This does not scale to any more complex scrolls, say with lines.
• complicated and robust solution: communicate some more formatting to the game engine (e.g. italics) and use that

How to deal with angles in clockwise direction

At the moment we're not distinguishing, if the direction of creating an angle is right. We always draw the angle that's smaller than 180°.
Mathematically correct would it be to draw the angle in counter-clockwise-direction then.
-> If so, we would make it possible to show a linerenderer-preview with angles > 180° and make it possible to create AngleGO's > 180° (with merging to anglesGO's together)

-> Question is if that's important for our Project till end of January/April

Communication Format for Virtual World Updates

We want a simple format to transmit updates to the virtual world (e.g. new facts: point, angle, etc) to MMT.
@Jazzpirate and @ComFreek should design the format.
It should be a JSON file but encode the information like this
OMS(p : URI)
Real(3.14159)
Point(3.1,2.8,0.3)
OMA(f,a1,...,an)
NewPoint(name,Point(...))
NewReal(name,Real(...))
NewFact(name,LeftSide,RightSide)
LeftSide ::= OMS | OMA
RightSide ::= Real | Point
name : |- \doteq
or maybe like this: https://gl.kwarc.info/FrameIT/blue/-/blob/master/interchange-language.md

To implement the requests on the Unity side, @richardmarcus and @SESch93 would like to know how the requests for the tree example should look in this format.

The following events are possible:

• point (coordinate)
• line (id1, id2)
• angle(id1, id2, id3)

We currently do not allow creation of lines or angles without creating points first.

Rethink scroll representation in Problem/Solution Theory

We think we should improve the meta scroll* part.
The current situation, where the meta annotations are on the problem theory are not ideal; since they include information about the solution theory. As Solution includes Problem, the annotation would be better on that. In particular, then a problem theory can be used in multiple scrolls.

BUT that is still not ideal, since we cannot have multiple scrolls per solution theory. Think different verbalizations for different audiences.

Let's be radical: I think a scroll should be an informal statement (in what theory?) or even an informal theory or maybe even an informal view, once we have them. cc: @Jazzpirate

Scroll assignment communication

After changing the way we send facts to MMT we also need to investigate how the server currently handles scroll assignments and how it should be solved in combination with the new format

Reflect "active document" server API in communication to game engine

update frameworld-1 to UFrameIt-R2

When we have the release, we want to update the game as well.

Add license

The paper currently claimed the license being MIT for the old FrameIT project. What license do we have here? Can we just choose one independent of the assets we copied from the Unity store?

script-architecture

split bloated scripts

Server: only selectively definition-expand things when sending facts to game engine

Currently, the server simplifies (incl. fully definition-expands) all scroll and situation theory declarations before sending them to the game engine.

I will explain why this is partially needed next. Consider the following "solution declaration" from the solution theory of the OppositeLen scroll:

deducedLineCA
            : Σ x:ℝ . ⊦ (d- C A) ≐ x ❘
            = ⟨(tan (πl angleB)) ⋅ (πl distanceBC), sketch "OppositeLen Scroll"⟩ ❘

After a successful scroll application, we push this out to the situation theory. Then, when we wish to communicate that pushed out declaration, of course, we want to first simplify the whole subexpression there (with tan) to a numeric value.

However, full definition-expanding is very inefficient and greatly affects performance. When caching the mapping FinalConstant in theory |-> SFact object sent to game engine, the performance hit is at least only noticeable upon cache misses (usually, in the first request).

Still, we should be smarter when definition-expanding. The MMT API offers Lookup.ExpandDefinition which only selectively definition-expands things.

What to do with name clashes with fact constants?

• If the game engine communicates a new fact, how should we name the constant in the situation theory?
• If we apply a scroll, how should we name the pushout-generated constants? Should we just keep the names? But what if a user applies a scroll twice? Should we do string interpolation in the labels? I think so!

Restarting game does not reset everything

1. Solve the tree height puzzle
2. Restart the game by pressing the restart button
3. Talk to the NPC
4. They still shout "Yay, you did it!" (even though the fact inventory is of course empty now)

Full-screen mode only renders 4:3, not 16:9 (black bars at left and right edge)

FrameIT vs. FrameIt in application and Meta INF --> reconcile

in MathHub/FrameIT/frameworld/MetaINF/MANIFEST.MF we find *FrameIt* which is very bad (for MMT and IntelliJ)
BUT the wrong string seems hardcoded into the frameworld game application (when Dennis changed it, it was pushed back)

This needs to be reconciled. I will refrain from just changing it for the moment.

How to visualize scrolls in-game (SVG/MathML/...)?

Problem: We'd like to visualize scrolls in-game, e.g. for the tree height problem in FrameWorld-1, we would like to show a triangle with named endpoints besides the scroll description. Then, if the player fills input slots, the scroll visualization should be updated as well:

(The scrawl should denote the textual description.)

Solutions:

• render HTML + JS

  • super flexible wrt. interpolation of scroll assignments
  • unsure whether there is a nice Unity way of doing this with an external engine (Awesomium might be working!)

• render SVG

  • Unity's SVG renderer cannot even render <text> elements, so unsure whether we can use this easily
  • @richardmarcus said it can process MathML, though!

• other ideas?

In any case, I envision the scroll annotations existing in the MMT formalizations to be extended with one more meta entry: a string of the scroll visualization or a path to a file containing it (i.e. containing HTML or SVG with interpolation variables).

Allow dragging of facts from one input slot to another

Support for reusable and complex verbalizations

E.g. we have

midpoint
    : point ❘
    = ⟨0.5 ⋅ (P_x + Q_x), 0.5 ⋅ (P_x + Q_x), 0.5 ⋅ (P_x + Q_x)⟩ ❘
    meta ?MetaAnnotations?label s"Mid[${lverb P Q}]" ❘

here, ${lverb P Q} is neither DRY or reusable: it has to be typed every time. Hence, let's support reusable verbalization snippets for complex expressions like line P Q that can be used as in ${lverb (line P Q)}.

Research questions:

• Where do the verbalizations go? E.g. do verbalizations for complex terms c t_1 ... t_n (where c is a constant reference) go into the meta data for c?
• But line is declared in the MitM archive — hence we definitely look for a general and reusable solution.
• Can we special case on some terms, e.g. can angle A B C for A, B, C on a 2D plane get a special verbalization?