metamath GUI/Game in Smalltalk

141 views
Skip to first unread message

Peter Meadows

unread,
Jun 25, 2022, 11:35:42 AM6/25/22
to Metamath

Jim Kingdon

unread,
Jun 25, 2022, 7:06:03 PM6/25/22
to 'Peter Meadows' via Metamath
Looks cool based on the screenshot and video.

Given how popular colorful syntax highlighting has been for code, seems like there could well be an appeal to do something sort of similar in terms of the display here.

On June 25, 2022 1:58:32 AM PDT, 'Peter Meadows' via Metamath <meta...@googlegroups.com> wrote:
https://github.com/Peter-H-Meadows/GtMetamath

Thoughts?

Peter H. Meadows

unread,
Jul 27, 2022, 10:15:38 AM7/27/22
to meta...@googlegroups.com
On Sun, 26 Jun 2022 at 00:06, Jim Kingdon <kin...@panix.com> wrote:
>
> Looks cool based on the screenshot and video.
>
> Given how popular colorful syntax highlighting has been for code, seems like there could well be an appeal to do something sort of similar in terms of the display here.
>

Thanks for the feedback.

My goal is to make the game as simple, and fun as possible.

Any ideas about how to make it fun for kids?

How best to explain/introduce the rules?
( Maybe say it's a factory that uses machines to make/convert raw
input into the result? modus ponens = detacher machine. etc.?
I'm thinking how 'manufactoria' games do it.
http://pleasingfungus.com/Manufactoria2022/ )

Jon P

unread,
Jul 27, 2022, 3:15:59 PM7/27/22
to Metamath
Looks like a fun thing you're making. 

I've done a little game design and here's a couple of thoughts. I made this game about the four colour theorem on steam (if anyone would like to play feel free to email for a steam key). 

One of the things I thought went best is that it doesn't have a tutorial, it's just a super slow ramp of complexity, each new idea is introduced with a couple of chances to play around with it before the next one. I'd really recommend an approach like that, especially if it's for kids, the hardest thing is walls of text, generally people learn easier by playing than reading. 


And then yeah another suggestion might be some sort of power connectors game? Like when you're doing a proof in MMJ2 you're trying to make sure every statement is connected to the rest. So you're hypotheses are sort of like your power sources and the theorem is like the lightbulb or something and what you're trying to do is make a complete chain in-between with no loose ends.

I really like the sound of what you're saying with factories etc, maybe little roads / power cables / conveyor belts / water pipes might communicate that idea of connections pretty well.

Cris Perdue

unread,
Jul 27, 2022, 8:47:48 PM7/27/22
to meta...@googlegroups.com
Not working so well for me.

I downloaded the M1 Mac version of Glamorous Toolkit, opened the Zip file, ran the app,
opened a playground, pasted in the code in the README, and pressed the "eval" button.

The result was an error, "Instance of GtPharoSourceCoderEvaluationContext did not understand #isForScripting".

Is there perhaps a problem with the M1 Mac version of GT, or perhaps something else?

Thanks,
Cris

On Sat, Jun 25, 2022 at 8:35 AM 'Peter Meadows' via Metamath <meta...@googlegroups.com> wrote:
https://github.com/Peter-H-Meadows/GtMetamath

Thoughts?

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/0249cd93-d4ec-486f-afa3-686f2380d34cn%40googlegroups.com.

Peter H. Meadows

unread,
Jul 28, 2022, 3:29:33 PM7/28/22
to meta...@googlegroups.com
On Thu, 28 Jul 2022 at 01:47, Cris Perdue <cr...@perdues.com> wrote:
>
> Not working so well for me.
>
> I downloaded the M1 Mac version of Glamorous Toolkit, opened the Zip file, ran the app,
> opened a playground, pasted in the code in the README, and pressed the "eval" button.
>
> The result was an error, "Instance of GtPharoSourceCoderEvaluationContext did not understand #isForScripting".
>
> Is there perhaps a problem with the M1 Mac version of GT, or perhaps something else?
>

Thanks for testing!

I haven't tried it on a Mac before, but it should work.

Does GT work fine before you tried to load the GtMetamath code?

Can you send me the full error? (you can just press the copy button in
the debugger and paste it here).

Thanks

Mo Ti

unread,
Jul 28, 2022, 3:29:47 PM7/28/22
to meta...@googlegroups.com
Its not working for me either. Windows 10. Did the same as Cris Perdue

Cris Perdue

unread,
Jul 28, 2022, 5:35:17 PM7/28/22
to meta...@googlegroups.com
The full error from Glamorous Toolkit. TL;DR:

GtPharoSourceCoderEvaluationContext(Object)>>doesNotUnderstand: #isForScripting
OCUndeclaredVariableWarning>>openMenuIn:
OCUndeclaredVariableWarning(OCSemanticWarning)>>defaultAction
OCUndeclaredVariableWarning>>defaultAction
UndefinedObject>>handleSignal:
Context>>handleSignal:
OCUndeclaredVariableWarning(Exception)>>pass
[ :anException |
"it is very important that the monitor is not locked when an exception happens"
monitor exit.
"after an #exit call the monitor is open for another process, so if users start to compile code
from within the debugger. If debugger code compilation is not wrapped in this critical block,
there might be a problem of code modification from multiple processes. The chance of this, however, is very slim."
anException pass ] in [
aBlock
on: Exception
do: [ :anException |
"it is very important that the monitor is not locked when an exception happens"
monitor exit.
"after an #exit call the monitor is open for another process, so if users start to compile code
from within the debugger. If debugger code compilation is not wrapped in this critical block,
there might be a problem of code modification from multiple processes. The chance of this, however, is very slim."
anException pass ] ] in GtPharoCodeModifier>>critical: in Block: [ :anException |...
FullBlockClosure(BlockClosure)>>cull:
Context>>evaluateSignal:
Context>>handleSignal:
Context>>handleSignal:
Context>>handleSignal:
OCUndeclaredVariableWarning(Exception)>>signal
OCASTSemanticAnalyzer>>undeclaredVariable:
OCASTSemanticAnalyzer>>resolveVariableNode:
OCASTSemanticAnalyzer>>visitVariableNode:
UnresolvedVariable(Variable)>>acceptVisitor:node:
RBVariableNode>>acceptVisitor:
OCASTSemanticAnalyzer(RBProgramNodeVisitor)>>visitNode:
OCASTSemanticAnalyzer(RBProgramNodeVisitor)>>visitMessageNode:
RBMessageNode>>acceptVisitor:
OCASTSemanticAnalyzer(RBProgramNodeVisitor)>>visitNode:
OCASTSemanticAnalyzer(RBProgramNodeVisitor)>>visitReturnNode:
RBReturnNode>>acceptVisitor:
OCASTSemanticAnalyzer(RBProgramNodeVisitor)>>visitNode:
[ :each | self visitNode: each ] in OCASTSemanticAnalyzer>>visitSequenceNode: in Block: [ :each | self visitNode: each ]
OrderedCollection>>do:
OCASTSemanticAnalyzer>>visitSequenceNode:
RBSequenceNode>>acceptVisitor:
OCASTSemanticAnalyzer(RBProgramNodeVisitor)>>visitNode:
OCASTSemanticAnalyzer>>visitMethodNode:
RBMethodNode>>acceptVisitor:
OCASTSemanticAnalyzer(RBProgramNodeVisitor)>>visitNode:
OCASTSemanticAnalyzer>>analyze:
RBMethodNode>>doSemanticAnalysis
[ast doSemanticAnalysis] in OpalCompiler>>doSemanticAnalysis in Block: [ast doSemanticAnalysis]
FullBlockClosure(BlockClosure)>>on:do:
OpalCompiler>>doSemanticAnalysis
OpalCompiler>>transformDoit
OpalCompiler>>parseDoIt
OpalCompiler>>compileDoit
[compilationContext noPattern
ifTrue: [ self compileDoit ]
ifFalse: [ self compileMethod ]] in OpalCompiler>>compile in Block: [compilationContext noPattern ...
FullBlockClosure(BlockClosure)>>on:do:
OpalCompiler>>compile
[
self class compiler
source: aSourceString;
class: methodClass newAnonymousSubclass;
context: aGtPharoSourceCoderEvaluationContext runtimeContext;
requestor: aGtPharoSourceCoderEvaluationContext;
noPattern: isForMethod not;
failBlock: anEvaluationFailBlock;
compile ] in GtPharoSnippetCoder(GtPharoSourceCoder)>>primitiveAnonymousCompile:inContext:onFailDo: in Block: [...
FullBlockClosure(BlockClosure)>>on:do:
[
aBlock
on: Exception
do: [ :anException |
"it is very important that the monitor is not locked when an exception happens"
monitor exit.
"after an #exit call the monitor is open for another process, so if users start to compile code
from within the debugger. If debugger code compilation is not wrapped in this critical block,
there might be a problem of code modification from multiple processes. The chance of this, however, is very slim."
anException pass ] ] in GtPharoCodeModifier>>critical: in Block: [...
[
self enter.
aBlock value] in Monitor>>critical: in Block: [...
FullBlockClosure(BlockClosure)>>ensure:
Monitor>>critical:
GtPharoCodeModifier>>critical:
GtPharoSnippetCoder(GtPharoSourceCoder)>>primitiveAnonymousCompile:inContext:onFailDo:
GtPharoSnippetCoder(GtPharoSourceCoder)>>primitiveEvaluate:inContext:onFailDo:
[
self
primitiveEvaluate: aDecoratedSourceString
inContext: aSourceCoderEvaluationContext
onFailDo: [
| aResultWithSyntaxError |

aResultWithSyntaxError := GtSourceCoderEvaluationResultWithSyntaxError new
evaluationContext: aSourceCoderEvaluationContext.
aThenBlock cull: aResultWithSyntaxError.
^ aResultWithSyntaxError ] ] in GtPharoSnippetCoder(GtSourceCoder)>>evaluate:decorated:inContext:thenDo: in Block: [ ...
FullBlockClosure(BlockClosure)>>on:do:
GtPharoSnippetCoder(GtSourceCoder)>>evaluateBlock:onErrorDo:
GtPharoSnippetCoder(GtSourceCoder)>>evaluate:decorated:inContext:thenDo:
GtPharoSnippetCoder(GtSourceCoder)>>evaluate:inContext:thenDo:
GtPharoSnippetCoder(GtSourceCoder)>>doItInContext:thenDo:
GtPharoSnippetCoder(GtSourceCoder)>>doItInContext:
GtPharoSnippetCoderViewModel(GtSourceCoderViewModel)>>doItAllRequestedBy:
GtPharoSnippetCoderViewModel(GtSourceCoderViewModel)>>doItRequestedBy:
GtPharoSnippetCoderViewModel(GtSourceCoderViewModel)>>doIt
[ self coderViewModel perform: action ] in GtCoderCodeExecutor>>execute in Block: [ self coderViewModel perform: action ]
[ activeProcess
psValueAt: index
put: anObject.
aBlock value ] in GtCoderExecutionContextVariable(DynamicVariable)>>value:during: in Block: [ activeProcess...
FullBlockClosure(BlockClosure)>>ensure:
GtCoderExecutionContextVariable(DynamicVariable)>>value:during:
GtCoderExecutionContextVariable class(DynamicVariable class)>>value:during:
GtCoderExecutionContextVariable class>>element:do:
GtCoderCodeExecutor>>execute
[ :aCoderUIModel :anElement |
GtCoderCodeExecutor doIt
coderViewModel: aCoderUIModel;
element: anElement;
execute ] in GtPharoSnippetCoder>>initializeAddOns: in Block: [ :aCoderUIModel :anElement | ...
FullBlockClosure(BlockClosure)>>gtValueWithArgs:
[ aGtCoderAction action
gtValueWithArgs:
{self textualCoderViewModel.
aButtonElement} ] in [ [ aGtCoderAction action
gtValueWithArgs:
{self textualCoderViewModel.
aButtonElement} ]
ensure: [ self enqueueEnableButton: aButtonElement action: aGtCoderAction ] ] in [ aButtonElement
enqueueTask:
(BlTaskAction new
action: [ [ aGtCoderAction action
gtValueWithArgs:
{self textualCoderViewModel.
aButtonElement} ]
ensure: [ self enqueueEnableButton: aButtonElement action: aGtCoderAction ] ]) ] in GtCoderActionsElement>>handleButton:action:onEvent: in Block: [ aGtCoderAction action...
FullBlockClosure(BlockClosure)>>ensure:
[ [ aGtCoderAction action
gtValueWithArgs:
{self textualCoderViewModel.
aButtonElement} ]
ensure: [ self enqueueEnableButton: aButtonElement action: aGtCoderAction ] ] in [ aButtonElement
enqueueTask:
(BlTaskAction new
action: [ [ aGtCoderAction action
gtValueWithArgs:
{self textualCoderViewModel.
aButtonElement} ]
ensure: [ self enqueueEnableButton: aButtonElement action: aGtCoderAction ] ]) ] in GtCoderActionsElement>>handleButton:action:onEvent: in Block: [ [ aGtCoderAction action...
FullBlockClosure(BlockClosure)>>cull:
BlTaskAction>>run:
[ aTask run: aWaker ] in [ BlTaskExecutionSignal for: aTask block: [ aTask run: aWaker ] ] in [ :aTask |
aTask setExecuting.

BlFrameTelemetry
timeSync: [ 'Run task {1} ({2})' format: { aTask class name . aTask } ]
during: [ BlTaskExecutionSignal for: aTask block: [ aTask run: aWaker ] ].
self onTaskExecuted: aTask.

aTask requeueTaskAfterExecution
ifTrue: [ self privateRequeueRepeating: aTask ]
ifFalse: [
tasks
lock: [ :theSpaceTasks |
(theSpaceTasks hasPendingTask: aTask)
ifFalse: [ aTask setComplete ] ]
ifNilPut: [ self newTasks ] ] ] in BlSpaceTaskQueue>>runOn: in Block: [ aTask run: aWaker ]
BlTaskExecutionSignal class>>for:block:
[ BlTaskExecutionSignal for: aTask block: [ aTask run: aWaker ] ] in [ :aTask |
aTask setExecuting.

BlFrameTelemetry
timeSync: [ 'Run task {1} ({2})' format: { aTask class name . aTask } ]
during: [ BlTaskExecutionSignal for: aTask block: [ aTask run: aWaker ] ].
self onTaskExecuted: aTask.

aTask requeueTaskAfterExecution
ifTrue: [ self privateRequeueRepeating: aTask ]
ifFalse: [
tasks
lock: [ :theSpaceTasks |
(theSpaceTasks hasPendingTask: aTask)
ifFalse: [ aTask setComplete ] ]
ifNilPut: [ self newTasks ] ] ] in BlSpaceTaskQueue>>runOn: in Block: [ BlTaskExecutionSignal for: aTask block: [ aTask ...etc...
NullTelemetry>>time:during:
BlSpaceTelemetry>>time:during:
BlFrameTelemetry(BaseProcessTelemetry)>>time:during:
BlFrameTelemetry(BaseProcessTelemetry)>>timeSync:during:
BlFrameTelemetry class(BaseProcessTelemetry class)>>timeSync:during:
[ :aTask |
aTask setExecuting.

BlFrameTelemetry
timeSync: [ 'Run task {1} ({2})' format: { aTask class name . aTask } ]
during: [ BlTaskExecutionSignal for: aTask block: [ aTask run: aWaker ] ].
self onTaskExecuted: aTask.

aTask requeueTaskAfterExecution
ifTrue: [ self privateRequeueRepeating: aTask ]
ifFalse: [
tasks
lock: [ :theSpaceTasks |
(theSpaceTasks hasPendingTask: aTask)
ifFalse: [ aTask setComplete ] ]
ifNilPut: [ self newTasks ] ] ] in BlSpaceTaskQueue>>runOn: in Block: [ :aTask |...
Array(SequenceableCollection)>>do:
BlSpaceTaskQueue>>runOn:
GtWorld(BlSpace)>>runTasks
[ :theSpace | theSpace runTasks ] in BlSpaceFrameTaskPhase>>runOn: in Block: [ :theSpace | theSpace runTasks ]
FullBlockClosure(BlockClosure)>>cull:
GtWorld(BlSpace)>>dispatchTimeEvent:during:
BlSpaceFrameTaskPhase>>runOn:
[ self currentPhase runOn: aSpace ] in BlSpaceFrame>>runCurrentPhaseOn: in Block: [ self currentPhase runOn: aSpace ]
NullTelemetry>>time:during:
BlSpaceTelemetry>>time:during:
BlFrameTelemetry(BaseProcessTelemetry)>>time:during:
BlFrameTelemetry class(BaseProcessTelemetry class)>>time:during:
BlSpaceFrame>>runCurrentPhaseOn:



--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

Peter H. Meadows

unread,
Aug 20, 2022, 8:10:42 PM8/20/22
to meta...@googlegroups.com
On Wed, 27 Jul 2022 at 20:16, Jon P <drjonp...@gmail.com> wrote:
>
> Looks like a fun thing you're making.

I think fun is key to learning! :)
(I'm sad that most schools seem to make learning mathematics boring).
"School is like going to the best restaurant in town and then being
told to eat the menu instead of the food."

>
> I've done a little game design and here's a couple of thoughts. I made this game about the four colour theorem on steam (if anyone would like to play feel free to email for a steam key).
>

Cool. I'm interested to study how my 8 year old nephew learns, so I'll
use your game as one of the tests :)

> One of the things I thought went best is that it doesn't have a tutorial, it's just a super slow ramp of complexity, each new idea is introduced with a couple of chances to play around with it before the next one. I'd really recommend an approach like that, especially if it's for kids, the hardest thing is walls of text, generally people learn easier by playing than reading.

Yep! Here is a video of the first few proofs/levels in GtMetamath.
https://youtu.be/TT5F75SK4gQ

Any feedback/thoughts?

weird words:

deduction, elimination, transposes, inference, implies, hypotheses,
assertion, antecedent, consequent, contraposition, axiom

ph implies ps = red blob links to blue blob
essential hypothesis = required input for transformer machine. and
given starting chains.
antecedent = thing at start (left-most)
consequent = thing at end (right-most)
modus ponens = detacher machine.
a1i = add-to-front machine.
syl = distributer machine.

Cheers




>
> https://store.steampowered.com/app/816770/The_Four_Colour_Theorem/
>
> And then yeah another suggestion might be some sort of power connectors game? Like when you're doing a proof in MMJ2 you're trying to make sure every statement is connected to the rest. So you're hypotheses are sort of like your power sources and the theorem is like the lightbulb or something and what you're trying to do is make a complete chain in-between with no loose ends.
>
> I really like the sound of what you're saying with factories etc, maybe little roads / power cables / conveyor belts / water pipes might communicate that idea of connections pretty well.
>
> On Wednesday, July 27, 2022 at 3:15:38 PM UTC+1 peter.h...@googlemail.com wrote:
>>
>> On Sun, 26 Jun 2022 at 00:06, Jim Kingdon <kin...@panix.com> wrote:
>> >
>> > Looks cool based on the screenshot and video.
>> >
>> > Given how popular colorful syntax highlighting has been for code, seems like there could well be an appeal to do something sort of similar in terms of the display here.
>> >
>>
>> Thanks for the feedback.
>>
>> My goal is to make the game as simple, and fun as possible.
>>
>> Any ideas about how to make it fun for kids?
>>
>> How best to explain/introduce the rules?
>> ( Maybe say it's a factory that uses machines to make/convert raw
>> input into the result? modus ponens = detacher machine. etc.?
>> I'm thinking how 'manufactoria' games do it.
>> http://pleasingfungus.com/Manufactoria2022/ )
>
> --
> You received this message because you are subscribed to a topic in the Google Groups "Metamath" group.
> To unsubscribe from this topic, visit https://groups.google.com/d/topic/metamath/sf5Ma5_NIlU/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to metamath+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c3fc0fda-0b18-4d72-8949-5f8a9b5e146fn%40googlegroups.com.

Peter Meadows

unread,
Aug 21, 2022, 12:33:07 PM8/21/22
to Metamath

The full error from Glamorous Toolkit. TL;DR:

thx. it might work now

Jon P

unread,
Aug 28, 2022, 7:00:18 AM8/28/22
to Metamath
That is really cool, yeah I really like the progress you've made on it.

I think it's great how clear and simple it all is just with the basic shapes. I also like how much reward there is in it with it going green and saying "well done" etc, that's very nice. I think giving lots of encouragement/stars/badges really helps.

A couple of thoughts:

Firstly it kind of looks like the squares are kind of items and the triangles are slots/boxes/containers where you can put the items. So I wonder if it might make sense to make that connection more obvious? Like rather than a triangle have a square which has a border and nothing in the middle, and that way it makes it clear you put a square in there.

Secondly, I don't know exactly how this would work logically, but yeah it might be nice if the first level is just 1 square and 1 slot and all you do is drag the square into the slot, that makes it super simple as a first step for people to understand what to do. Then maybe a nice second level is to have a more complex expression on the left to be dragged into a more complex set of connected slots on the right, that way it teaches you that you can drag larger objects.

Thirdly I think you currently have squares on the left, the goal in the middle and the triangle connectors on the right. Would it make more sense to have the triangle connectors in the middle and the goal on the right? That way it kind of reads left to right as "inputs" -> "transformers" -> "goal". Maybe that is less good if the screen ends up cluttered, the connectors could be along the bottom maybe?

Fourthly it reminded me of this game https://www.zachtronics.com/opus-magnum/ which has a similar vibe of taking the little orbs and using machines to combine them into larger objects. Could be a nice place to look for inspiration and graphics.

Not sure if any of that is useful, obviously feel free to ignore any or all of it. Overall I'd just like to be really encouraging! I think it's a really cool idea and I think you're close to having something really powerful.

Antony Bartlett

unread,
Aug 28, 2022, 3:44:11 PM8/28/22
to meta...@googlegroups.com
Hi Peter,

I'm afraid I seem to be unable to run GtMetamath on my crappy old Windows laptop.  When I follow the instructions on your README.md, the GtMetamath window as shown in your screenshots comes up and is the correct blackish background color, but I'm afraid it stays completely and stubbornly blank with no obvious error message.

    Best regards,

        Antony

You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/788b627d-2714-45a8-a1e9-7a129284d7edn%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages