From cd1d212a3c64308724b42af7ae2f0fbe162fc6e2 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 10 Jan 2024 15:40:57 +0100 Subject: [PATCH 01/16] npm audit --- package-lock.json | 448 +++++++++++++++++++++------------------------- package.json | 2 +- 2 files changed, 209 insertions(+), 241 deletions(-) diff --git a/package-lock.json b/package-lock.json index 7f459aa..ab1e455 100644 --- a/package-lock.json +++ b/package-lock.json @@ -32,7 +32,7 @@ "express": "^4.18.2", "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c", "lean4web": "github:hhu-adam/lean4web#b91645a7b88814675ba9f99817436d0a2ce3a0ec", - "octokit": "^2.0.14", + "octokit": "^3.1.2", "path-browserify": "^1.0.1", "react": "^18.2.0", "react-dom": "^18.2.0", @@ -2843,341 +2843,335 @@ } }, "node_modules/@octokit/app": { - "version": "13.1.8", - "resolved": "https://registry.npmjs.org/@octokit/app/-/app-13.1.8.tgz", - "integrity": "sha512-bCncePMguVyFpdBbnceFKfmPOuUD94T189GuQ0l00ZcQ+mX4hyPqnaWJlsXE2HSdA71eV7p8GPDZ+ErplTkzow==", + "version": "14.0.2", + "resolved": "https://registry.npmjs.org/@octokit/app/-/app-14.0.2.tgz", + "integrity": "sha512-NCSCktSx+XmjuSUVn2dLfqQ9WIYePGP95SDJs4I9cn/0ZkeXcPkaoCLl64Us3dRKL2ozC7hArwze5Eu+/qt1tg==", "dependencies": { - "@octokit/auth-app": "^4.0.13", - "@octokit/auth-unauthenticated": "^3.0.0", - "@octokit/core": "^4.0.0", - "@octokit/oauth-app": "^4.0.7", - "@octokit/plugin-paginate-rest": "^6.0.0", - "@octokit/types": "^9.0.0", - "@octokit/webhooks": "^10.0.0" + "@octokit/auth-app": "^6.0.0", + "@octokit/auth-unauthenticated": "^5.0.0", + "@octokit/core": "^5.0.0", + "@octokit/oauth-app": "^6.0.0", + "@octokit/plugin-paginate-rest": "^9.0.0", + "@octokit/types": "^12.0.0", + "@octokit/webhooks": "^12.0.4" }, "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/auth-app": { - "version": "4.0.13", - "resolved": "https://registry.npmjs.org/@octokit/auth-app/-/auth-app-4.0.13.tgz", - "integrity": "sha512-NBQkmR/Zsc+8fWcVIFrwDgNXS7f4XDrkd9LHdi9DPQw1NdGHLviLzRO2ZBwTtepnwHXW5VTrVU9eFGijMUqllg==", - "dependencies": { - "@octokit/auth-oauth-app": "^5.0.0", - "@octokit/auth-oauth-user": "^2.0.0", - "@octokit/request": "^6.0.0", - "@octokit/request-error": "^3.0.0", - "@octokit/types": "^9.0.0", + "version": "6.0.3", + "resolved": "https://registry.npmjs.org/@octokit/auth-app/-/auth-app-6.0.3.tgz", + "integrity": "sha512-9N7IlBAKEJR3tJgPSubCxIDYGXSdc+2xbkjYpk9nCyqREnH8qEMoMhiEB1WgoA9yTFp91El92XNXAi+AjuKnfw==", + "dependencies": { + "@octokit/auth-oauth-app": "^7.0.0", + "@octokit/auth-oauth-user": "^4.0.0", + "@octokit/request": "^8.0.2", + "@octokit/request-error": "^5.0.0", + "@octokit/types": "^12.0.0", "deprecation": "^2.3.1", - "lru-cache": "^9.0.0", - "universal-github-app-jwt": "^1.1.1", + "lru-cache": "^10.0.0", + "universal-github-app-jwt": "^1.1.2", "universal-user-agent": "^6.0.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/auth-app/node_modules/lru-cache": { - "version": "9.1.2", - "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-9.1.2.tgz", - "integrity": "sha512-ERJq3FOzJTxBbFjZ7iDs+NiK4VI9Wz+RdrrAB8dio1oV+YvdPzUEE4QNiT2VD51DkIbCYRUUzCRkssXCHqSnKQ==", + "version": "10.1.0", + "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-10.1.0.tgz", + "integrity": "sha512-/1clY/ui8CzjKFyjdvwPWJUYKiFVXG2I2cY0ssG7h4+hwk+XOIX7ZSG9Q7TW8TW3Kp3BUSqgFWBLgL4PJ+Blag==", "engines": { "node": "14 || >=16.14" } }, "node_modules/@octokit/auth-oauth-app": { - "version": "5.0.6", - "resolved": "https://registry.npmjs.org/@octokit/auth-oauth-app/-/auth-oauth-app-5.0.6.tgz", - "integrity": "sha512-SxyfIBfeFcWd9Z/m1xa4LENTQ3l1y6Nrg31k2Dcb1jS5ov7pmwMJZ6OGX8q3K9slRgVpeAjNA1ipOAMHkieqyw==", - "dependencies": { - "@octokit/auth-oauth-device": "^4.0.0", - "@octokit/auth-oauth-user": "^2.0.0", - "@octokit/request": "^6.0.0", - "@octokit/types": "^9.0.0", + "version": "7.0.1", + "resolved": "https://registry.npmjs.org/@octokit/auth-oauth-app/-/auth-oauth-app-7.0.1.tgz", + "integrity": "sha512-RE0KK0DCjCHXHlQBoubwlLijXEKfhMhKm9gO56xYvFmP1QTMb+vvwRPmQLLx0V+5AvV9N9I3lr1WyTzwL3rMDg==", + "dependencies": { + "@octokit/auth-oauth-device": "^6.0.0", + "@octokit/auth-oauth-user": "^4.0.0", + "@octokit/request": "^8.0.2", + "@octokit/types": "^12.0.0", "@types/btoa-lite": "^1.0.0", "btoa-lite": "^1.0.0", "universal-user-agent": "^6.0.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/auth-oauth-device": { - "version": "4.0.5", - "resolved": "https://registry.npmjs.org/@octokit/auth-oauth-device/-/auth-oauth-device-4.0.5.tgz", - "integrity": "sha512-XyhoWRTzf2ZX0aZ52a6Ew5S5VBAfwwx1QnC2Np6Et3MWQpZjlREIcbcvVZtkNuXp6Z9EeiSLSDUqm3C+aMEHzQ==", + "version": "6.0.1", + "resolved": "https://registry.npmjs.org/@octokit/auth-oauth-device/-/auth-oauth-device-6.0.1.tgz", + "integrity": "sha512-yxU0rkL65QkjbqQedgVx3gmW7YM5fF+r5uaSj9tM/cQGVqloXcqP2xK90eTyYvl29arFVCW8Vz4H/t47mL0ELw==", "dependencies": { - "@octokit/oauth-methods": "^2.0.0", - "@octokit/request": "^6.0.0", - "@octokit/types": "^9.0.0", + "@octokit/oauth-methods": "^4.0.0", + "@octokit/request": "^8.0.0", + "@octokit/types": "^12.0.0", "universal-user-agent": "^6.0.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/auth-oauth-user": { - "version": "2.1.2", - "resolved": "https://registry.npmjs.org/@octokit/auth-oauth-user/-/auth-oauth-user-2.1.2.tgz", - "integrity": "sha512-kkRqNmFe7s5GQcojE3nSlF+AzYPpPv7kvP/xYEnE57584pixaFBH8Vovt+w5Y3E4zWUEOxjdLItmBTFAWECPAg==", + "version": "4.0.1", + "resolved": "https://registry.npmjs.org/@octokit/auth-oauth-user/-/auth-oauth-user-4.0.1.tgz", + "integrity": "sha512-N94wWW09d0hleCnrO5wt5MxekatqEJ4zf+1vSe8MKMrhZ7gAXKFOKrDEZW2INltvBWJCyDUELgGRv8gfErH1Iw==", "dependencies": { - "@octokit/auth-oauth-device": "^4.0.0", - "@octokit/oauth-methods": "^2.0.0", - "@octokit/request": "^6.0.0", - "@octokit/types": "^9.0.0", + "@octokit/auth-oauth-device": "^6.0.0", + "@octokit/oauth-methods": "^4.0.0", + "@octokit/request": "^8.0.2", + "@octokit/types": "^12.0.0", "btoa-lite": "^1.0.0", "universal-user-agent": "^6.0.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/auth-token": { - "version": "3.0.4", - "resolved": "https://registry.npmjs.org/@octokit/auth-token/-/auth-token-3.0.4.tgz", - "integrity": "sha512-TWFX7cZF2LXoCvdmJWY7XVPi74aSY0+FfBZNSXEXFkMpjcqsQwDSYVv5FhRFaI0V1ECnwbz4j59T/G+rXNWaIQ==", + "version": "4.0.0", + "resolved": "https://registry.npmjs.org/@octokit/auth-token/-/auth-token-4.0.0.tgz", + "integrity": "sha512-tY/msAuJo6ARbK6SPIxZrPBms3xPbfwBrulZe0Wtr/DIY9lje2HeV1uoebShn6mx7SjCHif6EjMvoREj+gZ+SA==", "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/auth-unauthenticated": { - "version": "3.0.5", - "resolved": "https://registry.npmjs.org/@octokit/auth-unauthenticated/-/auth-unauthenticated-3.0.5.tgz", - "integrity": "sha512-yH2GPFcjrTvDWPwJWWCh0tPPtTL5SMgivgKPA+6v/XmYN6hGQkAto8JtZibSKOpf8ipmeYhLNWQ2UgW0GYILCw==", + "version": "5.0.1", + "resolved": "https://registry.npmjs.org/@octokit/auth-unauthenticated/-/auth-unauthenticated-5.0.1.tgz", + "integrity": "sha512-oxeWzmBFxWd+XolxKTc4zr+h3mt+yofn4r7OfoIkR/Cj/o70eEGmPsFbueyJE2iBAGpjgTnEOKM3pnuEGVmiqg==", "dependencies": { - "@octokit/request-error": "^3.0.0", - "@octokit/types": "^9.0.0" + "@octokit/request-error": "^5.0.0", + "@octokit/types": "^12.0.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/core": { - "version": "4.2.4", - "resolved": "https://registry.npmjs.org/@octokit/core/-/core-4.2.4.tgz", - "integrity": "sha512-rYKilwgzQ7/imScn3M9/pFfUf4I1AZEH3KhyJmtPdE2zfaXAn2mFfUy4FbKewzc2We5y/LlKLj36fWJLKC2SIQ==", - "dependencies": { - "@octokit/auth-token": "^3.0.0", - "@octokit/graphql": "^5.0.0", - "@octokit/request": "^6.0.0", - "@octokit/request-error": "^3.0.0", - "@octokit/types": "^9.0.0", + "version": "5.0.2", + "resolved": "https://registry.npmjs.org/@octokit/core/-/core-5.0.2.tgz", + "integrity": "sha512-cZUy1gUvd4vttMic7C0lwPed8IYXWYp8kHIMatyhY8t8n3Cpw2ILczkV5pGMPqef7v0bLo0pOHrEHarsau2Ydg==", + "dependencies": { + "@octokit/auth-token": "^4.0.0", + "@octokit/graphql": "^7.0.0", + "@octokit/request": "^8.0.2", + "@octokit/request-error": "^5.0.0", + "@octokit/types": "^12.0.0", "before-after-hook": "^2.2.0", "universal-user-agent": "^6.0.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/endpoint": { - "version": "7.0.6", - "resolved": "https://registry.npmjs.org/@octokit/endpoint/-/endpoint-7.0.6.tgz", - "integrity": "sha512-5L4fseVRUsDFGR00tMWD/Trdeeihn999rTMGRMC1G/Ldi1uWlWJzI98H4Iak5DB/RVvQuyMYKqSK/R6mbSOQyg==", + "version": "9.0.4", + "resolved": "https://registry.npmjs.org/@octokit/endpoint/-/endpoint-9.0.4.tgz", + "integrity": "sha512-DWPLtr1Kz3tv8L0UvXTDP1fNwM0S+z6EJpRcvH66orY6Eld4XBMCSYsaWp4xIm61jTWxK68BrR7ibO+vSDnZqw==", "dependencies": { - "@octokit/types": "^9.0.0", - "is-plain-object": "^5.0.0", + "@octokit/types": "^12.0.0", "universal-user-agent": "^6.0.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/graphql": { - "version": "5.0.6", - "resolved": "https://registry.npmjs.org/@octokit/graphql/-/graphql-5.0.6.tgz", - "integrity": "sha512-Fxyxdy/JH0MnIB5h+UQ3yCoh1FG4kWXfFKkpWqjZHw/p+Kc8Y44Hu/kCgNBT6nU1shNumEchmW/sUO1JuQnPcw==", + "version": "7.0.2", + "resolved": "https://registry.npmjs.org/@octokit/graphql/-/graphql-7.0.2.tgz", + "integrity": "sha512-OJ2iGMtj5Tg3s6RaXH22cJcxXRi7Y3EBqbHTBRq+PQAqfaS8f/236fUrWhfSn8P4jovyzqucxme7/vWSSZBX2Q==", "dependencies": { - "@octokit/request": "^6.0.0", - "@octokit/types": "^9.0.0", + "@octokit/request": "^8.0.1", + "@octokit/types": "^12.0.0", "universal-user-agent": "^6.0.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/oauth-app": { - "version": "4.2.4", - "resolved": "https://registry.npmjs.org/@octokit/oauth-app/-/oauth-app-4.2.4.tgz", - "integrity": "sha512-iuOVFrmm5ZKNavRtYu5bZTtmlKLc5uVgpqTfMEqYYf2OkieV6VdxKZAb5qLVdEPL8LU2lMWcGpavPBV835cgoA==", - "dependencies": { - "@octokit/auth-oauth-app": "^5.0.0", - "@octokit/auth-oauth-user": "^2.0.0", - "@octokit/auth-unauthenticated": "^3.0.0", - "@octokit/core": "^4.0.0", - "@octokit/oauth-authorization-url": "^5.0.0", - "@octokit/oauth-methods": "^2.0.0", + "version": "6.0.0", + "resolved": "https://registry.npmjs.org/@octokit/oauth-app/-/oauth-app-6.0.0.tgz", + "integrity": "sha512-bNMkS+vJ6oz2hCyraT9ZfTpAQ8dZNqJJQVNaKjPLx4ue5RZiFdU1YWXguOPR8AaSHS+lKe+lR3abn2siGd+zow==", + "dependencies": { + "@octokit/auth-oauth-app": "^7.0.0", + "@octokit/auth-oauth-user": "^4.0.0", + "@octokit/auth-unauthenticated": "^5.0.0", + "@octokit/core": "^5.0.0", + "@octokit/oauth-authorization-url": "^6.0.2", + "@octokit/oauth-methods": "^4.0.0", "@types/aws-lambda": "^8.10.83", - "fromentries": "^1.3.1", "universal-user-agent": "^6.0.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/oauth-authorization-url": { - "version": "5.0.0", - "resolved": "https://registry.npmjs.org/@octokit/oauth-authorization-url/-/oauth-authorization-url-5.0.0.tgz", - "integrity": "sha512-y1WhN+ERDZTh0qZ4SR+zotgsQUE1ysKnvBt1hvDRB2WRzYtVKQjn97HEPzoehh66Fj9LwNdlZh+p6TJatT0zzg==", + "version": "6.0.2", + "resolved": "https://registry.npmjs.org/@octokit/oauth-authorization-url/-/oauth-authorization-url-6.0.2.tgz", + "integrity": "sha512-CdoJukjXXxqLNK4y/VOiVzQVjibqoj/xHgInekviUJV73y/BSIcwvJ/4aNHPBPKcPWFnd4/lO9uqRV65jXhcLA==", "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/oauth-methods": { - "version": "2.0.6", - "resolved": "https://registry.npmjs.org/@octokit/oauth-methods/-/oauth-methods-2.0.6.tgz", - "integrity": "sha512-l9Uml2iGN2aTWLZcm8hV+neBiFXAQ9+3sKiQe/sgumHlL6HDg0AQ8/l16xX/5jJvfxueqTW5CWbzd0MjnlfHZw==", + "version": "4.0.1", + "resolved": "https://registry.npmjs.org/@octokit/oauth-methods/-/oauth-methods-4.0.1.tgz", + "integrity": "sha512-1NdTGCoBHyD6J0n2WGXg9+yDLZrRNZ0moTEex/LSPr49m530WNKcCfXDghofYptr3st3eTii+EHoG5k/o+vbtw==", "dependencies": { - "@octokit/oauth-authorization-url": "^5.0.0", - "@octokit/request": "^6.2.3", - "@octokit/request-error": "^3.0.3", - "@octokit/types": "^9.0.0", + "@octokit/oauth-authorization-url": "^6.0.2", + "@octokit/request": "^8.0.2", + "@octokit/request-error": "^5.0.0", + "@octokit/types": "^12.0.0", "btoa-lite": "^1.0.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/openapi-types": { - "version": "18.1.1", - "resolved": "https://registry.npmjs.org/@octokit/openapi-types/-/openapi-types-18.1.1.tgz", - "integrity": "sha512-VRaeH8nCDtF5aXWnjPuEMIYf1itK/s3JYyJcWFJT8X9pSNnBtriDf7wlEWsGuhPLl4QIH4xM8fqTXDwJ3Mu6sw==" + "version": "19.1.0", + "resolved": "https://registry.npmjs.org/@octokit/openapi-types/-/openapi-types-19.1.0.tgz", + "integrity": "sha512-6G+ywGClliGQwRsjvqVYpklIfa7oRPA0vyhPQG/1Feh+B+wU0vGH1JiJ5T25d3g1JZYBHzR2qefLi9x8Gt+cpw==" + }, + "node_modules/@octokit/plugin-paginate-graphql": { + "version": "4.0.0", + "resolved": "https://registry.npmjs.org/@octokit/plugin-paginate-graphql/-/plugin-paginate-graphql-4.0.0.tgz", + "integrity": "sha512-7HcYW5tP7/Z6AETAPU14gp5H5KmCPT3hmJrS/5tO7HIgbwenYmgw4OY9Ma54FDySuxMwD+wsJlxtuGWwuZuItA==", + "engines": { + "node": ">= 18" + }, + "peerDependencies": { + "@octokit/core": ">=5" + } }, "node_modules/@octokit/plugin-paginate-rest": { - "version": "6.1.2", - "resolved": "https://registry.npmjs.org/@octokit/plugin-paginate-rest/-/plugin-paginate-rest-6.1.2.tgz", - "integrity": "sha512-qhrmtQeHU/IivxucOV1bbI/xZyC/iOBhclokv7Sut5vnejAIAEXVcGQeRpQlU39E0WwK9lNvJHphHri/DB6lbQ==", + "version": "9.1.5", + "resolved": "https://registry.npmjs.org/@octokit/plugin-paginate-rest/-/plugin-paginate-rest-9.1.5.tgz", + "integrity": "sha512-WKTQXxK+bu49qzwv4qKbMMRXej1DU2gq017euWyKVudA6MldaSSQuxtz+vGbhxV4CjxpUxjZu6rM2wfc1FiWVg==", "dependencies": { - "@octokit/tsconfig": "^1.0.2", - "@octokit/types": "^9.2.3" + "@octokit/types": "^12.4.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" }, "peerDependencies": { - "@octokit/core": ">=4" + "@octokit/core": ">=5" } }, "node_modules/@octokit/plugin-rest-endpoint-methods": { - "version": "7.2.3", - "resolved": "https://registry.npmjs.org/@octokit/plugin-rest-endpoint-methods/-/plugin-rest-endpoint-methods-7.2.3.tgz", - "integrity": "sha512-I5Gml6kTAkzVlN7KCtjOM+Ruwe/rQppp0QU372K1GP7kNOYEKe8Xn5BW4sE62JAHdwpq95OQK/qGNyKQMUzVgA==", + "version": "10.2.0", + "resolved": "https://registry.npmjs.org/@octokit/plugin-rest-endpoint-methods/-/plugin-rest-endpoint-methods-10.2.0.tgz", + "integrity": "sha512-ePbgBMYtGoRNXDyKGvr9cyHjQ163PbwD0y1MkDJCpkO2YH4OeXX40c4wYHKikHGZcpGPbcRLuy0unPUuafco8Q==", "dependencies": { - "@octokit/types": "^10.0.0" + "@octokit/types": "^12.3.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" }, "peerDependencies": { - "@octokit/core": ">=3" - } - }, - "node_modules/@octokit/plugin-rest-endpoint-methods/node_modules/@octokit/types": { - "version": "10.0.0", - "resolved": "https://registry.npmjs.org/@octokit/types/-/types-10.0.0.tgz", - "integrity": "sha512-Vm8IddVmhCgU1fxC1eyinpwqzXPEYu0NrYzD3YZjlGjyftdLBTeqNblRC0jmJmgxbJIsQlyogVeGnrNaaMVzIg==", - "dependencies": { - "@octokit/openapi-types": "^18.0.0" + "@octokit/core": ">=5" } }, "node_modules/@octokit/plugin-retry": { - "version": "4.1.6", - "resolved": "https://registry.npmjs.org/@octokit/plugin-retry/-/plugin-retry-4.1.6.tgz", - "integrity": "sha512-obkYzIgEC75r8+9Pnfiiqy3y/x1bc3QLE5B7qvv9wi9Kj0R5tGQFC6QMBg1154WQ9lAVypuQDGyp3hNpp15gQQ==", + "version": "6.0.1", + "resolved": "https://registry.npmjs.org/@octokit/plugin-retry/-/plugin-retry-6.0.1.tgz", + "integrity": "sha512-SKs+Tz9oj0g4p28qkZwl/topGcb0k0qPNX/i7vBKmDsjoeqnVfFUquqrE/O9oJY7+oLzdCtkiWSXLpLjvl6uog==", "dependencies": { - "@octokit/types": "^9.0.0", + "@octokit/request-error": "^5.0.0", + "@octokit/types": "^12.0.0", "bottleneck": "^2.15.3" }, "engines": { - "node": ">= 14" + "node": ">= 18" }, "peerDependencies": { - "@octokit/core": ">=3" + "@octokit/core": ">=5" } }, "node_modules/@octokit/plugin-throttling": { - "version": "5.2.3", - "resolved": "https://registry.npmjs.org/@octokit/plugin-throttling/-/plugin-throttling-5.2.3.tgz", - "integrity": "sha512-C9CFg9mrf6cugneKiaI841iG8DOv6P5XXkjmiNNut+swePxQ7RWEdAZRp5rJoE1hjsIqiYcKa/ZkOQ+ujPI39Q==", + "version": "8.1.3", + "resolved": "https://registry.npmjs.org/@octokit/plugin-throttling/-/plugin-throttling-8.1.3.tgz", + "integrity": "sha512-pfyqaqpc0EXh5Cn4HX9lWYsZ4gGbjnSmUILeu4u2gnuM50K/wIk9s1Pxt3lVeVwekmITgN/nJdoh43Ka+vye8A==", "dependencies": { - "@octokit/types": "^9.0.0", + "@octokit/types": "^12.2.0", "bottleneck": "^2.15.3" }, "engines": { - "node": ">= 14" + "node": ">= 18" }, "peerDependencies": { - "@octokit/core": "^4.0.0" + "@octokit/core": "^5.0.0" } }, "node_modules/@octokit/request": { - "version": "6.2.8", - "resolved": "https://registry.npmjs.org/@octokit/request/-/request-6.2.8.tgz", - "integrity": "sha512-ow4+pkVQ+6XVVsekSYBzJC0VTVvh/FCTUUgTsboGq+DTeWdyIFV8WSCdo0RIxk6wSkBTHqIK1mYuY7nOBXOchw==", - "dependencies": { - "@octokit/endpoint": "^7.0.0", - "@octokit/request-error": "^3.0.0", - "@octokit/types": "^9.0.0", - "is-plain-object": "^5.0.0", - "node-fetch": "^2.6.7", + "version": "8.1.6", + "resolved": "https://registry.npmjs.org/@octokit/request/-/request-8.1.6.tgz", + "integrity": "sha512-YhPaGml3ncZC1NfXpP3WZ7iliL1ap6tLkAp6MvbK2fTTPytzVUyUesBBogcdMm86uRYO5rHaM1xIWxigWZ17MQ==", + "dependencies": { + "@octokit/endpoint": "^9.0.0", + "@octokit/request-error": "^5.0.0", + "@octokit/types": "^12.0.0", "universal-user-agent": "^6.0.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/request-error": { - "version": "3.0.3", - "resolved": "https://registry.npmjs.org/@octokit/request-error/-/request-error-3.0.3.tgz", - "integrity": "sha512-crqw3V5Iy2uOU5Np+8M/YexTlT8zxCfI+qu+LxUB7SZpje4Qmx3mub5DfEKSO8Ylyk0aogi6TYdf6kxzh2BguQ==", + "version": "5.0.1", + "resolved": "https://registry.npmjs.org/@octokit/request-error/-/request-error-5.0.1.tgz", + "integrity": "sha512-X7pnyTMV7MgtGmiXBwmO6M5kIPrntOXdyKZLigNfQWSEQzVxR4a4vo49vJjTWX70mPndj8KhfT4Dx+2Ng3vnBQ==", "dependencies": { - "@octokit/types": "^9.0.0", + "@octokit/types": "^12.0.0", "deprecation": "^2.0.0", "once": "^1.4.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" } }, - "node_modules/@octokit/tsconfig": { - "version": "1.0.2", - "resolved": "https://registry.npmjs.org/@octokit/tsconfig/-/tsconfig-1.0.2.tgz", - "integrity": "sha512-I0vDR0rdtP8p2lGMzvsJzbhdOWy405HcGovrspJ8RRibHnyRgggUSNO5AIox5LmqiwmatHKYsvj6VGFHkqS7lA==" - }, "node_modules/@octokit/types": { - "version": "9.3.2", - "resolved": "https://registry.npmjs.org/@octokit/types/-/types-9.3.2.tgz", - "integrity": "sha512-D4iHGTdAnEEVsB8fl95m1hiz7D5YiRdQ9b/OEb3BYRVwbLsGHcRVPz+u+BgRLNk0Q0/4iZCBqDN96j2XNxfXrA==", + "version": "12.4.0", + "resolved": "https://registry.npmjs.org/@octokit/types/-/types-12.4.0.tgz", + "integrity": "sha512-FLWs/AvZllw/AGVs+nJ+ELCDZZJk+kY0zMen118xhL2zD0s1etIUHm1odgjP7epxYU1ln7SZxEUWYop5bhsdgQ==", "dependencies": { - "@octokit/openapi-types": "^18.0.0" + "@octokit/openapi-types": "^19.1.0" } }, "node_modules/@octokit/webhooks": { - "version": "10.9.1", - "resolved": "https://registry.npmjs.org/@octokit/webhooks/-/webhooks-10.9.1.tgz", - "integrity": "sha512-5NXU4VfsNOo2VSU/SrLrpPH2Z1ZVDOWFcET4EpnEBX1uh/v8Uz65UVuHIRx5TZiXhnWyRE9AO1PXHa+M/iWwZA==", + "version": "12.0.11", + "resolved": "https://registry.npmjs.org/@octokit/webhooks/-/webhooks-12.0.11.tgz", + "integrity": "sha512-YEQOb7v0TZ662nh5jsbY1CMgJyMajCEagKrHWC30LTCwCtnuIrLtEpE20vq4AtH0SuZI90+PtV66/Bnnw0jkvg==", "dependencies": { - "@octokit/request-error": "^3.0.0", - "@octokit/webhooks-methods": "^3.0.0", - "@octokit/webhooks-types": "6.11.0", + "@octokit/request-error": "^5.0.0", + "@octokit/webhooks-methods": "^4.0.0", + "@octokit/webhooks-types": "7.1.0", "aggregate-error": "^3.1.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/webhooks-methods": { - "version": "3.0.3", - "resolved": "https://registry.npmjs.org/@octokit/webhooks-methods/-/webhooks-methods-3.0.3.tgz", - "integrity": "sha512-2vM+DCNTJ5vL62O5LagMru6XnYhV4fJslK+5YUkTa6rWlW2S+Tqs1lF9Wr9OGqHfVwpBj3TeztWfVON/eUoW1Q==", + "version": "4.0.0", + "resolved": "https://registry.npmjs.org/@octokit/webhooks-methods/-/webhooks-methods-4.0.0.tgz", + "integrity": "sha512-M8mwmTXp+VeolOS/kfRvsDdW+IO0qJ8kYodM/sAysk093q6ApgmBXwK1ZlUvAwXVrp/YVHp6aArj4auAxUAOFw==", "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/@octokit/webhooks-types": { - "version": "6.11.0", - "resolved": "https://registry.npmjs.org/@octokit/webhooks-types/-/webhooks-types-6.11.0.tgz", - "integrity": "sha512-AanzbulOHljrku1NGfafxdpTCfw2ENaWzH01N2vqQM+cUFbk868Cgh0xylz0JIM9BoKbfI++bdD6EYX0Q/UTEw==" + "version": "7.1.0", + "resolved": "https://registry.npmjs.org/@octokit/webhooks-types/-/webhooks-types-7.1.0.tgz", + "integrity": "sha512-y92CpG4kFFtBBjni8LHoV12IegJ+KFxLgKRengrVjKmGE5XMeCuGvlfRe75lTRrgXaG6XIWJlFpIDTlkoJsU8w==" }, "node_modules/@pmmmwh/react-refresh-webpack-plugin": { "version": "0.5.11", @@ -4932,9 +4926,9 @@ "dev": true }, "node_modules/@types/aws-lambda": { - "version": "8.10.124", - "resolved": "https://registry.npmjs.org/@types/aws-lambda/-/aws-lambda-8.10.124.tgz", - "integrity": "sha512-PHqK0SuAkFS3tZjceqRXecxxrWIN3VqTicuialtK2wZmvBy7H9WGc3u3+wOgaZB7N8SpSXDpWk9qa7eorpTStg==" + "version": "8.10.131", + "resolved": "https://registry.npmjs.org/@types/aws-lambda/-/aws-lambda-8.10.131.tgz", + "integrity": "sha512-IWmFpqnVDvskYWnNSiu/qlRn80XlIOU0Gy5rKCl/NjhnI95pV8qIHs6L5b+bpHhyzuOSzjLgBcwgFSXrC1nZWA==" }, "node_modules/@types/body-parser": { "version": "1.19.3", @@ -4960,9 +4954,9 @@ } }, "node_modules/@types/btoa-lite": { - "version": "1.0.0", - "resolved": "https://registry.npmjs.org/@types/btoa-lite/-/btoa-lite-1.0.0.tgz", - "integrity": "sha512-wJsiX1tosQ+J5+bY5LrSahHxr2wT+uME5UDwdN1kg4frt40euqA+wzECkmq4t5QbveHiJepfdThgQrPw6KiSlg==" + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/@types/btoa-lite/-/btoa-lite-1.0.2.tgz", + "integrity": "sha512-ZYbcE2x7yrvNFJiU7xJGrpF/ihpkM7zKgw8bha3LNJSesvTtUNxbpzaT7WXBIryf6jovisrxTBvymxMeLLj1Mg==" }, "node_modules/@types/connect": { "version": "3.4.36", @@ -5130,9 +5124,9 @@ "dev": true }, "node_modules/@types/jsonwebtoken": { - "version": "9.0.3", - "resolved": "https://registry.npmjs.org/@types/jsonwebtoken/-/jsonwebtoken-9.0.3.tgz", - "integrity": "sha512-b0jGiOgHtZ2jqdPgPnP6WLCXZk1T8p06A/vPGzUvxpFGgKMbjXJDjC5m52ErqBnIuWZFgGoIJyRdeG5AyreJjA==", + "version": "9.0.5", + "resolved": "https://registry.npmjs.org/@types/jsonwebtoken/-/jsonwebtoken-9.0.5.tgz", + "integrity": "sha512-VRLSGzik+Unrup6BsouBeHsf4d1hOEgYWTm/7Nmw1sXoN1+tRly/Gy/po3yeahnP4jfnQWWAhQAqcNfH7ngOkA==", "dependencies": { "@types/node": "*" } @@ -8007,9 +8001,9 @@ } }, "node_modules/follow-redirects": { - "version": "1.15.3", - "resolved": "https://registry.npmjs.org/follow-redirects/-/follow-redirects-1.15.3.tgz", - "integrity": "sha512-1VzOtuEM8pC9SFU1E+8KfTjZyMztRsgEfwQl44z8A25uy13jSzTj6dyK2Df52iV0vgHCfBwLhDWevLn95w5v6Q==", + "version": "1.15.4", + "resolved": "https://registry.npmjs.org/follow-redirects/-/follow-redirects-1.15.4.tgz", + "integrity": "sha512-Cr4D/5wlrb0z9dgERpUL3LrmPKVDsETIJhaCMeDfuFYcqa5bldGV6wBsAN6X/vxlXQtFBMrXdXxdL8CbDTGniw==", "funding": [ { "type": "individual", @@ -8071,25 +8065,6 @@ "node": ">= 0.6" } }, - "node_modules/fromentries": { - "version": "1.3.2", - "resolved": "https://registry.npmjs.org/fromentries/-/fromentries-1.3.2.tgz", - "integrity": "sha512-cHEpEQHUg0f8XdtZCc2ZAhrHzKzT0MrFUTcvx+hfxYu7rGMDc5SKoXFh+n4YigxsHXRzc6OrCshdR1bWH6HHyg==", - "funding": [ - { - "type": "github", - "url": "https://github.com/sponsors/feross" - }, - { - "type": "patreon", - "url": "https://www.patreon.com/feross" - }, - { - "type": "consulting", - "url": "https://feross.org/support" - } - ] - }, "node_modules/fs-extra": { "version": "8.1.0", "resolved": "https://registry.npmjs.org/fs-extra/-/fs-extra-8.1.0.tgz", @@ -9120,14 +9095,6 @@ "url": "https://github.com/sponsors/sindresorhus" } }, - "node_modules/is-plain-object": { - "version": "5.0.0", - "resolved": "https://registry.npmjs.org/is-plain-object/-/is-plain-object-5.0.0.tgz", - "integrity": "sha512-VRSzKkbMm5jMDoKLbltAkFQ5Qr7VDiTFGXxYFXXowVj387GeGNOCsOH6Msy00SGZ3Fp84b1Naa1psqgcCIEP5Q==", - "engines": { - "node": ">=0.10.0" - } - }, "node_modules/is-regex": { "version": "1.1.4", "resolved": "https://registry.npmjs.org/is-regex/-/is-regex-1.1.4.tgz", @@ -12581,22 +12548,23 @@ "peer": true }, "node_modules/octokit": { - "version": "2.1.0", - "resolved": "https://registry.npmjs.org/octokit/-/octokit-2.1.0.tgz", - "integrity": "sha512-Pxi6uKTjBRZWgAwsw1NgHdRlL+QASCN35OYS7X79o7PtBME0CLXEroZmPtEwlWZbPTP+iDbEy2wCbSOgm0uGIQ==", + "version": "3.1.2", + "resolved": "https://registry.npmjs.org/octokit/-/octokit-3.1.2.tgz", + "integrity": "sha512-MG5qmrTL5y8KYwFgE1A4JWmgfQBaIETE/lOlfwNYx1QOtCQHGVxkRJmdUJltFc1HVn73d61TlMhMyNTOtMl+ng==", "dependencies": { - "@octokit/app": "^13.1.5", - "@octokit/core": "^4.2.1", - "@octokit/oauth-app": "^4.2.1", - "@octokit/plugin-paginate-rest": "^6.1.0", - "@octokit/plugin-rest-endpoint-methods": "^7.1.1", - "@octokit/plugin-retry": "^4.1.3", - "@octokit/plugin-throttling": "^5.2.2", - "@octokit/request-error": "^v3.0.3", - "@octokit/types": "^9.2.2" + "@octokit/app": "^14.0.2", + "@octokit/core": "^5.0.0", + "@octokit/oauth-app": "^6.0.0", + "@octokit/plugin-paginate-graphql": "^4.0.0", + "@octokit/plugin-paginate-rest": "^9.0.0", + "@octokit/plugin-rest-endpoint-methods": "^10.0.0", + "@octokit/plugin-retry": "^6.0.0", + "@octokit/plugin-throttling": "^8.0.0", + "@octokit/request-error": "^5.0.0", + "@octokit/types": "^12.0.0" }, "engines": { - "node": ">= 14" + "node": ">= 18" } }, "node_modules/on-finished": { @@ -15473,18 +15441,18 @@ } }, "node_modules/universal-github-app-jwt": { - "version": "1.1.1", - "resolved": "https://registry.npmjs.org/universal-github-app-jwt/-/universal-github-app-jwt-1.1.1.tgz", - "integrity": "sha512-G33RTLrIBMFmlDV4u4CBF7dh71eWwykck4XgaxaIVeZKOYZRAAxvcGMRFTUclVY6xoUPQvO4Ne5wKGxYm/Yy9w==", + "version": "1.1.2", + "resolved": "https://registry.npmjs.org/universal-github-app-jwt/-/universal-github-app-jwt-1.1.2.tgz", + "integrity": "sha512-t1iB2FmLFE+yyJY9+3wMx0ejB+MQpEVkH0gQv7dR6FZyltyq+ZZO0uDpbopxhrZ3SLEO4dCEkIujOMldEQ2iOA==", "dependencies": { "@types/jsonwebtoken": "^9.0.0", - "jsonwebtoken": "^9.0.0" + "jsonwebtoken": "^9.0.2" } }, "node_modules/universal-user-agent": { - "version": "6.0.0", - "resolved": "https://registry.npmjs.org/universal-user-agent/-/universal-user-agent-6.0.0.tgz", - "integrity": "sha512-isyNax3wXoKaulPDZWHQqbmIx1k2tb9fb3GGDBRxCscfYV2Ch7WxPArBsFEG8s/safwXTT7H4QGhaIkTp9447w==" + "version": "6.0.1", + "resolved": "https://registry.npmjs.org/universal-user-agent/-/universal-user-agent-6.0.1.tgz", + "integrity": "sha512-yCzhz6FN2wU1NiiQRogkTQszlQSlpWaw8SvVegAc+bDxbzHgh1vX8uIe8OYyMH6DwH+sdTJsgMl36+mSMdRJIQ==" }, "node_modules/universalify": { "version": "0.1.2", diff --git a/package.json b/package.json index 8ac56a5..ca95f97 100644 --- a/package.json +++ b/package.json @@ -29,7 +29,7 @@ "express": "^4.18.2", "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c", "lean4web": "github:hhu-adam/lean4web#b91645a7b88814675ba9f99817436d0a2ce3a0ec", - "octokit": "^2.0.14", + "octokit": "^3.1.2", "path-browserify": "^1.0.1", "react": "^18.2.0", "react-dom": "^18.2.0", From 8c93b3c5b3be04b43d32c52301e673d27a384cc9 Mon Sep 17 00:00:00 2001 From: ran Date: Fri, 12 Jan 2024 23:29:03 +0800 Subject: [PATCH 02/16] Modify logic for all preferences --- client/src/app.tsx | 31 ++++++++----- client/src/components/infoview/context.ts | 17 +++++-- client/src/components/popup/preferences.tsx | 51 +++++++++++---------- client/src/components/welcome.tsx | 8 ++-- client/src/components/world_tree.tsx | 5 +- client/src/css/welcome.css | 12 +++++ client/src/hooks.ts | 24 ---------- client/src/state/local_storage.ts | 9 ++++ client/src/state/preferences.ts | 27 ++++++----- client/src/state/store.ts | 6 ++- 10 files changed, 107 insertions(+), 83 deletions(-) diff --git a/client/src/app.tsx b/client/src/app.tsx index 871c226..d5b8647 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -8,39 +8,48 @@ import '@fontsource/roboto/700.css'; import './css/reset.css'; import './css/app.css'; -import { MobileContext } from './components/infoview/context'; -import { useMobile } from './hooks'; -import { AUTO_SWITCH_THRESHOLD, getWindowDimensions} from './state/preferences'; +import { MobileContext, PreferencesContext} from './components/infoview/context'; +import { AUTO_SWITCH_THRESHOLD, getWindowDimensions, setLayout, setisSavePreferences, PreferencesState} from './state/preferences'; +import { useAppDispatch, useAppSelector } from './hooks'; export const GameIdContext = React.createContext(undefined); function App() { - const { mobile, setMobile, lockMobile, setLockMobile } = useMobile(); + const dispatch = useAppDispatch() const params = useParams() const gameId = "g/" + params.owner + "/" + params.repo + // TODO: + const [mobile, setMobile] = React.useState() + const layout = useAppSelector((state) => state.preferences.layout); + const changeLayout = (layout: PreferencesState["layout"]) => dispatch(setLayout(layout)) + const isSavePreferences = useAppSelector((state) => state.preferences.isSavePreferences); + const changeIsSavePreferences = (isSave: boolean) => dispatch(setisSavePreferences(isSave)) + const automaticallyAdjustLayout = () => { const {width} = getWindowDimensions() setMobile(width < AUTO_SWITCH_THRESHOLD) } React.useEffect(()=>{ - if (!lockMobile){ + if (layout === "auto"){ void automaticallyAdjustLayout() window.addEventListener('resize', automaticallyAdjustLayout) - return () => { - window.removeEventListener('resize', automaticallyAdjustLayout) - } + return () => window.removeEventListener('resize', automaticallyAdjustLayout) + } else { + setMobile(layout === "mobile") } - }, [lockMobile]) + }, [layout]) return (
- - + + + +
diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts index 8a62b36..948473b 100644 --- a/client/src/components/infoview/context.ts +++ b/client/src/components/infoview/context.ts @@ -5,6 +5,7 @@ import * as React from 'react'; import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' import { InteractiveDiagnostic, InteractiveTermGoal } from '@leanprover/infoview-api'; import { GameHint, InteractiveGoal, InteractiveGoals } from './rpc_api'; +import { PreferencesState } from '../../state/preferences'; export const MonacoEditorContext = React.createContext( null as any) @@ -62,18 +63,26 @@ export const ProofStateContext = React.createContext<{ setProofState: () => {}, }) +export interface IPreferencesContext extends PreferencesState{ + setLayout: React.Dispatch>; + setIsSavePreferences: React.Dispatch>; +} + +export const PreferencesContext = React.createContext({ + layout: "auto", + isSavePreferences: false, + setLayout: () => {}, + setIsSavePreferences: () => {} +}) + export interface IMobileContext { mobile : boolean, setMobile: React.Dispatch>, - lockMobile: boolean, - setLockMobile: React.Dispatch>, } export const MobileContext = React.createContext({ mobile: false, setMobile: () => {}, - lockMobile: false, - setLockMobile: () => {} }) export const WorldLevelIdContext = React.createContext<{ diff --git a/client/src/components/popup/preferences.tsx b/client/src/components/popup/preferences.tsx index 73b2dbe..fdda8e6 100644 --- a/client/src/components/popup/preferences.tsx +++ b/client/src/components/popup/preferences.tsx @@ -1,16 +1,20 @@ import * as React from 'react' import { Input, Typography } from '@mui/material' import Markdown from '../markdown' -import Switch from '@mui/material/Switch'; +import { Switch, Button, ButtonGroup } from '@mui/material'; + import FormControlLabel from '@mui/material/FormControlLabel'; import { IMobileContext } from "../infoview/context" +import { PreferencesState } from "../../state/preferences" -interface PreferencesPopupProps extends IMobileContext{ - handleClose: () => void -} +interface PreferencesPopupProps extends PreferencesState{ + handleClose: () => void, + setLayout: (layout: "mobile" | "auto" | "desktop") => void, + setIsSavePreferences: (isSave: boolean) => void +} -export function PreferencesPopup({ mobile, setMobile, lockMobile, setLockMobile, handleClose }: PreferencesPopupProps) { +export function PreferencesPopup({ layout, setLayout, isSavePreferences, setIsSavePreferences, handleClose }: PreferencesPopupProps) { return
@@ -18,34 +22,35 @@ export function PreferencesPopup({ mobile, setMobile, lockMobile, setLockMobile,
-

Mobile layout

+

Layout

-
+
setMobile(!mobile)} - name="checked" - color="primary" - /> + + + + + } - label="Enable" - labelPlacement="start" + label="" />
+
+ +
setLockMobile(!lockMobile)} - name="checked" - color="primary" - /> + setIsSavePreferences(!isSavePreferences)} + name="checked" + color="primary" + /> } - label="Auto" - labelPlacement="start" + label="Save my settings (in the browser store)" + labelPlacement="end" />
diff --git a/client/src/components/welcome.tsx b/client/src/components/welcome.tsx index 89b9adc..18f9f9d 100644 --- a/client/src/components/welcome.tsx +++ b/client/src/components/welcome.tsx @@ -10,7 +10,7 @@ import { useAppDispatch, useAppSelector } from '../hooks' import { changedOpenedIntro, selectOpenedIntro } from '../state/progress' import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api' import { Button } from './button' -import { MobileContext } from './infoview/context' +import { MobileContext, PreferencesContext } from './infoview/context' import { InventoryPanel } from './inventory' import { ErasePopup } from './popup/erase' import { InfoPopup } from './popup/game_info' @@ -64,7 +64,9 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string, /** main page of the game showing among others the tree of worlds/levels */ function Welcome() { const gameId = React.useContext(GameIdContext) - const {mobile, setMobile, lockMobile, setLockMobile} = React.useContext(MobileContext) + const {mobile, setMobile} = React.useContext(MobileContext) + const {layout, isSavePreferences, setLayout, setIsSavePreferences} = React.useContext(PreferencesContext) + const gameInfo = useGetGameInfoQuery({game: gameId}) const inventory = useLoadInventoryOverviewQuery({game: gameId}) @@ -134,7 +136,7 @@ function Welcome() { {eraseMenu? : null} {uploadMenu? : null} {info ? : null} - {preferencesPopup ? : null} + {preferencesPopup ? : null} } diff --git a/client/src/components/world_tree.tsx b/client/src/components/world_tree.tsx index 1aa495b..76cf5fb 100644 --- a/client/src/components/world_tree.tsx +++ b/client/src/components/world_tree.tsx @@ -11,11 +11,12 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faXmark, faCircleQuestion } from '@fortawesome/free-solid-svg-icons' import { GameIdContext } from '../app' -import { useAppDispatch, useMobile } from '../hooks' +import { useAppDispatch } from '../hooks' import { selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress' import { store } from '../state/store' import '../css/world_tree.css' +import { MobileContext } from './infoview/context' // Settings for the world tree cytoscape.use( klay ) @@ -197,7 +198,7 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) { const gameId = React.useContext(GameIdContext) const difficulty = useSelector(selectDifficulty(gameId)) const dispatch = useAppDispatch() - const { mobile } = useMobile() + const { mobile } = React.useContext(MobileContext) function label(x : number) { diff --git a/client/src/css/welcome.css b/client/src/css/welcome.css index 94e17e3..387bc48 100644 --- a/client/src/css/welcome.css +++ b/client/src/css/welcome.css @@ -187,3 +187,15 @@ h5, h6 { margin-left: 0.3rem; margin-right: 0.3rem; } + +.preferences-category.tail-category{ + margin-top: 2em; +} + +.preferences-item.first{ + margin-top: 1em; +} + +.preferences-item.leave-left-gap{ + margin-left: 1em; +} \ No newline at end of file diff --git a/client/src/hooks.ts b/client/src/hooks.ts index 0ac6e2f..afdce0a 100644 --- a/client/src/hooks.ts +++ b/client/src/hooks.ts @@ -1,30 +1,6 @@ import { TypedUseSelectorHook, useDispatch, useSelector } from 'react-redux' import type { RootState, AppDispatch } from './state/store' -import { setMobile as setMobileState, setLockMobile as setLockMobileState} from "./state/preferences" - // Use throughout your app instead of plain `useDispatch` and `useSelector` export const useAppDispatch: () => AppDispatch = useDispatch export const useAppSelector: TypedUseSelectorHook = useSelector - -export const useMobile = () => { - const dispatch = useAppDispatch(); - - const mobile = useAppSelector((state) => state.preferences.mobile); - const lockMobile = useAppSelector((state) => state.preferences.lockMobile); - - const setMobile = (val: boolean) => { - dispatch(setMobileState(val)); - }; - - const setLockMobile = (val: boolean) => { - dispatch(setLockMobileState(val)); - }; - - return { - mobile, - setMobile, - lockMobile, - setLockMobile, - }; -}; diff --git a/client/src/state/local_storage.ts b/client/src/state/local_storage.ts index ea165ce..098768e 100644 --- a/client/src/state/local_storage.ts +++ b/client/src/state/local_storage.ts @@ -57,3 +57,12 @@ export function savePreferences(state: any) { // Ignore } } + +export function removePreferences() { + try { + localStorage.removeItem(PREFERENCES_KEY); + } catch (e) { + // Ignore + } +} + diff --git a/client/src/state/preferences.ts b/client/src/state/preferences.ts index 6ee0fa1..b00dd71 100644 --- a/client/src/state/preferences.ts +++ b/client/src/state/preferences.ts @@ -1,10 +1,10 @@ import { createSlice } from "@reduxjs/toolkit"; -import { loadPreferences } from "./local_storage"; +import { loadPreferences, removePreferences, savePreferences } from "./local_storage"; -interface PreferencesState { - mobile: boolean; - lockMobile: boolean; +export interface PreferencesState { + layout: "mobile" | "auto" | "desktop"; + isSavePreferences: boolean; } export function getWindowDimensions() { @@ -12,26 +12,25 @@ export function getWindowDimensions() { return {width, height} } -const { width } = getWindowDimensions() - export const AUTO_SWITCH_THRESHOLD = 800 -const initialState: PreferencesState = loadPreferences() ?? { - mobile: width < AUTO_SWITCH_THRESHOLD, - lockMobile: false +const initialState: PreferencesState = loadPreferences() ??{ + layout: "auto", + isSavePreferences: false } export const preferencesSlice = createSlice({ name: "preferences", initialState, reducers: { - setMobile: (state, action) => { - state.mobile = action.payload; + setLayout: (state, action) => { + state.layout = action.payload; }, - setLockMobile: (state, action) => { - state.lockMobile = action.payload; + setisSavePreferences: (state, action) => { + state.isSavePreferences = action.payload; + action.payload ? savePreferences(state) : removePreferences() }, }, }); -export const { setMobile, setLockMobile } = preferencesSlice.actions; +export const { setLayout, setisSavePreferences } = preferencesSlice.actions; diff --git a/client/src/state/store.ts b/client/src/state/store.ts index 4406c84..cdda9c5 100644 --- a/client/src/state/store.ts +++ b/client/src/state/store.ts @@ -8,7 +8,7 @@ import { connection } from '../connection' import { apiSlice } from './api' import { progressSlice } from './progress' import { preferencesSlice } from "./preferences" -import { saveState, savePreferences } from "./local_storage"; +import { saveState, savePreferences, removePreferences} from "./local_storage"; export const store = configureStore({ @@ -29,7 +29,9 @@ export const store = configureStore({ store.subscribe( debounce(() => { saveState(store.getState()[progressSlice.name]); - savePreferences(store.getState()[preferencesSlice.name]); + + const preferencesState= store.getState()[preferencesSlice.name] + preferencesState.isSavePreferences ? savePreferences(preferencesState) : removePreferences() }, 800) ); From e15e5af1262947c96f26592c876e2f724f0e8e82 Mon Sep 17 00:00:00 2001 From: ran Date: Fri, 12 Jan 2024 23:31:22 +0800 Subject: [PATCH 03/16] Add todo about setMobile --- client/src/app.tsx | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/app.tsx b/client/src/app.tsx index d5b8647..653286f 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -20,7 +20,7 @@ function App() { const params = useParams() const gameId = "g/" + params.owner + "/" + params.repo - // TODO: + // TODO: Modifying setMobile will not change 'layout', and the setMobile function may not exist in the future. const [mobile, setMobile] = React.useState() const layout = useAppSelector((state) => state.preferences.layout); const changeLayout = (layout: PreferencesState["layout"]) => dispatch(setLayout(layout)) From d16956da9b581e2a06733ba864c463c1c492c68c Mon Sep 17 00:00:00 2001 From: ran Date: Fri, 12 Jan 2024 23:43:21 +0800 Subject: [PATCH 04/16] Modify the props definition of the preference popup component --- client/src/components/popup/preferences.tsx | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/client/src/components/popup/preferences.tsx b/client/src/components/popup/preferences.tsx index fdda8e6..ee24d6c 100644 --- a/client/src/components/popup/preferences.tsx +++ b/client/src/components/popup/preferences.tsx @@ -5,13 +5,10 @@ import { Switch, Button, ButtonGroup } from '@mui/material'; import FormControlLabel from '@mui/material/FormControlLabel'; -import { IMobileContext } from "../infoview/context" -import { PreferencesState } from "../../state/preferences" +import { IPreferencesContext } from "../infoview/context" -interface PreferencesPopupProps extends PreferencesState{ - handleClose: () => void, - setLayout: (layout: "mobile" | "auto" | "desktop") => void, - setIsSavePreferences: (isSave: boolean) => void +interface PreferencesPopupProps extends IPreferencesContext{ + handleClose: () => void } export function PreferencesPopup({ layout, setLayout, isSavePreferences, setIsSavePreferences, handleClose }: PreferencesPopupProps) { From 5d88cd67393331af02c69e61d1c9d501f723bc72 Mon Sep 17 00:00:00 2001 From: ran Date: Fri, 12 Jan 2024 23:44:43 +0800 Subject: [PATCH 05/16] Remove logically duplicated code --- client/src/state/preferences.ts | 1 - 1 file changed, 1 deletion(-) diff --git a/client/src/state/preferences.ts b/client/src/state/preferences.ts index b00dd71..f3c3fbb 100644 --- a/client/src/state/preferences.ts +++ b/client/src/state/preferences.ts @@ -28,7 +28,6 @@ export const preferencesSlice = createSlice({ }, setisSavePreferences: (state, action) => { state.isSavePreferences = action.payload; - action.payload ? savePreferences(state) : removePreferences() }, }, }); From 8929813e488af177152c3ce0183b2fff598ae8a5 Mon Sep 17 00:00:00 2001 From: ran Date: Fri, 12 Jan 2024 23:48:47 +0800 Subject: [PATCH 06/16] Added a missing space regarding code style in store.ts --- client/src/state/store.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/state/store.ts b/client/src/state/store.ts index cdda9c5..e73818e 100644 --- a/client/src/state/store.ts +++ b/client/src/state/store.ts @@ -30,7 +30,7 @@ store.subscribe( debounce(() => { saveState(store.getState()[progressSlice.name]); - const preferencesState= store.getState()[preferencesSlice.name] + const preferencesState = store.getState()[preferencesSlice.name] preferencesState.isSavePreferences ? savePreferences(preferencesState) : removePreferences() }, 800) ); From ab98eaa3ba0263fff43aec1df7cae4d6b9f7f7cb Mon Sep 17 00:00:00 2001 From: ran Date: Tue, 16 Jan 2024 11:21:46 +0800 Subject: [PATCH 07/16] Change the selected button to a slider --- client/src/components/popup/preferences.tsx | 47 ++++++++++++++++++--- client/src/css/welcome.css | 2 +- 2 files changed, 41 insertions(+), 8 deletions(-) diff --git a/client/src/components/popup/preferences.tsx b/client/src/components/popup/preferences.tsx index ee24d6c..2b6d29b 100644 --- a/client/src/components/popup/preferences.tsx +++ b/client/src/components/popup/preferences.tsx @@ -2,16 +2,41 @@ import * as React from 'react' import { Input, Typography } from '@mui/material' import Markdown from '../markdown' import { Switch, Button, ButtonGroup } from '@mui/material'; +import Box from '@mui/material/Box'; +import Slider from '@mui/material/Slider'; import FormControlLabel from '@mui/material/FormControlLabel'; import { IPreferencesContext } from "../infoview/context" -interface PreferencesPopupProps extends IPreferencesContext{ +interface PreferencesPopupProps extends IPreferencesContext { handleClose: () => void } -export function PreferencesPopup({ layout, setLayout, isSavePreferences, setIsSavePreferences, handleClose }: PreferencesPopupProps) { +export function PreferencesPopup({ layout, setLayout, isSavePreferences, setIsSavePreferences, handleClose }: PreferencesPopupProps) { + + const marks = [ + { + value: 0, + label: 'Mobile', + key: "mobile" + }, + { + value: 1, + label: 'Auto', + key: "auto" + }, + { + value: 2, + label: 'Desktop', + key: "desktop" + }, + ]; + + const handlerChangeLayout = (_: Event, value: number) => { + setLayout(marks[value].key as IPreferencesContext["layout"]) + } + return
@@ -24,11 +49,19 @@ export function PreferencesPopup({ layout, setLayout, isSavePreferences, setIsSa
- - - - + + item.key === layout).value} + step={1} + marks={marks} + max={2} + sx={{ + '& .MuiSlider-track': { display: 'none', }, + }} + onChange={handlerChangeLayout} + /> + } label="" /> diff --git a/client/src/css/welcome.css b/client/src/css/welcome.css index 387bc48..e48f7d0 100644 --- a/client/src/css/welcome.css +++ b/client/src/css/welcome.css @@ -197,5 +197,5 @@ h5, h6 { } .preferences-item.leave-left-gap{ - margin-left: 1em; + margin-left: 3em; } \ No newline at end of file From e277a48749dc43ca297a9878ff9b43106bcf9c22 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 18 Jan 2024 14:19:32 +0100 Subject: [PATCH 08/16] add changelog file --- doc/changelog.md | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 doc/changelog.md diff --git a/doc/changelog.md b/doc/changelog.md new file mode 100644 index 0000000..2677283 --- /dev/null +++ b/doc/changelog.md @@ -0,0 +1,7 @@ +# Changelog + +## v4.5.0 + +### Breaking changes + +## Other From c103eeacfab0796cb97d4e12f7fe4bd8e25dd5ad Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 18 Jan 2024 14:57:50 +0100 Subject: [PATCH 09/16] fix: case insensitive url in local store #183 --- client/src/state/progress.ts | 68 ++++++++++++++++++------------------ doc/changelog.md | 2 ++ 2 files changed, 36 insertions(+), 34 deletions(-) diff --git a/client/src/state/progress.ts b/client/src/state/progress.ts index c8c4242..c01eca0 100644 --- a/client/src/state/progress.ts +++ b/client/src/state/progress.ts @@ -53,22 +53,22 @@ const initalLevelProgressState: LevelProgressState = {code: "", completed: false /** Add an empty skeleton with progress for the current game */ function addGameProgress (state: ProgressState, action: PayloadAction<{game: string}>) { - if (!state.games[action.payload.game]) { - state.games[action.payload.game] = {inventory: [], openedIntro: true, data: {}, difficulty: DEFAULT_DIFFICULTY} + if (!state.games[action.payload.game.toLowerCase()]) { + state.games[action.payload.game.toLowerCase()] = {inventory: [], openedIntro: true, data: {}, difficulty: DEFAULT_DIFFICULTY} } - if (!state.games[action.payload.game].data) { - state.games[action.payload.game].data = {} + if (!state.games[action.payload.game.toLowerCase()].data) { + state.games[action.payload.game.toLowerCase()].data = {} } } /** Add an empty skeleton with progress for the current level */ function addLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) { addGameProgress(state, action) - if (!state.games[action.payload.game].data[action.payload.world]) { - state.games[action.payload.game].data[action.payload.world] = {} + if (!state.games[action.payload.game.toLowerCase()].data[action.payload.world]) { + state.games[action.payload.game.toLowerCase()].data[action.payload.world] = {} } - if (!state.games[action.payload.game].data[action.payload.world][action.payload.level]) { - state.games[action.payload.game].data[action.payload.world][action.payload.level] = {...initalLevelProgressState} + if (!state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level]) { + state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level] = {...initalLevelProgressState} } } @@ -79,58 +79,58 @@ export const progressSlice = createSlice({ /** put edited code in the state and set completed to false */ codeEdited(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, code: string}>) { addLevelProgress(state, action) - state.games[action.payload.game].data[action.payload.world][action.payload.level].code = action.payload.code - state.games[action.payload.game].data[action.payload.world][action.payload.level].completed = false + state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].code = action.payload.code + state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].completed = false }, /** TODO: docstring */ changedSelection(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, selections: Selection[]}>) { addLevelProgress(state, action) - state.games[action.payload.game].data[action.payload.world][action.payload.level].selections = action.payload.selections + state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].selections = action.payload.selections }, /** mark level as completed */ levelCompleted(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) { addLevelProgress(state, action) - state.games[action.payload.game].data[action.payload.world][action.payload.level].completed = true + state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].completed = true }, /** Set the list of rows where help is displayed */ helpEdited(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, help: number[]}>) { addLevelProgress(state, action) console.debug(`!setting help to: ${action.payload.help}`) - state.games[action.payload.game].data[action.payload.world][action.payload.level].help = action.payload.help + state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].help = action.payload.help }, /** delete all progress for this game */ deleteProgress(state: ProgressState, action: PayloadAction<{game: string}>) { - state.games[action.payload.game] = {inventory: [], data: {}, openedIntro: true, difficulty: DEFAULT_DIFFICULTY} + state.games[action.payload.game.toLowerCase()] = {inventory: [], data: {}, openedIntro: true, difficulty: DEFAULT_DIFFICULTY} }, /** delete progress for this level */ deleteLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) { addLevelProgress(state, action) - state.games[action.payload.game].data[action.payload.world][action.payload.level] = initalLevelProgressState + state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level] = initalLevelProgressState }, /** load progress, e.g. from external import */ loadProgress(state: ProgressState, action: PayloadAction<{game: string, data:GameProgressState}>) { console.debug(`setting data to:\n ${action.payload.data}`) - state.games[action.payload.game] = action.payload.data + state.games[action.payload.game.toLowerCase()] = action.payload.data }, /** set the current inventory */ changedInventory(state: ProgressState, action: PayloadAction<{game: string, inventory: string[]}>) { addGameProgress(state, action) - state.games[action.payload.game].inventory = action.payload.inventory + state.games[action.payload.game.toLowerCase()].inventory = action.payload.inventory }, /** set the difficulty */ changedDifficulty(state: ProgressState, action: PayloadAction<{game: string, difficulty: number}>) { addGameProgress(state, action) - state.games[action.payload.game].difficulty = action.payload.difficulty + state.games[action.payload.game.toLowerCase()].difficulty = action.payload.difficulty }, /** set the difficulty */ changedOpenedIntro(state: ProgressState, action: PayloadAction<{game: string, openedIntro: boolean}>) { addGameProgress(state, action) - state.games[action.payload.game].openedIntro = action.payload.openedIntro + state.games[action.payload.game.toLowerCase()].openedIntro = action.payload.openedIntro }, /** set the typewriter mode */ changeTypewriterMode(state: ProgressState, action: PayloadAction<{game: string, typewriterMode: boolean}>) { addGameProgress(state, action) - state.games[action.payload.game].typewriterMode = action.payload.typewriterMode + state.games[action.payload.game.toLowerCase()].typewriterMode = action.payload.typewriterMode } } }) @@ -138,74 +138,74 @@ export const progressSlice = createSlice({ /** if the level does not exist, return default values */ export function selectLevel(game: string, world: string, level: number) { return (state) =>{ - if (!state.progress.games[game]) { return initalLevelProgressState } - if (!state.progress.games[game].data[world]) { return initalLevelProgressState } - if (!state.progress.games[game].data[world][level]) { return initalLevelProgressState } - return state.progress.games[game].data[world][level] + if (!state.progress.games[game.toLowerCase()]) { return initalLevelProgressState } + if (!state.progress.games[game.toLowerCase()].data[world]) { return initalLevelProgressState } + if (!state.progress.games[game.toLowerCase()].data[world][level]) { return initalLevelProgressState } + return state.progress.games[game.toLowerCase()].data[world][level] } } /** return the code of the current level */ export function selectCode(game: string, world: string, level: number) { return (state) => { - return selectLevel(game, world, level)(state).code + return selectLevel(game.toLowerCase(), world, level)(state).code } } /** return the current inventory */ export function selectInventory(game: string) { return (state) => { - if (!state.progress.games[game]) { return [] } - return state.progress.games[game].inventory + if (!state.progress.games[game.toLowerCase()]) { return [] } + return state.progress.games[game.toLowerCase()].inventory } } /** return the code of the current level */ export function selectHelp(game: string, world: string, level: number) { return (state) => { - return selectLevel(game, world, level)(state).help + return selectLevel(game.toLowerCase(), world, level)(state).help } } /** return the selections made in the current level */ export function selectSelections(game: string, world: string, level: number) { return (state) => { - return selectLevel(game, world, level)(state).selections + return selectLevel(game.toLowerCase(), world, level)(state).selections } } /** return whether the current level is clompleted */ export function selectCompleted(game: string, world: string, level: number) { return (state) => { - return selectLevel(game, world, level)(state).completed + return selectLevel(game.toLowerCase(), world, level)(state).completed } } /** return progress for the current game if it exists */ export function selectProgress(game: string) { return (state) => { - return state.progress.games[game] ?? null + return state.progress.games[game.toLowerCase()] ?? null } } /** return difficulty for the current game if it exists */ export function selectDifficulty(game: string) { return (state) => { - return state.progress.games[game]?.difficulty ?? DEFAULT_DIFFICULTY + return state.progress.games[game.toLowerCase()]?.difficulty ?? DEFAULT_DIFFICULTY } } /** return whether the intro has been read */ export function selectOpenedIntro(game: string) { return (state) => { - return state.progress.games[game]?.openedIntro + return state.progress.games[game.toLowerCase()]?.openedIntro } } /** return typewriter mode for the current game if it exists */ export function selectTypewriterMode(game: string) { return (state) => { - return state.progress.games[game]?.typewriterMode ?? true + return state.progress.games[game.toLowerCase()]?.typewriterMode ?? true } } diff --git a/doc/changelog.md b/doc/changelog.md index 2677283..8c49c42 100644 --- a/doc/changelog.md +++ b/doc/changelog.md @@ -4,4 +4,6 @@ ### Breaking changes +* Fix (#183): local store accepts case insensitive URL. The game progress has previously been saved under case sensitive URLs. You might need to recover old progress from your browser storage. + ## Other From fd5e50754104d307b098b461da2a76fcdb70f0dd Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 19 Jan 2024 10:50:48 +0100 Subject: [PATCH 10/16] lint: fix line widths --- server/GameServer/FileWorker.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index aa1d80a..6ca86c3 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -632,8 +632,9 @@ def workerMain (opts : Options) (args : List String): IO UInt32 := do try let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir" let exitCode ← initAndRunWorker i o e opts gameDir - -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit, but we definitely don't - -- want to do that in the case of the worker processes, which can produce non-terminating tasks evaluating user code + -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit, + -- but we definitely don't want to do that in the case of the worker processes, + -- which can produce non-terminating tasks evaluating user code. o.flush e.flush IO.Process.exit exitCode.toUInt8 From ca576542bac5efceb35e9e5a52af56174b25f77c Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 19 Jan 2024 10:53:43 +0100 Subject: [PATCH 11/16] whitelist generalizing and says. #173 --- server/GameServer/FileWorker.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index 6ca86c3..c25910f 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -97,9 +97,10 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) for arg in args do findForbiddenTactics inputCtx gameWorkerState arg | .atom info val => - -- ignore syntax elements that do not start with a letter - -- and ignore "with" keyword - let allowed := ["with", "fun", "at", "only", "by", "to"] + -- Whitelisted keywords. + -- Note: We need a whitelist because we cannot really distinguish keywords from tactics. + let allowed := ["with", "fun", "at", "only", "by", "to", "generalizing", "says"] + -- ignore syntax elements that do not start with a letter or are allowed if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp` match levelInfo.tactics.find? (·.name.toString == val) with From ed017fa605212f979b10ff716989b19dd8b3a293 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 22 Jan 2024 14:06:52 +0100 Subject: [PATCH 12/16] documentation & cleanup in FileWorker --- server/GameServer/FileWorker.lean | 604 +++++++++++++++++------------- 1 file changed, 341 insertions(+), 263 deletions(-) diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index c25910f..8707894 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -5,6 +5,7 @@ import GameServer.ImportModules import GameServer.SaveData namespace MyModule + open Lean open Elab open Parser @@ -48,7 +49,8 @@ partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext) end MyModule -namespace MyServer.FileWorker +namespace GameServer.FileWorker + open Lean open Lean.Server open Lean.Server.FileWorker @@ -57,104 +59,146 @@ open IO open Snapshots open JsonRpc -structure GameWorkerState := +/-- +Game-specific state to be packed on top of the `Lean.Server.FileWorker.WorkerState` +used by the lean server. +-/ +structure WorkerState := + /-- + Collection of items which are considered unlocked. + Tactics and theorems are mixed together. + -/ inventory : Array String /-- - Check for tactics/theorems that are not unlocked. - 0: no check - 1: give warnings - 2: give errors + Difficulty determines whether tactics/theorems can be locked. + * 0: do not check + * 1: give warnings when locked items are used + * 2: give errors when locked items are used -/ difficulty : Nat + /-- + `levelInfo` contains all the (static) information about the level which is not influenced + by the user's progress. + -/ levelInfo : LevelInfo - deriving ToJson, FromJson +deriving ToJson, FromJson -abbrev GameWorkerM := StateT GameWorkerState Server.FileWorker.WorkerM +/-- +Pack the `GameServer.FileWorker.WorkerState` on top of the normal worker monad +`Server.FileWorker.WorkerM`. +-/ +abbrev WorkerM := StateT WorkerState Server.FileWorker.WorkerM section Elab +/-- Add a message. use `(severity := .warning)` to specify the severity-/ +def addMessage (info : SourceInfo) (inputCtx : Parser.InputContext) + (severity := MessageSeverity.warning) (s : MessageData) : + Elab.Command.CommandElabM Unit := do + modify fun st => { st with + messages := st.messages.add { + fileName := inputCtx.fileName + severity := severity + pos := inputCtx.fileMap.toPosition (info.getPos?.getD 0) + data := s }} + +/-- Deprecated! -/ def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) : Elab.Command.CommandElabM Unit := do modify fun st => { st with - messages := st.messages.add { - fileName := inputCtx.fileName - severity := MessageSeverity.error - pos := inputCtx.fileMap.toPosition (info.getPos?.getD 0) - data := s - } - } + messages := st.messages.add { + fileName := inputCtx.fileName + severity := MessageSeverity.error + pos := inputCtx.fileMap.toPosition (info.getPos?.getD 0) + data := s }} -- TODO: use HashSet for allowed tactics? -/-- Find all tactics in syntax object that are forbidden according to a -set `allowed` of allowed tactics. -/ -partial def findForbiddenTactics (inputCtx : Parser.InputContext) - (gameWorkerState : GameWorkerState) (stx : Syntax) : - Elab.Command.CommandElabM Unit := do - let levelInfo := gameWorkerState.levelInfo +/-- +Find all tactics in syntax object that are forbidden according to a +set `allowed` of allowed tactics. +-/ +partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState : WorkerState) + (stx : Syntax) : Elab.Command.CommandElabM Unit := do + let levelInfo := workerState.levelInfo + -- Parse the syntax object and look for tactics and declarations. match stx with | .missing => return () | .node _info _kind args => + -- Go inside a node. for arg in args do - findForbiddenTactics inputCtx gameWorkerState arg + findForbiddenTactics inputCtx workerState arg | .atom info val => - -- Whitelisted keywords. - -- Note: We need a whitelist because we cannot really distinguish keywords from tactics. + -- Atoms might be tactic names or other keywords. + -- Note: We whitelisted known keywords because we cannot + -- distinguish keywords from tactic names. let allowed := ["with", "fun", "at", "only", "by", "to", "generalizing", "says"] - -- ignore syntax elements that do not start with a letter or are allowed + -- Ignore syntax elements that do not start with a letter or are listed above. if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then - let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp` + -- Treat `simp?` and `simp!` like `simp` + let val := val.dropRightWhile (fun c => c == '!' || c == '?') match levelInfo.tactics.find? (·.name.toString == val) with | none => - -- Note: This case means that the tactic will never be introduced in the game. - match gameWorkerState.inventory.find? (· == val) with + -- Tactic will never be introduced in the game. + match workerState.inventory.find? (· == val) with + | some _ => + -- Tactic is in the inventory, allow it. + -- Note: This case shouldn't be possible... + pure () | none => - addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!" - | some _ => pure () -- tactic is in the inventory, allow it. + -- Tactic is not in the inventory. + addMessageByDifficulty info s!"The tactic '{val}' is not available in this game!" | some tac => + -- Tactic is introduced at some point in the game. if tac.locked then - match gameWorkerState.inventory.find? (· == val) with + match workerState.inventory.find? (· == val) with | none => - addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!" - | some _ => pure () -- tactic is in the inventory, allow it. + -- Tactic is marked as locked and not in the inventory. + addMessageByDifficulty info s!"You have not unlocked the tactic '{val}' yet!" + | some _ => + -- Tactic is in the inventory, allow it. + pure () else if tac.disabled then - addWarningMessage info s!"The tactic '{val}' is disabled in this level!" + -- Tactic is disabled in this level. + addMessageByDifficulty info s!"The tactic '{val}' is disabled in this level!" | .ident info _rawVal val _preresolved => + -- Try to resolve the name let ns ← try resolveGlobalConst (mkIdent val) - catch | _ => pure [] -- catch "unknown constant" error + -- Catch "unknown constant" error + catch | _ => pure [] for n in ns do let some (.thmInfo ..) := (← getEnv).find? n - | return () -- not a theorem -> ignore - -- Forbid the theorem we are proving currently + -- Not a theorem, no checks needed. + | return () if some n = levelInfo.statementName then - addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to proof itself!" - - let lemmasAndDefs := levelInfo.lemmas ++ levelInfo.definitions - match lemmasAndDefs.find? (fun l => l.name == n) with - | none => addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!" - | some lem => - if lem.locked then - addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!" - else if lem.disabled then - addWarningMessage info s!"The lemma/definition '{n}' is disabled in this level!" -where addWarningMessage (info : SourceInfo) (s : MessageData) := - let difficulty := gameWorkerState.difficulty + -- Forbid the theorem we are proving currently + addMessage info inputCtx (severity := .error) + s!"Structural recursion: you can't use '{n}' to proof itself!" + let theoremsAndDefs := levelInfo.lemmas ++ levelInfo.definitions + match theoremsAndDefs.find? (·.name == n) with + | none => + -- Theorem will never be introduced in this game + addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!" + | some thm => + -- Theorem is introduced at some point in the game. + if thm.locked then + -- Theorem is still locked. + addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!" + else if thm.disabled then + -- Theorem is disabled in this level. + addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!" +where addMessageByDifficulty (info : SourceInfo) (s : MessageData) := + -- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors + -- deppending on difficulty. + let difficulty := workerState.difficulty if difficulty > 0 then - modify fun st => { st with - messages := st.messages.add { - fileName := inputCtx.fileName - severity := if difficulty > 1 then MessageSeverity.error else MessageSeverity.warning - pos := inputCtx.fileMap.toPosition (info.getPos?.getD 0) - data := s - } - } + addMessage info inputCtx (if difficulty > 1 then .error else .warning) s else pure () --- where addErrorMessage (info : SourceInfo) (s : MessageData) := --- pure () open Elab Meta Expr in + def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool) - (couldBeEndSnap : Bool) (gameWorkerState : GameWorkerState) + (couldBeEndSnap : Bool) (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams) : IO Snapshot := do -- Recognize end snap if inputCtx.input.atEnd snap.mpState.pos ∧ couldBeEndSnap then @@ -288,7 +332,7 @@ where /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/ private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken) - (gameWorkerState : GameWorkerState) (initParams : Lsp.InitializeParams) + (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams) : AsyncElabM (Option Snapshot) := do cancelTk.check let s ← get @@ -328,7 +372,7 @@ where /-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/ def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken) - (startAfterMs : UInt32) (gameWorkerState : GameWorkerState) + (startAfterMs : UInt32) (gameWorkerState : WorkerState) : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do let ctx ← read let some headerSnap := snaps[0]? | panic! "empty snapshots" @@ -351,226 +395,254 @@ end Elab section Updates /-- Given the new document, updates editable doc state. -/ - def updateDocument (newMeta : DocumentMeta) : GameWorkerM Unit := do - let s ← get - let ctx ← read - let oldDoc := (← StateT.lift get).doc - oldDoc.cancelTk.set - let initHeaderStx := (← StateT.lift get).initHeaderStx - let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext - let cancelTk ← CancelToken.new - let headSnapTask := oldDoc.cmdSnaps.waitHead? - let newSnaps ← if initHeaderStx != newHeaderStx then - EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do - IO.sleep ctx.initParams.editDelay.toUInt32 - cancelTk.check - IO.Process.exit 2 - else EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) (prio := .dedicated) fun headSnap?? => do - -- There is always at least one snapshot absent exceptions - let some headSnap ← MonadExcept.ofExcept headSnap?? | panic! "empty snapshots" - let newHeaderSnap := { headSnap with stx := newHeaderStx, mpState := newMpState } - let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source - -- Ignore exceptions, we are only interested in the successful snapshots - let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix - -- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only - -- when really necessary, we could do a whitespace-aware `Syntax` comparison instead. - let mut validSnaps ← pure (cmdSnaps.takeWhile (fun s => s.endPos < changePos)) - if h : validSnaps.length ≤ 1 then - validSnaps := [newHeaderSnap] - else - /- When at least one valid non-header snap exists, it may happen that a change does not fall - within the syntactic range of that last snap but still modifies it by appending tokens. - We check for this here. We do not currently handle crazy grammars in which an appended - token can merge two or more previous commands into one. To do so would require reparsing - the entire file. -/ - have : validSnaps.length ≥ 2 := Nat.gt_of_not_le h - let mut lastSnap := validSnaps.getLast (by subst ·; simp at h) - let preLastSnap := - have : 0 < validSnaps.length := Nat.lt_of_lt_of_le (by decide) this - have : validSnaps.length - 2 < validSnaps.length := Nat.sub_lt this (by decide) - validSnaps[validSnaps.length - 2] - let newLastStx ← parseNextCmd newMeta.mkInputContext preLastSnap - if newLastStx != lastSnap.stx then - validSnaps := validSnaps.dropLast - -- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger - -- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable) - unfoldSnaps newMeta validSnaps.toArray cancelTk s ctx - (startAfterMs := ctx.initParams.editDelay.toUInt32) - StateT.lift <| modify fun st => { st with - doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }} +def updateDocument (newMeta : DocumentMeta) : WorkerM Unit := do + let s ← get + let ctx ← read + let oldDoc := (← StateT.lift get).doc + oldDoc.cancelTk.set + let initHeaderStx := (← StateT.lift get).initHeaderStx + let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext + let cancelTk ← CancelToken.new + let headSnapTask := oldDoc.cmdSnaps.waitHead? + let newSnaps ← if initHeaderStx != newHeaderStx then + EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do + IO.sleep ctx.initParams.editDelay.toUInt32 + cancelTk.check + IO.Process.exit 2 + else EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) (prio := .dedicated) fun headSnap?? => do + -- There is always at least one snapshot absent exceptions + let some headSnap ← MonadExcept.ofExcept headSnap?? | panic! "empty snapshots" + let newHeaderSnap := { headSnap with stx := newHeaderStx, mpState := newMpState } + let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source + -- Ignore exceptions, we are only interested in the successful snapshots + let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix + -- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only + -- when really necessary, we could do a whitespace-aware `Syntax` comparison instead. + let mut validSnaps ← pure (cmdSnaps.takeWhile (fun s => s.endPos < changePos)) + if h : validSnaps.length ≤ 1 then + validSnaps := [newHeaderSnap] + else + /- When at least one valid non-header snap exists, it may happen that a change does not fall + within the syntactic range of that last snap but still modifies it by appending tokens. + We check for this here. We do not currently handle crazy grammars in which an appended + token can merge two or more previous commands into one. To do so would require reparsing + the entire file. -/ + have : validSnaps.length ≥ 2 := Nat.gt_of_not_le h + let mut lastSnap := validSnaps.getLast (by subst ·; simp at h) + let preLastSnap := + have : 0 < validSnaps.length := Nat.lt_of_lt_of_le (by decide) this + have : validSnaps.length - 2 < validSnaps.length := Nat.sub_lt this (by decide) + validSnaps[validSnaps.length - 2] + let newLastStx ← parseNextCmd newMeta.mkInputContext preLastSnap + if newLastStx != lastSnap.stx then + validSnaps := validSnaps.dropLast + -- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger + -- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable) + unfoldSnaps newMeta validSnaps.toArray cancelTk s ctx + (startAfterMs := ctx.initParams.editDelay.toUInt32) + StateT.lift <| modify fun st => { st with + doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }} end Updates section Initialization - def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where - input := "" -- No header! - fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString - fileMap := default - - def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool) - (gameDir : String) (module : Name): - IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do - -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`. - let out ← IO.Process.output - { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] } - if out.exitCode != 0 then - throwServerError s!"Error while running Lake: {out.stderr}" - - -- Make the paths relative to the current directory - let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim - let currentDir ← IO.currentDir - let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p - - -- Set the search path - Lean.searchPathRef.set paths - - let env ← importModules' #[{ module := `Init : Import }, { module := module : Import }] - - -- use empty header - let (headerStx, headerParserState, msgLog) ← Parser.parseHeader - {m.mkInputContext with - input := "" - fileMap := FileMap.ofString ""} - (headerStx, ·) <$> EIO.asTask do - let mut srcSearchPath : SearchPath := paths --← initSrcSearchPath (← getBuildDir) - let headerEnv := env - let mut headerEnv := headerEnv - try - if let some path := System.Uri.fileUriToPath? m.uri then - headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none) - catch _ => pure () - let cmdState := Elab.Command.mkState headerEnv {} opts - let cmdState := { cmdState with infoState := { - enabled := true - trees := #[Elab.InfoTree.context ({ - env := headerEnv - fileMap := m.text - ngen := { namePrefix := `_worker } - }) (Elab.InfoTree.node - (Elab.Info.ofCommandInfo { elaborator := `header, stx := headerStx }) - (headerStx[1].getArgs.toList.map (fun importStx => - Elab.InfoTree.node (Elab.Info.ofCommandInfo { - elaborator := `import - stx := importStx - }) #[].toPArray' - )).toPArray' - )].toPArray' - }} - let headerSnap := { - beginPos := 0 - stx := headerStx - mpState := {} - cmdState := cmdState - interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets) - tacticCache := (← IO.mkRef {}) - } - publishDiagnostics m headerSnap.diagnostics.toArray hOut - return (headerSnap, srcSearchPath) - - def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options) - (gameDir : String) (gameWorkerState : GameWorkerState) : IO (WorkerContext × WorkerState) := do - let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false - - let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets) - gameDir gameWorkerState.levelInfo.module - let cancelTk ← CancelToken.new - let ctx := - { hIn := i - hOut := o - hLog := e - headerTask - initParams - clientHasWidgets - } - let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with - | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0) - | Except.error e => throw (e : ElabTaskError)) - let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk } - return (ctx, - { doc := doc - initHeaderStx := headerStx - currHeaderStx := headerStx - importCachingTask? := none - pendingRequests := RBMap.empty - rpcSessions := RBMap.empty - }) +def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where + input := "" -- No header! + fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString + fileMap := default + +def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool) + (gameDir : String) (module : Name): + IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do + -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`. + let out ← IO.Process.output + { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] } + if out.exitCode != 0 then + throwServerError s!"Error while running Lake: {out.stderr}" + + -- Make the paths relative to the current directory + let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim + let currentDir ← IO.currentDir + let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p + + -- Set the search path + Lean.searchPathRef.set paths + + let env ← importModules' #[{ module := `Init : Import }, { module := module : Import }] + + -- use empty header + let (headerStx, headerParserState, msgLog) ← Parser.parseHeader + {m.mkInputContext with + input := "" + fileMap := FileMap.ofString ""} + (headerStx, ·) <$> EIO.asTask do + let mut srcSearchPath : SearchPath := paths --← initSrcSearchPath (← getBuildDir) + let headerEnv := env + let mut headerEnv := headerEnv + try + if let some path := System.Uri.fileUriToPath? m.uri then + headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none) + catch _ => pure () + let cmdState := Elab.Command.mkState headerEnv {} opts + let cmdState := { cmdState with infoState := { + enabled := true + trees := #[Elab.InfoTree.context ({ + env := headerEnv + fileMap := m.text + ngen := { namePrefix := `_worker } + }) (Elab.InfoTree.node + (Elab.Info.ofCommandInfo { elaborator := `header, stx := headerStx }) + (headerStx[1].getArgs.toList.map (fun importStx => + Elab.InfoTree.node (Elab.Info.ofCommandInfo { + elaborator := `import + stx := importStx + }) #[].toPArray' + )).toPArray' + )].toPArray' + }} + let headerSnap := { + beginPos := 0 + stx := headerStx + mpState := {} + cmdState := cmdState + interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets) + tacticCache := (← IO.mkRef {}) + } + publishDiagnostics m headerSnap.diagnostics.toArray hOut + return (headerSnap, srcSearchPath) + +def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options) + (gameDir : String) (gameWorkerState : WorkerState) : IO (WorkerContext × Server.FileWorker.WorkerState) := do + let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false + + let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets) + gameDir gameWorkerState.levelInfo.module + let cancelTk ← CancelToken.new + let ctx := + { hIn := i + hOut := o + hLog := e + headerTask + initParams + clientHasWidgets + } + let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with + | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0) + | Except.error e => throw (e : ElabTaskError)) + let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk } + return (ctx, + { doc := doc + initHeaderStx := headerStx + currHeaderStx := headerStx + importCachingTask? := none + pendingRequests := RBMap.empty + rpcSessions := RBMap.empty + }) end Initialization section NotificationHandling - def handleDidChange (p : DidChangeTextDocumentParams) : GameWorkerM Unit := do - let docId := p.textDocument - let changes := p.contentChanges - let oldDoc := (← StateT.lift get).doc - let some newVersion ← pure docId.version? - | throwServerError "Expected version number" - if newVersion ≤ oldDoc.meta.version then - -- TODO(WN): This happens on restart sometimes. - IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}" - else if ¬ changes.isEmpty then - let newDocText := foldDocumentChanges changes oldDoc.meta.text - updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩ +def handleDidChange (p : DidChangeTextDocumentParams) : WorkerM Unit := do + let docId := p.textDocument + let changes := p.contentChanges + let oldDoc := (← StateT.lift get).doc + let some newVersion ← pure docId.version? + | throwServerError "Expected version number" + if newVersion ≤ oldDoc.meta.version then + -- TODO(WN): This happens on restart sometimes. + IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}" + else if ¬ changes.isEmpty then + let newDocText := foldDocumentChanges changes oldDoc.meta.text + updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩ end NotificationHandling section MessageHandling - def handleNotification (method : String) (params : Json) : GameWorkerM Unit := do - let handle := fun paramType [FromJson paramType] (handler : paramType → GameWorkerM Unit) => - (StateT.lift <| parseParams paramType params) >>= handler - match method with - | "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange) - | "$/cancelRequest" => handle CancelParams (handleCancelRequest ·) - | "$/setTrace" => pure () - | "$/lean/rpc/release" => handle RpcReleaseParams (handleRpcRelease ·) - | "$/lean/rpc/keepAlive" => handle RpcKeepAliveParams (handleRpcKeepAlive ·) - | _ => throwServerError s!"Got unsupported notification method: {method}" + +/-- +Modified notification handler. + +Compare to `Lean.Server.FileWorker.handleNotification`. +We use the modified `WorkerM` and use our custom `handleDidChange`. + +-/ +def handleNotification (method : String) (params : Json) : WorkerM Unit := do + let handle := fun paramType [FromJson paramType] (handler : paramType → WorkerM Unit) => + (StateT.lift <| parseParams paramType params) >>= handler + match method with + -- Modified `textDocument/didChange`, using a custom `handleDidChange` + | "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange) + -- unmodified + | "$/cancelRequest" => handle CancelParams (handleCancelRequest ·) + -- unmodified + | "$/lean/rpc/release" => handle RpcReleaseParams (handleRpcRelease ·) + -- unmodified + | "$/lean/rpc/keepAlive" => handle RpcKeepAliveParams (handleRpcKeepAlive ·) + -- New. TODO: What is this for? + | "$/setTrace" => pure () + | _ => throwServerError s!"Got unsupported notification method: {method}" end MessageHandling section MainLoop - partial def mainLoop : GameWorkerM Unit := do - let ctx ← read - let mut st ← StateT.lift get - let msg ← ctx.hIn.readLspMessage - let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit)) - : IO PendingRequestMap := do - if (← hasFinished task) then - /- Handler tasks are constructed so that the only possible errors here - are failures of writing a response into the stream. -/ - if let Except.error e := task.get then - throwServerError s!"Failed responding to request {id}: {e}" - pure <| acc.erase id - else pure acc - let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) st.pendingRequests - st := { st with pendingRequests } - - -- Opportunistically (i.e. when we wake up on messages) check if any RPC session has expired. - for (id, seshRef) in st.rpcSessions do - let sesh ← seshRef.get - if (← sesh.hasExpired) then - st := { st with rpcSessions := st.rpcSessions.erase id } - - set st - match msg with - | Message.request id method (some params) => - handleRequest id method (toJson params) - mainLoop - | Message.notification "exit" none => - let doc := st.doc - doc.cancelTk.set - return () - | Message.request id "shutdown" none => - ctx.hOut.writeLspResponse ⟨id, Json.null⟩ - mainLoop - | Message.notification method (some params) => - handleNotification method (toJson params) - mainLoop - | _ => throwServerError s!"Got invalid JSON-RPC message: {toJson msg}" + +/-- +Erase finished tasks if there are no errors. +-/ +private def filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) + (task : Task (Except IO.Error Unit)) : IO PendingRequestMap := do + if (← hasFinished task) then + /- Handler tasks are constructed so that the only possible errors here + are failures of writing a response into the stream. -/ + if let Except.error e := task.get then + throwServerError s!"Failed responding to request {id}: {e}" + pure <| acc.erase id + else pure acc + +/-- +The main-loop. +-/ +partial def mainLoop : WorkerM Unit := do + let ctx ← read + let mut st ← StateT.lift get + let msg ← ctx.hIn.readLspMessage + let pendingRequests ← st.pendingRequests.foldM (fun acc id task => + filterFinishedTasks acc id task) st.pendingRequests + st := { st with pendingRequests } + -- Opportunistically (i.e. when we wake up on messages) check if any RPC session has expired. + for (id, seshRef) in st.rpcSessions do + let sesh ← seshRef.get + if (← sesh.hasExpired) then + st := { st with rpcSessions := st.rpcSessions.erase id } + + set st + + -- Process the RPC-message and restart main-loop. + match msg with + | Message.request id "shutdown" none => + ctx.hOut.writeLspResponse ⟨id, Json.null⟩ + mainLoop + | Message.request id method (some params) => + -- Requests are handled by the unmodified lean server. + handleRequest id method (toJson params) + mainLoop + | Message.notification "exit" none => + let doc := st.doc + doc.cancelTk.set + return () + | Message.notification method (some params) => + -- Custom notification handler + handleNotification method (toJson params) + mainLoop + | _ => + throwServerError s!"Got invalid JSON-RPC message: {toJson msg}" + end MainLoop + def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : IO UInt32 := do let i ← maybeTee "fwIn.txt" false i let o ← maybeTee "fwOut.txt" true o @@ -609,12 +681,13 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I let levelInfo ← loadLevelData gameDir levelId.world levelId.level let some initializationOptions := initRequest.param.initializationOptions? | throwServerError "no initialization options found" - let gameWorkerState : GameWorkerState:= { + let gameWorkerState : WorkerState := { inventory := initializationOptions.inventory difficulty := initializationOptions.difficulty levelInfo } let (ctx, st) ← initializeWorker meta i o e initParams opts gameDir gameWorkerState + -- Run the main loop let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <| StateT.run (s := gameWorkerState) <| (mainLoop) return (0 : UInt32) @@ -626,6 +699,11 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I message := e.toString }] o return (1 : UInt32) +/-- +The main function. Simply wrapping `initAndRunWorker`. + +TODO: The first arg `args[0]` is always expected to be `--server`. We could drop this completely. +-/ def workerMain (opts : Options) (args : List String): IO UInt32 := do let i ← IO.getStdin let o ← IO.getStdout @@ -643,4 +721,4 @@ def workerMain (opts : Options) (args : List String): IO UInt32 := do e.putStrLn s!"worker initialization error: {err}" return (1 : UInt32) -end MyServer.FileWorker +end GameServer.FileWorker From 26202e5f36ec290caaf119c6dd27f62c04c4f848 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 22 Jan 2024 14:09:54 +0100 Subject: [PATCH 13/16] fix typo --- server/GameServer.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/GameServer.lean b/server/GameServer.lean index 730e69b..52d1cfb 100644 --- a/server/GameServer.lean +++ b/server/GameServer.lean @@ -11,7 +11,7 @@ unsafe def main : List String → IO UInt32 := fun args => do -- TODO: remove this argument if args[0]? == some "--server" then - MyServer.FileWorker.workerMain {} args + GameServer.FileWorker.workerMain {} args else e.putStrLn s!"Expected `--server`" return 1 From 9d4a6df139455e297a4205eb97958563017614c2 Mon Sep 17 00:00:00 2001 From: ran Date: Tue, 23 Jan 2024 22:59:43 +0800 Subject: [PATCH 14/16] Remove MobileContext and use PreferencesContext instead --- client/src/app.tsx | 33 ++--------------- client/src/components/app_bar.tsx | 6 +-- client/src/components/infoview/context.ts | 12 +----- client/src/components/infoview/main.tsx | 4 +- client/src/components/level.tsx | 10 ++--- client/src/components/popup/preferences.tsx | 2 +- client/src/components/welcome.tsx | 6 +-- client/src/components/world_tree.tsx | 4 +- client/src/state/hooks/use_preferences.ts | 41 +++++++++++++++++++++ client/src/state/preferences.ts | 4 +- 10 files changed, 65 insertions(+), 57 deletions(-) create mode 100644 client/src/state/hooks/use_preferences.ts diff --git a/client/src/app.tsx b/client/src/app.tsx index 653286f..64e5004 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -8,49 +8,24 @@ import '@fontsource/roboto/700.css'; import './css/reset.css'; import './css/app.css'; -import { MobileContext, PreferencesContext} from './components/infoview/context'; -import { AUTO_SWITCH_THRESHOLD, getWindowDimensions, setLayout, setisSavePreferences, PreferencesState} from './state/preferences'; -import { useAppDispatch, useAppSelector } from './hooks'; +import { PreferencesContext} from './components/infoview/context'; +import UsePreferences from "./state/hooks/use_preferences" export const GameIdContext = React.createContext(undefined); function App() { - const dispatch = useAppDispatch() const params = useParams() const gameId = "g/" + params.owner + "/" + params.repo - // TODO: Modifying setMobile will not change 'layout', and the setMobile function may not exist in the future. - const [mobile, setMobile] = React.useState() - const layout = useAppSelector((state) => state.preferences.layout); - const changeLayout = (layout: PreferencesState["layout"]) => dispatch(setLayout(layout)) - const isSavePreferences = useAppSelector((state) => state.preferences.isSavePreferences); - const changeIsSavePreferences = (isSave: boolean) => dispatch(setisSavePreferences(isSave)) - - const automaticallyAdjustLayout = () => { - const {width} = getWindowDimensions() - setMobile(width < AUTO_SWITCH_THRESHOLD) - } - - React.useEffect(()=>{ - if (layout === "auto"){ - void automaticallyAdjustLayout() - window.addEventListener('resize', automaticallyAdjustLayout) - - return () => window.removeEventListener('resize', automaticallyAdjustLayout) - } else { - setMobile(layout === "mobile") - } - }, [layout]) + const {mobile, layout, isSavePreferences, setLayout, setIsSavePreferences} = UsePreferences() return (
- - + -
) diff --git a/client/src/components/app_bar.tsx b/client/src/components/app_bar.tsx index ced97d5..f8a171f 100644 --- a/client/src/components/app_bar.tsx +++ b/client/src/components/app_bar.tsx @@ -7,7 +7,7 @@ import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome, faArrowRight, faArrowLeft, faXmark, faBars, faCode, faCircleInfo, faTerminal, faMobileScreenButton, faDesktop, faGear } from '@fortawesome/free-solid-svg-icons' import { GameIdContext } from "../app" -import { InputModeContext, MobileContext, WorldLevelIdContext } from "./infoview/context" +import { InputModeContext, PreferencesContext, WorldLevelIdContext } from "./infoview/context" import { GameInfo, useGetGameInfoQuery } from '../state/api' import { changedOpenedIntro, selectCompleted, selectDifficulty, selectProgress } from '../state/progress' import { useAppDispatch, useAppSelector } from '../hooks' @@ -162,7 +162,7 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres }) { const gameId = React.useContext(GameIdContext) const gameProgress = useAppSelector(selectProgress(gameId)) - const {mobile, setMobile} = React.useContext(MobileContext) + const {mobile} = React.useContext(PreferencesContext) const [navOpen, setNavOpen] = React.useState(false) return
@@ -212,7 +212,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber= }) { const gameId = React.useContext(GameIdContext) const {worldId, levelId} = React.useContext(WorldLevelIdContext) - const {mobile} = React.useContext(MobileContext) + const {mobile} = React.useContext(PreferencesContext) const [navOpen, setNavOpen] = React.useState(false) const gameInfo = useGetGameInfoQuery({game: gameId}) const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts index 948473b..e425749 100644 --- a/client/src/components/infoview/context.ts +++ b/client/src/components/infoview/context.ts @@ -64,27 +64,19 @@ export const ProofStateContext = React.createContext<{ }) export interface IPreferencesContext extends PreferencesState{ + mobile: boolean, // The variables that actually control the page 'layout' can only be changed through layout. setLayout: React.Dispatch>; setIsSavePreferences: React.Dispatch>; } export const PreferencesContext = React.createContext({ + mobile: false, layout: "auto", isSavePreferences: false, setLayout: () => {}, setIsSavePreferences: () => {} }) -export interface IMobileContext { - mobile : boolean, - setMobile: React.Dispatch>, -} - -export const MobileContext = React.createContext({ - mobile: false, - setMobile: () => {}, -}) - export const WorldLevelIdContext = React.createContext<{ worldId : string, levelId: number diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index c90eba8..956d2f6 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -27,7 +27,7 @@ import Markdown from '../markdown'; import { Infos } from './infos'; import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages'; import { Goal } from './goals'; -import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './context'; +import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './context'; import { Typewriter, hasErrors, hasInteractiveErrors } from './typewriter'; import { InteractiveDiagnostic } from '@leanprover/infoview/*'; import { Button } from '../button'; @@ -349,7 +349,7 @@ export function TypewriterInterface({props}) { const [disableInput, setDisableInput] = React.useState(false) const [loadingProgress, setLoadingProgress] = React.useState(0) const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext) - const {mobile} = React.useContext(MobileContext) + const {mobile} = React.useContext(PreferencesContext) const { proof } = React.useContext(ProofContext) const { setTypewriterInput } = React.useContext(InputModeContext) const { selectedStep, setSelectedStep } = React.useContext(SelectionContext) diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 4b5a53d..dbd62a5 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -27,7 +27,7 @@ import { Button } from './button' import Markdown from './markdown' import {InventoryPanel} from './inventory' import { hasInteractiveErrors } from './infoview/typewriter' -import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, +import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context' import { DualEditor } from './infoview/main' import { GameHint } from './infoview/rpc_api' @@ -74,7 +74,7 @@ function Level() { function ChatPanel({lastLevel}) { const chatRef = useRef(null) - const {mobile} = useContext(MobileContext) + const {mobile} = useContext(PreferencesContext) const gameId = useContext(GameIdContext) const {worldId, levelId} = useContext(WorldLevelIdContext) const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) @@ -215,7 +215,7 @@ function PlayableLevel({impressum, setImpressum}) { const codeviewRef = useRef(null) const gameId = React.useContext(GameIdContext) const {worldId, levelId} = useContext(WorldLevelIdContext) - const {mobile} = React.useContext(MobileContext) + const {mobile} = React.useContext(PreferencesContext) const dispatch = useAppDispatch() @@ -441,7 +441,7 @@ function PlayableLevel({impressum, setImpressum}) { function IntroductionPanel({gameInfo}) { const gameId = React.useContext(GameIdContext) const {worldId} = useContext(WorldLevelIdContext) - const {mobile} = React.useContext(MobileContext) + const {mobile} = React.useContext(PreferencesContext) let text: Array = gameInfo.data?.worlds.nodes[worldId].introduction.split(/\n(\s*\n)+/) @@ -468,7 +468,7 @@ export default Level /** The site with the introduction text of a world */ function Introduction({impressum, setImpressum}) { const gameId = React.useContext(GameIdContext) - const {mobile} = useContext(MobileContext) + const {mobile} = useContext(PreferencesContext) const inventory = useLoadInventoryOverviewQuery({game: gameId}) diff --git a/client/src/components/popup/preferences.tsx b/client/src/components/popup/preferences.tsx index 2b6d29b..aadc319 100644 --- a/client/src/components/popup/preferences.tsx +++ b/client/src/components/popup/preferences.tsx @@ -9,7 +9,7 @@ import FormControlLabel from '@mui/material/FormControlLabel'; import { IPreferencesContext } from "../infoview/context" -interface PreferencesPopupProps extends IPreferencesContext { +interface PreferencesPopupProps extends Omit { handleClose: () => void } diff --git a/client/src/components/welcome.tsx b/client/src/components/welcome.tsx index 18f9f9d..5d4b3de 100644 --- a/client/src/components/welcome.tsx +++ b/client/src/components/welcome.tsx @@ -10,7 +10,7 @@ import { useAppDispatch, useAppSelector } from '../hooks' import { changedOpenedIntro, selectOpenedIntro } from '../state/progress' import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api' import { Button } from './button' -import { MobileContext, PreferencesContext } from './infoview/context' +import { PreferencesContext } from './infoview/context' import { InventoryPanel } from './inventory' import { ErasePopup } from './popup/erase' import { InfoPopup } from './popup/game_info' @@ -27,7 +27,7 @@ import { Hint } from './hints' /** the panel showing the game's introduction text */ function IntroductionPanel({introduction, setPageNumber}: {introduction: string, setPageNumber}) { - const {mobile} = React.useContext(MobileContext) + const {mobile} = React.useContext(PreferencesContext) const gameId = React.useContext(GameIdContext) const dispatch = useAppDispatch() @@ -64,7 +64,7 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string, /** main page of the game showing among others the tree of worlds/levels */ function Welcome() { const gameId = React.useContext(GameIdContext) - const {mobile, setMobile} = React.useContext(MobileContext) + const {mobile} = React.useContext(PreferencesContext) const {layout, isSavePreferences, setLayout, setIsSavePreferences} = React.useContext(PreferencesContext) const gameInfo = useGetGameInfoQuery({game: gameId}) diff --git a/client/src/components/world_tree.tsx b/client/src/components/world_tree.tsx index 76cf5fb..65fcc8a 100644 --- a/client/src/components/world_tree.tsx +++ b/client/src/components/world_tree.tsx @@ -16,7 +16,7 @@ import { selectDifficulty, changedDifficulty, selectCompleted } from '../state/p import { store } from '../state/store' import '../css/world_tree.css' -import { MobileContext } from './infoview/context' +import { PreferencesContext } from './infoview/context' // Settings for the world tree cytoscape.use( klay ) @@ -198,7 +198,7 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) { const gameId = React.useContext(GameIdContext) const difficulty = useSelector(selectDifficulty(gameId)) const dispatch = useAppDispatch() - const { mobile } = React.useContext(MobileContext) + const { mobile } = React.useContext(PreferencesContext) function label(x : number) { diff --git a/client/src/state/hooks/use_preferences.ts b/client/src/state/hooks/use_preferences.ts new file mode 100644 index 0000000..3b4f66c --- /dev/null +++ b/client/src/state/hooks/use_preferences.ts @@ -0,0 +1,41 @@ +import React, { useState } from "react"; +import { useAppDispatch, useAppSelector } from "../../hooks"; +import { + PreferencesState, + setLayout as setPreferencesLayout, + setIsSavePreferences as setPreferencesIsSavePreferences, + getWindowDimensions, + AUTO_SWITCH_THRESHOLD +} from "../preferences"; + + +const UsePreferences = () => { + const dispatch = useAppDispatch() + const [mobile, setMobile] = React.useState() + + const layout = useAppSelector((state) => state.preferences.layout); + const setLayout = (layout: PreferencesState["layout"]) => dispatch(setPreferencesLayout(layout)) + + const isSavePreferences = useAppSelector((state) => state.preferences.isSavePreferences); + const setIsSavePreferences = (isSave: boolean) => dispatch(setPreferencesIsSavePreferences(isSave)) + + const automaticallyAdjustLayout = () => { + const {width} = getWindowDimensions() + setMobile(width < AUTO_SWITCH_THRESHOLD) + } + + React.useEffect(()=>{ + if (layout === "auto"){ + void automaticallyAdjustLayout() + window.addEventListener('resize', automaticallyAdjustLayout) + + return () => window.removeEventListener('resize', automaticallyAdjustLayout) + } else { + setMobile(layout === "mobile") + } + }, [layout]) + + return {mobile, layout, isSavePreferences, setLayout, setIsSavePreferences} +} + +export default UsePreferences; \ No newline at end of file diff --git a/client/src/state/preferences.ts b/client/src/state/preferences.ts index f3c3fbb..7ccbe30 100644 --- a/client/src/state/preferences.ts +++ b/client/src/state/preferences.ts @@ -26,10 +26,10 @@ export const preferencesSlice = createSlice({ setLayout: (state, action) => { state.layout = action.payload; }, - setisSavePreferences: (state, action) => { + setIsSavePreferences: (state, action) => { state.isSavePreferences = action.payload; }, }, }); -export const { setLayout, setisSavePreferences } = preferencesSlice.actions; +export const { setLayout, setIsSavePreferences } = preferencesSlice.actions; From 37582e04d4e759b0003a60067ed41e7e380bb015 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 26 Jan 2024 11:54:36 +0100 Subject: [PATCH 15/16] fix errors for disabled tactics #188 --- server/GameServer/FileWorker.lean | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index 8707894..c687d5a 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -149,7 +149,10 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState : addMessageByDifficulty info s!"The tactic '{val}' is not available in this game!" | some tac => -- Tactic is introduced at some point in the game. - if tac.locked then + if tac.disabled then + -- Tactic is disabled in this level. + addMessageByDifficulty info s!"The tactic '{val}' is disabled in this level!" + else if tac.locked then match workerState.inventory.find? (· == val) with | none => -- Tactic is marked as locked and not in the inventory. @@ -157,9 +160,6 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState : | some _ => -- Tactic is in the inventory, allow it. pure () - else if tac.disabled then - -- Tactic is disabled in this level. - addMessageByDifficulty info s!"The tactic '{val}' is disabled in this level!" | .ident info _rawVal val _preresolved => -- Try to resolve the name let ns ← @@ -181,12 +181,13 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState : addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!" | some thm => -- Theorem is introduced at some point in the game. - if thm.locked then - -- Theorem is still locked. - addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!" - else if thm.disabled then + if thm.disabled then -- Theorem is disabled in this level. addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!" + else if thm.locked then + -- Theorem is still locked. + addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!" + where addMessageByDifficulty (info : SourceInfo) (s : MessageData) := -- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors -- deppending on difficulty. From a67dcb306f591cd471924bb04ea6a8525d9508d3 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 26 Jan 2024 11:55:00 +0100 Subject: [PATCH 16/16] fix indent --- server/GameServer/FileWorker.lean | 50 +++++++++++++++---------------- 1 file changed, 25 insertions(+), 25 deletions(-) diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index c687d5a..ea9878b 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -161,32 +161,32 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState : -- Tactic is in the inventory, allow it. pure () | .ident info _rawVal val _preresolved => - -- Try to resolve the name - let ns ← - try resolveGlobalConst (mkIdent val) - -- Catch "unknown constant" error - catch | _ => pure [] - for n in ns do - let some (.thmInfo ..) := (← getEnv).find? n - -- Not a theorem, no checks needed. - | return () - if some n = levelInfo.statementName then - -- Forbid the theorem we are proving currently - addMessage info inputCtx (severity := .error) - s!"Structural recursion: you can't use '{n}' to proof itself!" - let theoremsAndDefs := levelInfo.lemmas ++ levelInfo.definitions - match theoremsAndDefs.find? (·.name == n) with - | none => - -- Theorem will never be introduced in this game + -- Try to resolve the name + let ns ← + try resolveGlobalConst (mkIdent val) + -- Catch "unknown constant" error + catch | _ => pure [] + for n in ns do + let some (.thmInfo ..) := (← getEnv).find? n + -- Not a theorem, no checks needed. + | return () + if some n = levelInfo.statementName then + -- Forbid the theorem we are proving currently + addMessage info inputCtx (severity := .error) + s!"Structural recursion: you can't use '{n}' to proof itself!" + let theoremsAndDefs := levelInfo.lemmas ++ levelInfo.definitions + match theoremsAndDefs.find? (·.name == n) with + | none => + -- Theorem will never be introduced in this game + addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!" + | some thm => + -- Theorem is introduced at some point in the game. + if thm.disabled then + -- Theorem is disabled in this level. + addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!" + else if thm.locked then + -- Theorem is still locked. addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!" - | some thm => - -- Theorem is introduced at some point in the game. - if thm.disabled then - -- Theorem is disabled in this level. - addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!" - else if thm.locked then - -- Theorem is still locked. - addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!" where addMessageByDifficulty (info : SourceInfo) (s : MessageData) := -- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors