Compare commits
2 Commits
main
...
v4.6.0-bum
| Author | SHA1 | Date |
|---|---|---|
Jon Eugster
|
ce739078b9 | 2 years ago |
|
Jon Eugster
|
a671bfa15f | 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,152 +0,0 @@
|
|||||||
const lean4gameConfig = require("./src/config.json")
|
|
||||||
|
|
||||||
const typescriptTransform = require('i18next-scanner-typescript');
|
|
||||||
|
|
||||||
const fs = require('fs');
|
|
||||||
const chalk = require('chalk');
|
|
||||||
const eol = require('eol');
|
|
||||||
const path = require('path');
|
|
||||||
const VirtualFile = require('vinyl');
|
|
||||||
|
|
||||||
function flush(done) {
|
|
||||||
const { parser } = this;
|
|
||||||
const { options } = parser;
|
|
||||||
|
|
||||||
// Flush to resource store
|
|
||||||
const resStore = parser.get({ sort: options.sort });
|
|
||||||
const { jsonIndent } = options.resource;
|
|
||||||
const lineEnding = String(options.resource.lineEnding).toLowerCase();
|
|
||||||
|
|
||||||
Object.keys(resStore).forEach((lng) => {
|
|
||||||
const namespaces = resStore[lng];
|
|
||||||
|
|
||||||
Object.keys(namespaces).forEach((ns) => {
|
|
||||||
const resPath = parser.formatResourceSavePath(lng, ns);
|
|
||||||
let resContent;
|
|
||||||
try {
|
|
||||||
resContent = JSON.parse(
|
|
||||||
fs.readFileSync(
|
|
||||||
fs.realpathSync(path.join('public', 'locales', resPath))
|
|
||||||
).toString('utf-8')
|
|
||||||
);
|
|
||||||
} catch (e) {
|
|
||||||
console.log("no previous translation found!")
|
|
||||||
resContent = {};
|
|
||||||
}
|
|
||||||
const obj = { ...namespaces[ns], ...resContent };
|
|
||||||
let text = JSON.stringify(obj, null, jsonIndent) + '\n';
|
|
||||||
|
|
||||||
if (lineEnding === 'auto') {
|
|
||||||
text = eol.auto(text);
|
|
||||||
} else if (lineEnding === '\r\n' || lineEnding === 'crlf') {
|
|
||||||
text = eol.crlf(text);
|
|
||||||
} else if (lineEnding === '\n' || lineEnding === 'lf') {
|
|
||||||
text = eol.lf(text);
|
|
||||||
} else if (lineEnding === '\r' || lineEnding === 'cr') {
|
|
||||||
text = eol.cr(text);
|
|
||||||
} else { // Defaults to LF
|
|
||||||
text = eol.lf(text);
|
|
||||||
}
|
|
||||||
|
|
||||||
let contents = null;
|
|
||||||
|
|
||||||
try {
|
|
||||||
// "Buffer.from(string[, encoding])" is added in Node.js v5.10.0
|
|
||||||
contents = Buffer.from(text);
|
|
||||||
} catch (e) {
|
|
||||||
// Fallback to "new Buffer(string[, encoding])" which is deprecated since Node.js v6.0.0
|
|
||||||
contents = new Buffer(text);
|
|
||||||
}
|
|
||||||
|
|
||||||
this.push(new VirtualFile({
|
|
||||||
path: resPath,
|
|
||||||
contents: contents
|
|
||||||
}));
|
|
||||||
});
|
|
||||||
});
|
|
||||||
|
|
||||||
done();
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
module.exports = {
|
|
||||||
input: [
|
|
||||||
'client/src/**/*.{tsx,ts}',
|
|
||||||
// Use ! to filter out files or directories
|
|
||||||
'!client/i18n/**',
|
|
||||||
'!**/node_modules/**',
|
|
||||||
],
|
|
||||||
options: {
|
|
||||||
debug: true,
|
|
||||||
removeUnusedKeys: true,
|
|
||||||
func: {
|
|
||||||
list: ['i18next.t', 'i18n.t', 't'],
|
|
||||||
extensions: ['.js', '.jsx'] // not .ts or .tsx since we use i18next-scanner-typescript!
|
|
||||||
},
|
|
||||||
trans: {
|
|
||||||
component: 'Trans',
|
|
||||||
i18nKey: 'i18nKey',
|
|
||||||
defaultsKey: 'defaults',
|
|
||||||
extensions: ['.js', '.jsx'], // not .ts or .tsx since we use i18next-scanner-typescript!
|
|
||||||
fallbackKey: (ns, value) => {return value},
|
|
||||||
|
|
||||||
// https://react.i18next.com/latest/trans-component#usage-with-simple-html-elements-like-less-than-br-greater-than-and-others-v10.4.0
|
|
||||||
supportBasicHtmlNodes: true, // Enables keeping the name of simple nodes (e.g. <br/>) in translations instead of indexed keys.
|
|
||||||
keepBasicHtmlNodesFor: ['br', 'strong', 'i', 'p'], // Which nodes are allowed to be kept in translations during defaultValue generation of <Trans>.
|
|
||||||
|
|
||||||
// // https://github.com/acornjs/acorn/tree/master/acorn#interface
|
|
||||||
// acorn: {
|
|
||||||
// ecmaVersion: 2020,
|
|
||||||
// sourceType: 'module', // defaults to 'module'
|
|
||||||
// }
|
|
||||||
},
|
|
||||||
lngs: lean4gameConfig.languages.map(e => e.iso),
|
|
||||||
ns: [],
|
|
||||||
defaultLng: 'en',
|
|
||||||
defaultNs: 'translation',
|
|
||||||
defaultValue: (lng, ns, key) => {
|
|
||||||
if (lng === 'en') {
|
|
||||||
return key; // Use key as value for base language
|
|
||||||
}
|
|
||||||
return ''; // Return empty string for other languages
|
|
||||||
},
|
|
||||||
resource: {
|
|
||||||
loadPath: './client/public/locales/{{lng}}/{{ns}}.json',
|
|
||||||
savePath: './client/public/locales/{{lng}}/{{ns}}.json',
|
|
||||||
jsonIndent: 2,
|
|
||||||
lineEnding: '\n'
|
|
||||||
},
|
|
||||||
nsSeparator: false, // namespace separator
|
|
||||||
keySeparator: false, // key separator
|
|
||||||
plurals: false,
|
|
||||||
interpolation: {
|
|
||||||
prefix: '{{',
|
|
||||||
suffix: '}}'
|
|
||||||
},
|
|
||||||
metadata: {},
|
|
||||||
allowDynamicKeys: false,
|
|
||||||
},
|
|
||||||
|
|
||||||
transform: typescriptTransform(
|
|
||||||
// options
|
|
||||||
{
|
|
||||||
// default value for extensions
|
|
||||||
extensions: [".ts", ".tsx"],
|
|
||||||
// optional ts configuration
|
|
||||||
tsOptions: {
|
|
||||||
target: "es2017",
|
|
||||||
},
|
|
||||||
},
|
|
||||||
|
|
||||||
function(outputText, file, enc, done) {
|
|
||||||
'use strict';
|
|
||||||
const parser = this.parser;
|
|
||||||
|
|
||||||
parser.parseTransFromString(outputText);
|
|
||||||
parser.parseFuncFromString(outputText);
|
|
||||||
|
|
||||||
done();
|
|
||||||
}
|
|
||||||
),
|
|
||||||
|
|
||||||
};
|
|
||||||
@ -1,99 +0,0 @@
|
|||||||
{
|
|
||||||
"Tactics": "Taktiken",
|
|
||||||
"Lean Game Server": "Lean-Lern-Spiel-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>Die Spielregeln bestimmen ob es erlaubt ist, Levels zu überspringen und ob das Spiel überprüft welche Taktiken und Theoreme freigeschaltet sind und nur diese im Beweis akzeptiert.</p><1>Bemerkung: \"Freigeschaltete\" Taktiken (und Theoreme) werden durch zwei Faktoren bestimmt: The Menge der Taktiken die minimal notwending sind um den Level zu lösen und dazu die Menge aller Taktiken, die in einem anderen Level freigeschaltet wurden. Das bedeutet wenn <1>simp</1> in einem Level freigeschaltet wird, kann diese Taktik danach in jeglichen Levels verwendet werden.",
|
|
||||||
"Game Rules": "Spielregeln",
|
|
||||||
"levels": "Level",
|
|
||||||
"tactics": "Taktiken",
|
|
||||||
"regular": "regulär",
|
|
||||||
"relaxed": "relaxed",
|
|
||||||
"none": "keine",
|
|
||||||
"Rules": "Regeln",
|
|
||||||
"Intro": "Prolog",
|
|
||||||
"Game Introduction": "Prolog",
|
|
||||||
"World selection": "Übersicht",
|
|
||||||
"Start": "Start",
|
|
||||||
"Inventory": "Inventar",
|
|
||||||
"next level": "nächstes Level",
|
|
||||||
"Next": "Weiter",
|
|
||||||
"back to world selection": "Zurück zur Übersicht",
|
|
||||||
"Leave World": "Welt verlassen",
|
|
||||||
"previous level": "voheriges Level",
|
|
||||||
"Previous": "Zurück",
|
|
||||||
"Editor mode is enforced!": "Editor kann nicht verlassen werden!",
|
|
||||||
"Editor mode": "Editor",
|
|
||||||
"Typewriter mode": "Schreibmaschine",
|
|
||||||
"information, Impressum, privacy policy": "Informationen, Impressum, Privacy Policy",
|
|
||||||
"Preferences": "Einstellungen",
|
|
||||||
"Game Info & Credits": "Spielinfo & Credits",
|
|
||||||
"Game Info": "Spielinfo",
|
|
||||||
"Clear Progress": "Spielstand löschen",
|
|
||||||
"Erase": "Löschen",
|
|
||||||
"Download Progress": "Spielstand herunterladen",
|
|
||||||
"Download": "Herunterladen",
|
|
||||||
"Load Progress from JSON": "Spielstand aus JSON laden",
|
|
||||||
"Upload": "Laden",
|
|
||||||
"Home": "Home",
|
|
||||||
"back to games selection": "Zurück zur Spielauswahl",
|
|
||||||
"close inventory": "Inventar schließen",
|
|
||||||
"show inventory": "Inventar öffnen",
|
|
||||||
"World": "Welt",
|
|
||||||
"Show more help!": "Mehr Hilfe",
|
|
||||||
"Goal": "Beweisziel",
|
|
||||||
"Current Goal": "Aktuelles Beweisziel",
|
|
||||||
"Objects": "Objekte",
|
|
||||||
"Assumptions": "Annahmen",
|
|
||||||
"Further Goals": "Weitere Ziele",
|
|
||||||
"No Goals": "Keine Beweisziele",
|
|
||||||
"Loading goal…": "Beweisziel wird geladen…",
|
|
||||||
"Click somewhere in the Lean file to enable the infoview.": "Ein Klick in den Lean-Code aktiviert den Infoview.",
|
|
||||||
"Waiting for Lean server to start…": "Warte auf den Lean-Server …",
|
|
||||||
"Level completed! 🎉": "Level gelöst! 🎉",
|
|
||||||
"Level completed with warnings 🎭": "Level mit Warnungen abgeschlossen 🎭",
|
|
||||||
"Active Goal": "Aktuelles Ziel",
|
|
||||||
"Crashed! Go to editor mode and fix your proof! Last server response:": "Abgestürzt! Wechsle in den Editor-Modus, um deinen Beweis zu repariaeren. Letzte Meldung vom Server:",
|
|
||||||
"Line": "Zeile",
|
|
||||||
"Character": "Charakter",
|
|
||||||
"Loading messages…": "Lade Meldungen …",
|
|
||||||
"Execute": "Ausführen",
|
|
||||||
"Definitions": "Definitionen",
|
|
||||||
"Theorems": "Theoreme",
|
|
||||||
"Not unlocked yet": "Noch nicht verfügbar",
|
|
||||||
"Not available in this level": "In diesem Level nicht verfügbar",
|
|
||||||
"A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "Eine Sammlung von Lernspielen für den Beweisassistenten <1>Lean</1> <i>(Lean 4)</i> und dessen mathematische Bibliothek <5>mathlib</5>",
|
|
||||||
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "Kein Spiel geladen. Öffne <1>http://localhost:3000/#/g/local/FOLDER</1> um ein Spiel direkt aus einem lokalen Ordner zu laden.",
|
|
||||||
"Prerequisites": "Voraussetzungen",
|
|
||||||
"Worlds": "Welten",
|
|
||||||
"Levels": "Level",
|
|
||||||
"Language": "Sprache",
|
|
||||||
"Development notes": "Entwicklungsstand",
|
|
||||||
"Adding new games": "Neue Spiele hinzufügen",
|
|
||||||
"Funding": "Finanzierung",
|
|
||||||
"<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>Soll der Spielstand unwiderruflich gelöscht werden?</p><p>(Dies löscht sämtliche Beweise und das gesammelte Inventar. Spielstände anderer Spiele werden nicht gelöscht.)</p>",
|
|
||||||
"Delete Progress?": "Spielstand löschen?",
|
|
||||||
"Delete": "Löschen",
|
|
||||||
"Download & Delete": "Herunterladen & löschen",
|
|
||||||
"Cancel": "Abbrechen",
|
|
||||||
"Layout": "Seitenlayout",
|
|
||||||
"Always visible": "Immer sichtbar",
|
|
||||||
"Save my settings (in the browser store)": "Einstellungen im Browser speichern.",
|
|
||||||
"<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>Wähle eine JSON-Datei mit einem Spielstand, um diesen zu laden.</p><1><0>Achtung:</0> Deraktuelle Spielstand wird dabei überschrieben! Wenn du noch einmal zum aktuellen Spielstand zurückkehren möchtest, solltest du zunächst den <2>aktuellen Spielstand herunterladen</2>!</1>",
|
|
||||||
"Upload Saved Progress": "Spielstand hochladen",
|
|
||||||
"Load selected file": "Ausgewählte Datei hochladen",
|
|
||||||
"Mobile": "Mobil",
|
|
||||||
"Auto": "Auto",
|
|
||||||
"Desktop": "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>Für alle, die selbst Spiel entwickeln möchten, gibt es ein <1>GameSkeleton Github Repo</1> als Vorlage und die Anleitung <3>How to Create a Game</3>.</0><1>Die <1>Anleitung</1> erklärt auch, wie ein solches Spiel mittels einer passenden URL auf den Sever geladen und gespiel werden kann. Fragen dazu beantworten wir gern.</1><p>Als Kacheln sichtbar ist auf dieser Seite nur eine kuratierte Auswahl an existierenden Spielen. Wir erweitern diese Auswahl auf Anfrage sehr gerne.</p>",
|
|
||||||
"Level": "Level",
|
|
||||||
"Introduction": "Prolog",
|
|
||||||
"Retry proof from here": "Ab hier neu ansetzen",
|
|
||||||
"Retry": "Noch einmal",
|
|
||||||
"Failed command": "Gescheiterter Befehl",
|
|
||||||
"<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>": "Diese Server läuft auf universitäter Infrastruktur mit begrenzten Kapazitäten. Wir schätzen, dass die Belastungsgrenze bei rund 70 gleichzeitig laufenden Spielen besteht.",
|
|
||||||
"<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>": "Der Spieleserver und die alle Spiele befinden sich in fortlaufender Entwicklung. Wir bitten darum, Fehler und Ungereimtheiten als <1>GitHub Issue</1> zu melden.",
|
|
||||||
"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.": "Die Lean-Spiele-Software und dieser Spiele-Server werden als Teils der Projekts <1>ADAM: Anticipating the Digital Age of Mathematics</1> an der Heinrich-Heine-Universität Düsseldorf entwickelt.",
|
|
||||||
"Server capacity": "Server-Auslastung",
|
|
||||||
"RAM": "RAM",
|
|
||||||
" used": "",
|
|
||||||
"CPU": "CPU"
|
|
||||||
}
|
|
||||||
@ -1,99 +0,0 @@
|
|||||||
{
|
|
||||||
"Tactics": "Tactics",
|
|
||||||
"Lean Game Server": "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>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>",
|
|
||||||
"Game Rules": "Game Rules",
|
|
||||||
"levels": "levels",
|
|
||||||
"tactics": "tactics",
|
|
||||||
"regular": "regular",
|
|
||||||
"relaxed": "relaxed",
|
|
||||||
"none": "none",
|
|
||||||
"Rules": "Rules",
|
|
||||||
"Intro": "Intro",
|
|
||||||
"Game Introduction": "Game Introduction",
|
|
||||||
"World selection": "World selection",
|
|
||||||
"Start": "Start",
|
|
||||||
"Inventory": "Inventory",
|
|
||||||
"next level": "next level",
|
|
||||||
"Next": "Next",
|
|
||||||
"back to world selection": "back to world selection",
|
|
||||||
"Leave World": "Leave World",
|
|
||||||
"previous level": "previous level",
|
|
||||||
"Previous": "Previous",
|
|
||||||
"Editor mode is enforced!": "Editor mode is enforced!",
|
|
||||||
"Editor mode": "Editor mode",
|
|
||||||
"Typewriter mode": "Typewriter mode",
|
|
||||||
"information, Impressum, privacy policy": "information, Impressum, privacy policy",
|
|
||||||
"Preferences": "Preferences",
|
|
||||||
"Game Info & Credits": "Game Info & Credits",
|
|
||||||
"Game Info": "Game Info",
|
|
||||||
"Clear Progress": "Clear Progress",
|
|
||||||
"Erase": "Erase",
|
|
||||||
"Download Progress": "Download Progress",
|
|
||||||
"Download": "Download",
|
|
||||||
"Load Progress from JSON": "Load Progress from JSON",
|
|
||||||
"Upload": "Upload",
|
|
||||||
"Home": "Home",
|
|
||||||
"back to games selection": "back to games selection",
|
|
||||||
"close inventory": "close inventory",
|
|
||||||
"show inventory": "show inventory",
|
|
||||||
"World": "World",
|
|
||||||
"Show more help!": "Show more help!",
|
|
||||||
"Goal": "Goal",
|
|
||||||
"Current Goal": "Current Goal",
|
|
||||||
"Objects": "Objects",
|
|
||||||
"Assumptions": "Assumptions",
|
|
||||||
"Further Goals": "Further Goals",
|
|
||||||
"No Goals": "No Goals",
|
|
||||||
"Loading goal…": "Loading goal…",
|
|
||||||
"Click somewhere in the Lean file to enable the infoview.": "Click somewhere in the Lean file to enable the infoview.",
|
|
||||||
"Waiting for Lean server to start…": "Waiting for Lean server to start…",
|
|
||||||
"Level completed! 🎉": "Level completed! 🎉",
|
|
||||||
"Level completed with warnings 🎭": "Level completed with warnings 🎭",
|
|
||||||
"Active Goal": "Active Goal",
|
|
||||||
"Crashed! Go to editor mode and fix your proof! Last server response:": "Crashed! Go to editor mode and fix your proof! Last server response:",
|
|
||||||
"Line": "Line",
|
|
||||||
"Character": "Character",
|
|
||||||
"Loading messages…": "Loading messages…",
|
|
||||||
"Execute": "Execute",
|
|
||||||
"Definitions": "Definitions",
|
|
||||||
"Theorems": "Theorems",
|
|
||||||
"Not unlocked yet": "Not unlocked yet",
|
|
||||||
"Not available in this level": "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>": "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>",
|
|
||||||
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.",
|
|
||||||
"Prerequisites": "Prerequisites",
|
|
||||||
"Worlds": "Worlds",
|
|
||||||
"Levels": "Levels",
|
|
||||||
"Language": "Language",
|
|
||||||
"Server capacity": "Server capacity",
|
|
||||||
"RAM": "RAM",
|
|
||||||
"CPU": "CPU",
|
|
||||||
"Development notes": "Development notes",
|
|
||||||
"Adding new games": "Adding new games",
|
|
||||||
"Funding": "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>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>",
|
|
||||||
"Delete Progress?": "Delete Progress?",
|
|
||||||
"Delete": "Delete",
|
|
||||||
"Download & Delete": "Download & Delete",
|
|
||||||
"Cancel": "Cancel",
|
|
||||||
"Layout": "Layout",
|
|
||||||
"Always visible": "Always visible",
|
|
||||||
"Save my settings (in the browser store)": "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>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>",
|
|
||||||
"Upload Saved Progress": "Upload Saved Progress",
|
|
||||||
"Load selected file": "Load selected file",
|
|
||||||
"Mobile": "Mobile",
|
|
||||||
"Auto": "Auto",
|
|
||||||
"Desktop": "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>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>",
|
|
||||||
"Level": "Level",
|
|
||||||
"Introduction": "Introduction",
|
|
||||||
"Retry proof from here": "Retry proof from here",
|
|
||||||
"Retry": "Retry",
|
|
||||||
"Failed command": "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>": "<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>": "<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.": "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": " used"
|
|
||||||
}
|
|
||||||
@ -1,99 +0,0 @@
|
|||||||
{
|
|
||||||
"Intro": "Introducción",
|
|
||||||
"Game Introduction": "Introducción del juego",
|
|
||||||
"World selection": "Seleccionar mundo",
|
|
||||||
"Start": "Empezar",
|
|
||||||
"Inventory": "Inventario",
|
|
||||||
"next level": "siguiente nivel",
|
|
||||||
"Next": "Siguiente",
|
|
||||||
"back to world selection": "volver a la selección de mundos",
|
|
||||||
"Leave World": "Abandonar mundo",
|
|
||||||
"previous level": "nivel anterior",
|
|
||||||
"Previous": "Anterior",
|
|
||||||
"Editor mode is enforced!": "¡El modo editor es obligatorio!",
|
|
||||||
"Editor mode": "Modo editor",
|
|
||||||
"Typewriter mode": "Modo línea a línea",
|
|
||||||
"information, Impressum, privacy policy": "información, Impressum, política de privacidad",
|
|
||||||
"Preferences": "Preferencias",
|
|
||||||
"Game Info & Credits": "Información del juego y reconocimientos",
|
|
||||||
"Game Info": "Información del juego",
|
|
||||||
"Clear Progress": "Limpiar el progreso",
|
|
||||||
"Erase": "Borrar",
|
|
||||||
"Download Progress": "Descargar progreso",
|
|
||||||
"Download": "Descargar",
|
|
||||||
"Load Progress from JSON": "Cargar progreso desde JSON",
|
|
||||||
"Upload": "Subir",
|
|
||||||
"Home": "Inicio",
|
|
||||||
"back to games selection": "volver a la selección de juegos",
|
|
||||||
"close inventory": "cerrar inventario",
|
|
||||||
"show inventory": "mostrar inventario",
|
|
||||||
"World": "Mundo",
|
|
||||||
"Show more help!": "¡Mostrar más ayuda!",
|
|
||||||
"Goal": "Objetivo",
|
|
||||||
"Objects": "Objetos",
|
|
||||||
"Assumptions": "Hipótesis",
|
|
||||||
"Current Goal": "Objetivo actual",
|
|
||||||
"Further Goals": "Objetivos pendientes",
|
|
||||||
"No Goals": "Sin objetivos",
|
|
||||||
"Loading goal…": "Cargando objetivo…",
|
|
||||||
"Click somewhere in the Lean file to enable the infoview.": "Pulsa en algún lugar del archivo Lean para habilitar la vista de información.",
|
|
||||||
"Waiting for Lean server to start…": "Esperando a que el servidor Lean se inicie…",
|
|
||||||
"Level completed! 🎉": "Nivel completado 🎉",
|
|
||||||
"Level completed with warnings 🎭": "Nivel completado con advertencias 🎭",
|
|
||||||
"Failed command": "Comando fallido",
|
|
||||||
"Retry proof from here": "Reintentar la prueba desde aquí",
|
|
||||||
"Retry": "Reintentar",
|
|
||||||
"Active Goal": "Objetivo activo",
|
|
||||||
"Crashed! Go to editor mode and fix your proof! Last server response:": "¡Error! Vaya al modo editor y corrija su prueba. Última respuesta del servidor:",
|
|
||||||
"Line": "Línea",
|
|
||||||
"Character": "Carácter",
|
|
||||||
"Loading messages…": "Cargando mensajes…",
|
|
||||||
"Execute": "Ejecutar",
|
|
||||||
"Tactics": "Tácticas",
|
|
||||||
"Definitions": "Definiciones",
|
|
||||||
"Theorems": "Teoremas",
|
|
||||||
"Not unlocked yet": "No desbloqueado aún",
|
|
||||||
"Not available in this level": "No disponible en este nivel",
|
|
||||||
"A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "Un repositorio de juegos para aprender el asistente de demostración <1>Lean</1>, <i>(Lean 4)</i> y su biblioteca matemática <5>mathlib</5> ",
|
|
||||||
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "No se ha cargado ningún juego. Use <1>http://localhost:3000/#/g/local/FOLDER</1> para abrir un juego directamente desde una carpeta local",
|
|
||||||
"<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>Si está considerando escribir su propio juego, use el <1>GameSkeleton Github Repo</1> como plantilla y lea <3>How to Create a Game</3>.</0><1>Puede cargar directamente los juegos en el servidor y jugarlo usando la URL adecuada. Las <1>instrucciones anteriores</1> también explican los detalles sobre cómo cargar su juego en el servidor. Le animamos a ponerse en contacto con nosotros si tiene preguntas.</1><p>Los juegos incluidos en esta página son añadidos manualmente. Por favor, contactenos y añadiremos el suyo encantados.</p>",
|
|
||||||
"Prerequisites": "Requisitos previos",
|
|
||||||
"Worlds": "Mundos",
|
|
||||||
"Levels": "Niveles",
|
|
||||||
"Language": "Idioma",
|
|
||||||
"Lean Game Server": "Servidor de Juegos de Lean",
|
|
||||||
"Development notes": "Notas de desarrollo",
|
|
||||||
"Adding new games": "Añadir nuevos juegos",
|
|
||||||
"Funding": "Financiación",
|
|
||||||
"Level": "Nivel",
|
|
||||||
"Introduction": "Introducción",
|
|
||||||
"<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>¿Desea eliminar su progreso guardado definitivamente?</p><p>(Esto elimina sus pruebas y su inventario recopilado. Los progresos guardados de otros juegos no se eliminan.)</p>",
|
|
||||||
"Delete Progress?": "¿Borrar Progreso?",
|
|
||||||
"Delete": "Borrar",
|
|
||||||
"Download & Delete": "Descargar y Borrar",
|
|
||||||
"Cancel": "Cancelar",
|
|
||||||
"Mobile": "Móvil",
|
|
||||||
"Auto": "Automático",
|
|
||||||
"Desktop": "Escritorio",
|
|
||||||
"Layout": "Diseño",
|
|
||||||
"Always visible": "Siempre visible",
|
|
||||||
"Save my settings (in the browser store)": "Guardar mis ajustes (en el almacenamiento del navegador)",
|
|
||||||
"<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>Las reglas del juego determinan si se permite saltarse niveles y si el juego realiza comprobaciones para permitir únicamente tácticas y teoremas desbloqueados en las pruebas.</p><1>Nota: las tácticas (o teoremas) \"Desbloqueadas\" está determinadas por dos cosas: el conjunto mínimo de tácticas necesarias para resolver un nivel, más cualquier táctica que hayas desbloqueado en otro nivel. Esto significa que si desbloqueas <1>simp</1> en un nivel, puedes usarlo a partir de entonces en cualquier nivel.</1><p>Las opciones son:</p>",
|
|
||||||
"Game Rules": "Reglas del juego",
|
|
||||||
"levels": "niveles",
|
|
||||||
"tactics": "tácticas",
|
|
||||||
"regular": "normal",
|
|
||||||
"relaxed": "relajado",
|
|
||||||
"none": "ninguno",
|
|
||||||
"<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>Seleccione un archivo JSON con el progreso del juego guardado para cargar su progreso.</p><1><0>Advertencia:</0> Esto borrará su progreso actual en el juego. Considere <2>descargar su progreso actual</2> antes</1>",
|
|
||||||
"Upload Saved Progress": "Subir progreso guardado",
|
|
||||||
"Load selected file": "Cargar archivo seleccionado",
|
|
||||||
"Rules": "Reglas",
|
|
||||||
"<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>": "<p>Como este servidor corre en máquinas de nuestra universidad, tiene una capacidad limitada. Nuestra estimación actual es de unos 70 juegos simultaneos.</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>": "<1>Muchos aspectos de los juegos y la infrastructura están aún en desarrollo. No dude en abrir una <1>GitHub Issue</1> sobre cualquier problema que experimente.</1>",
|
|
||||||
"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.": "Este servidor se ha desarrollado como parte del proyecto <1>ADAM: Anticipating the Digital Age of Mathematics</1> en la Heinrich-Heine-Universität de Düsseldorf.",
|
|
||||||
"Server capacity": "",
|
|
||||||
"RAM": "",
|
|
||||||
" used": "",
|
|
||||||
"CPU": ""
|
|
||||||
}
|
|
||||||
@ -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,37 +0,0 @@
|
|||||||
{
|
|
||||||
"allGames": [
|
|
||||||
"leanprover-community/nng4",
|
|
||||||
"hhu-adam/robo",
|
|
||||||
"djvelleman/stg4",
|
|
||||||
"trequetrum/lean4game-logic",
|
|
||||||
"jadabouhawili/knightsandknaves-lean4game"
|
|
||||||
],
|
|
||||||
|
|
||||||
"languages": [
|
|
||||||
{
|
|
||||||
"iso": "en",
|
|
||||||
"flag": "GB",
|
|
||||||
"name": "English"
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"iso": "de",
|
|
||||||
"flag": "DE",
|
|
||||||
"name": "Deutsch"
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"iso": "zh",
|
|
||||||
"flag": "CN",
|
|
||||||
"name": "中文"
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"iso": "es",
|
|
||||||
"flag": "ES",
|
|
||||||
"name": "Español"
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"iso": "ko",
|
|
||||||
"flag": "KR",
|
|
||||||
"name": "한국어"
|
|
||||||
}
|
|
||||||
]
|
|
||||||
}
|
|
||||||
@ -1,35 +0,0 @@
|
|||||||
import i18n from "i18next";
|
|
||||||
import Backend from "i18next-http-backend"
|
|
||||||
import { initReactI18next } from "react-i18next";
|
|
||||||
|
|
||||||
i18n
|
|
||||||
.use(initReactI18next)
|
|
||||||
.use(Backend)
|
|
||||||
.init({
|
|
||||||
ns: ['translation'],
|
|
||||||
backend: {
|
|
||||||
// > see https://github.com/i18next/i18next-http-backend
|
|
||||||
loadPath: function(lngs, namespaces: Array<string>) {
|
|
||||||
if (namespaces[0].startsWith("g/")) {
|
|
||||||
return '/i18n/{{ns}}/{{lng}}/Game.json';
|
|
||||||
} else {
|
|
||||||
return '/locales/{{lng}}/{{ns}}.json';
|
|
||||||
}
|
|
||||||
}
|
|
||||||
},
|
|
||||||
// > language to use, more information here:
|
|
||||||
// > https://www.i18next.com/overview/configuration-options#languages-namespaces-resources
|
|
||||||
lng: "en",
|
|
||||||
// we use natural language keys, so we don't need a fallback language.
|
|
||||||
fallbackLng: false,
|
|
||||||
// > you can use the i18n.changeLanguage function to change the language manually:
|
|
||||||
// > https://www.i18next.com/overview/api#changelanguage
|
|
||||||
// > if you're using a language detector, do not define the lng option
|
|
||||||
returnEmptyString: false,
|
|
||||||
interpolation: {
|
|
||||||
// > react already safes from xss
|
|
||||||
escapeValue: false
|
|
||||||
}
|
|
||||||
});
|
|
||||||
|
|
||||||
export default i18n;
|
|
||||||
@ -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,30 +0,0 @@
|
|||||||
# Translation
|
|
||||||
|
|
||||||
The game server supports internationalisation ("i18n") using [lean-i18n](https://github.com/hhu-adam/lean-i18n) and [i18next](https://www.npmjs.com/package/i18next).
|
|
||||||
|
|
||||||
The intended workflow currently is the following:
|
|
||||||
|
|
||||||
1. When you call `lake build` in your game, it should automatically create a template file `.i18n/en/Game.pot`. Alternatively you can call `lake exe i18n --template` to recreate it.
|
|
||||||
2. Open the file `Game.pot` (the "t" stands for "template") with [Poedit](https://poedit.net/) (or a similar software) and translate all strings. Save your work as `.i18n/{language}/Game.po`.
|
|
||||||
4. Call `lake exe i18n --export-json` to create all Json files `.i18n/{language}/Game.json` which the server needs.
|
|
||||||
5. Add your translations (i.e. `.po` and `.json`, but not the `.mo` files) and push your results, and [publish the game](publish_game.md).
|
|
||||||
|
|
||||||
If you choose the correct language in the "Preferences" of the game, you should see your translations.
|
|
||||||
|
|
||||||
## Alternative: avoiding .po
|
|
||||||
|
|
||||||
Note: This workflow is subject to change, and it might be that in future the server can directly read `.po` files. Until then, there is also an alternative workflow you might choose:
|
|
||||||
|
|
||||||
0. Add `useJson: true` to `.i18n/config.json`
|
|
||||||
1. `lake build` or `lake exe i18n --template` will now create a Json instead: `.i18n/en/Game.json`.
|
|
||||||
2. Add translations to a copy of this Json an save it as `.i18n/{language}/Game.json`
|
|
||||||
|
|
||||||
## Non-English games
|
|
||||||
|
|
||||||
For games written in a language different than English, you should set the correct source language (`sourceLang`) in `.i18n/config.json`. Afterwards, on `lake build` the template should appear under the chosen language, and can be translated (e.g. into English) as described above.
|
|
||||||
|
|
||||||
## New languages
|
|
||||||
|
|
||||||
The server has a set number of languages one can select.
|
|
||||||
If your game has been translated to a language not selectable, [open an issue at lean4game](https://github.com/leanprover-community/lean4game/issues) requesting this new language.
|
|
||||||
Or, even better, create a PR to translate the [server interface](https://github.com/leanprover-community/lean4game/tree/main/client/public/locales) into that new language.
|
|
||||||
@ -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,54 +0,0 @@
|
|||||||
import GameServer.AbstractCtx
|
|
||||||
|
|
||||||
/-!
|
|
||||||
This file contains anything related to the `Hint` tactic used to add hints to a game level.
|
|
||||||
-/
|
|
||||||
|
|
||||||
open Lean Meta Elab
|
|
||||||
|
|
||||||
namespace GameServer
|
|
||||||
|
|
||||||
syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
|
|
||||||
|
|
||||||
/-- A hint to help the user with a specific goal state -/
|
|
||||||
structure GoalHintEntry where
|
|
||||||
goal : AbstractCtxResult
|
|
||||||
/-- Text of the hint as an expression of type `Array Expr → MessageData` -/
|
|
||||||
text : Expr
|
|
||||||
rawText : String
|
|
||||||
/-- If true, then hint should be hidden and only be shown on player's request -/
|
|
||||||
hidden : Bool := false
|
|
||||||
/-- If true, then the goal must contain only the assumptions specified in `goal` and no others -/
|
|
||||||
strict : Bool := false
|
|
||||||
|
|
||||||
instance : Repr GoalHintEntry := {
|
|
||||||
reprPrec := fun a n => reprPrec a.text n
|
|
||||||
}
|
|
||||||
|
|
||||||
/-- For a hint `(hint : GoalHintEntry)` one uses `(← evalHintMessage hint.text) x`
|
|
||||||
where `(x : Array Expr)` contains the names of all the variables that should be inserted
|
|
||||||
in the text.
|
|
||||||
|
|
||||||
TODO: explain better. -/
|
|
||||||
unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
|
|
||||||
evalExpr (Array Expr → MessageData)
|
|
||||||
(.forallE default (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr))
|
|
||||||
(mkConst ``MessageData) .default)
|
|
||||||
|
|
||||||
@[implemented_by evalHintMessageUnsafe]
|
|
||||||
def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pure (fun _ => "")
|
|
||||||
|
|
||||||
/-- Remove any spaces at the beginning of a new line -/
|
|
||||||
partial def removeIndentation (s : String) : String :=
|
|
||||||
let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
|
|
||||||
let c := s.get i
|
|
||||||
let i := s.next i
|
|
||||||
if s.atEnd i then
|
|
||||||
acc.push c
|
|
||||||
else if removeSpaces && c == ' ' then
|
|
||||||
loop i acc (removeSpaces := true)
|
|
||||||
else if c == '\n' then
|
|
||||||
loop i (acc.push c) (removeSpaces := true)
|
|
||||||
else
|
|
||||||
loop i (acc.push c)
|
|
||||||
loop ⟨0⟩ ""
|
|
||||||
@ -1 +1 @@
|
|||||||
leanprover/lean4:v4.7.0
|
leanprover/lean4:v4.6.0-rc1
|
||||||
|
|||||||
@ -1,17 +0,0 @@
|
|||||||
import GameServer.Tactic.LetIntros
|
|
||||||
|
|
||||||
set_option linter.unusedVariables false in
|
|
||||||
|
|
||||||
example (f : Nat) :
|
|
||||||
let f := fun x ↦ x + 1
|
|
||||||
let g : Nat → Nat := fun y ↦ y
|
|
||||||
∀ x : Nat, x ≤ f x := by
|
|
||||||
let_intros
|
|
||||||
/-
|
|
||||||
f✝ : Nat
|
|
||||||
f : Nat → Nat := fun x => x + 1
|
|
||||||
g : Nat → Nat := fun y => y
|
|
||||||
⊢ ∀ (x : Nat), x ≤ f x
|
|
||||||
-/
|
|
||||||
intro x
|
|
||||||
exact Nat.le_succ x
|
|
||||||
Loading…
Reference in New Issue