Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
141 commits
Select commit Hold shift + click to select a range
d3a55a4
add Chinese translation
hydrogenbear Mar 28, 2024
1431ff8
remove the mistyped key
hydrogenbear Mar 28, 2024
1006097
Merge branch 'dev' of https://github.com/leanprover-community/lean4ga…
hydrogenbear Mar 30, 2024
470a184
some update
JiechengZhao Mar 31, 2024
af54268
Some updates, and fix.
JiechengZhao Apr 1, 2024
ded9c38
Merge remote-tracking branch 'upstream/dev' into cn-i18n
JiechengZhao Apr 10, 2024
3d9d244
mark another string from translation
joneugster Apr 10, 2024
848b2cd
fix hhu-adam/Robo#22
joneugster Apr 11, 2024
c5df85c
Add a missed translation
JiechengZhao Apr 11, 2024
62f1fb8
add numpad-enter key #212
joneugster Apr 17, 2024
f308e1a
fix CSS of tooltips #207
joneugster Apr 17, 2024
237371a
Merge branch 'main' of https://github.com/leanprover-community/lean4g…
JiechengZhao Apr 18, 2024
4e7c958
Update client/public/locales/zh/translation.json
joneugster Apr 18, 2024
3ddcc35
Merge pull request #206 from JiechengZhao/cn-i18n
joneugster Apr 18, 2024
8cf358e
add config option to disable flags in preferences #208
joneugster Apr 18, 2024
02978a3
add allowed keywords #215
joneugster Apr 18, 2024
a1b1a33
remove more flags #208
joneugster Apr 19, 2024
eac945e
update impressum & privacy policy
joneugster Apr 24, 2024
06cc52b
mark tabs with new theorems
joneugster Apr 24, 2024
1daef0d
show exercise name even if no text present
joneugster Apr 25, 2024
05fbee9
mark inventory item from the last level
joneugster Apr 25, 2024
b9112bf
add 'using' as known keyword
joneugster May 3, 2024
5765c78
add submenu for inventory categories
joneugster May 3, 2024
08875e4
style error page
joneugster May 7, 2024
d82ef8a
refactor: navigation and other stuff
joneugster May 16, 2024
c1642cf
cleanup: popups
joneugster May 16, 2024
8b5d6ff
improve language selection
joneugster May 16, 2024
895c71d
cleanup
joneugster May 16, 2024
369b77f
add search parameter to set language #220
joneugster May 16, 2024
c735211
cleanup
joneugster May 16, 2024
a7d746a
add defeq-hints #45
joneugster May 23, 2024
71fad56
turn defeq-hints on by default #45
joneugster May 23, 2024
8e3dfde
wip
joneugster May 24, 2024
adeed03
cleanup; including cleaning up chat
joneugster Jun 5, 2024
cdffe03
cleanup chat
joneugster Jun 5, 2024
6da902a
cleanup chat css
joneugster Jun 5, 2024
714b4f4
redefine chat scrolling #230
joneugster Jun 6, 2024
80d4b88
mostly remove 'world' as a word #237
joneugster Jun 6, 2024
7dc0a50
fix css
joneugster Jun 6, 2024
f158250
improve chat scrolling #82
joneugster Jun 10, 2024
4652f6d
add support for external images in chat #235
joneugster Jun 10, 2024
762c1ef
drop comment
joneugster Jun 10, 2024
02d0d57
fail gracefully on bad gameId #150
joneugster Jun 10, 2024
096bd55
image for world intro
joneugster Jun 10, 2024
b669542
cleanup context
joneugster Jun 10, 2024
72ccdd1
move Button and Markdown
joneugster Jun 10, 2024
9f4fe65
style
joneugster Jun 10, 2024
925d729
doc
joneugster Jun 10, 2024
d684f26
cleanup imports of world_tree
joneugster Jun 10, 2024
aedf073
unlock inventory items in relaxed mode #194
joneugster Jun 11, 2024
2a07033
side-by-side goals #90
joneugster Jun 11, 2024
17d2ba5
use JuliaMono and Roboto as fonts consistently #192
joneugster Jun 11, 2024
1f14ad1
internally rename lemma to theorem #108
joneugster Jun 11, 2024
aed2899
do not display any errors before the first step #209
joneugster Jun 11, 2024
503ea51
add framework to allow unbundle hypotheses #105
joneugster Jun 11, 2024
b1cdcfc
press enter to go to next level #170
joneugster Jun 11, 2024
c03e2f1
add next/home back button to chat
joneugster Jun 11, 2024
dea5fd0
add buttons to delete level/world only #199
joneugster Jun 11, 2024
a0ecaee
fix button display #199
joneugster Jun 11, 2024
8b4215e
update documentation about opening local notations #216
joneugster Jun 12, 2024
b815b86
sort theorems alphabetically #110
joneugster Jun 12, 2024
75b367e
remove LemmaDoc etc.
joneugster Jun 12, 2024
937c471
update game info
joneugster Jun 12, 2024
30d9b88
use GoalsTab in editor mode
joneugster Jun 12, 2024
2896237
css
joneugster Jun 13, 2024
67090f5
add basic infos to inventory
joneugster Jun 18, 2024
5310e69
cleanup
joneugster Jun 18, 2024
aab6dbb
cleanup
joneugster Jun 18, 2024
d05767d
add dev version of new typewriter input
joneugster Jun 18, 2024
fbe48d2
add support for diags in chat
joneugster Jun 20, 2024
5b6f5f0
adding keys
joneugster Jul 31, 2024
38cac49
fix maximal recursion in useEffect
joneugster Jul 31, 2024
5a09776
npm audit fix
joneugster Aug 20, 2024
545ac8b
grey-out locked items
joneugster Aug 26, 2024
3a88524
WIP implementing new editor
joneugster Aug 28, 2024
64ad36d
wip
joneugster Sep 12, 2024
92acdb7
wip
joneugster Oct 10, 2024
e5a1303
update toolchain, add test lib
joneugster Dec 23, 2024
c16d840
simple fixes
joneugster Dec 23, 2024
866cfb8
easy fixes
joneugster Dec 23, 2024
3525d9f
add new copy of Fileworker
joneugster Jan 9, 2025
a5d4509
wip
joneugster Feb 20, 2025
7340c1a
bump v4.15
joneugster Feb 20, 2025
d48224c
Merge branch 'bump_v4.14' into dev
joneugster Feb 20, 2025
73a8b9d
restructuring
joneugster Feb 21, 2025
84e9d11
further separation
joneugster Feb 21, 2025
91a0518
update gitignore
joneugster Feb 21, 2025
f9313aa
improve tests
joneugster Feb 21, 2025
db56cd5
move files
joneugster Feb 21, 2025
aa71193
further restructuring
joneugster Feb 21, 2025
d753dec
display empty documentation if not existent
joneugster Feb 24, 2025
34099ab
work on client
joneugster Feb 25, 2025
f878dd8
add missing files
joneugster Feb 25, 2025
28da6ea
chore: hidden tactics do not need a doc entry #300
joneugster Feb 25, 2025
368b154
fix: also check existance of first world of a Dependency arrow #292
joneugster Feb 25, 2025
d5bfd46
feat: show local games on landing page
joneugster Feb 25, 2025
9800876
update TestGame
joneugster Feb 25, 2025
ae87d45
fixing mobile layout
joneugster Feb 26, 2025
0173688
align relay with file from lean4web
joneugster Feb 26, 2025
c199947
work on client
joneugster Feb 26, 2025
a0edece
wip
joneugster Feb 27, 2025
ee0b66c
Ignore .idea folder
tautastic Feb 27, 2025
ee77db2
Add cypress
tautastic Feb 27, 2025
4c37a94
Add scripts to run cypress
tautastic Feb 27, 2025
9ec29bc
Add basic cypress setup and first tests
tautastic Feb 27, 2025
e14888b
fix
joneugster Feb 27, 2025
a82031a
Add basic cypress setup and first tests
tautastic Feb 27, 2025
f721de7
Add more tests
tautastic Feb 27, 2025
a6a0835
Add custom 'map' command
tautastic Feb 28, 2025
865de3a
Add a few more tests
tautastic Feb 28, 2025
b710822
Try adding test github action
tautastic Feb 28, 2025
4335b86
Ignore uncaught exceptions
tautastic Feb 28, 2025
4c3d73e
Build lean before caching
tautastic Feb 28, 2025
5e54be9
Remove `add-cypress` from workflow file
tautastic Feb 28, 2025
6ed1c13
introduce gameserver proxy
joneugster Mar 3, 2025
858348c
Merge branch 'dev' into add-cypress
joneugster Mar 3, 2025
e407bb2
Merge pull request #306 from tautastic/add-cypress
joneugster Mar 3, 2025
55e33bd
Merge branch 'dev' of github.com:leanprover-community/lean4game into dev
joneugster Mar 3, 2025
37431c3
fix cypress script
joneugster Mar 3, 2025
7f6471d
udpate cypress workflow
joneugster Mar 3, 2025
839c573
update workflow
joneugster Mar 3, 2025
f132a88
wip client
joneugster Mar 3, 2025
49e5343
update action
joneugster Mar 3, 2025
9a56eb9
update action
joneugster Mar 3, 2025
1d4299e
add missing dependency
joneugster Mar 3, 2025
13b31c6
update action
joneugster Mar 3, 2025
491be06
rename npm scripts
joneugster Mar 3, 2025
7cc82bd
Regenerate package-lock.json
tautastic Mar 3, 2025
df32d03
Add `-s first` flag to `concurrently` such that Cypress's return valu…
tautastic Mar 3, 2025
45382dc
Merge pull request #307 from tautastic/fix-action
joneugster Mar 3, 2025
5a8379d
Fix assigning the return values of cypress usages, instead use aliases
tautastic Mar 4, 2025
1c6d7fa
Merge pull request #308 from tautastic/fix-usage-of-cypress
joneugster Mar 6, 2025
a20f3be
add debugging option for gameserver executable
joneugster Mar 3, 2025
30f987a
bump v4.17.0
joneugster Mar 4, 2025
9bd2c19
work on proxy: wrap sample code around editor
joneugster Mar 6, 2025
a4cf973
first RPC test
joneugster Mar 11, 2025
2572df4
Update .gitignore
matlorr Jun 20, 2025
fdf4371
Update .gitignore
matlorr Jun 20, 2025
58d057b
Merge branch 'bugfix/start-up' into dev
matlorr Jun 20, 2025
e0039ed
Adjust startup settings
matlorr Jun 20, 2025
7ae82ef
Access Game.po file
matlorr Dec 17, 2025
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
53 changes: 38 additions & 15 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
@@ -1,23 +1,46 @@
name: Build
run-name: Build the project
name: Build and Test
run-name: Build and Test
on:
workflow_dispatch:
push:
branches:
- "main"
- "dev"
pull_request:
branches:
- "main"
- "dev"
paths:
- ".github/workflows/build.yml"

