Running Abella in the browser #156
Comments
|
This has already been done once before:
https://abella-prover.org/tutorial/try
It's a few versions old, but updating it to the current version is one of
the things I hope to do after the deadline season is over.
(The dependency on curl could easily be mocked for the javascript target
using fetch(), but that's a minor concern.)
…On Sun, May 19, 2024 at 5:28 PM Taus ***@***.***> wrote:
Inspired by @jcreedcmu <https://github.com/jcreedcmu>'s recent success
with getting Twelf to run in the browser (see
https://github.com/jcreedcmu/twelf-wasm), I wanted to see if we could get
something similar working for Abella.
TL;DR: I think the answer is "probably, with a bit of work". My
observations are below.
Building Abella
This was straightforward after installing opam and cloning this repo. I
did find, however, that I needed to do opam install ./abella.opam in
order for make to succeed, otherwise it would complain about missing
dependencies. (This is perhaps obvious to people who use opam regularly,
but it might be worth pointing out in the README anyway.)
Building Abella with js_of_ocaml
After installing js_of_ocaml with opam, getting it to build with dune was
as easy as adding js as a mode for the abella executable:
--- a/src/dune+++ b/src/dune@@ -1,6 +1,6 @@
(executable
(name abella)- (modes byte exe) + (modes byte exe js)
(modules abella)
Running dune build src/abella.bc.js then creates the desired JavaScript
file.
libcurl woes
Alas, attempting to actually run it isn't as successful:
~/abella$ node _build/default/src/abella.bc.js
/home/tausbn/abella/_build/default/src/abella.bc.js:3153
throw err;
^
TypeError: runtime.caml_curl_version is not a function
at Curl (/home/tausbn/abella/_build/default/src/abella.bc.js:42843:37)
at caml_call1 (/home/tausbn/abella/_build/default/src/abella.bc.js:56476:15)
at /home/tausbn/abella/_build/default/src/abella.bc.js:56558:11
at Object.<anonymous> (/home/tausbn/abella/_build/default/src/abella.bc.js:56986:3)
at Module._compile (node:internal/modules/cjs/loader:1275:14)
at Module._extensions..js (node:internal/modules/cjs/loader:1329:10)
at Module.load (node:internal/modules/cjs/loader:1133:32)
at Module._load (node:internal/modules/cjs/loader:972:12)
at Function.executeUserEntryPoint [as runMain] (node:internal/modules/run_main:83:12)
at node:internal/main/run_main_module:23:47
Node.js v19.9.0
The culprit turns out to be the support for loading files over the
internet. (I had to do a bit of spelunking to figure out what cURL was even
being used for. It seems the change log entry was removed
<70ea6dd>
in the 2.0.8.1 release. Perhaps this entry should be added back if that
feature is here to stay?)
Because js_of_ocaml has no idea what to do about this external library,
it simply inserts a stub that throws an exception when the relevant
function is called.
However, in this case, we're only using the library to print out its
version, so what if we just get rid of that code?
--- a/src/source.ml+++ b/src/source.ml@@ -44,9 +44,8 @@ open struct
"Jul" ; "Aug" ; "Sep" ; "Oct" ; "Nov" ; "Dec" |]
let abella_agent =- Printf.sprintf "Abella %s (using libcurl %s)"+ Printf.sprintf "Abella %s (using libcurl)"
Version.version- (Curl.version ())
let http_strftime t =
let tm = Unix.gmtime t in
Success...ish
With the above patch, abella.bc.js successfully builds *and runs*:
~/abella$ node _build/default/src/abella.bc.js
Welcome to Abella 2.1.0-dev.
Abella < Kind t type.
Abella < Type a t.
Abella < Theorem refl : a = a.
============================
a = a
refl < search.
Proof completed
It's not quite *perfect*, though. In particular, exiting abella using
Ctrl-D results in the following error message:
Abella < Fatal error: exception Sys_error("Cannot flush a closed channel")
The same thing happens if you run Abella in batch mode.
It's also not happy about importing other files:
~/abella$ node _build/default/src/abella.bc.js ../abella-reasoning/lib/merge.thm
Type is_o o -> prop.
Import "perm" with is_o := is_o.
Importing: "../abella-reasoning/lib/perm".
/bin/sh: 1: /home/tausbn/abella/_build/default/src/abella.bc.js: Permission denied
Error: Could not create "../abella-reasoning/lib/perm.thc"
(The same thing happens when using an absolute path instead.)
In the browser
Alas, it doesn't seem to run properly in the browser, and I'm not really
sure why.
With a simple HTML file that just tries to load the abella.bc.js file in
a script tag, I get the following error:
Uncaught
Array(3) [ 0, (3) […], "/static/a.out: No such file or directory" ]
+fail.js:25:48
caml_raise_with_arg +fail.js:25
caml_raise_with_string +fail.js:34
caml_raise_sys_error +sys.js:23
caml_raise_no_such_file +fs.js:193
open +fs_fake.js:236
caml_sys_open +io.js:71
open_in_gen stdlib.ml:405
open_in_bin stdlib.ml:404
caml_call1 abella.bc.js:24155
file digest.ml:39
caml_call1 abella.bc.js:42867
<anonymous> version.ml:9
<anonymous> abella.bc.js:42880
where the array returned is as follows:
[
0,
[
248,
"Sys_error",
-2
],
"/static/a.out: No such file or directory"
]
Where to go from here
In order to get this running properly, I think we would need to address
the following points:
-
Exposing the main functionality of Abella as a JS library.
For this, the best solution would probably be to expose a JavaScript
function for posting a command (i.e. string) to the Abella kernel (and
getting a response in return). This would bypass the need to run a
toplevel, and circumvent the printing of the libcurl version that is
causing issues right now (as well as the "closed channel" error).
-
Exposing an interface of file access callbacks.
By this I mean a mechanism of telling the kernel "when you want to
read/write a file (or URL), call *this* function". That way, something
like accessing a URL can be delegated to the JavaScript side (and be
implemented using the fetch API or something along those lines).
Making this layer abstract would also enable running Abella on iOS via
a-Shell <https://github.com/holzschu/a-shell> (which provides its own
set of JavaScript functions for interacting with the iOS file system).
It's unclear how much effort would be needed to do the above things. My
knowledge of OCaml is extremely rusty (and my knowledge of the Abella code
base in particular is basically non-existent), so I don't think these are
tasks I can take on myself.
Still, given that compiling to JavaScript seems to work basically without
any issues (apart from some headaches in the interface layer), I think it
would be worthwhile to see if we could get Abella running fully in the
browser. It would be *fantastic* to have this available in the
walkthrough, for instance (and this I would gladly help out with).
—
Reply to this email directly, view it on GitHub
<#156>, or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAEMD2HCBG6NR7LOGRZAIEDZDDAJJAVCNFSM6AAAAABH6OSNROVHI2DSMVQWIX3LMV43ASLTON2WKOZSGMYDINRWGIYTSNQ>
.
You are receiving this because you are subscribed to this thread.Message
ID: ***@***.***>
|
|
Ah! I had no idea! I'll go play with that in the meantime, then. 🙂 |
|
There have been a few recent feature requests for updating the Abella on the web implementation, perhaps using the wasm backend. It's now a new "milestone" on Github. Let's hope creating the milestone gives us an incentive to make progress. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Inspired by @jcreedcmu's recent success with getting Twelf to run in the browser (see https://github.com/jcreedcmu/twelf-wasm), I wanted to see if we could get something similar working for Abella.
TL;DR: I think the answer is "probably, with a bit of work". My observations are below.
Building Abella
This was straightforward after installing
opamand cloning this repo. I did find, however, that I needed to doopam install ./abella.opamin order formaketo succeed, otherwise it would complain about missing dependencies. (This is perhaps obvious to people who useopamregularly, but it might be worth pointing out in the README anyway.)Building Abella with
js_of_ocamlAfter installing
js_of_ocamlwithopam, getting it to build withdunewas as easy as addingjsas a mode for theabellaexecutable:Running
dune build src/abella.bc.jsthen creates the desired JavaScript file.libcurlwoesAlas, attempting to actually run it isn't as successful:
The culprit turns out to be the support for loading files over the internet. (I had to do a bit of spelunking to figure out what cURL was even being used for. It seems the change log entry was removed in the 2.0.8.1 release. Perhaps this entry should be added back if that feature is here to stay?)
Because
js_of_ocamlhas no idea what to do about this external library, it simply inserts a stub that throws an exception when the relevant function is called.However, in this case, we're only using the library to print out its version, so what if we just get rid of that code?
Success...ish
With the above patch,
abella.bc.jssuccessfully builds and runs:It's not quite perfect, though. In particular, exiting
abellausing Ctrl-D results in the following error message:The same thing happens if you run Abella in batch mode.
It's also not happy about importing other files:
(The same thing happens when using an absolute path instead.)
In the browser
Alas, it doesn't seem to run properly in the browser, and I'm not really sure why.
With a simple HTML file that just tries to load the
abella.bc.jsfile in ascripttag, I get the following error:where the array returned is as follows:
Where to go from here
In order to get this running properly, I think we would need to address the following points:
Exposing the main functionality of Abella as a JS library.
For this, the best solution would probably be to expose a JavaScript function for posting a command (i.e. string) to the Abella kernel (and getting a response in return). This would bypass the need to run a toplevel, and circumvent the printing of the
libcurlversion that is causing issues right now (as well as the "closed channel" error).Exposing an interface of file access callbacks.
By this I mean a mechanism of telling the kernel "when you want to read/write a file (or URL), call this function". That way, something like accessing a URL can be delegated to the JavaScript side (and be implemented using the
fetchAPI or something along those lines). Making this layer abstract would also enable running Abella on iOS via a-Shell (which provides its own set of JavaScript functions for interacting with the iOS file system).It's unclear how much effort would be needed to do the above things. My knowledge of OCaml is extremely rusty (and my knowledge of the Abella code base in particular is basically non-existent), so I don't think these are tasks I can take on myself.
Still, given that compiling to JavaScript seems to work basically without any issues (apart from some headaches in the interface layer), I think it would be worthwhile to see if we could get Abella running fully in the browser. It would be fantastic to have this available in the walkthrough, for instance (and this I would gladly help out with).
The text was updated successfully, but these errors were encountered: