phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
525 Commits 19 Branches 10 Tags
620cf0597ee2ce3f6c45dd95402fb0446b7648eb
Commit Graph
100 Commits
This Branch
This Branch
All Branches
Author SHA1 Message Date
Alexander Bentkamp 620cf0597e add path for local game 2023-06-13 11:44:09 +02:00
Alexander Bentkamp 9354724327 node_modules regex does not seem to work on windows 2023-06-07 09:40:21 +02:00
Alexander Bentkamp aece2b5645 use cross-env to make npm scripts work on windows 2023-06-06 13:08:09 +02:00
Alexander Bentkamp 839910a408 running games locally documentation 2023-06-06 10:59:58 +02:00
Alexander Bentkamp 2402c2a515 add forward to keep old address alive 2023-05-25 11:47:38 +02:00
Alexander Bentkamp fddbcb5548 unzip 2023-05-15 17:47:47 +02:00
Alexander Bentkamp 46de9fcb77 unzip -o 2023-05-15 17:02:03 +02:00
Alexander Bentkamp e17616b73d add __dirname def 2023-05-15 16:45:17 +02:00
Alexander Bentkamp ca2c3d001f use __dirname 2023-05-15 16:40:37 +02:00
Alexander Bentkamp d6f50fc51a use bash script for unpacking during import 2023-05-15 16:22:23 +02:00
Alexander Bentkamp e30eee92ed latest required in manifest.json 2023-05-15 13:00:02 +02:00
Alexander Bentkamp ef8815f306 use only lower case docker image names 2023-05-15 12:47:26 +02:00
Alexander Bentkamp 6cda39a778 wait 3s until artifacts are available 2023-05-11 09:37:20 +02:00
Alexander Bentkamp e9a434e26c remove landing page html file 2023-05-10 15:50:22 +02:00
Alexander Bentkamp 9ba5acef4d support arbitrary docker containers as games 2023-05-10 11:44:25 +02:00
Alexander Bentkamp 161c88d58f delete temporary files after import 2023-05-09 13:44:19 +02:00
Alexander Bentkamp cf5783f2e4 remove alternative import 2023-05-09 12:19:06 +02:00
Alexander Bentkamp 035a66c930 more import 2023-05-09 12:17:53 +02:00
Alexander Bentkamp 76ce856082 import experimentation 2023-05-09 12:17:53 +02:00
Alexander Bentkamp 9514e558ad fix build.sh for real 2023-05-05 14:42:49 +02:00
Alexander Bentkamp b222cff665 fix build.sh 2023-05-05 14:33:55 +02:00
Alexander Bentkamp 105dd39f12 update build script 2023-05-05 14:11:33 +02:00
Alexander Bentkamp eaf0d13c2f make game directory more configurable 2023-05-04 11:48:32 +02:00
Alexander Bentkamp bbe38ddc7c rename testgame to adam, part 2 2023-03-23 17:10:44 +01:00
Alexander Bentkamp 5c73d3bddb rename testgame to adam 2023-03-23 17:10:13 +01:00
Alexander Bentkamp cbc9576f98 add support for multiple games in redux state 2023-03-23 16:23:06 +01:00
Alexander Bentkamp dac15d84b5 add build mechanism for nng 2023-03-23 16:23:06 +01:00
Alexander Bentkamp 7992cffa26 add minimal NNG dummy 2023-03-23 16:23:06 +01:00
Alexander Bentkamp bf2315b474 remove references to testgame on the server, add gameId to router 2023-03-23 16:23:06 +01:00
Alexander Bentkamp a4d1130487 refine_struct 2023-03-21 11:01:36 +01:00
Alexander Bentkamp b0d9816ce6 simpler solution to remove indented lines 2023-03-15 17:41:52 +01:00
Alexander Bentkamp 86302522a5 add atomic to fix interpolatedStr issue 2023-03-15 17:02:43 +01:00
Alexander Bentkamp f2eed5fc0c repair command line 2023-03-15 16:55:50 +01:00
Alexander Bentkamp 07ec94b7c2 fix strinterpolation again 2023-03-15 12:32:19 +01:00
Alexander Bentkamp 18f16bfe1c disabled applies only to current level 
Fixes #48
 2023-03-13 13:53:31 +01:00