concurrency:
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
cancel-in-progress: true

defaults:
run:
shell: bash

jobs:
build:
runs-on: ubuntu-latest
steps:
- name: install elan
run: |
set -o pipefail
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
./elan-init -y
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- uses: actions/checkout@v4
- uses: actions/setup-node@v3
- name: print lean and lake versions
run: |
lean --version
lake --version
- run: npm install
- run: npm run build
- uses: actions/setup-node@v4
- name: Install elan, build and test server
uses: leanprover/lean-action@v1
with:
lake-package-directory: "server"
use-mathlib-cache: false
use-github-cache: false
auto-config: false
build: true
test: true
lint: false
- name: Install dependencies
run: npm install
- name: Build client for production
run: npm run build:client
- name: Cypress tests
if: always()
run: npm test
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -6,4 +6,7 @@ server/.lake
**/.DS_Store
logs/
relay/prev_cpu_metric
relay/dist
**/.i18n
.idea
test.ecosystem.config.cjs
2 changes: 1 addition & 1 deletion client/i18next-scanner.config.cjs
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ module.exports = {
// sourceType: 'module', // defaults to 'module'
// }
},
lngs: lean4gameConfig.languages.map(e => e.iso),
lngs: lean4gameConfig.languages.keys(),
ns: [],
defaultLng: 'en',
defaultNs: 'translation',
Expand Down
Binary file added client/public/RoboSurprised.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added client/public/fonts/JuliaMono-Regular.ttf
Binary file not shown.
93 changes: 93 additions & 0 deletions client/public/fonts/LICENSE-JuliaMono
Original file line number Diff line number Diff line change
@@ -0,0 +1,93 @@
Copyright (c) 2020 - 2023, cormullion
with Reserved Font Name JuliaMono.

