Compare commits
1 Commits
main
...
bump_v4.8.
| Author | SHA1 | Date |
|---|---|---|
Jon Eugster
|
446d0296f0 | 2 years ago |
@ -1,8 +0,0 @@
|
|||||||
node_modules
|
|
||||||
client/dist
|
|
||||||
games/
|
|
||||||
server/.lake
|
|
||||||
**/.DS_Store
|
|
||||||
logs/
|
|
||||||
relay/prev_cpu_metric
|
|
||||||
test.ecosystem.config.cjs
|
|
||||||
@ -1,29 +0,0 @@
|
|||||||
FROM node:23-bookworm
|
|
||||||
|
|
||||||
RUN apt update && apt upgrade -y
|
|
||||||
RUN apt install -y bubblewrap
|
|
||||||
|
|
||||||
WORKDIR /app
|
|
||||||
|
|
||||||
# Install elan
|
|
||||||
RUN 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
|
|
||||||
|
|
||||||
ENV PATH="/root/.elan/bin:${PATH}"
|
|
||||||
|
|
||||||
# Copy package files
|
|
||||||
COPY package.json package-lock.json ./
|
|
||||||
|
|
||||||
# Install dependencies
|
|
||||||
RUN npm install
|
|
||||||
|
|
||||||
# Copy project files
|
|
||||||
COPY . .
|
|
||||||
|
|
||||||
# Build the project
|
|
||||||
RUN npm run build
|
|
||||||
|
|
||||||
EXPOSE 8080
|
|
||||||
|
|
||||||
# Set the entrypoint
|
|
||||||
CMD ["npm", "run", "production"]
|
|
||||||
@ -1,8 +0,0 @@
|
|||||||
/ko-level1.tmx
|
|
||||||
/ko-level2.tmx
|
|
||||||
/ko-omegat.tmx
|
|
||||||
/**/*.bak
|
|
||||||
/omegat/last_entry.properties
|
|
||||||
/omegat/files_order.txt
|
|
||||||
/omegat/project_stats.txt
|
|
||||||
/tm/*.tmx
|
|
||||||
@ -1,15 +0,0 @@
|
|||||||
# 린 4 게임
|
|
||||||
|
|
||||||
[English (영어)](./README.md) | 한국어
|
|
||||||
|
|
||||||
## 기여하기
|
|
||||||
|
|
||||||
`lean4game`의 한국어 번역에 기여하는 활동은 언제든지 환영합니다!
|
|
||||||
|
|
||||||
### 한국어 번역
|
|
||||||
|
|
||||||
저([차불휘][bc])는 [오메가T(OmegaT)][omt]를 이용해 영어 문서를 한국어로 번역합니다. 오메가T 프로젝트는 이 디렉터리, 다시 말해 `client/public/locales/ko`에 있습니다. 오메가T로 JSON 파일을 구문 분석 하려면 [오메가T를 위한 오카피(Okapi) 필터 플러그인][okapi]을 설치해야 됩니다.
|
|
||||||
|
|
||||||
[bc]: https://github.com/chabulhwi
|
|
||||||
[omt]: https://omegat.org/
|
|
||||||
[okapi]: https://okapiframework.org/wiki/index.php/Okapi_Filters_Plugin_for_OmegaT
|
|
||||||
@ -1,18 +0,0 @@
|
|||||||
# Lean 4 Game
|
|
||||||
|
|
||||||
English | [한국어[Korean]](./README.ko.md)
|
|
||||||
|
|
||||||
## Contributing
|
|
||||||
|
|
||||||
Contributions to the Korean translation of `lean4game` are always welcome!
|
|
||||||
|
|
||||||
### Korean Translation
|
|
||||||
|
|
||||||
I ([Bulhwi Cha][bc]) use [OmegaT][omt] to translate English documentation into
|
|
||||||
Korean. The OmegaT project is in this directory, that is,
|
|
||||||
`client/public/locales/ko`. You need to install the [Okapi filters plugin for
|
|
||||||
OmegaT][okapi] to make OmegaT parse JSON files.
|
|
||||||
|
|
||||||
[bc]: https://github.com/chabulhwi
|
|
||||||
[omt]: https://omegat.org/
|
|
||||||
[okapi]: https://okapiframework.org/wiki/index.php/Okapi_Filters_Plugin_for_OmegaT
|
|
||||||
@ -1,167 +0,0 @@
|
|||||||
# Glossary in tab-separated format -*- coding: utf-8 -*-
|
|
||||||
St. Anselm 안셀무스
|
|
||||||
ontological 존재론적
|
|
||||||
argument 논증
|
|
||||||
argument 인수
|
|
||||||
Lean 린
|
|
||||||
Lean community 린 커뮤니티
|
|
||||||
God 신
|
|
||||||
Alvin Plantinga 앨빈 플랜팅아
|
|
||||||
exist 존재하다
|
|
||||||
existence 존재
|
|
||||||
the understanding 지성
|
|
||||||
reality 현실
|
|
||||||
assumption 가정
|
|
||||||
reductio 귀류법
|
|
||||||
great 큰
|
|
||||||
premise 전제
|
|
||||||
being 존재자
|
|
||||||
conceive 생각하다
|
|
||||||
definition 정의
|
|
||||||
true 참
|
|
||||||
true 참인
|
|
||||||
false 거짓
|
|
||||||
false 거짓인
|
|
||||||
formulate 정식화하다
|
|
||||||
formulation 정식화
|
|
||||||
formalize 형식화하다
|
|
||||||
formalization 형식화
|
|
||||||
property 속성
|
|
||||||
redundant 불필요한
|
|
||||||
sentence 문장
|
|
||||||
state 진술하다
|
|
||||||
statement 진술
|
|
||||||
proposition 명제
|
|
||||||
negation 부정
|
|
||||||
axiom 공리
|
|
||||||
theorem 정리
|
|
||||||
theory 이론
|
|
||||||
conclude 결론하다
|
|
||||||
prove 증명하다
|
|
||||||
SEP 스탠퍼드 철학 백과사전
|
|
||||||
Eric Wieser 에릭 비저
|
|
||||||
Alistair Tucker 앨리스터 터커
|
|
||||||
philosophy 철학
|
|
||||||
Owl of Sogang 서강올빼미
|
|
||||||
type theory 유형론
|
|
||||||
universe level 유형 세계 변수
|
|
||||||
type 유형
|
|
||||||
type 입력하다
|
|
||||||
type check 유형을 확인하다
|
|
||||||
type check 유형이 확인되다
|
|
||||||
type check 유형 확인이 잘되다
|
|
||||||
type class 유형 클래스
|
|
||||||
instance 사례
|
|
||||||
category mistake 범주 실수
|
|
||||||
class 클래스
|
|
||||||
example 보기
|
|
||||||
example 예
|
|
||||||
inductive type 귀납형
|
|
||||||
define 정의하다
|
|
||||||
constructor 구성자
|
|
||||||
Apache License, Version 2.0 아파치 라이선스, 버전 2.0
|
|
||||||
under the terms of 의 조건에 따라
|
|
||||||
OmegaT 오메가T
|
|
||||||
symbolic link 심벌릭 링크
|
|
||||||
directory 디렉터리
|
|
||||||
root directory 최상위 디렉터리
|
|
||||||
documentation 문서
|
|
||||||
English 영어
|
|
||||||
Korean 한국어
|
|
||||||
chapter 장
|
|
||||||
quiz 퀴즈
|
|
||||||
question 문제
|
|
||||||
command 명령어
|
|
||||||
error 오류
|
|
||||||
code 코드
|
|
||||||
evaluate 계산하다
|
|
||||||
keyword 핵심어
|
|
||||||
declare 선언하다
|
|
||||||
constant 상수
|
|
||||||
reference 참고 문헌
|
|
||||||
universe-polymorphic 세계 다형적
|
|
||||||
parametrically polymorphic 매개 변수 다형적
|
|
||||||
function 함수
|
|
||||||
identifier 식별자
|
|
||||||
definitionally equal 정의상 같은
|
|
||||||
natural number 자연수
|
|
||||||
input 입력값
|
|
||||||
return 반환하다
|
|
||||||
non-zero 영이 아닌
|
|
||||||
zero 영
|
|
||||||
alpha-equivalent 알파 동등한
|
|
||||||
less-than-or-equal-to sign 작거나 같음 부호
|
|
||||||
dependent function 의존 함수
|
|
||||||
dependent function type 의존 함수형
|
|
||||||
dependent product 의존곱
|
|
||||||
dependent product type 의존곱형
|
|
||||||
underscore 밑줄
|
|
||||||
implicit 암시적
|
|
||||||
explicit 명시적
|
|
||||||
sigma type 시그마
|
|
||||||
propositional logic 명제 논리
|
|
||||||
term 항
|
|
||||||
contemporary 동시대
|
|
||||||
term 용어
|
|
||||||
truth-value 진릿값
|
|
||||||
bearer 담지자
|
|
||||||
propositional attitudes 명제적 태도
|
|
||||||
believe 믿다
|
|
||||||
doubt 의심하다
|
|
||||||
South Korea 한국
|
|
||||||
school mathematics 학교 수학
|
|
||||||
sentence 문장
|
|
||||||
high school mathematics 고등학교 수학
|
|
||||||
teacher 교사
|
|
||||||
Stanford Encyclopedia of Philosophy 스탠퍼드 철학 백과사전
|
|
||||||
ordered triple 순서세짝
|
|
||||||
conjecture 추측
|
|
||||||
Goldbach's conjecture 골드바흐의 추측
|
|
||||||
interactive theorem prover 상호 작용 정리 증명기
|
|
||||||
truth 참
|
|
||||||
falsity 거짓
|
|
||||||
rule of inference 추론 규칙
|
|
||||||
introduction rule 도입 규칙
|
|
||||||
elimination rule 제거 규칙
|
|
||||||
ex falso quodlibet 엑스 팔소 세퀴투르 쿠오들리베트
|
|
||||||
principle of explosion 폭발 원리
|
|
||||||
propositional connective 명제 연결사
|
|
||||||
symbol 기호
|
|
||||||
refutation by contradiction 모순에 따른 부인
|
|
||||||
contradiction 모순
|
|
||||||
conjunction 연언
|
|
||||||
disjunction 선언(選言)
|
|
||||||
implication 함의
|
|
||||||
material implication 내용적 함의
|
|
||||||
conditional 조건문
|
|
||||||
modus ponens 긍정 논법[모더스 포넨스]
|
|
||||||
necessary condition 필요조건
|
|
||||||
conversion 역
|
|
||||||
inversion 이(裏)
|
|
||||||
contraposition 대우(對偶)
|
|
||||||
equivalence 동등
|
|
||||||
biconditional 쌍조건문
|
|
||||||
abbreviation 준말
|
|
||||||
if and only if …일 때 그리고 그럴 때만
|
|
||||||
editor 편집기
|
|
||||||
shortcut 단축키
|
|
||||||
Theorem Proving in Lean 4 린 4로 하는 정리 증명
|
|
||||||
exercise 연습 문제
|
|
||||||
repository 저장소
|
|
||||||
Jeremy Avigad 제러미 아비가드
|
|
||||||
Leonardo de Moura 레오나르두 지 모라
|
|
||||||
Soonho Kong 공순호
|
|
||||||
Sebastian Ullrich 제바스티안 울리히
|
|
||||||
file 파일
|
|
||||||
Markdown 마크다운
|
|
||||||
quiz 퀴즈
|
|
||||||
translation 번역
|
|
||||||
contribute 기여하다
|
|
||||||
progress 진도
|
|
||||||
capacity 이용량
|
|
||||||
GitHub 깃허브
|
|
||||||
repo 저장소
|
|
||||||
game rule 게임 규칙
|
|
||||||
unlocked 잠금 해제가 된
|
|
||||||
unlock 잠금 해제를 하다
|
|
||||||
Markdown 마크다운
|
|
||||||
@ -1,33 +0,0 @@
|
|||||||
<?xml version="1.0" encoding="UTF-8" standalone="yes"?>
|
|
||||||
<omegat>
|
|
||||||
<project version="1.0">
|
|
||||||
<source_dir>__DEFAULT__</source_dir>
|
|
||||||
<source_dir_excludes>
|
|
||||||
<mask>**/.svn/**</mask>
|
|
||||||
<mask>**/CVS/**</mask>
|
|
||||||
<mask>**/.cvs/**</mask>
|
|
||||||
<mask>**/.git/**</mask>
|
|
||||||
<mask>**/.hg/**</mask>
|
|
||||||
<mask>**/.repositories/**</mask>
|
|
||||||
<mask>**/desktop.ini</mask>
|
|
||||||
<mask>**/Thumbs.db</mask>
|
|
||||||
<mask>**/.DS_Store</mask>
|
|
||||||
<mask>**/~$*</mask>
|
|
||||||
</source_dir_excludes>
|
|
||||||
<target_dir>__DEFAULT__</target_dir>
|
|
||||||
<tm_dir>__DEFAULT__</tm_dir>
|
|
||||||
<glossary_dir>__DEFAULT__</glossary_dir>
|
|
||||||
<glossary_file>__DEFAULT__</glossary_file>
|
|
||||||
<dictionary_dir>__DEFAULT__</dictionary_dir>
|
|
||||||
<export_tm_dir>__DEFAULT__</export_tm_dir>
|
|
||||||
<export_tm_levels>omegat level1 level2</export_tm_levels>
|
|
||||||
<source_lang>en</source_lang>
|
|
||||||
<target_lang>ko</target_lang>
|
|
||||||
<source_tok>org.omegat.tokenizer.LuceneEnglishTokenizer</source_tok>
|
|
||||||
<target_tok>org.omegat.tokenizer.HunspellTokenizer</target_tok>
|
|
||||||
<sentence_seg>true</sentence_seg>
|
|
||||||
<support_default_translations>true</support_default_translations>
|
|
||||||
<remove_tags>false</remove_tags>
|
|
||||||
<external_command></external_command>
|
|
||||||
</project>
|
|
||||||
</omegat>
|
|
||||||
File diff suppressed because it is too large
Load Diff
@ -1 +0,0 @@
|
|||||||
../README.md
|
|
||||||
@ -1 +0,0 @@
|
|||||||
../../en/translation.json
|
|
||||||
@ -1,15 +0,0 @@
|
|||||||
# 린 4 게임
|
|
||||||
|
|
||||||
[English (영어)](./README.md) | 한국어
|
|
||||||
|
|
||||||
## 기여하기
|
|
||||||
|
|
||||||
`lean4game`의 한국어 번역에 기여하는 활동은 언제든지 환영합니다!
|
|
||||||
|
|
||||||
### 한국어 번역
|
|
||||||
|
|
||||||
저([차불휘][bc])는 [오메가T(OmegaT)][omt]를 이용해 영어 문서를 한국어로 번역합니다. 오메가T 프로젝트는 이 디렉터리, 다시 말해 `client/public/locales/ko`에 있습니다. 오메가T로 JSON 파일을 구문 분석 하려면 [오메가T를 위한 오카피(Okapi) 필터 플러그인][okapi]을 설치해야 됩니다.
|
|
||||||
|
|
||||||
[bc]: https://github.com/chabulhwi
|
|
||||||
[omt]: https://omegat.org/
|
|
||||||
[okapi]: https://okapiframework.org/wiki/index.php/Okapi_Filters_Plugin_for_OmegaT
|
|
||||||
@ -1,99 +0,0 @@
|
|||||||
{
|
|
||||||
"Tactics": "전략",
|
|
||||||
"Lean Game Server": "린 게임 서버",
|
|
||||||
"<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>게임 규칙에 따라, 단계들을 건너뛰어도 되는지 그리고 증명을 작성할 때 잠금 해제가 된 전략과 정리만 이용할 수 있는지가 정해집니다.</p><1>\n\n참고: '잠금 해제'가 된 전략이나 정리는 다음 두 부류로 정해집니다. (1) 해당 단계를 푸는 데 필요한 최소한의 전략이나 정리의 모임, (2) 다른 단계에서 잠금 해제를 한 전략이나 정리. 따라서 여러분이 <1>simp</1> 전략을 잠금 해제 하면, 그 뒤로 어느 단계에서든 이 전략을 이용할 수 있습니다.</1><p>선택할 수 있는 게임 규칙은 다음과 같습니다.</p>",
|
|
||||||
"Game Rules": "게임 규칙",
|
|
||||||
"levels": "단계",
|
|
||||||
"tactics": "전략",
|
|
||||||
"regular": "일반",
|
|
||||||
"relaxed": "완화됨",
|
|
||||||
"none": "없음",
|
|
||||||
"Rules": "규칙",
|
|
||||||
"Intro": "소개",
|
|
||||||
"Game Introduction": "게임 소개",
|
|
||||||
"World selection": "세계 선택",
|
|
||||||
"Start": "시작하기",
|
|
||||||
"Inventory": "인벤토리",
|
|
||||||
"next level": "다음 단계",
|
|
||||||
"Next": "다음",
|
|
||||||
"back to world selection": "세계 선택하러 돌아가기",
|
|
||||||
"Leave World": "세계에서 나가기",
|
|
||||||
"previous level": "이전 단계",
|
|
||||||
"Previous": "이전",
|
|
||||||
"Editor mode is enforced!": "편집기 모드가 강제됐습니다!",
|
|
||||||
"Editor mode": "편집기 모드",
|
|
||||||
"Typewriter mode": "타자기 모드",
|
|
||||||
"information, Impressum, privacy policy": "정보, 관리자 정보, 사생활 정책",
|
|
||||||
"Preferences": "기본 설정",
|
|
||||||
"Game Info & Credits": "게임 정보 및 제작자 명단",
|
|
||||||
"Game Info": "게임 정보",
|
|
||||||
"Clear Progress": "진도 없애기",
|
|
||||||
"Erase": "지우기",
|
|
||||||
"Download Progress": "진도 내려받기",
|
|
||||||
"Download": "내려받기",
|
|
||||||
"Load Progress from JSON": "JSON에서 진도 불러오기",
|
|
||||||
"Upload": "업로드",
|
|
||||||
"Home": "홈",
|
|
||||||
"back to games selection": "게임 선택하러 돌아가기",
|
|
||||||
"close inventory": "인벤토리 닫기",
|
|
||||||
"show inventory": "인벤토리 보기",
|
|
||||||
"World": "세계",
|
|
||||||
"Show more help!": "도움말 더 보기!",
|
|
||||||
"Goal": "목표",
|
|
||||||
"Current Goal": "현재 목표",
|
|
||||||
"Objects": "객체",
|
|
||||||
"Assumptions": "가정",
|
|
||||||
"Further Goals": "이후 목표",
|
|
||||||
"No Goals": "목표 없음",
|
|
||||||
"Loading goal…": "목표 불러오는 중…",
|
|
||||||
"Click somewhere in the Lean file to enable the infoview.": "린 파일의 아무 곳이나 눌러 정보창을 여십시오.",
|
|
||||||
"Waiting for Lean server to start…": "린 서버가 시작하기를 기다리는 중…",
|
|
||||||
"Level completed! 🎉": "단계 완료! 🎉",
|
|
||||||
"Level completed with warnings 🎭": "경고 있는 채로 단계 완료 🎭",
|
|
||||||
"Active Goal": "활성화된 목표",
|
|
||||||
"Crashed! Go to editor mode and fix your proof! Last server response:": "시스템 다운됨! 편집기 모드에서 증명을 고치십시오! 마지막 서버 응답:",
|
|
||||||
"Line": "줄",
|
|
||||||
"Character": "문자",
|
|
||||||
"Loading messages…": "메시지 불러오는 중…",
|
|
||||||
"Execute": "실행하기",
|
|
||||||
"Definitions": "정의",
|
|
||||||
"Theorems": "정리",
|
|
||||||
"Not unlocked yet": "아직 잠금 해제가 안 됨",
|
|
||||||
"Not available in this level": "이 단계에서 쓸 수 없음",
|
|
||||||
"A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "<1>린(Lean 4)</1> 증명 보조기와 그 수학 라이브러리 <5>매스리브(mathlib)</5>를 학습하기 위한 게임들의 저장소",
|
|
||||||
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "불러온 게임 없음. <1>http://localhost:3000/#/g/local/FOLDER</1>를 이용해 지역[로컬] 폴더에서 게임을 직접 여십시오.",
|
|
||||||
"Prerequisites": "선행 요건",
|
|
||||||
"Worlds": "세계",
|
|
||||||
"Levels": "단계",
|
|
||||||
"Language": "언어",
|
|
||||||
"Server capacity": "서버 이용량",
|
|
||||||
"RAM": "램",
|
|
||||||
"CPU": "CPU",
|
|
||||||
"Development notes": "개발 노트",
|
|
||||||
"Adding new games": "새 게임 추가하기",
|
|
||||||
"Funding": "재정 지원",
|
|
||||||
"<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "<p>저장된 진도를 불가역적으로 삭제하시겠습니까?</p><p>(이를 선택하시면 증명과 인벤토리 안의 수집 항목들이 삭제됩니다. 다른 게임에 저장된 정보는 삭제되지 않습니다.)</p>",
|
|
||||||
"Delete Progress?": "진도를 삭제하시겠습니까?",
|
|
||||||
"Delete": "삭제하기",
|
|
||||||
"Download & Delete": "내려받고 삭제하기",
|
|
||||||
"Cancel": "취소하기",
|
|
||||||
"Layout": "레이아웃",
|
|
||||||
"Always visible": "항상 보임",
|
|
||||||
"Save my settings (in the browser store)": "(브라우저에) 설정 저장하기",
|
|
||||||
"<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>저장된 게임 진도가 있는 JSON 파일을 선택해 진도를 불러오십시오.</p><1><0>경고:</0> 이를 실행하면 현재의 게임 진도가 삭제됩니다! <2>현재의 게임 진도</2>를 먼저 내려받을지 판단하십시오!</1>",
|
|
||||||
"Upload Saved Progress": "저장된 진도 업로드",
|
|
||||||
"Load selected file": "선택한 파일 열기",
|
|
||||||
"Mobile": "모바일",
|
|
||||||
"Auto": "자동",
|
|
||||||
"Desktop": "데스크톱",
|
|
||||||
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>여러분이 직접 게임을 작성할 생각이 있다면, <1>GameSkeleton 깃허브 저장소</1>를 양식[템플릿]으로 이용하고 <3>'게임 만들기(Creating a Game)'</3> 문서를 읽으십시오.</0><1>여러분이 작성한 게임을 직접 서버에서 불러오고, 정확한 URL을 이용해 그 게임을 하실 수 있습니다. 여러분의 게임을 서버에서 불러오는 방법에 관한 세부 사항도 위의 <1>설명서</1>에 나와 있습니다. 궁금한 점이 있으면 저희에게 연락해 주십시오.</1><p>이 페이지에 실린 게임들은 수동으로 추가됐습니다. 저희에게 연락하시면 여러분의 게임을 기꺼이 추가하겠습니다.",
|
|
||||||
"Level": "단계",
|
|
||||||
"Introduction": "소개",
|
|
||||||
"Retry proof from here": "여기부터 증명 다시 시도하기",
|
|
||||||
"Retry": "다시 시도하기",
|
|
||||||
"Failed command": "실패한 명령",
|
|
||||||
"<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>": "",
|
|
||||||
"<0>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</0>": "",
|
|
||||||
"This server has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich Heine University Düsseldorf.": "",
|
|
||||||
" used": ""
|
|
||||||
}
|
|
||||||
@ -1 +0,0 @@
|
|||||||
target/translation.json
|
|
||||||
@ -1,78 +0,0 @@
|
|||||||
There are multiple ways how to format the text content of your game. Notably Markdown with KaTeX.
|
|
||||||
|
|
||||||
# Escaping
|
|
||||||
Generally, if you add text inside quotes `" "` (e.g. in `Hint`) you need to escape
|
|
||||||
backslashes, but if you provide text inside a doc comment
|
|
||||||
`/-- -/` (e.g. in the `Statement` description) you do not!
|
|
||||||
|
|
||||||
This means for example you'd write `/-- $\iff$ -/` but `"$\\iff$"`.
|
|
||||||
|
|
||||||
Furthermore, inside `Hint` you need to escape all opening curly brackets as `\{` since `{h}` is syntax for inserting a variable name `h`.
|
|
||||||
|
|
||||||
# KaTeX
|
|
||||||
|
|
||||||
LaTeX syntax is provided trough the [KaTeX library](https://katex.org). KateX supports most but not all of latex and its packages.
|
|
||||||
See [supported](https://katex.org/docs/supported.html).
|
|
||||||
|
|
||||||
## Examples
|
|
||||||
|
|
||||||
### Commutative diagrams
|
|
||||||
|
|
||||||
Here is an example of how to write a commutative diagram in KaTeX:
|
|
||||||
|
|
||||||
$$
|
|
||||||
\begin{CD}
|
|
||||||
A @>{f}>> B @<{g}<< C \\
|
|
||||||
@V{h}VV @V{i}VV @V{j}VV \\
|
|
||||||
D @<{k}<< E @>{l}>> F \\
|
|
||||||
@A{m}AA @A{n}AA @V{p}VV \\
|
|
||||||
G @<{q}<< H @>{r}>> I
|
|
||||||
\end{CD}
|
|
||||||
$$
|
|
||||||
|
|
||||||
```
|
|
||||||
$$
|
|
||||||
\begin{CD}
|
|
||||||
A @>{f}>> B @<{g}<< C \\
|
|
||||||
@V{h}VV @V{i}VV @V{j}VV \\
|
|
||||||
D @<{k}<< E @>{l}>> F \\
|
|
||||||
@A{m}AA @A{n}AA @V{p}VV \\
|
|
||||||
G @<{q}<< H @>{r}>> I
|
|
||||||
\end{CD}
|
|
||||||
$$
|
|
||||||
```
|
|
||||||
|
|
||||||
Again, note that inside a string like `Hint`/`Introduction`/`Conclusion`/etc. you need to escape `\` and potentially `{`.
|
|
||||||
|
|
||||||
E.g. `\begin` as `\\begin`, `\\` as `\\\\` and inside a
|
|
||||||
`Hint`, `@>{f}>>` as `@>\{f}>>`.
|
|
||||||
|
|
||||||
See https://www.jmilne.org/not/Mamscd.pdf
|
|
||||||
|
|
||||||
### Truth Tables
|
|
||||||
|
|
||||||
KaTeX does not support the tabular environment. You can use the array environment instead.
|
|
||||||
|
|
||||||
$$
|
|
||||||
\begin{array}{|c|c|}
|
|
||||||
\hline
|
|
||||||
P & ¬P \\
|
|
||||||
\hline
|
|
||||||
T & F \\
|
|
||||||
F & T \\
|
|
||||||
\hline
|
|
||||||
\end{array}
|
|
||||||
$$
|
|
||||||
|
|
||||||
```
|
|
||||||
$$
|
|
||||||
\begin{array}{|c|c|}
|
|
||||||
\hline
|
|
||||||
P & ¬P \\
|
|
||||||
\hline
|
|
||||||
T & F \\
|
|
||||||
F & T \\
|
|
||||||
\hline
|
|
||||||
\end{array}
|
|
||||||
$$
|
|
||||||
```
|
|
||||||
@ -1,14 +0,0 @@
|
|||||||
services:
|
|
||||||
lean4game:
|
|
||||||
build: .
|
|
||||||
privileged: true # needed to run bubblewrap inside docker
|
|
||||||
environment:
|
|
||||||
- LEAN4GAME_GITHUB_USER=${LEAN4GAME_GITHUB_USER}
|
|
||||||
- LEAN4GAME_GITHUB_TOKEN=${LEAN4GAME_GITHUB_TOKEN}
|
|
||||||
ports:
|
|
||||||
- "8080:8080"
|
|
||||||
volumes:
|
|
||||||
- games_data:/app/games
|
|
||||||
|
|
||||||
volumes:
|
|
||||||
games_data:
|
|
||||||
File diff suppressed because it is too large
Load Diff
@ -1,43 +0,0 @@
|
|||||||
import time
|
|
||||||
|
|
||||||
def measure_proc_stat() -> dict[str, int]:
|
|
||||||
proc_stat_header = open("/proc/stat", "r").readline()
|
|
||||||
proc_stat = proc_stat_header.split(' ')[2:]
|
|
||||||
proc_stat[-1] = proc_stat[-1].removesuffix('\n')
|
|
||||||
proc_stat = list(map(int, proc_stat))
|
|
||||||
|
|
||||||
proc_stat_dict= {'user': proc_stat[0],
|
|
||||||
'nice': proc_stat[1],
|
|
||||||
'system': proc_stat[2],
|
|
||||||
'idle': proc_stat[3],
|
|
||||||
'iowait': proc_stat[4],
|
|
||||||
'irq': proc_stat[5],
|
|
||||||
'softirq': proc_stat[6],
|
|
||||||
'steal': proc_stat[7],
|
|
||||||
'guest': proc_stat[8],
|
|
||||||
'guest_nice': proc_stat[9]}
|
|
||||||
|
|
||||||
return proc_stat_dict
|
|
||||||
|
|
||||||
if __name__ == "__main__":
|
|
||||||
"""
|
|
||||||
Script emulates htop calculation of CPU at the
|
|
||||||
moment of calling.
|
|
||||||
"""
|
|
||||||
prev = measure_proc_stat()
|
|
||||||
prev_idle = prev.get('idle') + prev.get('iowait')
|
|
||||||
prev_non_idle = prev.get('user') + prev.get('nice') + prev.get('system') + prev.get('irq') + prev.get('softirq') + prev.get('steal')
|
|
||||||
prev_total = prev_idle + prev_non_idle
|
|
||||||
|
|
||||||
time.sleep(0.1)
|
|
||||||
|
|
||||||
curr = measure_proc_stat()
|
|
||||||
curr_idle = curr.get('idle') + curr.get('iowait')
|
|
||||||
curr_non_idle = curr.get('user') + curr.get('nice') + curr.get('system') + curr.get('irq') + curr.get('softirq') + curr.get('steal')
|
|
||||||
curr_total = curr_idle + curr_non_idle
|
|
||||||
|
|
||||||
d_total = curr_total - prev_total
|
|
||||||
d_idle = curr_idle - prev_idle
|
|
||||||
|
|
||||||
cpu_usage = ((d_total - d_idle)/d_total)
|
|
||||||
print(cpu_usage)
|
|
||||||
@ -1,12 +0,0 @@
|
|||||||
#!/usr/bin/env bash
|
|
||||||
|
|
||||||
# Load python interpreter
|
|
||||||
python=/usr/bin/python3
|
|
||||||
# Load python script
|
|
||||||
cpu_usage=relay/cpu_usage.py
|
|
||||||
# Execute python script
|
|
||||||
cpu=$($python $cpu_usage)
|
|
||||||
# Calculate memory usage by computing 1 - %free_memory
|
|
||||||
mem=$(free | sed '2q;d' | awk '{print 1 - ($4/$2)}')
|
|
||||||
|
|
||||||
printf "CPU, MEM\n%f, %f\n" $cpu $mem
|
|
||||||
@ -1 +1 @@
|
|||||||
leanprover/lean4:v4.7.0
|
leanprover/lean4:v4.8.0
|
||||||
|
|||||||
Loading…
Reference in New Issue