some stuff
Alexander Bentkamp
2 years ago
parent
c9f97b3285
commit
afae75e41f
@ -0,0 +1,93 @@
|
|||||||
|
var stderrBuffer = ""
|
||||||
|
var messageBuffer = []
|
||||||
|
var initialized = false;
|
||||||
|
var flushing = false;
|
||||||
|
|
||||||
|
var headerMode = true;
|
||||||
|
var header="";
|
||||||
|
var re = /Content-Length: (\d+)\r\n/i;
|
||||||
|
var contentLength = 0;
|
||||||
|
var content = []
|
||||||
|
var utf8decoder = new TextDecoder();
|
||||||
|
|
||||||
|
|
||||||
|
function flushMessageBuffer(){
|
||||||
|
if (initialized && !flushing) {
|
||||||
|
while(messageBuffer.length > 0) {
|
||||||
|
flushing = true;
|
||||||
|
var msg = messageBuffer.shift();
|
||||||
|
console.log(`Send message: ${msg}`);
|
||||||
|
Module.ccall('send_message', 'void', ['string'], [msg]);
|
||||||
|
console.log(`Message done: ${msg}`);
|
||||||
|
}
|
||||||
|
flushing = false;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
var Module = {
|
||||||
|
"arguments": ["--worker"],
|
||||||
|
"preRun": [function() {
|
||||||
|
function stdin() {
|
||||||
|
return null;
|
||||||
|
}
|
||||||
|
|
||||||
|
function stdout(asciiCode) {
|
||||||
|
if (headerMode) {
|
||||||
|
header += String.fromCharCode(asciiCode)
|
||||||
|
if (header.endsWith('\r\n\r\n')) {
|
||||||
|
const found = header.match(re)
|
||||||
|
if (found == null) { console.error(`Invalid header: ${header}`) }
|
||||||
|
contentLength = parseInt(found[1])
|
||||||
|
content = []
|
||||||
|
headerMode = false
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
content.push(asciiCode)
|
||||||
|
if (content.length == contentLength) {
|
||||||
|
const message = utf8decoder.decode(new Uint8Array(content))
|
||||||
|
console.log(`Server: ${message}`)
|
||||||
|
postMessage(message);
|
||||||
|
headerMode = true
|
||||||
|
header = ''
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
function stderr(asciiCode) {
|
||||||
|
stderrBuffer += String.fromCharCode(asciiCode)
|
||||||
|
}
|
||||||
|
|
||||||
|
FS.init(stdin, stdout, stderr);
|
||||||
|
}],
|
||||||
|
"noInitialRun": true,
|
||||||
|
"onRuntimeInitialized": () => {
|
||||||
|
Module.ccall('main', 'void', [], []);
|
||||||
|
initialized = true;
|
||||||
|
if (stderrBuffer !== "") {
|
||||||
|
console.log(stderrBuffer);
|
||||||
|
stderrBuffer = ""
|
||||||
|
}
|
||||||
|
flushMessageBuffer();
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
importScripts("server.js")
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
onmessage = (ev) => {
|
||||||
|
console.log(`Client: ${ev.data}`)
|
||||||
|
messageBuffer.push(ev.data);
|
||||||
|
flushMessageBuffer();
|
||||||
|
}
|
||||||
|
|
||||||
|
setInterval(() => {
|
||||||
|
if (stderrBuffer !== "") {
|
||||||
|
console.log(stderrBuffer);
|
||||||
|
stderrBuffer = ""
|
||||||
|
}
|
||||||
|
}, 1000)
|
||||||
|
|
||||||
|
setTimeout(() =>{
|
||||||
|
|
||||||
|
},2000)
|
||||||
@ -0,0 +1,339 @@
|
|||||||
|
import { DataCallback, AbstractMessageReader, MessageReader } from 'vscode-jsonrpc/lib/common/messageReader.js';
|
||||||
|
|
||||||
|
import { Message } from 'vscode-jsonrpc/lib/common/messages.js';
|
||||||
|
import { AbstractMessageWriter, MessageWriter } from 'vscode-jsonrpc/lib/common/messageWriter.js';
|
||||||
|
import { Emitter } from 'vscode-jsonrpc/lib/common/events.js';
|
||||||
|
import { Disposable, IWebSocket } from 'vscode-ws-jsonrpc/.';
|
||||||
|
|
||||||
|
declare var IO: any;
|
||||||
|
|
||||||
|
export class WasmWriter implements MessageWriter {
|
||||||
|
protected errorCount = 0;
|
||||||
|
errorEmitter
|
||||||
|
closeEmitter
|
||||||
|
constructor(private worker: Worker) {
|
||||||
|
this.errorEmitter = new Emitter()
|
||||||
|
this.closeEmitter = new Emitter()
|
||||||
|
}
|
||||||
|
dispose() {
|
||||||
|
this.errorEmitter.dispose();
|
||||||
|
this.closeEmitter.dispose();
|
||||||
|
}
|
||||||
|
get onError() {
|
||||||
|
return this.errorEmitter.event;
|
||||||
|
}
|
||||||
|
fireError(error, message, count) {
|
||||||
|
this.errorEmitter.fire([this.asError(error), message, count]);
|
||||||
|
}
|
||||||
|
get onClose() {
|
||||||
|
return this.closeEmitter.event;
|
||||||
|
}
|
||||||
|
fireClose() {
|
||||||
|
this.closeEmitter.fire(undefined);
|
||||||
|
}
|
||||||
|
asError(error) {
|
||||||
|
if (error instanceof Error) {
|
||||||
|
return error;
|
||||||
|
}
|
||||||
|
else {
|
||||||
|
return new Error(`Writer received error. Reason: ${error.message}`);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
end(): void {
|
||||||
|
}
|
||||||
|
|
||||||
|
async write(msg: Message): Promise<void> {
|
||||||
|
try {
|
||||||
|
const content = JSON.stringify(msg);
|
||||||
|
this.worker.postMessage(content)
|
||||||
|
} catch (e) {
|
||||||
|
this.errorCount++;
|
||||||
|
this.fireError(e, msg, this.errorCount);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
export class WasmReader implements MessageReader {
|
||||||
|
protected state: 'initial' | 'listening' | 'closed' = 'initial';
|
||||||
|
protected callback: DataCallback | undefined;
|
||||||
|
protected readonly events: { message?: any, error?: any }[] = [];
|
||||||
|
|
||||||
|
constructor(private worker: Worker) {
|
||||||
|
this.worker.onmessage = (ev) => {
|
||||||
|
this.readMessage(ev.data)
|
||||||
|
}
|
||||||
|
// this.socket.onMessage(message =>
|
||||||
|
// this.readMessage(message)
|
||||||
|
// );
|
||||||
|
// this.socket.onError(error =>
|
||||||
|
// this.fireError(error)
|
||||||
|
// );
|
||||||
|
// this.socket.onClose((code, reason) => {
|
||||||
|
// if (code !== 1000) {
|
||||||
|
// const error: Error = {
|
||||||
|
// name: '' + code,
|
||||||
|
// message: `Error during socket reconnect: code = ${code}, reason = ${reason}`
|
||||||
|
// };
|
||||||
|
// this.fireError(error);
|
||||||
|
// }
|
||||||
|
// this.fireClose();
|
||||||
|
// });
|
||||||
|
this.errorEmitter = new Emitter()
|
||||||
|
this.closeEmitter = new Emitter()
|
||||||
|
this.partialMessageEmitter = new Emitter()
|
||||||
|
}
|
||||||
|
|
||||||
|
protected errorCount = 0;
|
||||||
|
errorEmitter
|
||||||
|
closeEmitter
|
||||||
|
partialMessageEmitter
|
||||||
|
|
||||||
|
dispose() {
|
||||||
|
this.errorEmitter.dispose();
|
||||||
|
this.closeEmitter.dispose();
|
||||||
|
}
|
||||||
|
get onError() {
|
||||||
|
return this.errorEmitter.event;
|
||||||
|
}
|
||||||
|
get onClose() {
|
||||||
|
return this.closeEmitter.event;
|
||||||
|
}
|
||||||
|
get onPartialMessage() {
|
||||||
|
return this.partialMessageEmitter.event;
|
||||||
|
}
|
||||||
|
firePartialMessage(info) {
|
||||||
|
this.partialMessageEmitter.fire(info);
|
||||||
|
}
|
||||||
|
asError(error) {
|
||||||
|
if (error instanceof Error) {
|
||||||
|
return error;
|
||||||
|
}
|
||||||
|
else {
|
||||||
|
return new Error(`Reader received error. Reason: ${error.message ? error.message : 'unknown'}`);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
listen(callback: DataCallback): Disposable {
|
||||||
|
if (this.state === 'initial') {
|
||||||
|
this.state = 'listening';
|
||||||
|
this.callback = callback;
|
||||||
|
while (this.events.length !== 0) {
|
||||||
|
const event = this.events.pop()!;
|
||||||
|
if (event.message) {
|
||||||
|
this.readMessage(event.message);
|
||||||
|
} else if (event.error) {
|
||||||
|
this.fireError(event.error);
|
||||||
|
} else {
|
||||||
|
this.fireClose();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return {
|
||||||
|
dispose: () => {
|
||||||
|
if (this.callback === callback) {
|
||||||
|
this.callback = undefined;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
};
|
||||||
|
}
|
||||||
|
|
||||||
|
protected readMessage(message: any): void {
|
||||||
|
if (this.state === 'initial') {
|
||||||
|
this.events.splice(0, 0, { message });
|
||||||
|
} else if (this.state === 'listening') {
|
||||||
|
try {
|
||||||
|
const data = JSON.parse(message);
|
||||||
|
this.callback!(data);
|
||||||
|
} catch (err) {
|
||||||
|
const error: Error = {
|
||||||
|
name: '' + 400,
|
||||||
|
message: `Error during message parsing, reason = ${typeof err === 'object' ? (err as any).message : 'unknown'}`
|
||||||
|
};
|
||||||
|
this.fireError(error);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
protected fireError(error: any): void {
|
||||||
|
if (this.state === 'initial') {
|
||||||
|
this.events.splice(0, 0, { error });
|
||||||
|
} else if (this.state === 'listening') {
|
||||||
|
|
||||||
|
this.errorEmitter.fire(this.asError(error));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
protected fireClose(): void {
|
||||||
|
if (this.state === 'initial') {
|
||||||
|
this.events.splice(0, 0, {});
|
||||||
|
} else if (this.state === 'listening') {
|
||||||
|
this.closeEmitter.fire(undefined);
|
||||||
|
}
|
||||||
|
this.state = 'closed';
|
||||||
|
}
|
||||||
|
}
|
||||||
|
export class WebSocketMessageWriter implements MessageWriter {
|
||||||
|
protected errorCount = 0;
|
||||||
|
errorEmitter
|
||||||
|
closeEmitter
|
||||||
|
|
||||||
|
constructor(protected readonly socket: IWebSocket) {
|
||||||
|
this.errorEmitter = new Emitter();
|
||||||
|
this.closeEmitter = new Emitter();
|
||||||
|
}
|
||||||
|
dispose() {
|
||||||
|
this.errorEmitter.dispose();
|
||||||
|
this.closeEmitter.dispose();
|
||||||
|
}
|
||||||
|
get onError() {
|
||||||
|
return this.errorEmitter.event;
|
||||||
|
}
|
||||||
|
fireError(error, message, count) {
|
||||||
|
this.errorEmitter.fire([this.asError(error), message, count]);
|
||||||
|
}
|
||||||
|
get onClose() {
|
||||||
|
return this.closeEmitter.event;
|
||||||
|
}
|
||||||
|
fireClose() {
|
||||||
|
this.closeEmitter.fire(undefined);
|
||||||
|
}
|
||||||
|
asError(error) {
|
||||||
|
if (error instanceof Error) {
|
||||||
|
return error;
|
||||||
|
}
|
||||||
|
else {
|
||||||
|
return new Error(`Writer received error. Reason: ${(error.message) ? error.message : 'unknown'}`);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
end(): void {
|
||||||
|
}
|
||||||
|
|
||||||
|
async write(msg: Message): Promise<void> {
|
||||||
|
console.log("WRITE",msg)
|
||||||
|
try {
|
||||||
|
const content = JSON.stringify(msg);
|
||||||
|
this.socket.send(content);
|
||||||
|
} catch (e) {
|
||||||
|
this.errorCount++;
|
||||||
|
this.fireError(e, msg, this.errorCount);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
export class WebSocketMessageReader implements MessageReader {
|
||||||
|
protected state: 'initial' | 'listening' | 'closed' = 'initial';
|
||||||
|
protected callback: DataCallback | undefined;
|
||||||
|
protected readonly events: { message?: any, error?: any }[] = [];
|
||||||
|
errorEmitter
|
||||||
|
closeEmitter
|
||||||
|
partialMessageEmitter
|
||||||
|
|
||||||
|
constructor(protected readonly socket: IWebSocket) {
|
||||||
|
this.errorEmitter = new Emitter();
|
||||||
|
this.closeEmitter = new Emitter();
|
||||||
|
this.partialMessageEmitter = new Emitter();
|
||||||
|
this.socket.onMessage(message =>{
|
||||||
|
console.log("READ", message)
|
||||||
|
this.readMessage(message)
|
||||||
|
});
|
||||||
|
this.socket.onError(error =>
|
||||||
|
this.fireError(error)
|
||||||
|
);
|
||||||
|
this.socket.onClose((code, reason) => {
|
||||||
|
if (code !== 1000) {
|
||||||
|
const error: Error = {
|
||||||
|
name: '' + code,
|
||||||
|
message: `Error during socket reconnect: code = ${code}, reason = ${reason}`
|
||||||
|
};
|
||||||
|
this.fireError(error);
|
||||||
|
}
|
||||||
|
this.fireClose();
|
||||||
|
});
|
||||||
|
}
|
||||||
|
dispose() {
|
||||||
|
this.errorEmitter.dispose();
|
||||||
|
this.closeEmitter.dispose();
|
||||||
|
}
|
||||||
|
get onError() {
|
||||||
|
return this.errorEmitter.event;
|
||||||
|
}
|
||||||
|
get onClose() {
|
||||||
|
return this.closeEmitter.event;
|
||||||
|
}
|
||||||
|
get onPartialMessage() {
|
||||||
|
return this.partialMessageEmitter.event;
|
||||||
|
}
|
||||||
|
firePartialMessage(info) {
|
||||||
|
this.partialMessageEmitter.fire(info);
|
||||||
|
}
|
||||||
|
asError(error) {
|
||||||
|
if (error instanceof Error) {
|
||||||
|
return error;
|
||||||
|
}
|
||||||
|
else {
|
||||||
|
return new Error(`Reader received error. Reason: ${(error.message) ? error.message : 'unknown'}`);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
listen(callback: DataCallback): Disposable {
|
||||||
|
if (this.state === 'initial') {
|
||||||
|
this.state = 'listening';
|
||||||
|
this.callback = callback;
|
||||||
|
while (this.events.length !== 0) {
|
||||||
|
const event = this.events.pop()!;
|
||||||
|
if (event.message) {
|
||||||
|
this.readMessage(event.message);
|
||||||
|
} else if (event.error) {
|
||||||
|
this.fireError(event.error);
|
||||||
|
} else {
|
||||||
|
this.fireClose();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return {
|
||||||
|
dispose: () => {
|
||||||
|
if (this.callback === callback) {
|
||||||
|
this.callback = undefined;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
};
|
||||||
|
}
|
||||||
|
|
||||||
|
protected readMessage(message: any): void {
|
||||||
|
if (this.state === 'initial') {
|
||||||
|
this.events.splice(0, 0, { message });
|
||||||
|
} else if (this.state === 'listening') {
|
||||||
|
try {
|
||||||
|
const data = JSON.parse(message);
|
||||||
|
this.callback!(data);
|
||||||
|
} catch (err) {
|
||||||
|
const error: Error = {
|
||||||
|
name: '' + 400,
|
||||||
|
message: `Error during message parsing, reason = ${typeof err === 'object' ? (err as any).message : 'unknown'}`
|
||||||
|
};
|
||||||
|
this.fireError(error);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
protected fireError(error: any): void {
|
||||||
|
if (this.state === 'initial') {
|
||||||
|
this.events.splice(0, 0, { error });
|
||||||
|
} else if (this.state === 'listening') {
|
||||||
|
this.errorEmitter.fire(this.asError(error));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
protected fireClose(): void {
|
||||||
|
if (this.state === 'initial') {
|
||||||
|
this.events.splice(0, 0, {});
|
||||||
|
} else if (this.state === 'listening') {
|
||||||
|
this.closeEmitter.fire(undefined);
|
||||||
|
}
|
||||||
|
this.state = 'closed';
|
||||||
|
}
|
||||||
|
}
|
||||||
@ -0,0 +1,37 @@
|
|||||||
|
#!/bin/bash
|
||||||
|
|
||||||
|
cd server
|
||||||
|
|
||||||
|
mkdir -p .lake/toolchains
|
||||||
|
if [ ! -f .lake/toolchains/lean-4.3.0-rc2-linux_wasm32.tar.zst ]
|
||||||
|
then
|
||||||
|
wget -P .lake/toolchains https://github.com/leanprover/lean4/releases/download/v4.3.0-rc2/lean-4.3.0-rc2-linux_wasm32.tar.zst
|
||||||
|
tar --use-compress-program=unzstd -xvf .lake/toolchains/lean-4.3.0-rc2-linux_wasm32.tar.zst -C .lake/toolchains
|
||||||
|
fi
|
||||||
|
if [ ! -f .lake/toolchains/lean-4.3.0-rc2-linux_x86.tar.zst ]
|
||||||
|
then
|
||||||
|
wget -P .lake/toolchains https://github.com/leanprover/lean4/releases/download/v4.3.0-rc2/lean-4.3.0-rc2-linux_x86.tar.zst
|
||||||
|
tar --use-compress-program=unzstd -xvf .lake/toolchains/lean-4.3.0-rc2-linux_x86.tar.zst -C .lake/toolchains
|
||||||
|
fi
|
||||||
|
|
||||||
|
# Linking will fail, but that's ok. We only need the c files.
|
||||||
|
.lake/toolchains/lean-4.3.0-rc2-linux_x86/bin/lake build -f=lakefile32.lean
|
||||||
|
|
||||||
|
|
||||||
|
lake build
|
||||||
|
|
||||||
|
|
||||||
|
OUT_DIR=../client/public
|
||||||
|
LEAN_SYSROOT=.lake/toolchains/lean-4.3.0-rc2-linux_wasm32
|
||||||
|
LEAN_LIBDIR=$LEAN_SYSROOT/lib/lean
|
||||||
|
|
||||||
|
emcc -o $OUT_DIR/server.js main.c -I $LEAN_SYSROOT/include -L $LEAN_LIBDIR .lake/build/ir/GameServer/*.c -lInit -lLean -lleancpp -lleanrt \
|
||||||
|
-sFORCE_FILESYSTEM -lnodefs.js -s EXIT_RUNTIME=0 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto \
|
||||||
|
-sPTHREAD_POOL_SIZE_STRICT=2 \
|
||||||
|
--preload-file "${LEAN_SYSROOT}/lib/lean/Init"@/lib/Init \
|
||||||
|
--preload-file "${LEAN_SYSROOT}/lib/lean/Init.olean"@/lib/Init.olean \
|
||||||
|
--preload-file "${LEAN_SYSROOT}/lib/lean/Init.ilean"@/lib/Init.ilean \
|
||||||
|
--preload-file "${LEAN_SYSROOT}/lib/lean/Lean"@/lib/Lean \
|
||||||
|
--preload-file "${LEAN_SYSROOT}/lib/lean/Lean.olean"@/lib/Lean.olean \
|
||||||
|
--preload-file "${LEAN_SYSROOT}/lib/lean/Lean.ilean"@/lib/Lean.ilean \
|
||||||
|
--preload-file "./.lake/build32/lib"@/gamelib
|
||||||
Loading…
Reference in New Issue