search

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
Other
269 stars 35 forks source link

Build with js_of_ocaml? #844

Open nathancarter opened 2 years ago

nathancarter commented 2 years ago

I'm curious as to whether anyone has tried compiling lambdapi (or the original Dedukti, or the main engine behind each, not necessarily including the specific command-line interface components) into JavaScript using something like js_of_ocaml. I'm working on a web-based logic software project and would be very interested to know if this is possible. I recall several years ago I tried this myself as a quick one-day experiment, but it wasn't straightforward, and both projects (Dedukti and js_of_ocaml) have changed a lot since then. Is this sort of thing expected to work, so perhaps I should try it? Or are there reasons why it won't work? Or has anyone already done it? Any tips or thoughts are welcome. Thank you!

fblanqui commented 2 years ago

Hello @nathancarter . I didn't try myself but @ejgallego did it for Coq and it worked very well (see https://github.com/jscoq/jscoq), and I would be very interested to have lambdapi run online in a web browser too! :-)

ejgallego commented 2 years ago

I think it should be pretty easy, you can indeed start from jsCoq. I'm working on having a more generic setup before working on lambdapi myself.