diff --git a/cryptol.cabal b/cryptol.cabal index 951ca07d1..3b91b2683 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -92,8 +92,11 @@ library if flag(ffi) build-depends: hgmp, - libffi >= 0.2, - unix + libffi >= 0.2 + if os(windows) + build-depends: Win32 + else + build-depends: unix cpp-options: -DFFI_ENABLED Build-tool-depends: alex:alex, happy:happy diff --git a/docs/RefMan/FFI.rst b/docs/RefMan/FFI.rst index e484092f0..6d4a41c5a 100644 --- a/docs/RefMan/FFI.rst +++ b/docs/RefMan/FFI.rst @@ -7,8 +7,9 @@ C (or other languages that use the C calling convention). Platform support ---------------- -The FFI is currently **not supported on Windows**, and only works on Unix-like -systems (macOS and Linux). +The FFI is built on top of the C ``libffi`` library, and as such, it should be +portable across many operating systems. We have tested it to work on Linux, +macOS, and Windows. Basic usage ----------- @@ -52,6 +53,7 @@ extension it uses is platform-specific: * On Linux, it looks for the extension ``.so``. * On macOS, it looks for the extension ``.dylib``. +* On Windows, it looks for the extension ``.dll``. For example, if you are on Linux and your ``foreign`` declaration is in ``Foo.cry``, Cryptol will dynamically load ``Foo.so``. Then for each ``foreign`` @@ -90,6 +92,7 @@ simple usages, you can do this manually with the following commands: * Linux: ``cc -fPIC -shared Foo.c -o Foo.so`` * macOS: ``cc -dynamiclib Foo.c -o Foo.dylib`` +* Windows: ``cc -fPIC -shared Foo.c -o Foo.dll`` Converting between Cryptol and C types -------------------------------------- diff --git a/docs/RefMan/_build/doctrees/BasicSyntax.doctree b/docs/RefMan/_build/doctrees/BasicSyntax.doctree index 8a593c36c..61a0b9c4a 100644 Binary files a/docs/RefMan/_build/doctrees/BasicSyntax.doctree and b/docs/RefMan/_build/doctrees/BasicSyntax.doctree differ diff --git a/docs/RefMan/_build/doctrees/BasicTypes.doctree b/docs/RefMan/_build/doctrees/BasicTypes.doctree index 4720a0195..dade46df2 100644 Binary files a/docs/RefMan/_build/doctrees/BasicTypes.doctree and b/docs/RefMan/_build/doctrees/BasicTypes.doctree differ diff --git a/docs/RefMan/_build/doctrees/Expressions.doctree b/docs/RefMan/_build/doctrees/Expressions.doctree index 92cf850cc..3b164e8fa 100644 Binary files a/docs/RefMan/_build/doctrees/Expressions.doctree and b/docs/RefMan/_build/doctrees/Expressions.doctree differ diff --git a/docs/RefMan/_build/doctrees/FFI.doctree b/docs/RefMan/_build/doctrees/FFI.doctree index eaea59628..4223404b1 100644 Binary files a/docs/RefMan/_build/doctrees/FFI.doctree and b/docs/RefMan/_build/doctrees/FFI.doctree differ diff --git a/docs/RefMan/_build/doctrees/Modules.doctree b/docs/RefMan/_build/doctrees/Modules.doctree index c202df73d..5de0831f5 100644 Binary files a/docs/RefMan/_build/doctrees/Modules.doctree and b/docs/RefMan/_build/doctrees/Modules.doctree differ diff --git a/docs/RefMan/_build/doctrees/OverloadedOperations.doctree b/docs/RefMan/_build/doctrees/OverloadedOperations.doctree index 1a637b221..8797caaeb 100644 Binary files a/docs/RefMan/_build/doctrees/OverloadedOperations.doctree and b/docs/RefMan/_build/doctrees/OverloadedOperations.doctree differ diff --git a/docs/RefMan/_build/doctrees/RefMan.doctree b/docs/RefMan/_build/doctrees/RefMan.doctree index 4cdda2ce3..b6debdce8 100644 Binary files a/docs/RefMan/_build/doctrees/RefMan.doctree and b/docs/RefMan/_build/doctrees/RefMan.doctree differ diff --git a/docs/RefMan/_build/doctrees/TypeDeclarations.doctree b/docs/RefMan/_build/doctrees/TypeDeclarations.doctree index fec21f4c1..353c3286b 100644 Binary files a/docs/RefMan/_build/doctrees/TypeDeclarations.doctree and b/docs/RefMan/_build/doctrees/TypeDeclarations.doctree differ diff --git a/docs/RefMan/_build/doctrees/environment.pickle b/docs/RefMan/_build/doctrees/environment.pickle index 6547d32f8..a6a301772 100644 Binary files a/docs/RefMan/_build/doctrees/environment.pickle and b/docs/RefMan/_build/doctrees/environment.pickle differ diff --git a/docs/RefMan/_build/html/.buildinfo b/docs/RefMan/_build/html/.buildinfo index 3b4193dce..b0149fc3a 100644 --- a/docs/RefMan/_build/html/.buildinfo +++ b/docs/RefMan/_build/html/.buildinfo @@ -1,4 +1,4 @@ # Sphinx build info version 1 # This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done. -config: 41758cdb8fafe65367e2aa727ac7d826 +config: 69485412ee215e2257ea16f8a42506fe tags: 645f666f9bcd5a90fca523b33c5a78b7 diff --git a/docs/RefMan/_build/html/BasicSyntax.html b/docs/RefMan/_build/html/BasicSyntax.html index 79fc359cf..3bbc07fbb 100644 --- a/docs/RefMan/_build/html/BasicSyntax.html +++ b/docs/RefMan/_build/html/BasicSyntax.html @@ -1,34 +1,66 @@ + + - + +
- - - + + + +