diff --git a/doc/.gitignore b/doc/.gitignore index d1f7293..0ee9bab 100644 --- a/doc/.gitignore +++ b/doc/.gitignore @@ -1,2 +1,3 @@ -# these are derived files from markdown -*.html \ No newline at end of file +# these are the files generated by Jekyll +_site +.sass-cache diff --git a/doc/_config.yml b/doc/_config.yml new file mode 100644 index 0000000..08597e5 --- /dev/null +++ b/doc/_config.yml @@ -0,0 +1,24 @@ +# Welcome to Jekyll! +# +# This config file is meant for settings that affect your whole blog, values +# which you are expected to set up once and rarely need to edit after that. +# For technical reasons, this file is *NOT* reloaded automatically when you use +# 'jekyll serve'. If you change this file, please restart the server process. + +# Site settings +title: "IVy" +description: > # this means to ignore newlines until "baseurl:" + + IVy is a research tool intended to allow interactive development of + protocols and their proofs of correctness and to provide a platform + for developing and experimenting with automated proof techniques. In + particular, IVy provides interactive visualization of automated + proofs, and supports a use model in which the human protocol + designer and the automated tool interact to expose errors and prove + correctness. + +baseurl: "" # the subpath of your site, e.g. /blog +url: "http://microsoft.github.io/ivy" # the base hostname & protocol for your site + +# Build settings +markdown: kramdown diff --git a/doc/_data/contents.yml b/doc/_data/contents.yml new file mode 100644 index 0000000..dc90e5b --- /dev/null +++ b/doc/_data/contents.yml @@ -0,0 +1,5 @@ +- title: Documentation + docs: + - install + - language + diff --git a/doc/_includes/contents.html b/doc/_includes/contents.html new file mode 100644 index 0000000..370f3f3 --- /dev/null +++ b/doc/_includes/contents.html @@ -0,0 +1,8 @@ +
+ +
diff --git a/doc/_includes/contents_ul.html b/doc/_includes/contents_ul.html new file mode 100644 index 0000000..bf82d95 --- /dev/null +++ b/doc/_includes/contents_ul.html @@ -0,0 +1,7 @@ + diff --git a/doc/_includes/footer.html b/doc/_includes/footer.html new file mode 100644 index 0000000..c70228c --- /dev/null +++ b/doc/_includes/footer.html @@ -0,0 +1,36 @@ + diff --git a/doc/_includes/head.html b/doc/_includes/head.html new file mode 100644 index 0000000..1598d6f --- /dev/null +++ b/doc/_includes/head.html @@ -0,0 +1,12 @@ + + + + + + {% if page.title %}{{ page.title | escape }}{% else %}{{ site.title | escape }}{% endif %} + + + + + + diff --git a/doc/_includes/header.html b/doc/_includes/header.html new file mode 100644 index 0000000..b9b5c33 --- /dev/null +++ b/doc/_includes/header.html @@ -0,0 +1,27 @@ +
+ +
+ + {{ site.title }} + + + +
+ +
diff --git a/doc/_includes/icon-github.html b/doc/_includes/icon-github.html new file mode 100644 index 0000000..e501a16 --- /dev/null +++ b/doc/_includes/icon-github.html @@ -0,0 +1 @@ +{% include icon-github.svg %}{{ include.username }} diff --git a/doc/_includes/icon-github.svg b/doc/_includes/icon-github.svg new file mode 100644 index 0000000..4422c4f --- /dev/null +++ b/doc/_includes/icon-github.svg @@ -0,0 +1 @@ + diff --git a/doc/_includes/icon-twitter.html b/doc/_includes/icon-twitter.html new file mode 100644 index 0000000..e623dbd --- /dev/null +++ b/doc/_includes/icon-twitter.html @@ -0,0 +1 @@ +{% include icon-twitter.svg %}{{ include.username }} diff --git a/doc/_includes/icon-twitter.svg b/doc/_includes/icon-twitter.svg new file mode 100644 index 0000000..dcf660e --- /dev/null +++ b/doc/_includes/icon-twitter.svg @@ -0,0 +1 @@ + diff --git a/doc/_layouts/default.html b/doc/_layouts/default.html new file mode 100644 index 0000000..e4ab96f --- /dev/null +++ b/doc/_layouts/default.html @@ -0,0 +1,20 @@ + + + + {% include head.html %} + + + + {% include header.html %} + +
+
+ {{ content }} +
+
+ + {% include footer.html %} + + + + diff --git a/doc/_layouts/page.html b/doc/_layouts/page.html new file mode 100644 index 0000000..63f6dca --- /dev/null +++ b/doc/_layouts/page.html @@ -0,0 +1,29 @@ +--- +layout: default +--- + +
+ +
+ + +
+ +
+

{{ page.title }}

+
+ +
+ {{ content }} +
+ +
+ +
+ + {% include contents.html %} + +
+ +
+ diff --git a/doc/_layouts/post.html b/doc/_layouts/post.html new file mode 100644 index 0000000..3a0fb52 --- /dev/null +++ b/doc/_layouts/post.html @@ -0,0 +1,15 @@ +--- +layout: default +--- +
+ +
+

{{ page.title }}

+

{% if page.author %} • {% endif %}

+
+ +
+ {{ content }} +
+ +
diff --git a/doc/_sass/_base.scss b/doc/_sass/_base.scss new file mode 100644 index 0000000..0883c3c --- /dev/null +++ b/doc/_sass/_base.scss @@ -0,0 +1,206 @@ +/** + * Reset some basic elements + */ +body, h1, h2, h3, h4, h5, h6, +p, blockquote, pre, hr, +dl, dd, ol, ul, figure { + margin: 0; + padding: 0; +} + + + +/** + * Basic styling + */ +body { + font: $base-font-weight #{$base-font-size}/#{$base-line-height} $base-font-family; + color: $text-color; + background-color: $background-color; + -webkit-text-size-adjust: 100%; + -webkit-font-feature-settings: "kern" 1; + -moz-font-feature-settings: "kern" 1; + -o-font-feature-settings: "kern" 1; + font-feature-settings: "kern" 1; + font-kerning: normal; +} + + + +/** + * Set `margin-bottom` to maintain vertical rhythm + */ +h1, h2, h3, h4, h5, h6, +p, blockquote, pre, +ul, ol, dl, figure, +%vertical-rhythm { + margin-bottom: $spacing-unit / 2; +} + + + +/** + * Images + */ +img { + max-width: 100%; + vertical-align: middle; +} + + + +/** + * Figures + */ +figure > img { + display: block; +} + +figcaption { + font-size: $small-font-size; +} + + + +/** + * Lists + */ +ul, ol { + margin-left: $spacing-unit; +} + +li { + > ul, + > ol { + margin-bottom: 0; + } +} + + + +/** + * Headings + */ +h1, h2, h3, h4, h5, h6 { + font-weight: $base-font-weight; +} + + + +/** + * Links + */ +a { + color: $brand-color; + text-decoration: none; + + &:visited { + color: darken($brand-color, 15%); + } + + &:hover { + color: $text-color; + text-decoration: underline; + } +} + + + +/** + * Blockquotes + */ +blockquote { + color: $grey-color; + border-left: 4px solid $grey-color-light; + padding-left: $spacing-unit / 2; + font-size: 18px; + letter-spacing: -1px; + font-style: italic; + + > :last-child { + margin-bottom: 0; + } +} + + + +/** + * Code formatting + */ +pre, +code { + font-size: 15px; + border: 1px solid $grey-color-light; + border-radius: 3px; + background-color: #eef; +} + +code { + padding: 1px 5px; +} + +pre { + padding: 8px 12px; + overflow-x: auto; + + > code { + border: 0; + padding-right: 0; + padding-left: 0; + } +} + + + +/** + * Wrapper + */ +.wrapper { + max-width: -webkit-calc(#{$content-width} - (#{$spacing-unit} * 2)); + max-width: calc(#{$content-width} - (#{$spacing-unit} * 2)); + margin-right: auto; + margin-left: auto; + padding-right: $spacing-unit; + padding-left: $spacing-unit; + @extend %clearfix; + + @include media-query($on-laptop) { + max-width: -webkit-calc(#{$content-width} - (#{$spacing-unit})); + max-width: calc(#{$content-width} - (#{$spacing-unit})); + padding-right: $spacing-unit / 2; + padding-left: $spacing-unit / 2; + } +} + + + +/** + * Clearfix + */ +%clearfix { + + &:after { + content: ""; + display: table; + clear: both; + } +} + + + +/** + * Icons + */ +.icon { + + > svg { + display: inline-block; + width: 16px; + height: 16px; + vertical-align: middle; + + path { + fill: $grey-color; + } + } +} diff --git a/doc/_sass/_gridism.scss b/doc/_sass/_gridism.scss new file mode 100644 index 0000000..61698ef --- /dev/null +++ b/doc/_sass/_gridism.scss @@ -0,0 +1,124 @@ +/* + * Gridism + * A simple, responsive, and handy CSS grid by @cobyism + * https://github.com/cobyism/gridism + */ + +/* Preserve some sanity */ +.grid, +.unit { + -webkit-box-sizing: border-box; + -moz-box-sizing: border-box; + box-sizing: border-box; +} + +/* Set up some rules to govern the grid */ +.grid { + display: block; + clear: both; +} +.grid .unit { + float: left; + width: 100%; + padding: 10px; +} + +/* This ensures the outer gutters are equal to the (doubled) inner gutters. */ +.grid .unit:first-child { padding-left: 20px; } +.grid .unit:last-child { padding-right: 20px; } + +/* Nested grids already have padding though, so let’s nuke it */ +.unit .unit:first-child { padding-left: 0; } +.unit .unit:last-child { padding-right: 0; } +.unit .grid:first-child > .unit { padding-top: 0; } +.unit .grid:last-child > .unit { padding-bottom: 0; } + +/* Let people nuke the gutters/padding completely in a couple of ways */ +.no-gutters .unit, +.unit.no-gutters { + padding: 0 !important; +} + +/* Wrapping at a maximum width is optional */ +.wrap .grid, +.grid.wrap { + max-width: 978px; + margin: 0 auto; +} + +/* Width classes also have shorthand versions numbered as fractions + * For example: for a grid unit 1/3 (one third) of the parent width, + * simply apply class="w-1-3" to the element. */ +.grid .whole, .grid .w-1-1 { width: 100%; } +.grid .half, .grid .w-1-2 { width: 50%; } +.grid .one-third, .grid .w-1-3 { width: 33.3332%; } +.grid .two-thirds, .grid .w-2-3 { width: 66.6665%; } +.grid .one-quarter, +.grid .one-fourth, .grid .w-1-4 { width: 25%; } +.grid .three-quarters, +.grid .three-fourths, .grid .w-3-4 { width: 75%; } +.grid .one-fifth, .grid .w-1-5 { width: 20%; } +.grid .two-fifths, .grid .w-2-5 { width: 40%; } +.grid .three-fifths, .grid .w-3-5 { width: 60%; } +.grid .four-fifths, .grid .w-4-5 { width: 80%; } +.grid .golden-small, .grid .w-g-s { width: 38.2716%; } /* Golden section: smaller piece */ +.grid .golden-large, .grid .w-g-l { width: 61.7283%; } /* Golden section: larger piece */ + +/* Clearfix after every .grid */ +.grid { + *zoom: 1; +} +.grid:before, .grid:after { + display: table; + content: ""; + line-height: 0; +} +.grid:after { + clear: both; +} + +/* Utility classes */ +.align-center { text-align: center; } +.align-left { text-align: left; } +.align-right { text-align: right; } +.pull-left { float: left; } +.pull-right { float: right; } + +/* A property for a better rendering of images in units: in + this way bigger pictures are just resized if the unit + becomes smaller */ +.unit img { + max-width: 100%; +} + +/* Responsive Stuff */ +@media screen and (max-width: 568px) { + /* Stack anything that isn’t full-width on smaller screens + and doesn't provide the no-stacking-on-mobiles class */ + .grid:not(.no-stacking-on-mobiles) > .unit { + width: 100% !important; + padding-left: 20px; + padding-right: 20px; + } + .unit .grid .unit { + padding-left: 0px; + padding-right: 0px; + } + + /* Sometimes, you just want to be different on small screens */ + .center-on-mobiles { + text-align: center !important; + } + .hide-on-mobiles { + display: none !important; + } +} + +/* Expand the wrap a bit further on larger screens */ +@media screen and (min-width: 1180px) { + .wider .grid, + .grid.wider { + max-width: 1180px; + margin: 0 auto; + } +} diff --git a/doc/_sass/_layout.scss b/doc/_sass/_layout.scss new file mode 100644 index 0000000..b0900de --- /dev/null +++ b/doc/_sass/_layout.scss @@ -0,0 +1,286 @@ +/** + * Site header + */ +.site-header { + border-top: 5px solid $grey-color-dark; + border-bottom: 1px solid $grey-color-light; + min-height: 56px; + + // Positioning context for the mobile navigation icon + position: relative; +} + +.site-title { + font-size: 26px; + font-weight: 300; + line-height: 56px; + letter-spacing: -1px; + margin-bottom: 0; + float: left; + + &, + &:visited { + color: $grey-color-dark; + } +} + +.site-nav { + float: right; + line-height: 56px; + + .menu-icon { + display: none; + } + + .page-link { + color: $text-color; + line-height: $base-line-height; + + // Gaps between nav items, but not on the last one + &:not(:last-child) { + margin-right: 20px; + } + } + + @include media-query($on-palm) { + position: absolute; + top: 9px; + right: $spacing-unit / 2; + background-color: $background-color; + border: 1px solid $grey-color-light; + border-radius: 5px; + text-align: right; + + .menu-icon { + display: block; + float: right; + width: 36px; + height: 26px; + line-height: 0; + padding-top: 10px; + text-align: center; + + > svg { + width: 18px; + height: 15px; + + path { + fill: $grey-color-dark; + } + } + } + + .trigger { + clear: both; + display: none; + } + + &:hover .trigger { + display: block; + padding-bottom: 5px; + } + + .page-link { + display: block; + padding: 5px 10px; + + &:not(:last-child) { + margin-right: 0; + } + margin-left: 20px; + } + } +} + + + +/** + * Site footer + */ +.site-footer { + border-top: 1px solid $grey-color-light; + padding: $spacing-unit 0; +} + +.footer-heading { + font-size: 18px; + margin-bottom: $spacing-unit / 2; +} + +.contact-list, +.social-media-list { + list-style: none; + margin-left: 0; +} + +.footer-col-wrapper { + font-size: 15px; + color: $grey-color; + margin-left: -$spacing-unit / 2; + @extend %clearfix; +} + +.footer-col { + float: left; + margin-bottom: $spacing-unit / 2; + padding-left: $spacing-unit / 2; +} + +.footer-col-1 { + width: -webkit-calc(35% - (#{$spacing-unit} / 2)); + width: calc(35% - (#{$spacing-unit} / 2)); +} + +.footer-col-2 { + width: -webkit-calc(20% - (#{$spacing-unit} / 2)); + width: calc(20% - (#{$spacing-unit} / 2)); +} + +.footer-col-3 { + width: -webkit-calc(45% - (#{$spacing-unit} / 2)); + width: calc(45% - (#{$spacing-unit} / 2)); +} + +@include media-query($on-laptop) { + .footer-col-1, + .footer-col-2 { + width: -webkit-calc(50% - (#{$spacing-unit} / 2)); + width: calc(50% - (#{$spacing-unit} / 2)); + } + + .footer-col-3 { + width: -webkit-calc(100% - (#{$spacing-unit} / 2)); + width: calc(100% - (#{$spacing-unit} / 2)); + } +} + +@include media-query($on-palm) { + .footer-col { + float: none; + width: -webkit-calc(100% - (#{$spacing-unit} / 2)); + width: calc(100% - (#{$spacing-unit} / 2)); + } +} + + + +/** + * Page content + */ +.page-content { + padding: $spacing-unit 0; +} + +.page-heading { + font-size: 20px; +} + +.post-list { + margin-left: 0; + list-style: none; + + > li { + margin-bottom: $spacing-unit; + } +} + +.post-meta { + font-size: $small-font-size; + color: $grey-color; +} + +.post-link { + display: block; + font-size: 24px; +} + + + +/** + * Posts + */ +.post-header { + margin-bottom: $spacing-unit; +} + +.post-title { + font-size: 42px; + letter-spacing: -1px; + line-height: 1; + + @include media-query($on-laptop) { + font-size: 36px; + } +} + +.post-content { + margin-bottom: $spacing-unit; + + h2 { + font-size: 32px; + + @include media-query($on-laptop) { + font-size: 28px; + } + } + + h3 { + font-size: 26px; + + @include media-query($on-laptop) { + font-size: 22px; + } + } + + h4 { + font-size: 20px; + + @include media-query($on-laptop) { + font-size: 18px; + } + } +} + +/* Right-side nav */ + +aside { + padding-top: 0px; + + h4 { + text-transform: uppercase; + font-size: 14px; + font-weight: 700; + padding: 0 0 10px 30px; + margin-left: -30px; + display: inline-block; + border-bottom: 1px solid #888; + } + + ul { + padding-left: 0; + + &:first-child { margin-top: 0; } + } + + li { + list-style-type: none; + + a { + font-size: 16px; + position: relative; + margin-left: -30px; + } + + &.current a:before { + content: ""; + border-color: transparent transparent transparent #444; + border-style: solid; + border-width: 10px; + width: 0; + height: 0; + position: absolute; + top: 0; + left: -15px; + } + } +} diff --git a/doc/_sass/_syntax-highlighting.scss b/doc/_sass/_syntax-highlighting.scss new file mode 100644 index 0000000..8fac597 --- /dev/null +++ b/doc/_sass/_syntax-highlighting.scss @@ -0,0 +1,71 @@ +/** + * Syntax highlighting styles + */ +.highlight { + background: #fff; + @extend %vertical-rhythm; + + .highlighter-rouge & { + background: #eef; + } + + .c { color: #998; font-style: italic } // Comment + .err { color: #a61717; background-color: #e3d2d2 } // Error + .k { font-weight: bold } // Keyword + .o { font-weight: bold } // Operator + .cm { color: #998; font-style: italic } // Comment.Multiline + .cp { color: #999; font-weight: bold } // Comment.Preproc + .c1 { color: #998; font-style: italic } // Comment.Single + .cs { color: #999; font-weight: bold; font-style: italic } // Comment.Special + .gd { color: #000; background-color: #fdd } // Generic.Deleted + .gd .x { color: #000; background-color: #faa } // Generic.Deleted.Specific + .ge { font-style: italic } // Generic.Emph + .gr { color: #a00 } // Generic.Error + .gh { color: #999 } // Generic.Heading + .gi { color: #000; background-color: #dfd } // Generic.Inserted + .gi .x { color: #000; background-color: #afa } // Generic.Inserted.Specific + .go { color: #888 } // Generic.Output + .gp { color: #555 } // Generic.Prompt + .gs { font-weight: bold } // Generic.Strong + .gu { color: #aaa } // Generic.Subheading + .gt { color: #a00 } // Generic.Traceback + .kc { font-weight: bold } // Keyword.Constant + .kd { font-weight: bold } // Keyword.Declaration + .kp { font-weight: bold } // Keyword.Pseudo + .kr { font-weight: bold } // Keyword.Reserved + .kt { color: #458; font-weight: bold } // Keyword.Type + .m { color: #099 } // Literal.Number + .s { color: #d14 } // Literal.String + .na { color: #008080 } // Name.Attribute + .nb { color: #0086B3 } // Name.Builtin + .nc { color: #458; font-weight: bold } // Name.Class + .no { color: #008080 } // Name.Constant + .ni { color: #800080 } // Name.Entity + .ne { color: #900; font-weight: bold } // Name.Exception + .nf { color: #900; font-weight: bold } // Name.Function + .nn { color: #555 } // Name.Namespace + .nt { color: #000080 } // Name.Tag + .nv { color: #008080 } // Name.Variable + .ow { font-weight: bold } // Operator.Word + .w { color: #bbb } // Text.Whitespace + .mf { color: #099 } // Literal.Number.Float + .mh { color: #099 } // Literal.Number.Hex + .mi { color: #099 } // Literal.Number.Integer + .mo { color: #099 } // Literal.Number.Oct + .sb { color: #d14 } // Literal.String.Backtick + .sc { color: #d14 } // Literal.String.Char + .sd { color: #d14 } // Literal.String.Doc + .s2 { color: #d14 } // Literal.String.Double + .se { color: #d14 } // Literal.String.Escape + .sh { color: #d14 } // Literal.String.Heredoc + .si { color: #d14 } // Literal.String.Interpol + .sx { color: #d14 } // Literal.String.Other + .sr { color: #009926 } // Literal.String.Regex + .s1 { color: #d14 } // Literal.String.Single + .ss { color: #990073 } // Literal.String.Symbol + .bp { color: #999 } // Name.Builtin.Pseudo + .vc { color: #008080 } // Name.Variable.Class + .vg { color: #008080 } // Name.Variable.Global + .vi { color: #008080 } // Name.Variable.Instance + .il { color: #099 } // Literal.Number.Integer.Long +} diff --git a/doc/credits.md b/doc/credits.md new file mode 100644 index 0000000..d8a4a45 --- /dev/null +++ b/doc/credits.md @@ -0,0 +1,14 @@ +--- +layout: page +title: Credits +tags: "top-nav" +--- + +The following people have contributed ideas, code or examples to IVy. + +* [Ken McMillan](http://kenmcmil.com), Microsoft Research +* Oded Padon, Tel Aviv University +* [Aurojit Panda](https://www.eecs.berkeley.edu/~apanda/), UC Berkeley +* [Mooly Sagiv](https://www.cs.tau.ac.il/~msagiv/), Tel Aviv University +* [Sharon Shoham](http://www2.mta.ac.il/~sharon.shoham/), Academic College of Tel Aviv Yaffo + diff --git a/doc/css/main.scss b/doc/css/main.scss new file mode 100644 index 0000000..5ed0c81 --- /dev/null +++ b/doc/css/main.scss @@ -0,0 +1,54 @@ +--- +# Only the main Sass file needs front matter (the dashes are enough) +--- +@charset "utf-8"; + + + +// Our variables +$base-font-family: "Helvetica Neue", Helvetica, Arial, sans-serif; +$base-font-size: 16px; +$base-font-weight: 400; +$small-font-size: $base-font-size * 0.875; +$base-line-height: 1.5; + +$spacing-unit: 30px; + +$text-color: #111; +$background-color: #fdfdfd; +$brand-color: #2a7ae2; + +$grey-color: #828282; +$grey-color-light: lighten($grey-color, 40%); +$grey-color-dark: darken($grey-color, 25%); + +// Width of the content area +$content-width: 800px; + +$on-palm: 600px; +$on-laptop: 800px; + + + +// Use media queries like this: +// @include media-query($on-palm) { +// .wrapper { +// padding-right: $spacing-unit / 2; +// padding-left: $spacing-unit / 2; +// } +// } +@mixin media-query($device) { + @media screen and (max-width: $device) { + @content; + } +} + + + +// Import partials from `sass_dir` (defaults to `_sass`) +@import + "base", + "layout", + "gridism", + "syntax-highlighting" +; diff --git a/doc/index.md b/doc/index.md index 8ceaa45..833bd34 100644 --- a/doc/index.md +++ b/doc/index.md @@ -1,6 +1,7 @@ --- layout: page -title: IVy +title: Home +tags: "top-nav" ---