Alexander Bentkamp a876b71d85 fix strinterpolation 2023-03-13 12:24:05 +01:00
Alexander Bentkamp 66f506c5b2 more elegant this way 2023-03-10 16:37:04 +01:00
Alexander Bentkamp 481f2b5cbb refactor level code 2023-03-10 16:20:02 +01:00
Alexander Bentkamp 35eb6c3ec0 refactor LevelAppBar 2023-03-10 16:11:11 +01:00
Alexander Bentkamp 5dfa7b56ec doc panel 2023-03-10 15:48:22 +01:00
Alexander Bentkamp 07b5c22dda allow initial white space in hints 2023-03-10 15:30:38 +01:00
Alexander Bentkamp 27532a7688 fix errors during merge 2023-03-10 10:14:51 +01:00
Alexander Bentkamp c8c85195d7 Branch 2023-03-10 10:11:36 +01:00
Alexander Bentkamp b3a38ee080 strict and hidden options 2023-03-10 10:11:36 +01:00
Alexander Bentkamp 625e224d1e hide internal Hint log messages 2023-03-10 10:11:36 +01:00
Alexander Bentkamp b0d3da99bc reimplement matchDecls 2023-03-10 10:11:36 +01:00
Alexander Bentkamp 1d7facd8dd use fvars instead of mvars for hints 2023-03-10 10:11:36 +01:00
Alexander Bentkamp f540b63764 test example 2023-03-10 10:10:55 +01:00
Alexander Bentkamp 97fd51686f basic inline hints 2023-03-10 10:09:26 +01:00
Alexander Bentkamp 3f39db59ab Update NOTES.md 2023-03-08 10:13:58 +01:00
Alexander Bentkamp d71f43b854 hide hidden hints again when goal changes 2023-03-07 09:25:57 +01:00
Alexander Bentkamp 1c3fa815da fix bug: level completed on reload 2023-03-07 08:59:48 +01:00
Alexander Bentkamp a01212e3ca Merge branch 'story' 2023-03-06 12:38:32 +01:00
Alexander Bentkamp 874999ed34 show summary permanently 2023-03-06 10:19:45 +01:00
Alexander Bentkamp 1c7169d34a show buttons on level completion 2023-03-06 10:17:41 +01:00
Alexander Bentkamp c35b66a0c6 use hints for initial texts 2023-03-06 10:04:40 +01:00
Alexander Bentkamp 4158283eb3 Merge branch 'main' into story 2023-03-06 09:55:57 +01:00
Alexander Bentkamp e8b6770bab display level conclusion 2023-03-06 09:55:39 +01:00
Alexander Bentkamp 2d96279203 make it compile 2023-03-06 09:46:22 +01:00
Alexander Bentkamp 5af93f0a2a Improve texts 2023-03-03 17:00:05 +01:00
Alexander Bentkamp a42841ba97 small css issues 2023-03-03 16:48:56 +01:00
Alexander Bentkamp e6c481a9a4 a few examples of the new feature 2023-03-03 16:36:13 +01:00
Alexander Bentkamp ff0adf12c8 fix metavariable issue 2023-03-03 16:30:25 +01:00
Alexander Bentkamp 86f3e07b27 fix escaping issue 2023-03-03 15:58:17 +01:00
Alexander Bentkamp 3cbb4774f1 hints with variable names 2023-03-03 15:55:32 +01:00
Alexander Bentkamp a783e1dffc Add tabs for lemmas #23 2023-03-02 12:15:34 +01:00
Alexander Bentkamp 7748eefa4a fix lemma check 
Fixes #36
 2023-03-02 10:25:34 +01:00
