uframeit / uframeit Goto Github PK
View Code? Open in Web Editor NEWThe current Unity-based implementation of the FrameIT approach
Home Page: https://uframeit.org
License: GNU General Public License v3.0
The current Unity-based implementation of the FrameIT approach
Home Page: https://uframeit.org
License: GNU General Public License v3.0
Overall
Graphics
Logic
Need to implement user dialogue and visual effects for temporary facts to support this feature
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
List + Datatypes
Nullspace-management
split bloated scripts
Might grow over time and be nice to have in the future.
Preliminary list:
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:
We currently do not allow creation of lines or angles without creating points first.
The groundwork of algorithms has already been implemented by @Jazzpirate. This just needs to be lightly interfaced with.
labelOf
to theory FrameIT/frameworld@MetaAnnotations
meta ?scrollDescription ... ${labelOf ...?uriOfFactSlotInProblemTheory}
render(meta: MetaDatum, scrollApplication: PartialScrollApplication)
E.g. currently it says "11,38 m". If the rest of the UI is in English, we should render "11.38 m".
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.
Even loading both seperate scenes has some issues so we will need combine them into a single one
Requests of some type (e.g. /scroll/list) take a really long time upon the first request. Sometimes up to 14 seconds.
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?
-resourcefolder ????
-uniform parents for scaling
Current style of formalization:
angle : Σ α: ℝ. ⊦ ( ∠ A,B,C ) ≐ α
.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.
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
render SVG
<text>
elements, so unsure whether we can use this easilyother 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).
I think it just confuses beginners when a seemingly irrelevant scroll (like MidPoint) is autoselected upon game start.
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:
c t_1 ... t_n
(where c
is a constant reference) go into the meta data for c
?line
is declared in the MitM archive — hence we definitely look for a general and reusable solution.angle A B C
for A
, B
, C
on a 2D plane get a special verbalization?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?
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.
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.
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
Implement the dynamic scroll API that
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?
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
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?)
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?
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:
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
We also play sound for rain, so why not for fireworks, too? 😄
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.
When we have the release, we want to update the game as well.
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
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?
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.
using the FrameIT2.0 Features.
Not critical, will only eventually lead to typechecking reporting warnings. So lest I forget, I document this here.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.