|Pat Hickey 197ce335ee tower backend: add attrProxy definition to Attr.hs.template||7 years ago|
|executables||8 years ago|
|src||7 years ago|
|support||7 years ago|
|tests||7 years ago|
|.gitignore||8 years ago|
|.travis.yml||7 years ago|
|LICENSE||8 years ago|
|Makefile||7 years ago|
|Makefile.deps||8 years ago|
|Makefile.sandbox||8 years ago|
|README.md||7 years ago|
|Setup.hs||8 years ago|
|gidl.cabal||8 years ago|
Gidl (for Galois Interface Description Language) is a simple IDL for describing structured types and RPC-style interfaces.
Jump right to an example of gidl.
Gidl has a type language which permits the user to define types using the following primitives:
Gidl interfaces are composed of the following primitives:
Interfaces can be composed by subtyping. (We expect interface composition may change in the future.)
Protocol drift is detected by identifying each stream and attribute message on the wire by a hash of its name, its type, and all child types. Therefore
The gidl IDL uses a s-expression based format. The IDL format currently is
Gidl currently has backends for:
cerealinstances for serialization.
ivory-serializeinstances for serialization.
Gidl requires the GHC 7.8 haskell compiler, and a modern Cabal (>= 1.18).
It also requires the
s-cargot package, which is not yet available
through hackage. In the parent directory, run
git clone https://github.com/aisamanra/s-cargot
In order to build the code generated by the the Ivory and Tower backends, we require the Ivory, Tower, and ivory-tower-stm32 repositories. These should also be found, by default, in the parent directory.
git clone https://github.com/galoisinc/ivory git clone https://github.com/galoisinc/tower git clone https://github.com/galoisinc/ivory-tower-stm32
create-sandbox target in the Makefile to create a local cabal
sandbox and install all dependencies.
The default target builds the gidl library. You can then use
cabal run gidl --
<OPTIONS> to run the code generator. Use the
--help option to get usage
test target in the Makefile to generate and test each backend
tests/example.gidl file is used as the input language.
You may then browse generated code for each implementation, which is generated
and built in subdirectories of the
There is a vim-mode available at
If you use the vundle package manager, add the line
.vimrc, then run
If you use the Pathogen package manager, clone the
vim-gidl repo into your
There is an emacs-mode available at
and through an elisp archive at
If an emacs user uses the emacs package manager, they can just add a line to
.emacs and then install it either interactively with
or automatically with
(use-package gidl-mode :ensure t)
Gidl was created at Galois by Pat Hickey, with help from Getty Ritter and Trevor Elliott, as part of the SMACCMPilot project.
Gidl was inspired in part by John Van Enk's excellent Cauterize tools. Look for gidl to switch to using cauterize as the type language in the future!
Gidl is still experimental - anything may change at any time. Please get in touch if you're interested in using or working on gidl.