Alexander Bentkamp a44efef7de add definitions 2023-03-01 17:31:58 +01:00
Alexander Bentkamp 9a97b569b5 unify code for tactics and lemmas 2023-03-01 17:14:01 +01:00
Alexander Bentkamp 676560a0df revert to use isDefEq for hints 2023-03-01 14:41:29 +01:00
Alexander Bentkamp bc6c4a57e7 treat simp? and simp! like simp 2023-03-01 11:37:34 +01:00
Alexander Bentkamp bf7c68d4f9 pass lemma/tactic status to file worker 2023-03-01 11:20:32 +01:00
Alexander Bentkamp 4f93dbf928 disable automatic compilation of lean files 2023-03-01 10:55:03 +01:00
Alexander Bentkamp a85f40541e custom unification for hint trigger 2023-03-01 10:38:02 +01:00
Alexander Bentkamp bc7533d18f loading icon for loading goals 2023-02-28 14:37:14 +01:00
Alexander Bentkamp 604e6757ec Import only specific Level file 
Fixes #35
 2023-02-28 13:03:46 +01:00
Alexander Bentkamp 591423b308 make opening namespaces work properly 2023-02-24 16:37:40 +01:00
Alexander Bentkamp 5921de848d Preload all files in a world #15 2023-02-23 17:11:11 +01:00
Alexander Bentkamp 82af2ded8e Speed up loading by process queue #15 2023-02-23 10:18:02 +01:00
Alexander Bentkamp 09137c7019 remove set_option tactic.hygienic false 2023-02-22 17:55:46 +01:00
Alexander Bentkamp 404062c015 Use local scope from level file in game 
Fixes #31
 2023-02-22 17:45:08 +01:00
Alexander Bentkamp 49f9ff035f fix version of lean4 infoview 2023-02-22 15:48:46 +01:00
Alexander Bentkamp 1f0d9aea43 check if tactic doc exists 
Fixes #34
 2023-02-22 15:10:46 +01:00
Alexander Bentkamp f17246f6d4 check lemma names 2023-02-22 11:44:13 +01:00
Alexander Bentkamp 06f4f4e223 typo 2023-02-22 11:41:26 +01:00
Alexander Bentkamp 02ac370a62 Run -> Execute 2023-02-09 15:48:52 +01:00
Alexander Bentkamp 84ce05a548 more styling 2023-02-09 15:42:10 +01:00
Alexander Bentkamp 116026428f show lemma and tactic docs 2023-02-09 15:34:37 +01:00
Alexander Bentkamp 891d51829c rename leftpanel to inventory 2023-02-09 14:26:57 +01:00
Alexander Bentkamp 622aca644e correct shrinking of command line 2023-02-09 13:54:06 +01:00
Alexander Bentkamp ca329a933c make command line look the same on all browsers 2023-02-09 13:43:59 +01:00
Alexander Bentkamp 6e8a47b1a7 lemma inventory 2023-02-09 13:25:52 +01:00
Alexander Bentkamp c628d0eec4 new tactic display 2023-02-09 13:25:52 +01:00
Alexander Bentkamp c93f6bfc15 allow "rcases with" tactic 2023-02-09 13:25:52 +01:00
Alexander Bentkamp e264f11d60 inventory experiment 2023-02-09 13:25:52 +01:00
Alexander Bentkamp 7510b83591 hide command line in "other goals" 
Fixes #30
 2023-02-07 16:03:04 +01:00
Alexander Bentkamp 278aedb20c more monaco command line 
fixes #32
 2023-02-07 15:39:40 +01:00
Alexander Bentkamp a3b1011035 monaco command line 2023-02-07 13:25:57 +01:00
Alexander Bentkamp cd27b2026c OnlyTactics command #16 2023-02-06 15:31:26 +01:00
Alexander Bentkamp 51f82cf9eb disabled tactics command #16 2023-02-06 14:59:41 +01:00