require('./lean.js') kills repl

Open vird opened this issue 10 years ago • 1 comments

I used this one https://raw.githubusercontent.com/leanprover/lean.js/7cdb005b6b96b9d6dd6a6caa0407c682f6e82b3f/lean.js

node
require('./lean.js')

Sep 06 '15 08:09 vird

I can reproduce this one, but I have no idea where the problem comes from, yet.

FYI, we have a shell-script to run a .lean file using a compiled lean.js: https://github.com/leanprover/lean.js/blob/master/run_lean_js.sh

Basically, it puts extra code in front of lean.js and at the end of lean.js, and execute it with node.js. That was all I could do at that time. I'm happy to see an improvement.

Sep 06 '15 15:09 soonhokong