This repo contains a scripts, wrappers, and libraries to run F* in the browser. More precisely, it includes the following:
- Scripts and adapters (
src/ocaml/) to compile F* to JavaScript using js_of_ocaml. - TypeScript libraries to connect JavaScript builds of F* to Z3.wasm.
- TypeScript sources and CSS styles to turn literate-F* documents compiled with
fslitinto interactive F* notebooks.
Loading Z3 and F* and downloading F* libraries is fairly slow (~15 seconds on Chrome, though less than 1 second on Firefox), but verification performance is fairly good (typically within a factor 2-5 of native on Chrome, and 3-10 of native on Firefox).
Pre-built archives are available at https://github.com/cpitclaudel/fstar.js/releases.
Clone this repository:
git clone --recurse-submodules git@github.com:cpitclaudel/fstar.js.git
Switch to OCaml 4.04.0 and install dependencies:
opam switch 4.04.0 eval `opam config env` opam install batteries menhir pprint stdint ulex yojson zarith js_of_ocaml js_of_ocaml-ppx (cd lib; npm install)
Compile
js_of_ocaml:# Install dependencies listed in vendor/js_of_ocaml/manual/contribute.wiki make -C vendor/js_of_ocaml
Fetch a release of
z3.wasmfrom https://github.com/cpitclaudel/z3.wasm/releases/ and extract it tovendor/z3.wasm.Compile F* and the supporting libraries to JavaScript:
make make dist
Make sure that everything works:
make serve chromium-browser http://localhost:8000/web/fstar.cli.html chromium-browser http://localhost:8000/web/fstar.ide.literate.stlc.html chromium-browser http://localhost:8000/web/fstar.ide.literate.client.html
The recommended way to integrate F*.js in your documents is to use fslit and Sphinx.
Other options are listed below:
web/fstar.cli.htmldemonstrates how to setupF*.jsfor single-file verification.Add the following style sheets in your page's
<head>:<link rel="stylesheet" href="./fstar.js/cm.tango.css" /> <link rel="stylesheet" href="./fstar.js/fstar.cli.css" /> <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.36.0/codemirror.min.css" />
Add the following scripts to the end of page's your
<body>:<script src="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.36.0/codemirror.min.js"></script> <script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.2.1/jquery.min.js"></script> <script src="https://cdnjs.cloudflare.com/ajax/libs/underscore.js/1.8.3/underscore-min.js"></script> <script src="./fstar.js/fstar.cm.js"></script> <script src="./fstar.js/fstar.client.js"></script>
Set up the CLI integration:
<script> // Tell F*.js where to look for web worker scripts FStar.CLI.WORKER_DIRECTORY = "./fstar.js/"; // Set up the CLI backend var $editor = $(".standalone-editor"); var client = new FStar.CLI.Client($editor, "file-name.fst", $editor.text()); </script>
web/fstar.ide.literate.stlc.htmldemonstrates how to turn a literate-F* document into an interactive F* notebook. Most of this can be done for you byfslit.Add the following style sheets in your page's
<head>:<link rel="stylesheet" href="./fslit.css" /> <link rel="stylesheet" href="./fstar.js/cm.tango.css" /> <link rel="stylesheet" href="./fstar.js/fstar.ide.css" /> <link rel="stylesheet" href="./fstar.js/fstar.cli.css" /> <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.36.0/codemirror.min.css" />
Add the following scripts to the end of page's your
<body>:<script src="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.36.0/codemirror.min.js"></script> <script src="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.36.0/addon/runmode/runmode.min.js"></script> <script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.2.1/jquery.min.js"></script> <script src="https://cdnjs.cloudflare.com/ajax/libs/underscore.js/1.8.3/underscore-min.js"></script> <script src="https://cdnjs.cloudflare.com/ajax/libs/mustache.js/2.3.0/mustache.js"></script> <script src="./fslit.js"></script> <script src="./fstar.js/fstar.cm.js"></script> <script src="./fstar.js/fstar.client.js"></script>
Set up the CLI integration:
<script> // Tell F*.js where to look for web worker scripts FStar.CLI.WORKER_DIRECTORY = "./fstar.js/"; FStar.IDE.WORKER_DIRECTORY = "./fstar.js/"; // Set up the IDE backend (this turns all DOM elements with class ``fstar`` // into interactive snippets). FStar.IDE.LiterateClient.run("file-name.fst"); </script>
The build script places all artefacts in dist/:
fstar.core.js: F*, compiled to JavaScript.fs/: A copy of F*'s standard library, along with index files to allowF*.jsto fetch library files on demand.fstar.client.js,fstar.cli.worker.js,fstar.ide.worker.js: Libraries to load and drivefstar.core.js, verify individual files, talk to F* using the IDE protocol, and embedF*.jsin literate F* documents.workerfiles are intended to be run in web workers.- ,
fstar.cli.css,fstar.ide.css: CSS styles for standalone F* CLI interface and for F* snippets embedded in an HTML document. fstar.cm.js,cm.tango.css: Basic F* syntax highlighting for CodeMirror
The JavaScript libraries are built from TypeScript sources in lib/: each file has a small header summarizing its purpose.