This Font Software is licensed under the SIL Open Font License, Version 1.1.
This license is copied below, and is also available with a FAQ at:
http://scripts.sil.org/OFL

-----------------------------------------------------------
SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
-----------------------------------------------------------

PREAMBLE
The goals of the Open Font License (OFL) are to stimulate worldwide
development of collaborative font projects, to support the font creation
efforts of academic and linguistic communities, and to provide a free and
open framework in which fonts may be shared and improved in partnership
with others.

The OFL allows the licensed fonts to be used, studied, modified and
redistributed freely as long as they are not sold by themselves. The
fonts, including any derivative works, can be bundled, embedded,
redistributed and/or sold with any software provided that any reserved
names are not used by derivative works. The fonts and derivatives,
however, cannot be released under any other type of license. The
requirement for fonts to remain under this license does not apply
to any document created using the fonts or their derivatives.

DEFINITIONS
"Font Software" refers to the set of files released by the Copyright
Holder(s) under this license and clearly marked as such. This may
include source files, build scripts and documentation.

"Reserved Font Name" refers to any names specified as such after the
copyright statement(s).

"Original Version" refers to the collection of Font Software components as
distributed by the Copyright Holder(s).

"Modified Version" refers to any derivative made by adding to, deleting,
or substituting -- in part or in whole -- any of the components of the
Original Version, by changing formats or by porting the Font Software to a
new environment.

