Coder Social home page Coder Social logo

uframeit / uframeit Goto Github PK

View Code? Open in Web Editor NEW
10.0 6.0 3.0 473.43 MB

The current Unity-based implementation of the FrameIT approach

Home Page: https://uframeit.org

License: GNU General Public License v3.0

C# 17.39% ShaderLab 2.51% HLSL 0.28% HTML 74.07% CSS 0.65% Shell 0.02% Batchfile 0.03% JavaScript 5.05%
educational-game unity logic mathematical-knowledge-management research-project

uframeit's Introduction

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
  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

Useful Links for new Developers

UFrameIT Unity Plugin

FrameIT Server

Formalized Knowledge

uframeit's People

Contributors

bboesl avatar comfreek avatar dependabot[bot] avatar fastrich avatar kohlhase avatar mazifau avatar richardmarcus avatar sesch93 avatar t-schoener avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar

uframeit's Issues

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.

Merge Scenes

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

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

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.

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

prefab fixing

-resourcefolder ????
-uniform parents for scaling

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:

image

(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).

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.

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)

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)

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?)

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)

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

feel free to edit this post


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.

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?

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?

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!

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

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?

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.

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?)

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

View Completion in Unity

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

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

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.

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

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

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

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

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?

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.