{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean.js/issues/2","labels_url":"https://api.github.com/repos/leanprover/lean.js/issues/2/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean.js/issues/2/comments","events_url":"https://api.github.com/repos/leanprover/lean.js/issues/2/events","html_url":"https://github.com/leanprover/lean.js/issues/2","id":97907100,"number":2,"title":"add version which uses HoTT ","user":{"login":"fpvandoorn","id":7376012,"avatar_url":"https://avatars.githubusercontent.com/u/7376012?v=3","gravatar_id":"","url":"https://api.github.com/users/fpvandoorn","html_url":"https://github.com/fpvandoorn","followers_url":"https://api.github.com/users/fpvandoorn/followers","following_url":"https://api.github.com/users/fpvandoorn/following{/other_user}","gists_url":"https://api.github.com/users/fpvandoorn/gists{/gist_id}","starred_url":"https://api.github.com/users/fpvandoorn/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/fpvandoorn/subscriptions","organizations_url":"https://api.github.com/users/fpvandoorn/orgs","repos_url":"https://api.github.com/users/fpvandoorn/repos","events_url":"https://api.github.com/users/fpvandoorn/events{/privacy}","received_events_url":"https://api.github.com/users/fpvandoorn/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/leanprover/lean.js/labels/enhancement","name":"enhancement","color":"84b6eb"}],"state":"open","locked":false,"assignee":{"login":"soonhokong","id":403281,"avatar_url":"https://avatars.githubusercontent.com/u/403281?v=3","gravatar_id":"","url":"https://api.github.com/users/soonhokong","html_url":"https://github.com/soonhokong","followers_url":"https://api.github.com/users/soonhokong/followers","following_url":"https://api.github.com/users/soonhokong/following{/other_user}","gists_url":"https://api.github.com/users/soonhokong/gists{/gist_id}","starred_url":"https://api.github.com/users/soonhokong/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/soonhokong/subscriptions","organizations_url":"https://api.github.com/users/soonhokong/orgs","repos_url":"https://api.github.com/users/soonhokong/repos","events_url":"https://api.github.com/users/soonhokong/events{/privacy}","received_events_url":"https://api.github.com/users/soonhokong/received_events","type":"User","site_admin":false},"milestone":null,"comments":15,"created_at":"2015-07-29T10:24:21Z","updated_at":"2015-12-19T12:15:10Z","closed_at":null,"body":"I want to write an article about Lean for the HoTT blog in August, and it would be nice if I can then point to a on-line version of Lean which uses the HoTT instantiation of the kernel and the HoTT library.\r\n\r\nIt can wait until after CADE, because I think you are busy enough until then, but it would be nice if it would be added soon after that."},"comment":{"url":"https://api.github.com/repos/leanprover/lean.js/issues/comments/165981002","html_url":"https://github.com/leanprover/lean.js/issues/2#issuecomment-165981002","issue_url":"https://api.github.com/repos/leanprover/lean.js/issues/2","id":165981002,"user":{"login":"wizardbc","id":16331157,"avatar_url":"https://avatars.githubusercontent.com/u/16331157?v=3","gravatar_id":"","url":"https://api.github.com/users/wizardbc","html_url":"https://github.com/wizardbc","followers_url":"https://api.github.com/users/wizardbc/followers","following_url":"https://api.github.com/users/wizardbc/following{/other_user}","gists_url":"https://api.github.com/users/wizardbc/gists{/gist_id}","starred_url":"https://api.github.com/users/wizardbc/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/wizardbc/subscriptions","organizations_url":"https://api.github.com/users/wizardbc/orgs","repos_url":"https://api.github.com/users/wizardbc/repos","events_url":"https://api.github.com/users/wizardbc/events{/privacy}","received_events_url":"https://api.github.com/users/wizardbc/received_events","type":"User","site_admin":false},"created_at":"2015-12-19T12:15:10Z","updated_at":"2015-12-19T12:15:10Z","body":"I've made some progress in this issue.\r\n\r\n* Change Makefile, major cahnges are as follows:\r\n```Makefile\r\nall: hlean.js\r\n        echo \"done\"\r\n\r\nhlean.js: libs/libgmp.so libs/libmpfr.so libs/liblua.so build/lean/source/lean-master/shell/lean build/lean/source/lean-master/hott.tar.gz\r\n        python build_all.py lean_js\r\n        rm -rf build/lean_js/source/lean-master/shell/hott\r\n        cd build/lean_js/source/lean-master/shell && tar xvfz ../../../../lean/source/lean-master/hott.tar.gz\r\n        rm -rf build/lean_js/source/lean-master/shell/lean.*\r\n        emmake make -C build/lean_js/source/lean-master/ || emmake make -C build/lean_js/source/lean-master/ || emmake make -C build/lean_js/source/lean-master/\r\n\r\nbuild/lean/source/lean-master/hott.tar.gz: build/lean/source/lean-master/shell/lean\r\n        cp .project build/lean/source/lean-master/hott\r\n        cd build/lean/source/lean-master/hott && find . -name \"*.olean\" -delete\r\n        cd build/lean/source/lean-master/hott && ../bin/linja clean && ../bin/linja -X\r\n        cd build/lean/source/lean-master && tar cvfz hott.tar.gz `find hott -name \"*.olean\"`\r\n```\r\n\r\n* Edit .project file:\r\n```\r\n+ *.lean\r\n+ *.hlean\r\n- flycheck*.lean\r\n- flycheck*.hlean\r\n- .#*.lean\r\n- .#*.lean\r\n- theories/\r\n```\r\n\r\n* Do `make`.\r\n\r\n* It will stop with error, because `O_CREAT` is undefined. Insert `#include <fcntl.h>` in 'build/lean_js/source/lean-master/src/util/file_lock.cpp'.\r\n\r\n* Comment out `#python build_all.py lean_js` in the Makefile and do `make` again.\r\n\r\n* Now we are trying to make Lean think it is in HoTT mode by default.\r\n\r\n* In 'build/lean_js/source/lean-master/src/shell/lean.cpp`, line 286,\r\n```cpp\r\n    //input_kind default_k = input_kind::Unspecified;\r\n    input_kind default_k = input_kind::HLean;\r\n```\r\n\r\n* In 'build/lean_js/source/lean-master/src/shell/emscripten.cpp`, line 11,\r\n```cpp\r\n//#include \"library/standard_kernel.h\"\r\n#include \"library/hott_kernel.h\"\r\n```\r\n,line 33\r\n```cpp\r\n        //env(mk_environment(trust_lvl)), ios(opts, lean::mk_pretty_formatter_factory()),\r\n        env(mk_hott_environment(trust_lvl)), ios(opts, lean::mk_pretty_formatter_factory()),\r\n```\r\n\r\n* in 'build/lean_js/source/lean-master/src/util/init_module.cpp', line 28,\r\n```cpp\r\n    //initialize_lean_path();\r\n    initialize_lean_path(true);\r\n```\r\n\r\n* In 'build/lean_js/source/lean-master/src/util/lean_path.cpp', line 121,\r\n```cpp\r\n#if defined(LEAN_EMSCRIPTEN)\r\n    //*g_lean_path = \"/library\";\r\n    if (use_hott)\r\n        *g_lean_path = \"/hott\";\r\n    else\r\n        *g_lean_path = \"/library\";\r\n    g_lean_path_vector->push_back(*g_lean_path);\r\n#else\r\n```\r\n\r\n* In `build/lean_js/source/lean-master/shell/CMakeFiles/lean.js.dir/link.txt` add `--embed-file hott`.\r\n\r\n* Finally, do `make`.\r\n\r\n* In 'run_lean_js.sh', line 46, remove `Module.lean_import_module('standard');` and add below:\r\n```shell-script\r\nModule.lean_import_module('core');\r\n```\r\n\r\n* Let's do some test.\r\n```shell-script\r\n$ ./run_lean_js.sh build/lean_js/source/lean-master/shell/lean.js some.hlean\r\n```\r\n\r\n* I've tried @fpvandoorn 's `cpp.hlean` and it looks like working. But, I'm not an expert in this area, pleas check it. \r\n\r\n* You can test this lean.js at https://wizard.undo.it/lean/hlean.html?live\r\nBut, this server is unstable and untrusted.\r\n\r\n\r\nThank you."}}