"Author" refers to any designer, engineer, programmer, technical
writer or other person who contributed to the Font Software.

PERMISSION & CONDITIONS
Permission is hereby granted, free of charge, to any person obtaining
a copy of the Font Software, to use, study, copy, merge, embed, modify,
redistribute, and sell modified and unmodified copies of the Font
Software, subject to the following conditions:

1) Neither the Font Software nor any of its individual components,
in Original or Modified Versions, may be sold by itself.

2) Original or Modified Versions of the Font Software may be bundled,
redistributed and/or sold with any software, provided that each copy
contains the above copyright notice and this license. These can be
included either as stand-alone text files, human-readable headers or
in the appropriate machine-readable metadata fields within text or
binary files as long as those fields can be easily viewed by the user.

3) No Modified Version of the Font Software may use the Reserved Font
Name(s) unless explicit written permission is granted by the corresponding
Copyright Holder. This restriction only applies to the primary font name as
presented to the users.

4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
Software shall not be used to promote, endorse or advertise any
Modified Version, except to acknowledge the contribution(s) of the
Copyright Holder(s) and the Author(s) or with their explicit written
permission.

5) The Font Software, modified or unmodified, in part or in whole,
must be distributed entirely under this license, and must not be
distributed under any other license. The requirement for fonts to
remain under this license does not apply to any document created
using the Font Software.

TERMINATION
This license becomes null and void if any of the above conditions are
not met.

DISCLAIMER
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
OTHER DEALINGS IN THE FONT SOFTWARE.
93 changes: 93 additions & 0 deletions client/public/fonts/LICENSE-NotoColorEmoji
Original file line number Diff line number Diff line change
@@ -0,0 +1,93 @@
Copyright 2021 Google Inc. All Rights Reserved.

This Font Software is licensed under the SIL Open Font License, Version 1.1.
This license is copied below, and is also available with a FAQ at:
https://openfontlicense.org


-----------------------------------------------------------
SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
-----------------------------------------------------------

PREAMBLE
The goals of the Open Font License (OFL) are to stimulate worldwide
development of collaborative font projects, to support the font creation
efforts of academic and linguistic communities, and to provide a free and
open framework in which fonts may be shared and improved in partnership
with others.

The OFL allows the licensed fonts to be used, studied, modified and
redistributed freely as long as they are not sold by themselves. The
fonts, including any derivative works, can be bundled, embedded,
redistributed and/or sold with any software provided that any reserved
names are not used by derivative works. The fonts and derivatives,
however, cannot be released under any other type of license. The
requirement for fonts to remain under this license does not apply
to any document created using the fonts or their derivatives.

DEFINITIONS
"Font Software" refers to the set of files released by the Copyright
Holder(s) under this license and clearly marked as such. This may
include source files, build scripts and documentation.

"Reserved Font Name" refers to any names specified as such after the
copyright statement(s).

"Original Version" refers to the collection of Font Software components as
distributed by the Copyright Holder(s).

"Modified Version" refers to any derivative made by adding to, deleting,
or substituting -- in part or in whole -- any of the components of the
Original Version, by changing formats or by porting the Font Software to a
new environment.

"Author" refers to any designer, engineer, programmer, technical
writer or other person who contributed to the Font Software.

PERMISSION & CONDITIONS
Permission is hereby granted, free of charge, to any person obtaining
a copy of the Font Software, to use, study, copy, merge, embed, modify,
redistribute, and sell modified and unmodified copies of the Font
Software, subject to the following conditions:

1) Neither the Font Software nor any of its individual components,
in Original or Modified Versions, may be sold by itself.

2) Original or Modified Versions of the Font Software may be bundled,
redistributed and/or sold with any software, provided that each copy
contains the above copyright notice and this license. These can be
included either as stand-alone text files, human-readable headers or
in the appropriate machine-readable metadata fields within text or
binary files as long as those fields can be easily viewed by the user.

3) No Modified Version of the Font Software may use the Reserved Font
Name(s) unless explicit written permission is granted by the corresponding
Copyright Holder. This restriction only applies to the primary font name as
presented to the users.

4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
Software shall not be used to promote, endorse or advertise any
Modified Version, except to acknowledge the contribution(s) of the
Copyright Holder(s) and the Author(s) or with their explicit written
permission.

5) The Font Software, modified or unmodified, in part or in whole,
must be distributed entirely under this license, and must not be
distributed under any other license. The requirement for fonts to
remain under this license does not apply to any document created
using the Font Software.

TERMINATION
This license becomes null and void if any of the above conditions are
not met.

DISCLAIMER
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
OTHER DEALINGS IN THE FONT SOFTWARE.
Loading
Loading