phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
487 Commits 19 Branches 10 Tags
9514e558ad22c98940eaf5faf5e5896c56a1a7a9
Commit Graph
100 Commits
This Branch
This Branch
All Branches
Author SHA1 Message Date
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
Alexander Bentkamp dd4fe60f7e update package json 2023-02-06 14:24:30 +01:00
Alexander Bentkamp a4987f14cf forbidden tactics error message #16 2023-02-06 12:25:27 +01:00
Alexander Bentkamp 76d1a08948 compute which tactics are available in which level 2023-02-03 17:04:09 +01:00
Alexander Bentkamp 03faa3ffed fix lean server error 2023-02-03 16:39:47 +01:00
Alexander Bentkamp 85a96579a5 remove tactic set for real 2023-02-03 16:31:56 +01:00
Alexander Bentkamp d1eee327dd graph algos 2023-02-03 16:29:16 +01:00
Alexander Bentkamp 3f433507db remove TacticSet command 
This is not necessary because there aren't that many tactics
 2023-02-03 15:45:49 +01:00
Alexander Bentkamp 41cc23543b fix command line bug 2023-02-02 09:35:03 +01:00
Alexander Bentkamp 73a44bd057 disable undo button 2023-01-30 15:30:48 +01:00
Alexander Bentkamp 5025fa939b show line numbers only in editor mode 2023-01-30 15:18:06 +01:00
Alexander Bentkamp 45f88cf5a8 undo button 2023-01-30 15:15:39 +01:00
Alexander Bentkamp fbdc1afe34 hide command line properly 2023-01-30 13:18:02 +01:00
Alexander Bentkamp f73dac8353 prettier command line 2023-01-30 12:28:25 +01:00
Alexander Bentkamp 48de58416d editor mode 2023-01-30 12:00:33 +01:00
Alexander Bentkamp e2ea6fa85e resizable panels 2023-01-30 11:19:33 +01:00
Alexander Bentkamp 2774fab98c replace mui buttons, move them into bar 2023-01-27 17:28:32 +01:00
Alexander Bentkamp 8c83e802e9 center loading icon 2023-01-27 16:39:00 +01:00
Alexander Bentkamp 6d567a696f add command line #26 2023-01-27 12:14:08 +01:00
Alexander Bentkamp 450f32a56b disable quickSuggestions 
Fixes #10
 2023-01-26 16:28:08 +01:00