Improve functionality for newer lean versions

bin/make-lean-game

@@ -27,6 +27,9 @@ def render_lean_project(outdir=None, nolib=False, devmode=False, locale='en'):
     if 'extra_files' in game_config and Path(game_config['extra_files']).is_dir():
         distutils.dir_util.copy_tree(str(Path('.')/game_config['extra_files']), str(Path(outdir)/game_config['extra_files']))
 
+    lean_server_path = None
+    if 'lean_server_path' in game_config:
+        lean_server_path = Path('.') / game_config['lean_server_path']
 
     name = game_config.get('name', 'Lean game')
     version = str(game_config.get('version', ''))
@@ -45,8 +48,11 @@ def render_lean_project(outdir=None, nolib=False, devmode=False, locale='en'):
     }
 
 
-    InteractiveServer(interactive_path=interactive_path, outdir=outdir,
-            library_zip_fn= game_data['library_zip_fn']).copy_files(make_lib = not nolib)
+    InteractiveServer(
+        interactive_path=interactive_path,
+        outdir=outdir,
+        library_zip_fn= game_data['library_zip_fn']
+    ).copy_files(lean_server_path, make_lib = not nolib, devmode = devmode)
 
 
     file_reader = FileReader(translator, default_line_handler, readers_list)

setup.py

@@ -26,5 +26,14 @@
         '': ['*.css', '*.css.map', '*.js', 'templates/*'] + interactive_files,
     },
     scripts=['bin/make-lean-game'],
-    install_requires=['regex >= 2018.7.11', 'jinja2 >= 2.10', 'mistletoe >= 0.7.1', 'toml >= 0.10.0', 'fire >= 0.1.3', 'jsonpickle >= 1.2', 'polib >= 1.1.0'])
+    install_requires=[
+        'regex >= 2018.7.11',
+        'jinja2 >= 2.10',
+        'mistletoe >= 0.7.1',
+        'toml >= 0.10.0',
+        'fire >= 0.1.3',
+        'jsonpickle >= 1.2',
+        'polib >= 1.1.0',
+        'requests >= 2.28.2',
+    ])
 

src/interactive_interface/package.json

