latte-central / LaTTe

LaTTe : a Laboratory for Type Theory experiments (in clojure)
http://latte-central.github.io/LaTTe/
MIT License
256 stars 13 forks source link

port the code to be clojurescript and self-host friendly #4

Closed viebel closed 7 years ago

viebel commented 8 years ago

It would be great to be able to run LaTTE in the browser with the klipse plugin for instance. For that purpose, one needs to port the code to clojurescript (with cljc) and also make it compatible with self-host (a.k.a. bootstraped) clojurescript.

viebel commented 8 years ago

@fredokun I have start to work on the port of LaTTE here but it's quite hard.

fredokun commented 8 years ago

Wow! You've started! Sadly I cannot look at this closely at the moment, but I can create a branch "cljs" and when time permits try to follow what you are doing. Is there a place to learn about "self-host-friendliness" ? (One of the important part of LaTTe is that the proofs are checked at macro-expansion time, but this requirement could be released for the specific need of in-browser evaluation)

fredokun commented 8 years ago

Thinking about this... I think the top-level forms should be somewhat different in the cljs case. maybe the kernel should go in a separate repo. (I will consider this in time...).

viebel commented 8 years ago

Why the top level forms should be different in cljs?

fredokun commented 8 years ago

Well, I think the semantics of the 'clj/jvm' and the 'cljs/klipse' workflows should be slightly different. Klipse would be mainly to make "live mathematics" webpages whereas the main objective of "plain" LaTTe is to create mathematical libraries (hopefully .cljc libraries so that everything is compatible). But you know much better about the cljs/klipse part so I will not take any action for now ;-). (and what about the cljs branch? I can make you a collaborator ...)

viebel commented 8 years ago

Cljs braxh is a good idea. Please call it self-host

On Fri, Sep 2, 2016, 11:24 Frederic Peschanski notifications@github.com wrote:

Well, I think the semantics of the 'clj/jvm' and the 'cljs/klipse' workflows should be slightly different. Klipse would be mainly to make "live mathematics" webpages whereas the main objective of "plain" LaTTe is to create mathematical libraries (hopefully .cljc libraries so that everything is compatible). But you know much better about the cljs/klipse part so I will not take any action for now ;-). (and what about the cljs branch? I can make you a collaborator ...)

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/fredokun/LaTTe/issues/4#issuecomment-244314012, or mute the thread https://github.com/notifications/unsubscribe-auth/AA6VPrsuSIuuW0kItotCr5GE_C7tJLXWks5ql90ngaJpZM4JwKR8 .

fredokun commented 8 years ago

I think because of the heavy use of macro-expansion for checking proof (proofs are checked at compile-time) I think it's difficult to port LaTTe as it is... But I have the idea of a port of just the kernel and then work on clojurescript (and Klipse) specific top level forms (only for making interactive documents, but the sharing of libraries might be a problem...).

viebel commented 8 years ago

I'd love to help porting the kernel.

And good luck for EuroClojure!

fredokun commented 7 years ago

I am finding some spare time to rewrite the LaTTe kernel in a cljs-friendly way. This happens at: https://github.com/latte-central/latte-kernel.