Skip to content

beurdouche/kremlin

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

189 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

KreMLin

Build Status

Transforms a subset of F* into C code. See the ML Workshop Paper for more information.

Build

Just run make from this directory. The test suite (make test) requires the latest version of F*.

License

This new variant of F* is released under the Apache 2.0 license; see LICENSE for more details.

Installation

Make sure you run opam update to get process-0.2.1 (version 0.2 doesn't work on Windows). Install all of the packages below, possibly following instructions from https://github.com/FStarLang/FStar/wiki for "difficult" packages (e.g. ppx_deriving) on Windows.

opam install ppx_deriving_yojson zarith pprint menhir ulex process fix

Make sure fstar.exe is in your path. Run make.

File a bug if things don't work!

About

An intermediate language to translate F*'s extraction to C

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

 
 
 

Contributors

Languages

  • OCaml 91.0%
  • C 5.8%
  • Shell 1.6%
  • Makefile 1.2%
  • Standard ML 0.4%