@@ -9,7 +9,7 @@
   "author": "Mohammad Pedramfar",
   "license": "Apache-2.0",
   "dependencies": {
-    "@bryangingechen/lean-client-js-browser": "^1.4.0",
+    "lean-client-js-browser": "^3.0.0",
     "@types/node": "^12.12.36",
     "@types/react": "^16.9.34",
     "@types/react-dom": "^16.9.6",

src/interactive_interface/src/index.tsx

@@ -1,5 +1,5 @@
 /// <reference types="monaco-editor" />
-import { InfoRecord, LeanJsOpts, Message } from '@bryangingechen/lean-client-js-browser';
+import { InfoRecord, LeanJsOpts, Message } from 'lean-client-js-browser';
 import * as React from 'react';
 import { findDOMNode, render } from 'react-dom';
 import { allMessages, checkInputCompletionChange, checkInputCompletionPosition, currentlyRunning, delayMs,
@@ -1708,4 +1708,4 @@ class PageManager {
 }
 
 
-PageManager.run();
+PageManager.run();

src/interactive_interface/src/langservice.ts

@@ -1,5 +1,5 @@
 /// <reference types="monaco-editor" />
-import * as lean from '@bryangingechen/lean-client-js-browser';
+import * as lean from 'lean-client-js-browser';
 import { leanSyntax } from './syntax';
 import * as translations from './translations.json';
 

src/interactive_interface/src/translations.json

@@ -387,6 +387,10 @@
     "tau": "τ",
     "top": "⊤",
     "to": "→",
+    "smul": "•",
+    "scalar": "•",
+    "bsmul": "•",
+    "bullet": "•",
     "def=": "≝",
     "defs": "≙",
     "degree": "°",

src/lean_game_maker/interactive_loader.py

@@ -4,6 +4,9 @@
 import glob, distutils.dir_util
 from pathlib import Path
 import toml
+from typing import Optional, Tuple
+from requests import get
+from io import BytesIO
 
 
 class InteractiveServer:
@@ -18,16 +21,18 @@ def __init__(self, interactive_path, outdir, library_zip_fn):
             raise FileNotFoundError("Couldn't find a leanpkg.toml, I give up.")
         toolchain = leanpkg_toml['package']['lean_version']
 
-        if os.name == 'nt':
-            self.js_wasm_path = Path(self.interactive_path / 'lean_server' / toolchain.replace(':', ' '))
+        if ':' in toolchain:
+            repo, _, ver = toolchain.partition(':')
+            self.toolchain = (repo, ver)
         else:
-            self.js_wasm_path = Path(self.interactive_path / 'lean_server' / toolchain)
+            self.toolchain = ('leanprover/lean', toolchain)
 
-    def make_library(self):
+    def make_library(self, devmode: bool):
         library_zip_fn = self.library_zip_fn
 
         source_lib = "."
         source_lib_path = str(Path(source_lib).resolve()) + '/src'
+        compression = None if devmode else 9
 
         subprocess.call(['leanpkg', 'build'])
 
@@ -47,7 +52,9 @@ def make_library(self):
         oleans = {}
         num_olean = {}
         Path(library_zip_fn).parent.mkdir(parents=True, exist_ok=True)
-        with zipfile.ZipFile(library_zip_fn, mode='w', compression=zipfile.ZIP_DEFLATED, allowZip64=False, compresslevel=9) as zf:
+        with zipfile.ZipFile(library_zip_fn, mode='w',
+                             compression=zipfile.ZIP_DEFLATED,
+                             allowZip64=False, compresslevel=compression) as zf:
             for p in lean_path:
                 parts = p.parts
                 if str(p.resolve()) == source_lib_path: # if using source_lib/src
@@ -106,17 +113,37 @@ def make_library(self):
                 f.write('\n')
                 print('Wrote olean map to {0}'.format(map_fn))        
 
-    def check_server_exists(self):
-        self.js_wasm_path.mkdir(parents=True, exist_ok=True)
+    def check_server_exists(self, js_wasm_path: Path):
         for f in ['lean_js_js.js', 'lean_js_wasm.js', 'lean_js_wasm.wasm']:
-            if not (self.js_wasm_path/f).is_file():
-                raise FileNotFoundError(f'Could not find the file "{self.js_wasm_path/f}" which is necessary to run Lean in the browser.')
+            if not (js_wasm_path/f).is_file():
+                raise FileNotFoundError(f'Could not find the file "{js_wasm_path/f}" which is necessary to run Lean in the browser.')
 
+    def get_lean_server(self, js_wasm_path: Path):
+        print(f'Lean server not found; downloading to {js_wasm_path}')
+        url = f'https://github.com/{self.toolchain[0]}/releases/download/v{self.toolchain[1]}/lean-{self.toolchain[1]}--browser.zip'
+        r = get(url)
+        with zipfile.ZipFile(BytesIO(r.content)) as zip:
+            for f in ['lean_js_js.js', 'lean_js_wasm.js', 'lean_js_wasm.wasm']:
+                zip.getinfo(f'build/shell/{f}').filename = f
+                zip.extract(f'build/shell/{f}', js_wasm_path)
 
-    def copy_files(self, make_lib=True):
-        self.check_server_exists()
+
+    def copy_files(self, lean_server_path: Optional[Path], make_lib=True, devmode=False):
+        if lean_server_path:
+            if not lean_server_path.is_dir():
+                raise FileNotFoundError(f'Could not find the manually specified lean_server_path: {lean_server_path}')
+            js_wasm_path = lean_server_path
+        else:
+            js_wasm_path = Path('./lean_server') / self.toolchain[0] / self.toolchain[1]
+            js_wasm_path.mkdir(parents=True, exist_ok=True)
+            try:
+                self.check_server_exists(js_wasm_path)
+            except FileNotFoundError:
+                self.get_lean_server(js_wasm_path)
+
+        self.check_server_exists(js_wasm_path)
 
         distutils.dir_util.copy_tree(self.interactive_path / 'dist', str(Path(self.outdir)))
-        distutils.dir_util.copy_tree(self.js_wasm_path, str(Path(self.outdir)))
+        distutils.dir_util.copy_tree(js_wasm_path, str(Path(self.outdir)))
         if make_lib:
-            self.make_library()
+            self.make_library(devmode)